awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst : Std.Commutative op
inst_1 : Std.Associative op
simp_rw :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s.disjSum t).val) =
    op (Multiset.fold op b₁ (Multiset.map (fun (x : α) ↦ f (inl x)) s.val))
      (Multiset.fold op b₂ (Multiset.map (fun (x : β) ↦ f (inr x)) t.val))
⊢ fold op (op b₁ b₂) f (s.disjSum t) =
    op (fold op b₁ (fun (x : α) ↦ f (inl x)) s) (fold op b₂ (fun (x : β) ↦ f (inr x)) t)
have simp_rw₁ : Multiset.fold op (op b₁ b₂) (Multiset.map f (s.val.disjSum t.val)) =
  op (Multiset.fold op b₁ (Multiset.map (fun (x : α) ↦ f (inl x)) s.val))
    (Multiset.fold op b₂ (Multiset.map (fun (x : β) ↦ f (inr x)) t.val))
Tactic: simp_rw [fold, disjSum, Multiset.map_disjSum, fold_add]
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst : Std.Commutative op
inst_1 : Std.Associative op
simp_rw :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s.disjSum t).val) =
    op (Multiset.fold op b₁ (Multiset.map (fun (x : α) ↦ f (inl x)) s.val))
      (Multiset.fold op b₂ (Multiset.map (fun (x : β) ↦ f (inr x)) t.val))
simp_rw₁ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s.val.disjSum t.val)) =
    op (Multiset.fold op b₁ (Multiset.map (fun (x : α) ↦ f (inl x)) s.val))
      (Multiset.fold op b₂ (Multiset.map (fun (x : β) ↦ f (inr x)) t.val))
⊢ fold op (op b₁ b₂) f (s.disjSum t) =
    op (fold op b₁ (fun (x : α) ↦ f (inl x)) s) (fold op b₂ (fun (x : β) ↦ f (inr x)) t)
have simp_rw₂ : Multiset.fold op (op b₁ b₂)
    (HAdd.hAdd (α := Multiset γ) (Multiset.map (fun (x : α) ↦ f (inl x)) s.val)
      (Multiset.map (fun (x : β) ↦ f (inr x)) t.val)) =
  op (Multiset.fold op b₁ (Multiset.map (fun (x : α) ↦ f (inl x)) s.val))
    (Multiset.fold op b₂ (Multiset.map (fun (x : β) ↦ f (inr x)) t.val))
Tactic: simp_rw [fold, disjSum, Multiset.map_disjSum, fold_add]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s t : Finset α
⊢ (s ∪ t).powerset = s.powerset ⊻ t.powerset
have h : ∀ (u : Finset α), u ∈ (s ∪ t).powerset ↔ u ∈ s.powerset ⊻ t.powerset
Tactic: ext u
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
⊢ u ∈ (s ∪ t).powerset ↔ u ∈ s.powerset ⊻ t.powerset
have h : u ⊆ s ∪ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u
Tactic: simp only [mem_sups, mem_powerset, sup_eq_union]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
⊢ u ⊆ s ∪ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u
have h : ∀ (h : u ⊆ s ∪ t), s ∩ u ∪ t ∩ u = u
Tactic: refine ⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
h : ∀ (h : u ⊆ s ∪ t), s ∩ u ∪ t ∩ u = u
⊢ u ⊆ s ∪ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u
have h₁ : (∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u) → u ⊆ s ∪ t
Tactic: refine ⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
h : u ⊆ s ∪ t
⊢ s ∩ u ∪ t ∩ u = u
have h₁ : (s ∪ t) ∩ u = u
Tactic: rwa [← union_inter_distrib_right, inter_eq_right]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s t : Finset α
⊢ (s ∩ t).powerset = s.powerset ⊼ t.powerset
have h : ∀ (u : Finset α), u ∈ (s ∩ t).powerset ↔ u ∈ s.powerset ⊼ t.powerset
Tactic: ext u
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
⊢ u ∈ (s ∩ t).powerset ↔ u ∈ s.powerset ⊼ t.powerset
have h : u ⊆ s ∩ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u
Tactic: simp only [mem_infs, mem_powerset, inf_eq_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
⊢ u ⊆ s ∩ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u
have h : ∀ (h : u ⊆ s ∩ t), s ∩ u ∩ (t ∩ u) = u
Tactic: refine ⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
h : ∀ (h : u ⊆ s ∩ t), s ∩ u ∩ (t ∩ u) = u
⊢ u ⊆ s ∩ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u
have h₁ : (∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u) → u ⊆ s ∩ t
Tactic: refine ⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
⊢ s ○ t ⊆ s ⊻ t
have simp_rw : ∀ ⦃x : α⦄, (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = x
Tactic: simp_rw [subset_iff, mem_sups, mem_disjSups]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
p : α → Prop
⊢ (∀ c ∈ s ○ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
have simp_rw : (∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
Tactic: simp_rw [mem_disjSups]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
p : α → Prop
⊢ (∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
have refine : (∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)) → ∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c
Tactic: refine ⟨fun h a ha b hb hab => h _ ⟨_, ha, _, hb, hab, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
⊢ (s ○ t).Nonempty → s.Nonempty
have simp_rw : (∃ (x : α), ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ (x : α), x ∈ s
Tactic: simp_rw [Finset.Nonempty, mem_disjSups]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
⊢ (s ○ t).Nonempty → t.Nonempty
have simp_rw : (∃ (x : α), ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ (x : α), x ∈ t
Tactic: simp_rw [Finset.Nonempty, mem_disjSups]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
a b : α
⊢ Eq (α := Finset α) ({a} ○ {b}) (if Disjoint a b then {a ⊔ b} else ∅)
have pos : ∀ (h : Disjoint a b), Eq (α := Finset α) ({a} ○ {b}) {a ⊔ b}
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
a b : α
pos : ∀ (h : Disjoint a b), Eq (α := Finset α) ({a} ○ {b}) {a ⊔ b}
⊢ Eq (α := Finset α) ({a} ○ {b}) (if Disjoint a b then {a ⊔ b} else ∅)
have neg : ∀ (h : ¬Disjoint a b), Eq (α := Finset α) ({a} ○ {b}) ∅
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
⊢ ∀ (s t u : Finset α), s ○ t ○ u = s ○ (t ○ u)
have refine : ∀ (a b c : Finset α), a ○ b ○ c ≤ a ○ (b ○ c)
Tactic: refine (associative_of_commutative_of_le inferInstance ?_).assoc
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
⊢ ∀ (a b c : Finset α), a ○ b ○ c ≤ a ○ (b ○ c)
have simp : ∀ (a b c : Finset α) (a_1 : α),
  (∃ a_2 ∈ a, ∃ b_1 ∈ b, Disjoint a_2 b_1 ∧ a_2 ⊔ b_1 = a_1) →
    ∀ b_1 ∈ c,
      Disjoint a_1 b_1 →
        ∃ a_5 ∈ a,
          ∃ (b_2 : α), (∃ a ∈ b, ∃ b ∈ c, Disjoint a b ∧ a ⊔ b = b_2) ∧ Disjoint a_5 b_2 ∧ a_5 ⊔ b_2 = a_1 ⊔ b_1
Tactic: simp only [le_eq_subset, disjSups_subset_iff, mem_disjSups]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t u : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
c : α
hc : c ∈ u
habc : Disjoint (a ⊔ b) c
⊢ ∃ a_1 ∈ s, ∃ (b_1 : α), (∃ a ∈ t, ∃ b ∈ u, Disjoint a b ∧ a ⊔ b = b_1) ∧ Disjoint a_1 b_1 ∧ a_1 ⊔ b_1 = a ⊔ b ⊔ c
have habc₁ : Disjoint a c ∧ Disjoint b c
Tactic: rw [disjoint_sup_left] at habc
Cleared hypotheses: habc
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t u : Finset α
⊢ s ○ (t ○ u) = t ○ (s ○ u)
have simp_rw : s ○ t ○ u = t ○ s ○ u
Tactic: simp_rw [← disjSups_assoc, disjSups_comm s]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t u : Finset α
⊢ s ○ t ○ u = s ○ u ○ t
have simp_rw : s ○ (t ○ u) = s ○ (u ○ t)
Tactic: simp_rw [disjSups_assoc, disjSups_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t u v : Finset α
⊢ s ○ t ○ (u ○ v) = s ○ u ○ (t ○ v)
have simp_rw : s ○ t ○ u ○ v = s ○ u ○ t ○ v
Tactic: simp_rw [← disjSups_assoc, disjSups_right_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
a : α
⊢ a ∈ sᶜˢ ↔ aᶜ ∈ s
have rw : aᶜ ∈ s ↔ a ∈ sᶜˢ
Tactic: rw [Iff.comm, ← mem_map' ⟨compl, compl_injective⟩, Embedding.coeFn_mk, compl_compl, compls]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
a : α
rw : aᶜ ∈ s ↔ a ∈ sᶜˢ
⊢ a ∈ sᶜˢ ↔ aᶜ ∈ s
have rw₁ : Membership.mem (α := α) (map { toFun := compl, inj' := sorry : α ↪ α } s)
    (({ toFun := compl, inj' := sorry } : (a : α) → α) aᶜ : α) ↔
  a ∈ sᶜˢ
Tactic: rw [Iff.comm, ← mem_map' ⟨compl, compl_injective⟩, Embedding.coeFn_mk, compl_compl, compls]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
a : α
rw : aᶜ ∈ s ↔ a ∈ sᶜˢ
rw₁ :
  Membership.mem (α := α) (map { toFun := compl, inj' := ⋯ : α ↪ α } s)
      (({ toFun := compl, inj' := ⋯ } : (a : α) → α) aᶜ : α) ↔
    a ∈ sᶜˢ
⊢ a ∈ sᶜˢ ↔ aᶜ ∈ s
have rw₂ : aᶜᶜ ∈ map { toFun := compl, inj' := sorry : α ↪ α } s ↔ a ∈ sᶜˢ
Tactic: rw [Iff.comm, ← mem_map' ⟨compl, compl_injective⟩, Embedding.coeFn_mk, compl_compl, compls]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
a : α
rw : aᶜ ∈ s ↔ a ∈ sᶜˢ
rw₁ :
  Membership.mem (α := α) (map { toFun := compl, inj' := ⋯ : α ↪ α } s)
      (({ toFun := compl, inj' := ⋯ } : (a : α) → α) aᶜ : α) ↔
    a ∈ sᶜˢ
rw₂ : aᶜᶜ ∈ map { toFun := compl, inj' := ⋯ : α ↪ α } s ↔ a ∈ sᶜˢ
⊢ a ∈ sᶜˢ ↔ aᶜ ∈ s
have rw₃ : a ∈ map { toFun := compl, inj' := sorry : α ↪ α } s ↔ a ∈ sᶜˢ
Tactic: rw [Iff.comm, ← mem_map' ⟨compl, compl_injective⟩, Embedding.coeFn_mk, compl_compl, compls]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
a : α
rw : aᶜ ∈ s ↔ a ∈ sᶜˢ
rw₁ :
  Membership.mem (α := α) (map { toFun := compl, inj' := ⋯ : α ↪ α } s)
      (({ toFun := compl, inj' := ⋯ } : (a : α) → α) aᶜ : α) ↔
    a ∈ sᶜˢ
rw₂ : aᶜᶜ ∈ map { toFun := compl, inj' := ⋯ : α ↪ α } s ↔ a ∈ sᶜˢ
rw₃ : a ∈ map { toFun := compl, inj' := ⋯ : α ↪ α } s ↔ a ∈ sᶜˢ
⊢ a ∈ sᶜˢ ↔ aᶜ ∈ s
have rw₄ : a ∈ map { toFun := compl, inj' := sorry : α ↪ α } s ↔ a ∈ map { toFun := compl, inj' := sorry : α ↪ α } s
Tactic: rw [Iff.comm, ← mem_map' ⟨compl, compl_injective⟩, Embedding.coeFn_mk, compl_compl, compls]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
⊢ sᶜˢᶜˢ = s
have h : ∀ (a : α), a ∈ sᶜˢᶜˢ ↔ a ∈ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s t : Finset α
⊢ sᶜˢ ⊆ t ↔ s ⊆ tᶜˢ
have rw : sᶜˢᶜˢ ⊆ tᶜˢ ↔ s ⊆ tᶜˢ
Tactic: rw [← compls_subset_compls, compls_compls]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s t : Finset α
rw : sᶜˢᶜˢ ⊆ tᶜˢ ↔ s ⊆ tᶜˢ
⊢ sᶜˢ ⊆ t ↔ s ⊆ tᶜˢ
have rw₁ : s ⊆ tᶜˢ ↔ s ⊆ tᶜˢ
Tactic: rw [← compls_subset_compls, compls_compls]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : Fintype α
⊢ Eq.{u_2 + 1} (α := Finset α) univᶜˢ univ
have h : ∀ (a : α), Membership.mem (γ := Finset α) univᶜˢ a ↔ Membership.mem (γ := Finset α) univ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
⊢ (s ⊼ t)ᶜˢ = sᶜˢ ⊻ tᶜˢ
have simp_rw : image compl (s ⊼ t) = image compl s ⊻ image compl t
Tactic: simp_rw [← image_compl]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
⊢ (s ⊻ t)ᶜˢ = sᶜˢ ⊼ tᶜˢ
have simp_rw : image compl (s ⊻ t) = image compl s ⊼ image compl t
Tactic: simp_rw [← image_compl]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
⊢ s ⊼ tᶜˢ = s \\ t
have h : ∀ (a : α), a ∈ s ⊼ tᶜˢ ↔ a ∈ s \\ t
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s ⊼ tᶜˢ ↔ a ∈ s \\ t
have h : (∃ a_1 ∈ s, ∃ (b : α), bᶜ ∈ t ∧ a_1 ⊓ b = a) ↔ ∃ a_1 ∈ s, ∃ b ∈ t, a_1 ⊓ bᶜ = a
Tactic: simp [sdiff_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
⊢ sᶜˢ ⊼ t = t \\ s
have rw : t ⊼ sᶜˢ = t \\ s
Tactic: rw [infs_comm, infs_compls_eq_diffs]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
rw : t ⊼ sᶜˢ = t \\ s
⊢ sᶜˢ ⊼ t = t \\ s
have rw₁ : t \\ s = t \\ s
Tactic: rw [infs_comm, infs_compls_eq_diffs]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
⊢ s \\ tᶜˢ = s ⊼ t
have rw : s ⊼ tᶜˢᶜˢ = s ⊼ t
Tactic: rw [← infs_compls_eq_diffs, compls_compls]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
rw : s ⊼ tᶜˢᶜˢ = s ⊼ t
⊢ s \\ tᶜˢ = s ⊼ t
have rw₁ : s ⊼ t = s ⊼ t
Tactic: rw [← infs_compls_eq_diffs, compls_compls]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_4
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
n : ℕ
h𝒜 : Set.Sized n (↑𝒜 : Set (Finset α))
s : Finset α
hs : s ∈ 𝒜
⊢ #sᶜ = Fintype.card α - n
have rw : Fintype.card α - #s = Fintype.card α - n
Tactic: rw [Finset.card_compl, h𝒜 hs]
-- Lean 4 proof step from Mathlib.Data.Finset.Sups (goal)
Goal:
α : Type u_4
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
n : ℕ
h𝒜 : Set.Sized n (↑𝒜 : Set (Finset α))
s : Finset α
hs : s ∈ 𝒜
rw : Fintype.card α - #s = Fintype.card α - n
⊢ #sᶜ = Fintype.card α - n
have rw₁ : Fintype.card α - n = Fintype.card α - n
Tactic: rw [Finset.card_compl, h𝒜 hs]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
a b : α
⊢ s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s
have rw : s(a, b) ∈ s.sym2.val ↔ a ∈ s ∧ b ∈ s
Tactic: rw [mem_mk, sym2_val, Multiset.mk_mem_sym2_iff, mem_mk, mem_mk]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
a b : α
rw : s(a, b) ∈ s.sym2.val ↔ a ∈ s ∧ b ∈ s
⊢ s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s
have rw₁ : s(a, b) ∈ s.val.sym2 ↔ a ∈ s ∧ b ∈ s
Tactic: rw [mem_mk, sym2_val, Multiset.mk_mem_sym2_iff, mem_mk, mem_mk]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
a b : α
rw : s(a, b) ∈ s.sym2.val ↔ a ∈ s ∧ b ∈ s
rw₁ : s(a, b) ∈ s.val.sym2 ↔ a ∈ s ∧ b ∈ s
⊢ s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s
have rw₂ : a ∈ s.val ∧ b ∈ s.val ↔ a ∈ s ∧ b ∈ s
Tactic: rw [mem_mk, sym2_val, Multiset.mk_mem_sym2_iff, mem_mk, mem_mk]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
a b : α
rw : s(a, b) ∈ s.sym2.val ↔ a ∈ s ∧ b ∈ s
rw₁ : s(a, b) ∈ s.val.sym2 ↔ a ∈ s ∧ b ∈ s
rw₂ : a ∈ s.val ∧ b ∈ s.val ↔ a ∈ s ∧ b ∈ s
⊢ s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s
have rw₃ : a ∈ s.val ∧ b ∈ s.val ↔ a ∈ s.val ∧ b ∈ s
Tactic: rw [mem_mk, sym2_val, Multiset.mk_mem_sym2_iff, mem_mk, mem_mk]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
a b : α
rw : s(a, b) ∈ s.sym2.val ↔ a ∈ s ∧ b ∈ s
rw₁ : s(a, b) ∈ s.val.sym2 ↔ a ∈ s ∧ b ∈ s
rw₂ : a ∈ s.val ∧ b ∈ s.val ↔ a ∈ s ∧ b ∈ s
rw₃ : a ∈ s.val ∧ b ∈ s.val ↔ a ∈ s.val ∧ b ∈ s
⊢ s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s
have rw₄ : a ∈ s.val ∧ b ∈ s.val ↔ a ∈ s.val ∧ b ∈ s.val
Tactic: rw [mem_mk, sym2_val, Multiset.mk_mem_sym2_iff, mem_mk, mem_mk]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
m : Sym2 α
⊢ m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s
have rw : (∀ y ∈ m, y ∈ s.val) ↔ ∀ a ∈ m, a ∈ s
Tactic: rw [mem_mk, sym2_val, Multiset.mem_sym2_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).sym2 = image (fun (b : α) ↦ s(a, b)) (insert a s) ∪ s.sym2
have inl : ∀ (ha : a ∈ s), (insert a s).sym2 = image (fun (b : α) ↦ s(a, b)) (insert a s) ∪ s.sym2
Tactic: obtain ha | ha := Decidable.em (a ∈ s)
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
inl : ∀ (ha : a ∈ s), (insert a s).sym2 = image (fun (b : α) ↦ s(a, b)) (insert a s) ∪ s.sym2
⊢ (insert a s).sym2 = image (fun (b : α) ↦ s(a, b)) (insert a s) ∪ s.sym2
have inr : ∀ (ha : a ∉ s), (insert a s).sym2 = image (fun (b : α) ↦ s(a, b)) (insert a s) ∪ s.sym2
Tactic: obtain ha | ha := Decidable.em (a ∈ s)
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∈ s
⊢ (insert a s).sym2 = image (fun (b : α) ↦ s(a, b)) (insert a s) ∪ s.sym2
have inl : ∀ x ∈ s, s(a, x) ∈ s.sym2
Tactic: simp only [insert_eq_of_mem ha, right_eq_union, image_subset_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
⊢ (image f s).sym2 = image (Sym2.map f) s.sym2
have a : (image f s).sym2.val = (image (Sym2.map f) s.sym2).val
Tactic: apply val_injective
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
⊢ (image f s).sym2.val = (image (Sym2.map f) s.sym2).val
have a : (Multiset.map f s.val).dedup.sym2 = (Multiset.map (Sym2.map f) s.val.sym2).dedup
Tactic: dsimp [Finset.sym2]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
⊢ (Multiset.map f s.val).dedup.sym2 = (Multiset.map (Sym2.map f) s.val.sym2).dedup
have a : (Multiset.map f s.val).sym2.dedup = (Multiset.map (Sym2.map f) s.val.sym2).dedup
Tactic: rw [← Multiset.dedup_sym2, Multiset.sym2_map]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
a : (Multiset.map f s.val).sym2.dedup = (Multiset.map (Sym2.map f) s.val.sym2).dedup
⊢ (Multiset.map f s.val).dedup.sym2 = (Multiset.map (Sym2.map f) s.val.sym2).dedup
have a₁ : (Multiset.map (Sym2.map f) s.val.sym2).dedup = (Multiset.map (Sym2.map f) s.val.sym2).dedup
Tactic: rw [← Multiset.dedup_sym2, Multiset.sym2_map]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : Fintype α
x : Sym2 α
⊢ Membership.mem (γ := Finset (Sym2 α)) (Finset.sym2 univ) x
have rw : ∀ a ∈ x, Membership.mem (γ := Finset α) univ a
Tactic: rw [mem_sym2_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
inst_1 : Fintype α
inst : Fintype (Sym2 α)
⊢ Eq.{u_1 + 1} (α := Finset (Sym2 α)) (Finset.sym2 univ) univ
have h : ∀ (a : Sym2 α),
  Membership.mem (γ := Finset (Sym2 α)) (Finset.sym2 univ) a ↔ Membership.mem (γ := Finset (Sym2 α)) univ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s t : Finset α
h : s.sym2 = t.sym2
⊢ s = t
have h₁ : ∀ (x : α), x ∈ s ↔ x ∈ t
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
⊢ m.toFinset.sym2 = m.sym2.toFinset
have h : ∀ (z : Sym2 α), z ∈ m.toFinset.sym2 ↔ z ∈ m.sym2.toFinset
Tactic: ext z
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
z : Sym2 α
⊢ z ∈ m.toFinset.sym2 ↔ z ∈ m.sym2.toFinset
have h : ∀ (x y : α), s(x, y) ∈ m.toFinset.sym2 ↔ s(x, y) ∈ m.sym2.toFinset
Tactic: refine z.ind fun x y ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
⊢ s.sym2 = ∅ ↔ s = ∅
have rw : s.sym2.val = 0 ↔ s = ∅
Tactic: rw [← val_eq_zero, sym2_val, Multiset.sym2_eq_zero_iff, val_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
rw : s.sym2.val = 0 ↔ s = ∅
⊢ s.sym2 = ∅ ↔ s = ∅
have rw₁ : s.val.sym2 = 0 ↔ s = ∅
Tactic: rw [← val_eq_zero, sym2_val, Multiset.sym2_eq_zero_iff, val_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
rw : s.sym2.val = 0 ↔ s = ∅
rw₁ : s.val.sym2 = 0 ↔ s = ∅
⊢ s.sym2 = ∅ ↔ s = ∅
have rw₂ : s.val = 0 ↔ s = ∅
Tactic: rw [← val_eq_zero, sym2_val, Multiset.sym2_eq_zero_iff, val_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
rw : s.sym2.val = 0 ↔ s = ∅
rw₁ : s.val.sym2 = 0 ↔ s = ∅
rw₂ : s.val = 0 ↔ s = ∅
⊢ s.sym2 = ∅ ↔ s = ∅
have rw₃ : s = ∅ ↔ s = ∅
Tactic: rw [← val_eq_zero, sym2_val, Multiset.sym2_eq_zero_iff, val_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
⊢ s.sym2.Nonempty ↔ s.Nonempty
have contrapose! : s.sym2 = ∅ ↔ s = ∅
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
⊢ #s.sym2 = (#s + 1).choose 2
have rw : s.sym2.val.card = (#s + 1).choose 2
Tactic: rw [card_def, sym2_val, Multiset.card_sym2, ← card_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
rw : s.sym2.val.card = (#s + 1).choose 2
⊢ #s.sym2 = (#s + 1).choose 2
have rw₁ : s.val.sym2.card = (#s + 1).choose 2
Tactic: rw [card_def, sym2_val, Multiset.card_sym2, ← card_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
rw : s.sym2.val.card = (#s + 1).choose 2
rw₁ : s.val.sym2.card = (#s + 1).choose 2
⊢ #s.sym2 = (#s + 1).choose 2
have rw₂ : (s.val.card + 1).choose 2 = (#s + 1).choose 2
Tactic: rw [card_def, sym2_val, Multiset.card_sym2, ← card_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
rw : s.sym2.val.card = (#s + 1).choose 2
rw₁ : s.val.sym2.card = (#s + 1).choose 2
rw₂ : (s.val.card + 1).choose 2 = (#s + 1).choose 2
⊢ #s.sym2 = (#s + 1).choose 2
have rw₃ : (#s + 1).choose 2 = (#s + 1).choose 2
Tactic: rw [card_def, sym2_val, Multiset.card_sym2, ← card_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ s.sym2 = image (Function.uncurry Sym2.mk) (s ×ˢ s)
have h : ∀ (a : Sym2 α) (a b : α),
  Quot.mk (Sym2.Rel α) (a, b) ∈ s.sym2 ↔ Quot.mk (Sym2.Rel α) (a, b) ∈ image (Function.uncurry Sym2.mk) (s ×ˢ s)
Tactic: ext ⟨a, b⟩