awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
h : Nonempty α
⊢ (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)
have inr : Ne (α := ℚ≥0) (↑(Fintype.card α) : ℚ≥0) 0
Tactic: rw [dens, mul_div_cancel₀]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
⊢ s.dens * (↑(Fintype.card α) : ℚ≥0) = (↑(#s) : ℚ≥0)
have rw : (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)
Tactic: rw [mul_comm, card_mul_dens]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
rw : (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)
⊢ s.dens * (↑(Fintype.card α) : ℚ≥0) = (↑(#s) : ℚ≥0)
have rw₁ : Eq (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(#s) : ℚ≥0)
Tactic: rw [mul_comm, card_mul_dens]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
⊢ s.dens ≤ 1
have inl : IsEmpty α → s.dens ≤ 1
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
inl : IsEmpty α → s.dens ≤ 1
⊢ s.dens ≤ 1
have inr : Nonempty α → s.dens ≤ 1
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
⊢ (s ∪ t).dens + (s ∩ t).dens = s.dens + t.dens
have simp_rw : HDiv.hDiv (α := ℚ≥0) (↑(#(s ∪ t)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
    HDiv.hDiv (α := ℚ≥0) (↑(#(s ∩ t)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
  HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
    HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
Tactic: simp_rw [dens, ← add_div, ← Nat.cast_add, card_union_add_card_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
simp_rw :
  HDiv.hDiv (α := ℚ≥0) (↑(#(s ∪ t)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#(s ∩ t)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
⊢ (s ∪ t).dens + (s ∩ t).dens = s.dens + t.dens
have simp_rw₁ : HAdd.hAdd (α := ℚ≥0) (↑(#(s ∪ t)) : ℚ≥0) (↑(#(s ∩ t)) : ℚ≥0) / (↑(Fintype.card α) : ℚ≥0) =
  HAdd.hAdd (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(#t) : ℚ≥0) / (↑(Fintype.card α) : ℚ≥0)
Tactic: simp_rw [dens, ← add_div, ← Nat.cast_add, card_union_add_card_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
simp_rw :
  HDiv.hDiv (α := ℚ≥0) (↑(#(s ∪ t)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#(s ∩ t)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
simp_rw₁ :
  HAdd.hAdd (α := ℚ≥0) (↑(#(s ∪ t)) : ℚ≥0) (↑(#(s ∩ t)) : ℚ≥0) / (↑(Fintype.card α) : ℚ≥0) =
    HAdd.hAdd (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(#t) : ℚ≥0) / (↑(Fintype.card α) : ℚ≥0)
⊢ (s ∪ t).dens + (s ∩ t).dens = s.dens + t.dens
have simp_rw₂ : HDiv.hDiv (α := ℚ≥0) (↑(#(s ∪ t) + #(s ∩ t)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
  HDiv.hDiv (α := ℚ≥0) (↑(#s + #t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
Tactic: simp_rw [dens, ← add_div, ← Nat.cast_add, card_union_add_card_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
⊢ (s ∩ t).dens + (s ∪ t).dens = s.dens + t.dens
have rw : (s ∪ t).dens + (s ∩ t).dens = s.dens + t.dens
Tactic: rw [add_comm, dens_union_add_dens_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
rw : (s ∪ t).dens + (s ∩ t).dens = s.dens + t.dens
⊢ (s ∩ t).dens + (s ∪ t).dens = s.dens + t.dens
have rw₁ : s.dens + t.dens = s.dens + t.dens
Tactic: rw [add_comm, dens_union_add_dens_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
inst_1 : DecidableEq α
h : Disjoint s t
⊢ (s ∪ t).dens = s.dens + t.dens
have rw : (s.disjUnion t h).dens = s.dens + t.dens
Tactic: rw [← disjUnion_eq_union s t h, dens_disjUnion _ _ _]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
inst_1 : DecidableEq α
h : Disjoint s t
rw : (s.disjUnion t h).dens = s.dens + t.dens
⊢ (s ∪ t).dens = s.dens + t.dens
have rw₁ : s.dens + t.dens = s.dens + t.dens
Tactic: rw [← disjUnion_eq_union s t h, dens_disjUnion _ _ _]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
⊢ (s \ t).dens + t.dens = (s ∪ t).dens
have rw : (s \ t ∪ t).dens = (s ∪ t).dens
Tactic: rw [← dens_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
rw : (s \ t ∪ t).dens = (s ∪ t).dens
⊢ (s \ t).dens + t.dens = (s ∪ t).dens
have rw₁ : (s ∪ t).dens = (s ∪ t).dens
Tactic: rw [← dens_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
inst_1 : DecidableEq α
h : #s = #t
simp_rw simp_rw₁ : (s \ t).dens + t.dens = (t \ s).dens + t.dens
⊢ Eq (α := ℚ≥0) ((fun (x : ℚ≥0) ↦ x + t.dens) (s \ t).dens) ((fun (x : ℚ≥0) ↦ x + t.dens) (t \ s).dens)
have simp_rw₂ : (s ∪ t).dens = (t \ s).dens + t.dens
Tactic: simp_rw [dens_sdiff_add_dens, union_comm s, ← dens_sdiff_add_dens, dens, h]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
inst_1 : DecidableEq α
h : #s = #t
simp_rw simp_rw₁ : (s \ t).dens + t.dens = (t \ s).dens + t.dens
simp_rw₂ : (s ∪ t).dens = (t \ s).dens + t.dens
⊢ Eq (α := ℚ≥0) ((fun (x : ℚ≥0) ↦ x + t.dens) (s \ t).dens) ((fun (x : ℚ≥0) ↦ x + t.dens) (t \ s).dens)
have simp_rw₃ : (t ∪ s).dens = (t \ s).dens + t.dens
Tactic: simp_rw [dens_sdiff_add_dens, union_comm s, ← dens_sdiff_add_dens, dens, h]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
inst_1 : DecidableEq α
h : #s = #t
simp_rw simp_rw₁ : (s \ t).dens + t.dens = (t \ s).dens + t.dens
simp_rw₂ : (s ∪ t).dens = (t \ s).dens + t.dens
simp_rw₃ : (t ∪ s).dens = (t \ s).dens + t.dens
⊢ Eq (α := ℚ≥0) ((fun (x : ℚ≥0) ↦ x + t.dens) (s \ t).dens) ((fun (x : ℚ≥0) ↦ x + t.dens) (t \ s).dens)
have simp_rw₄ : (t \ s).dens + s.dens = (t \ s).dens + t.dens
Tactic: simp_rw [dens_sdiff_add_dens, union_comm s, ← dens_sdiff_add_dens, dens, h]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
inst_1 : DecidableEq α
h : #s = #t
simp_rw simp_rw₁ : (s \ t).dens + t.dens = (t \ s).dens + t.dens
simp_rw₂ : (s ∪ t).dens = (t \ s).dens + t.dens
simp_rw₃ : (t ∪ s).dens = (t \ s).dens + t.dens
simp_rw₄ : (t \ s).dens + s.dens = (t \ s).dens + t.dens
⊢ Eq (α := ℚ≥0) ((fun (x : ℚ≥0) ↦ x + t.dens) (s \ t).dens) ((fun (x : ℚ≥0) ↦ x + t.dens) (t \ s).dens)
have simp_rw₅ : HDiv.hDiv (α := ℚ≥0) (↑(#(t \ s)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
  HDiv.hDiv (α := ℚ≥0) (↑(#(t \ s)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
    HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
Tactic: simp_rw [dens_sdiff_add_dens, union_comm s, ← dens_sdiff_add_dens, dens, h]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
⊢ (s \ t).dens + (s ∩ t).dens = s.dens
have rw : (s \ t ∪ s ∩ t).dens = s.dens
Tactic: rw [← dens_union_of_disjoint (disjoint_sdiff_inter _ _), sdiff_union_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
rw : (s \ t ∪ s ∩ t).dens = s.dens
⊢ (s \ t).dens + (s ∩ t).dens = s.dens
have rw₁ : s.dens = s.dens
Tactic: rw [← dens_union_of_disjoint (disjoint_sdiff_inter _ _), sdiff_union_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
⊢ (s ∩ t).dens + (s \ t).dens = s.dens
have rw : (s \ t).dens + (s ∩ t).dens = s.dens
Tactic: rw [add_comm, dens_sdiff_add_dens_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
rw : (s \ t).dens + (s ∩ t).dens = s.dens
⊢ (s ∩ t).dens + (s \ t).dens = s.dens
have rw₁ : s.dens = s.dens
Tactic: rw [add_comm, dens_sdiff_add_dens_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_4
inst : Fintype α
s : Finset α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : (x : α) → Decidable ¬p x
⊢ {a ∈ s | p a}.dens + {a ∈ s | ¬p a}.dens = s.dens
have rw : ({a ∈ s | p a} ∪ {a ∈ s | ¬p a}).dens = s.dens
Tactic: rw [← dens_union_of_disjoint (disjoint_filter_filter_not ..), filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_4
inst : Fintype α
s : Finset α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : (x : α) → Decidable ¬p x
rw : ({a ∈ s | p a} ∪ {a ∈ s | ¬p a}).dens = s.dens
⊢ {a ∈ s | p a}.dens + {a ∈ s | ¬p a}.dens = s.dens
have rw₁ : s.dens = s.dens
Tactic: rw [← dens_union_of_disjoint (disjoint_filter_filter_not ..), filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_4
inst : Fintype α
s : Finset α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : (x : α) → Decidable ¬p x
⊢ {a ∈ s | p a}.dens + {a ∈ s | ¬p a}.dens = s.dens
have rw : ({a ∈ s | p a} ∪ {a ∈ s | ¬p a}).dens = s.dens
Tactic: classical
  rw [← dens_union_of_disjoint (disjoint_filter_filter_not ..), filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_4
inst : Fintype α
s : Finset α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : (x : α) → Decidable ¬p x
rw : ({a ∈ s | p a} ∪ {a ∈ s | ¬p a}).dens = s.dens
⊢ {a ∈ s | p a}.dens + {a ∈ s | ¬p a}.dens = s.dens
have rw₁ : s.dens = s.dens
Tactic: classical
  rw [← dens_union_of_disjoint (disjoint_filter_filter_not ..), filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Disjoint (goal)
Goal:
α : Type u_2
s t : Finset α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
have rw : Disjoint t s ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
Tactic: rw [_root_.disjoint_comm, disjoint_left]
-- Lean 4 proof step from Mathlib.Data.Finset.Disjoint (goal)
Goal:
α : Type u_2
s t : Finset α
rw : Disjoint t s ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
have rw₁ : (∀ ⦃a : α⦄, a ∈ t → a ∉ s) ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
Tactic: rw [_root_.disjoint_comm, disjoint_left]
-- Lean 4 proof step from Mathlib.Data.Finset.Disjoint (goal)
Goal:
α : Type u_2
s t : Finset α
x : α
⊢ ¬(x ∈ s → x ∉ t) ↔ x ∈ s ∧ x ∈ t
have rw : x ∈ s ∧ ¬x ∉ t ↔ x ∈ s ∧ x ∈ t
Tactic: rw [Classical.not_imp, not_not]
-- Lean 4 proof step from Mathlib.Data.Finset.Disjoint (goal)
Goal:
α : Type u_2
s t : Finset α
x : α
rw : x ∈ s ∧ ¬x ∉ t ↔ x ∈ s ∧ x ∈ t
⊢ ¬(x ∈ s → x ∉ t) ↔ x ∈ s ∧ x ∈ t
have rw₁ : x ∈ s ∧ x ∈ t ↔ x ∈ s ∧ x ∈ t
Tactic: rw [Classical.not_imp, not_not]
-- Lean 4 proof step from Mathlib.Data.Finset.Disjoint (goal)
Goal:
α : Type u_2
a b : α
⊢ Disjoint (α := Finset α) {a} {b} ↔ a ≠ b
have rw : a ∉ {b} ↔ a ≠ b
Tactic: rw [disjoint_singleton_left, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Disjoint (goal)
Goal:
α : Type u_2
a b : α
rw : a ∉ {b} ↔ a ≠ b
⊢ Disjoint (α := Finset α) {a} {b} ↔ a ≠ b
have rw₁ : ¬a = b ↔ a ≠ b
Tactic: rw [disjoint_singleton_left, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Disjoint (goal)
Goal:
α : Type u_5
s t : Finset α
h : Disjoint s t
a : α
⊢ a ∈ s.disjUnion t h ↔ a ∈ s ∨ a ∈ t
have mk : ∀ (val : Multiset α) (s : List α) (nodup : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s))
  {h : Disjoint { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α } t},
  a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α }.disjUnion t h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α } ∨ a ∈ t
Tactic: rcases s with ⟨⟨s⟩⟩
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Finset.Disjoint (goal)
Goal:
α : Type u_5
t : Finset α
a : α
val : Multiset α
s : List α
nodup : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)
h : Disjoint { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α } t
⊢ a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α }.disjUnion t h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α } ∨ a ∈ t
have mk : ∀ (val : Multiset α) (t : List α) (nodup_1 : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) t))
  {h :
    Disjoint { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α }
      { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) t, nodup := nodup_1 }},
  a ∈
      { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α }.disjUnion
        { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) t, nodup := nodup_1 : Finset α } h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α } ∨
      a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) t, nodup := nodup_1 : Finset α }
Tactic: rcases t with ⟨⟨t⟩⟩
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.Finset.Disjoint (goal)
Goal:
α : Type u_2
s : Finset α
a : α
h : Disjoint s {a}
⊢ s.disjUnion {a} h = cons a s ⋯
have rw : disjUnion {a} s sorry = cons a s sorry
Tactic: rw [disjUnion_comm, singleton_disjUnion]
-- Lean 4 proof step from Mathlib.Data.Finset.Disjoint (goal)
Goal:
α : Type u_2
s : Finset α
a : α
h : Disjoint s {a}
rw : disjUnion {a} s ⋯ = cons a s ⋯
⊢ s.disjUnion {a} h = cons a s ⋯
have rw₁ : cons a s sorry = cons a s sorry
Tactic: rw [disjUnion_comm, singleton_disjUnion]
-- Lean 4 proof step from Mathlib.Data.Finset.Disjoint (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (insert a t) s ↔ a ∉ s ∧ Disjoint s t
have rw : a ∉ s ∧ Disjoint t s ↔ a ∉ s ∧ Disjoint s t
Tactic: rw [disjoint_insert_left, _root_.disjoint_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Disjoint (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s t : Finset α
a : α
rw : a ∉ s ∧ Disjoint t s ↔ a ∉ s ∧ Disjoint s t
⊢ Disjoint (insert a t) s ↔ a ∉ s ∧ Disjoint s t
have rw₁ : a ∉ s ∧ Disjoint s t ↔ a ∉ s ∧ Disjoint s t
Tactic: rw [disjoint_insert_left, _root_.disjoint_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Erase (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ∈ s.erase b
have simp : a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s
Tactic: simp only [mem_erase]
-- Lean 4 proof step from Mathlib.Data.Finset.Filter (goal)
Goal:
α : Type u_1
h : DecidablePred fun (x : α) ↦ True
s : Finset α
⊢ filter (fun (x : α) ↦ True) s = s
have h₁ : ∀ (a : α), a ∈ filter (fun (x : α) ↦ True) s ↔ a ∈ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Filter (goal)
Goal:
α : Type u_1
h : DecidablePred fun (x : α) ↦ False
s : Finset α
⊢ filter (fun (x : α) ↦ False) s = ∅
have h₁ : ∀ (a : α), a ∈ filter (fun (x : α) ↦ False) s ↔ Membership.mem (γ := Finset α) ∅ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Filter (goal)
Goal:
α : Type u_1
p : Prop
inst : Decidable p
s : Finset α
⊢ filter (fun (_a : α) ↦ p) s = if p then s else ∅
have pos : p → filter (fun (_a : α) ↦ p) s = s
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Finset.Filter (goal)
Goal:
α : Type u_1
p : Prop
inst : Decidable p
s : Finset α
pos : p → filter (fun (_a : α) ↦ p) s = s
⊢ filter (fun (_a : α) ↦ p) s = if p then s else ∅
have neg : ¬p → filter (fun (_a : α) ↦ p) s = ∅
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Finset.Filter (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) i
hj : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
⊢ Membership.mem (γ := Finset α) ⊥ x
have h₁ : f x ≠ j
Tactic: obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = i := by simpa using hi hx
Cleared hypotheses: i, h, hi
-- Lean 4 proof step from Mathlib.Data.Finset.Filter (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) i
hj : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
h₁ : f x ≠ j
⊢ Membership.mem (γ := Finset α) ⊥ x
have hi₁ : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) (f x)
Tactic: obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = i := by simpa using hi hx
Cleared hypotheses: i, h, hi
-- Lean 4 proof step from Mathlib.Data.Finset.Filter (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Set β
t : Finset α
j : β
u : Finset α
hj : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
h : f x ≠ j
hi hj₁ : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) (f x)
⊢ Membership.mem (γ := Finset α) ⊥ x
have h₁ : f x ≠ f x
Tactic: obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = j := by simpa using hj hx
Cleared hypotheses: j, hj, h
-- Lean 4 proof step from Mathlib.Data.Finset.Filter (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
s x : Finset α
htp : x ≤ filter (fun (x : α) ↦ p x ∧ ¬q x) s
htq : x ≤ filter (fun (x : α) ↦ q x ∧ ¬p x) s
⊢ x ≤ ⊥
have simp : x = ∅
Tactic: simp only [bot_eq_empty, le_eq_subset, subset_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Filter (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
s x : Finset α
htp : x ≤ filter (fun (x : α) ↦ p x ∧ ¬q x) s
htq : x ≤ filter (fun (x : α) ↦ q x ∧ ¬p x) s
⊢ x = ∅
have by_contra! : ∀ (w : α) (hx : w ∈ x), False
Tactic: by_contra! ⟨_, hx⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Fin (goal)
Goal:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ (↑(s.attachFin h) : Set (Fin n)) = Fin.val ⁻¹' (↑s : Set ℕ)
have h₁ : ∀ (x : Fin n), x ∈ (↑(s.attachFin h) : Set (Fin n)) ↔ Membership.mem (γ := Set (Fin n)) (Fin.val ⁻¹' (↑s : Set ℕ)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Fin (goal)
Goal:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ image Fin.val (s.attachFin h) = s
have a : (↑(image Fin.val (s.attachFin h)) : Set ℕ) = (↑s : Set ℕ)
Tactic: apply coe_injective
-- Lean 4 proof step from Mathlib.Data.Finset.Fin (goal)
Goal:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ (↑(image Fin.val (s.attachFin h)) : Set ℕ) = (↑s : Set ℕ)
have a : (↑s : Set ℕ) ⊆ Set.range (ι := Fin n) Fin.val
Tactic: rw [coe_image, coe_attachFin, Set.image_preimage_eq_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ Membership.mem (γ := Finset (ι →₀ α)) (s.finsupp t) f ↔
    f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)
have refine_1 : (∃ a ∈ s.pi (β := fun (a : ι) ↦ α) t,
    ({ toFun := indicator s, inj' := sorry } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) a = f) →
  f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)
Tactic: refine mem_map.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
refine_1 :
  (∃ a ∈ s.pi (β := fun (a : ι) ↦ α) t,
      ({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) a = f) →
    f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)
⊢ Membership.mem (γ := Finset (ι →₀ α)) (s.finsupp t) f ↔
    f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)
have refine_2 : (f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)) →
  ∃ a ∈ s.pi (β := fun (a : ι) ↦ α) t, ({ toFun := indicator s, inj' := sorry } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) a = f
Tactic: refine mem_map.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi (β := fun (a : ι) ↦ α) t
⊢ support.{u_1, u_2} (M := α) (({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f) ⊆ s ∧
    ∀ i ∈ s,
      Membership.mem (α := α) (t i)
        (((({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f : ι →₀ α) : (a : ι) → α) i : α)
have refine_1 : ∀ (i : ι) (hi : i ∈ s),
  Membership.mem (α := α) (t i)
    (((({ toFun := indicator s, inj' := sorry } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f : ι →₀ α) : (a : ι) → α) i : α)
Tactic: refine ⟨support_indicator_subset _ _, fun i hi => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi (β := fun (a : ι) ↦ α) t
i : ι
hi : i ∈ s
⊢ Membership.mem (α := α) (t i)
    (((({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f : ι →₀ α) : (a : ι) → α) i : α)
have h : ((({ toFun := indicator s, inj' := sorry } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f : ι →₀ α) : (a : ι) → α) i = f i hi
Tactic: convert! mem_pi.1 hf i hi
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)) →
    ∃ a ∈ s.pi (β := fun (a : ι) ↦ α) t,
      ({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) a = f
have refine_2 : ∀ (h : f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)),
  (({ toFun := indicator s, inj' := sorry } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) fun (i : ι) (x : i ∈ s) ↦
      (f : (a : ι) → α) i) =
    f
Tactic: refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)
⊢ (({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) fun (i : ι) (x : i ∈ s) ↦
      (f : (a : ι) → α) i) =
    f
have refine_2 : ∀ (i : ι),
  Eq.{u_2 + 1} (α := α)
    ((({ toFun := indicator s, inj' := sorry } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) fun (i : ι) (x : i ∈ s) ↦
            (f : (a : ι) → α) i :
          (a : ι) → α)
        i :
      α)
    ((f : (a : ι) → α) i : α)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ Membership.mem (γ := Finset (ι →₀ α)) (s.finsupp t) f ↔
    f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)
have refine_1 : (∃ a ∈ s.pi (β := fun (a : ι) ↦ α) t,
    ({ toFun := indicator s, inj' := sorry } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) a = f) →
  f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)
Tactic: classical
  refine mem_map.trans ⟨?_, ?_⟩
  · rintro ⟨f, hf, rfl⟩
    refine ⟨support_indicator_subset _ _, fun i hi => ?_⟩
    convert! mem_pi.1 hf i hi
    exact indicator_of_mem hi _
  · refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩
    ext i
    exact ite_eq_left_iff.2 fun hi => (notMem_support_iff.1 fun H => hi <| h.1 H).symm