awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ (↑k : Multiset α).prod = ∏ d ∈ s, d ^ Multiset.count d (↑k : Multiset α)
have rw : Eq (α := α) (∏ i ∈ s, i ^ Multiset.count i (↑k : Multiset α)) (∏ d ∈ s, d ^ Multiset.count d (↑k : Multiset α))
Tactic: rw [Finset.prod_multiset_count_of_subset _ s]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
rw : Eq (α := α) (∏ i ∈ s, i ^ Multiset.count i (↑k : Multiset α)) (∏ d ∈ s, d ^ Multiset.count d (↑k : Multiset α))
⊢ (↑k : Multiset α).prod = ∏ d ∈ s, d ^ Multiset.count d (↑k : Multiset α)
have rw₁ : (↑k : Multiset α).toFinset ⊆ s
Tactic: rw [Finset.prod_multiset_count_of_subset _ s]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
x : α
hx : x ∈ (↑k : Multiset α).toFinset
⊢ x ∈ s
have hx₁ : x ∈ k
Tactic: simp only [Sym.val_eq_coe, Multiset.mem_toFinset, Sym.mem_coe] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
x : α
hx : x ∈ k
⊢ x ∈ s
have hk₁ : ∀ a ∈ k, a ∈ s
Tactic: simp only [Finset.mem_sym_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.Finset.SymmDiff (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
have simp_rw : a ∈ s \ t ⊔ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
Tactic: simp_rw [symmDiff, sup_eq_union, mem_union, mem_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.SymmDiff (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
simp_rw : a ∈ s \ t ⊔ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
⊢ a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
have simp_rw₁ : a ∈ s \ t ∪ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
Tactic: simp_rw [symmDiff, sup_eq_union, mem_union, mem_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.SymmDiff (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
simp_rw : a ∈ s \ t ⊔ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
simp_rw₁ : a ∈ s \ t ∪ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
⊢ a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
have simp_rw₂ : a ∈ s \ t ∨ a ∈ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
Tactic: simp_rw [symmDiff, sup_eq_union, mem_union, mem_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s : Set α).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1) : Set β).PairwiseDisjoint g
a : ↥s
h : a ∈ (↑s.attach : Set ↥s)
b : ↥s
h_1 : b ∈ (↑s.attach : Set ↥s)
hab : a ≠ b
x : γ
hxa : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) a) x
hxb : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) b) x
⊢ False
have obtain : ∀ (xa : β) (hfa : xa ∈ f (↑a : α)) (hga : x ∈ g xa), False
Tactic: obtain ⟨xa, hfa, hga⟩ := mem_disjiUnion.mp hxa
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s : Set α).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1) : Set β).PairwiseDisjoint g
a : ↥s
h : a ∈ (↑s.attach : Set ↥s)
b : ↥s
h_1 : b ∈ (↑s.attach : Set ↥s)
hab : a ≠ b
x : γ
hxa : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) a) x
hxb : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) b) x
xa : β
hfa : xa ∈ f (↑a : α)
hga : x ∈ g xa
⊢ False
have obtain : ∀ (xb : β) (hfb : xb ∈ f (↑b : α)) (hgb : x ∈ g xb), False
Tactic: obtain ⟨xb, hfb, hgb⟩ := mem_disjiUnion.mp hxb
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s : Set α).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1) : Set β).PairwiseDisjoint g
a : ↥s
h : a ∈ (↑s.attach : Set ↥s)
b : ↥s
h_1 : b ∈ (↑s.attach : Set ↥s)
hab : a ≠ b
x : γ
hxa : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) a) x
hxb : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) b) x
xa : β
hfa : xa ∈ f (↑a : α)
hga : x ∈ g xa
xb : β
hfb : xb ∈ f (↑b : α)
hgb : x ∈ g xb
⊢ False
have refine : xa ≠ xb
Tactic: refine disjoint_left.mp
            (h2 (mem_disjiUnion.mpr ⟨_, a.prop, hfa⟩) (mem_disjiUnion.mpr ⟨_, b.prop, hfb⟩) ?_) hga
            hgb
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
⊢ ⋃₀ (↑(I.disjiUnion f hf) : Set (Set β)) = ⋃ a ∈ I, ⋃₀ (↑(f a) : Set (Set β))
have h : ∀ (x : β),
  x ∈ ⋃₀ (↑(I.disjiUnion f hf) : Set (Set β)) ↔ Membership.mem (γ := Set β) (⋃ a ∈ I, ⋃₀ (↑(f a) : Set (Set β))) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
⊢ x ∈ ⋃₀ (↑(I.disjiUnion f hf) : Set (Set β)) ↔ Membership.mem (γ := Set β) (⋃ a ∈ I, ⋃₀ (↑(f a) : Set (Set β))) x
have h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
Tactic: simp only [coe_disjiUnion, Set.mem_sUnion, Set.mem_iUnion, mem_coe, exists_prop]
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
⊢ (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
have h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
⊢ (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
have h₁ : (∃ i ∈ I, ∃ t ∈ f i, x ∈ t) → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁ : (∃ i ∈ I, ∃ t ∈ f i, x ∈ t) → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
⊢ (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
have h₂ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁ : (∃ i ∈ I, ∃ t ∈ f i, x ∈ t) → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₂ h₃ h₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
⊢ (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
have h₅ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁ : (∃ i ∈ I, ∃ t ∈ f i, x ∈ t) → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₂ h₃ h₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₅ h₆ h₇ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₈ h₉ h₁₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₁ h₁₂ h₁₃ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₁₄ h₁₅ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
⊢ (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
have h₁₆ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁ : (∃ i ∈ I, ∃ t ∈ f i, x ∈ t) → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₂ h₃ h₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₅ h₆ h₇ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₈ h₉ h₁₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₁ h₁₂ h₁₃ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₁₄ h₁₅ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₆ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
⊢ (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
have h₁₇ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁ : (∃ i ∈ I, ∃ t ∈ f i, x ∈ t) → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₂ h₃ h₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₅ h₆ h₇ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₈ h₉ h₁₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₁ h₁₂ h₁₃ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₁₄ h₁₅ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₆ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₇ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₁₈ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₉ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
⊢ (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
have h₂₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁ : (∃ i ∈ I, ∃ t ∈ f i, x ∈ t) → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₂ h₃ h₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₅ h₆ h₇ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₈ h₉ h₁₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₁ h₁₂ h₁₃ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₁₄ h₁₅ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₆ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₇ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₁₈ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₉ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I
⊢ (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
have h₂₁ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁ : (∃ i ∈ I, ∃ t ∈ f i, x ∈ t) → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₂ h₃ h₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₅ h₆ h₇ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₈ h₉ h₁₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₁ h₁₂ h₁₃ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₁₄ h₁₅ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₆ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₇ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₁₈ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₉ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I
h₂₁ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₂ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₃ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I
h₂₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₅ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₆ h₂₇ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₈ h₂₉ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
⊢ (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
have h₃₀ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → (∃ i ∈ I, w_1 ∈ f i) ∧ x ∈ w_1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁ : (∃ i ∈ I, ∃ t ∈ f i, x ∈ t) → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₂ h₃ h₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₅ h₆ h₇ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₈ h₉ h₁₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₁ h₁₂ h₁₃ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₁₄ h₁₅ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₆ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₇ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₁₈ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₉ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I
h₂₁ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₂ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₃ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I
h₂₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₅ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₆ h₂₇ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₈ h₂₉ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₃₀ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → (∃ i ∈ I, w_1 ∈ f i) ∧ x ∈ w_1
⊢ (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
have h₃₁ : (w : α) → w ∈ I → (w_1 : Set β) → w_1 ∈ f w → x ∈ w_1 → Set β
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁ : (∃ i ∈ I, ∃ t ∈ f i, x ∈ t) → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₂ h₃ h₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₅ h₆ h₇ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₈ h₉ h₁₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₁ h₁₂ h₁₃ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₁₄ h₁₅ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₆ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₇ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₁₈ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₉ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I
h₂₁ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₂ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₃ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I
h₂₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₅ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₆ h₂₇ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₈ h₂₉ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₃₀ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → (∃ i ∈ I, w_1 ∈ f i) ∧ x ∈ w_1
h₃₁ : (w : α) → w ∈ I → (w_1 : Set β) → w_1 ∈ f w → x ∈ w_1 → Set β
h₃₂ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → (∃ i ∈ I, w_1 ∈ f i) ∧ x ∈ w_1
h₃₃ : (w : α) → w ∈ I → (w_1 : Set β) → w_1 ∈ f w → x ∈ w_1 → Set β
⊢ (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
have h₃₄ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ i ∈ I, w_1 ∈ f i
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁ : (∃ i ∈ I, ∃ t ∈ f i, x ∈ t) → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₂ h₃ h₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₅ h₆ h₇ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₈ h₉ h₁₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₁ h₁₂ h₁₃ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₁₄ h₁₅ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₆ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₇ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₁₈ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₉ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I
h₂₁ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₂ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₃ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I
h₂₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₅ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₆ h₂₇ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₈ h₂₉ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₃₀ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → (∃ i ∈ I, w_1 ∈ f i) ∧ x ∈ w_1
h₃₁ : (w : α) → w ∈ I → (w_1 : Set β) → w_1 ∈ f w → x ∈ w_1 → Set β
h₃₂ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → (∃ i ∈ I, w_1 ∈ f i) ∧ x ∈ w_1
h₃₃ : (w : α) → w ∈ I → (w_1 : Set β) → w_1 ∈ f w → x ∈ w_1 → Set β
h₃₄ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ i ∈ I, w_1 ∈ f i
⊢ (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
have h₃₅ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → x ∈ w_1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ (↑t : Set β)
y' : β
hy : y' ∈ (↑t : Set β)
hne : x' ≠ y'
⊢ Function.onFun.{u_2 + 1, u_1 + 1, 1} (β := Finset α) Disjoint (fun (a : β) ↦ {x ∈ s | f x = a}) x' y'
have simp_rw : ∀ ⦃a : α⦄, a ∈ s ∧ f a = x' → ¬(a ∈ s ∧ f a = y')
Tactic: simp_rw [disjoint_left, mem_filter]
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
hf : Function.Injective f
⊢ s.disjiUnion (fun (a : α) ↦ {f a}) ⋯ = map { toFun := f, inj' := hf : α ↪ β } s
have h : ∀ (a : β),
  Membership.mem (γ := Finset β) (s.disjiUnion (fun (a : α) ↦ {f a}) sorry) a ↔ a ∈ map { toFun := f, inj' := hf : α ↪ β } s
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → Finset β
hf : (↑s : Set α).PairwiseDisjoint f
t : Finset β
⊢ Disjoint (s.disjiUnion f hf) t ↔ ∀ i ∈ s, Disjoint (f i) t
have empty : ∀ (hf : (↑∅ : Set α).PairwiseDisjoint f),
  Disjoint (disjiUnion ∅ f hf) t ↔ ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Disjoint (f i) t
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → Finset β
hf : (↑s : Set α).PairwiseDisjoint f
t : Finset β
empty :
  ∀ (hf : (↑∅ : Set α).PairwiseDisjoint f),
    Disjoint (disjiUnion ∅ f hf) t ↔ ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Disjoint (f i) t
⊢ Disjoint (s.disjiUnion f hf) t ↔ ∀ i ∈ s, Disjoint (f i) t
have cons : ∀ (a : α) (s : Finset α) (h : a ∉ s),
  (∀ (hf : (↑s : Set α).PairwiseDisjoint f), Disjoint (s.disjiUnion f hf) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
    ∀ (hf : (↑(cons a s h) : Set α).PairwiseDisjoint f),
      Disjoint ((cons a s h).disjiUnion f hf) t ↔ ∀ i ∈ cons a s h, Disjoint (f i) t
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f_1 : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s : Set α).Pairwise fun (a₁ a₂ : α) ↦ Disjoint (f a₁) (g a₂)
hf : (↑s : Set α).PairwiseDisjoint f
hg : (↑s : Set α).PairwiseDisjoint g
⊢ Disjoint (s.disjiUnion f hf) (s.disjiUnion g hg)
have simp_rw : ∀ i ∈ s, ∀ i_1 ∈ s, Disjoint (f i) (g i_1)
Tactic: simp_rw [disjoint_disjiUnion_left, disjoint_disjiUnion_right]
-- Lean 4 proof step from Mathlib.Data.Finset.Union (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f_1 : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s : Set α).Pairwise fun (a₁ a₂ : α) ↦ Disjoint (f a₁) (g a₂)
hf : (↑s : Set α).PairwiseDisjoint f
hg : (↑s : Set α).PairwiseDisjoint g
i : α
hi : i ∈ s
j : α
hj : j ∈ s
⊢ Disjoint (f i) (g j)
have hfg'₁ : i ≠ j → (fun (a₁ a₂ : α) ↦ Disjoint (f a₁) (g a₂)) i j
Tactic: specialize hfg' hi hj
Cleared hypotheses: hfg'
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst : DecidableEq β
⊢ (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty
have simp : (∃ (x : β), ∃ a ∈ s, x ∈ t a) ↔ ∃ x ∈ s, ∃ (x_1 : β), x_1 ∈ t x
Tactic: simp only [Finset.Nonempty, mem_biUnion]
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst : DecidableEq β
⊢ (∃ (x : β), ∃ a ∈ s, x ∈ t a) ↔ ∃ x ∈ s, ∃ (x_1 : β), x_1 ∈ t x
have rw : (∃ (b : α) (a : β), b ∈ s ∧ a ∈ t b) ↔ ∃ x ∈ s, ∃ (x_1 : β), x_1 ∈ t x
Tactic: rw [exists_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t
have refine_1 : Disjoint (Finset.biUnion ∅ f) t ↔ ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Disjoint (f i) t
Tactic: refine s.induction ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
refine_1 : Disjoint (Finset.biUnion ∅ f) t ↔ ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Disjoint (f i) t
⊢ Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t
have refine_2 : ∀ (a : α) (s : Finset α),
  a ∉ s →
    (Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
      (Disjoint ((insert a s).biUnion f) t ↔ ∀ i ∈ insert a s, Disjoint (f i) t)
Tactic: refine s.induction ?_ ?_