α : Type u_1
β : Type u_2
γ : Type ?u.506363
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
hs : s₁ = s₂
ht : ∀ (a : α), a ∈ s₁ → t₁ a = t₂ a
x : β
⊢ (∃ a, a ∈ s₁ ∧ x ∈ t₁ a) ↔ ∃ a, a ∈ s₂ ∧ x ∈ t₂ a
α : Type u_1
β : Type u_2
γ : Type ?u.506363
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
hs : s₁ = s₂
ht : ∀ (a : α), a ∈ s₁ → t₁ a = t₂ a
x : β
⊢ x ∈ Finset.biUnion s₁ t₁ ↔ x ∈ Finset.biUnion s₂ t₂
simp_rw [mem_biUnion]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.506363
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
hs : s₁ = s₂
ht : ∀ (a : α), a ∈ s₁ → t₁ a = t₂ a
x : β
⊢ ∀ (a : α), a ∈ s₁ ∧ x ∈ t₁ a ↔ a ∈ s₂ ∧ x ∈ t₂ a
α : Type u_1
β : Type u_2
γ : Type ?u.506363
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
hs : s₁ = s₂
ht : ∀ (a : α), a ∈ s₁ → t₁ a = t₂ a
x : β
⊢ (∃ a, a ∈ s₁ ∧ x ∈ t₁ a) ↔ ∃ a, a ∈ s₂ ∧ x ∈ t₂ a
apply exists_congr
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.506363
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
hs : s₁ = s₂
ht : ∀ (a : α), a ∈ s₁ → t₁ a = t₂ a
x : β
⊢ ∀ (a : α), a ∈ s₁ ∧ x ∈ t₁ a ↔ a ∈ s₂ ∧ x ∈ t₂ a
simp (config := { contextual := true }) only [hs, and_congr_right_iff, ht, implies_true]