awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ s.erase a = ∅ ↔ s = ∅ ∨ s = {a}
have rw : s \ {a} = ∅ ↔ s = ∅ ∨ s = {a}
Tactic: rw [← sdiff_singleton_eq_erase, sdiff_eq_empty_iff_subset, subset_singleton_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
rw : s \ {a} = ∅ ↔ s = ∅ ∨ s = {a}
⊢ s.erase a = ∅ ↔ s = ∅ ∨ s = {a}
have rw₁ : s ⊆ {a} ↔ s = ∅ ∨ s = {a}
Tactic: rw [← sdiff_singleton_eq_erase, sdiff_eq_empty_iff_subset, subset_singleton_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
rw : s \ {a} = ∅ ↔ s = ∅ ∨ s = {a}
rw₁ : s ⊆ {a} ↔ s = ∅ ∨ s = {a}
⊢ s.erase a = ∅ ↔ s = ∅ ∨ s = {a}
have rw₂ : s = ∅ ∨ s = {a} ↔ s = ∅ ∨ s = {a}
Tactic: rw [← sdiff_singleton_eq_erase, sdiff_eq_empty_iff_subset, subset_singleton_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
s : Finset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
⊢ Disjoint (filter p s) (filter q s) ↔ ∀ x ∈ s, p x → ¬q x
have mp : Disjoint (filter p s) (filter q s) → ∀ x ∈ s, p x → ¬q x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
s : Finset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
mp : Disjoint (filter p s) (filter q s) → ∀ x ∈ s, p x → ¬q x
⊢ Disjoint (filter p s) (filter q s) ↔ ∀ x ∈ s, p x → ¬q x
have mpr : (∀ x ∈ s, p x → ¬q x) → Disjoint (filter p s) (filter q s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
s t : Finset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : Disjoint p q
⊢ Disjoint (filter p s) (filter q t)
have simp_rw : ∀ ⦃a : α⦄, a ∈ s ∧ p a → ¬(a ∈ t ∧ q a)
Tactic: simp_rw [disjoint_left, mem_filter]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
s t : Finset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : Disjoint p q
a : α
left : a ∈ s
hp : p a
left_1 : a ∈ t
hq : q a
⊢ False
have rw : ∀ (h : ∀ (i : α), Disjoint (p i) (q i)) ⦃a : α⦄, a ∈ s → ∀ (hp : p a), a ∈ t → ∀ (hq : q a), False
Tactic: rw [Pi.disjoint_iff] at h
Cleared hypotheses: h, a, left, hp, left_1, hq
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
⊢ ∃ (s₁ : Finset α) (s₂ : Finset α), s₁ ∪ s₂ = s ∧ (↑s₁ : Set α) ⊆ t₁ ∧ (↑s₂ : Set α) ⊆ t₂ \ t₁
have refine_1 : filter (fun (x : α) ↦ x ∈ t₁) s ∪ filter (fun (x : α) ↦ x ∉ t₁) s = s
Tactic: refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
refine_1 : filter (fun (x : α) ↦ x ∈ t₁) s ∪ filter (fun (x : α) ↦ x ∉ t₁) s = s
⊢ ∃ (s₁ : Finset α) (s₂ : Finset α), s₁ ∪ s₂ = s ∧ (↑s₁ : Set α) ⊆ t₁ ∧ (↑s₂ : Set α) ⊆ t₂ \ t₁
have refine_2 : (↑(filter (fun (x : α) ↦ x ∈ t₁) s) : Set α) ⊆ t₁
Tactic: refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
refine_1 : filter (fun (x : α) ↦ x ∈ t₁) s ∪ filter (fun (x : α) ↦ x ∉ t₁) s = s
refine_2 : (↑(filter (fun (x : α) ↦ x ∈ t₁) s) : Set α) ⊆ t₁
⊢ ∃ (s₁ : Finset α) (s₂ : Finset α), s₁ ∪ s₂ = s ∧ (↑s₁ : Set α) ⊆ t₁ ∧ (↑s₂ : Set α) ⊆ t₂ \ t₁
have refine_3 : (↑(filter (fun (x : α) ↦ x ∉ t₁) s) : Set α) ⊆ t₂ \ t₁
Tactic: refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ (↑(filter (fun (x : α) ↦ x ∉ t₁) s) : Set α) → x ∈ t₂ \ t₁
have refine_3 : x ∈ s → x ∉ t₁ → x ∈ t₂ \ t₁
Tactic: simp only [coe_filter, Set.mem_setOf_eq, and_imp]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
⊢ ∃ (s₁ : Finset α) (s₂ : Finset α), s₁ ∪ s₂ = s ∧ (↑s₁ : Set α) ⊆ t₁ ∧ (↑s₂ : Set α) ⊆ t₂ \ t₁
have refine_1 : filter (fun (x : α) ↦ x ∈ t₁) s ∪ filter (fun (x : α) ↦ x ∉ t₁) s = s
Tactic: classical
    refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩
    · grind
    · grind
    · intro x
      simp only [coe_filter, Set.mem_setOf_eq, and_imp]
      intro hx hx₂
      exact ⟨Or.resolve_left (h hx) hx₂, hx₂⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
refine_1 : filter (fun (x : α) ↦ x ∈ t₁) s ∪ filter (fun (x : α) ↦ x ∉ t₁) s = s
⊢ ∃ (s₁ : Finset α) (s₂ : Finset α), s₁ ∪ s₂ = s ∧ (↑s₁ : Set α) ⊆ t₁ ∧ (↑s₂ : Set α) ⊆ t₂ \ t₁
have refine_2 : (↑(filter (fun (x : α) ↦ x ∈ t₁) s) : Set α) ⊆ t₁
Tactic: classical
    refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩
    · grind
    · grind
    · intro x
      simp only [coe_filter, Set.mem_setOf_eq, and_imp]
      intro hx hx₂
      exact ⟨Or.resolve_left (h hx) hx₂, hx₂⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
refine_1 : filter (fun (x : α) ↦ x ∈ t₁) s ∪ filter (fun (x : α) ↦ x ∉ t₁) s = s
refine_2 : (↑(filter (fun (x : α) ↦ x ∈ t₁) s) : Set α) ⊆ t₁
⊢ ∃ (s₁ : Finset α) (s₂ : Finset α), s₁ ∪ s₂ = s ∧ (↑s₁ : Set α) ⊆ t₁ ∧ (↑s₂ : Set α) ⊆ t₂ \ t₁
have refine_3 : (↑(filter (fun (x : α) ↦ x ∉ t₁) s) : Set α) ⊆ t₂ \ t₁
Tactic: classical
    refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩
    · grind
    · grind
    · intro x
      simp only [coe_filter, Set.mem_setOf_eq, and_imp]
      intro hx hx₂
      exact ⟨Or.resolve_left (h hx) hx₂, hx₂⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
m n : ℕ
⊢ range m ∩ range n = range (min m n)
have h : ∀ (a : ℕ), a ∈ range m ∩ range n ↔ a ∈ range (min m n)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
m n : ℕ
⊢ range m ∪ range n = range (max m n)
have h : ∀ (a : ℕ), a ∈ range m ∪ range n ↔ a ∈ range (max m n)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ (s ∪ t).toFinset = s.toFinset ∪ t.toFinset
have h : ∀ (a : α), a ∈ (s ∪ t).toFinset ↔ a ∈ s.toFinset ∪ t.toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
p : α → Prop
inst_1 : DecidablePred p
⊢ (filter p s).toFinset = Finset.filter p s.toFinset
have h : ∀ (a : α), a ∈ (filter p s).toFinset ↔ a ∈ Finset.filter p s.toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
⊢ (l ∪ l').toFinset = l.toFinset ∪ l'.toFinset
have h : ∀ (a : α), a ∈ (l ∪ l').toFinset ↔ a ∈ l.toFinset ∪ l'.toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
⊢ (l ∩ l').toFinset = l.toFinset ∩ l'.toFinset
have h : ∀ (a : α), a ∈ (l ∩ l').toFinset ↔ a ∈ l.toFinset ∩ l'.toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : List α
p : α → Bool
⊢ (filter p s).toFinset = Finset.filter (fun (x : α) ↦ p x = true) s.toFinset
have h : ∀ (a : α), a ∈ (filter p s).toFinset ↔ a ∈ Finset.filter (fun (x : α) ↦ p x = true) s.toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
ι : Type u_5
inst : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α (↑i : ι)
g : (i : ↥t) → α (↑i : ι)
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ Eq.{u_4 + 1} (α := α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    ((piFinsetUnion α h : (a : ((i : ↥s) → α (↑i : ι)) × ((i : ↥t) → α (↑i : ι))) → (i : ↥(s ∪ t)) → α (↑i : ι)) (f, g)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))
have simp_rw : Eq.{u_4 + 1} (α := α i)
  (Eq.rec (motive :=
      fun (x : ↥(s ∪ t))
        (x_1 :
          (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
              ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
                (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')) =
            x) ↦
      α (↑x : ι))
      (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
        ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
          (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')))
      sorry :
    α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
  (f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))
Tactic: simp_rw [piFinsetUnion, sumPiEquivProdPi, piCongrLeft, piCongrLeft', trans_apply, coe_fn_symm_mk]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
ι : Type u_5
inst : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α (↑i : ι)
g : (i : ↥t) → α (↑i : ι)
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ Eq.{u_4 + 1} (α := α i)
    (Eq.rec (motive :=
        fun (x : ↥(s ∪ t))
          (x_1 :
            (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
                ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')) =
              x) ↦
        α (↑x : ι))
        (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
          ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')))
        ⋯ :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))
have rw! : Eq.{u_4 + 1} (α := α i)
  (@Eq.rec _ _
      (fun (x : ↥(s ∪ t))
          (x_1 :
            (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
                (Sum.inl (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) =
              x) ↦
        α (↑x : ι))
      (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
        (Sum.inl (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)))
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') sorry :
    α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
  (f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))
Tactic: rw! [Finset.union_symm_left h hi hi']
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
ι : Type u_5
inst : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α (↑i : ι)
g : (i : ↥t) → α (↑i : ι)
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ Eq.{u_4 + 1} (α := α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    ((piFinsetUnion α h : (a : ((i : ↥s) → α (↑i : ι)) × ((i : ↥t) → α (↑i : ι))) → (i : ↥(s ∪ t)) → α (↑i : ι)) (f, g)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (g (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : ι))
have simp_rw : Eq.{u_4 + 1} (α := α i)
  (Eq.rec (motive :=
      fun (x : ↥(s ∪ t))
        (x_1 :
          (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
              ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
                (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')) =
            x) ↦
      α (↑x : ι))
      (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
        ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
          (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')))
      sorry :
    α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
  (g (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : ι))
Tactic: simp_rw [piFinsetUnion, sumPiEquivProdPi, piCongrLeft, piCongrLeft', trans_apply, coe_fn_symm_mk]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
ι : Type u_5
inst : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α (↑i : ι)
g : (i : ↥t) → α (↑i : ι)
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ Eq.{u_4 + 1} (α := α i)
    (Eq.rec (motive :=
        fun (x : ↥(s ∪ t))
          (x_1 :
            (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
                ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')) =
              x) ↦
        α (↑x : ι))
        (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
          ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')))
        ⋯ :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (g (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : ι))
have rw! : Eq.{u_4 + 1} (α := α i)
  (@Eq.rec _ _
      (fun (x : ↥(s ∪ t))
          (x_1 :
            (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
                (Sum.inr (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi)) =
              x) ↦
        α (↑x : ι))
      (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
        (Sum.inr (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi)))
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') sorry :
    α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
  (g (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : ι))
Tactic: rw! [Finset.union_symm_right h hi hi']
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
a : α
⊢ (replicate n a).toFinset = if n = 0 then ∅ else {a}
have h : ∀ (x : α), x ∈ (replicate n a).toFinset ↔ Membership.mem (γ := Finset α) (if n = 0 then ∅ else {a}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
a x : α
⊢ x ∈ (replicate n a).toFinset ↔ Membership.mem (γ := Finset α) (if n = 0 then ∅ else {a}) x
have h : n ≠ 0 ∧ x = a ↔ Membership.mem (γ := Finset α) (if n = 0 then ∅ else {a}) x
Tactic: simp only [mem_toFinset, mem_replicate]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
a x : α
⊢ n ≠ 0 ∧ x = a ↔ Membership.mem (γ := Finset α) (if n = 0 then ∅ else {a}) x
have pos : ∀ (hn : n = 0), n ≠ 0 ∧ x = a ↔ Membership.mem (γ := Finset α) ∅ x
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
a x : α
pos : ∀ (hn : n = 0), n ≠ 0 ∧ x = a ↔ Membership.mem (γ := Finset α) ∅ x
⊢ n ≠ 0 ∧ x = a ↔ Membership.mem (γ := Finset α) (if n = 0 then ∅ else {a}) x
have neg : ∀ (hn : ¬n = 0), n ≠ 0 ∧ x = a ↔ Membership.mem (γ := Finset α) {a} x
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
⊢ x ∈ s ∪ t ↔ Xor (x ∈ s) (x ∈ t)
have rw : x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
Tactic: rw [Finset.mem_union, Xor]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (hypothesis)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
Tactic: have := disjoint_left.1 h
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mpr : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → x ∈ s ∨ x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mpr : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → x ∈ s ∨ x ∈ t
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp₁ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mpr : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → x ∈ s ∨ x ∈ t
mp₁ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp₂ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mpr : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → x ∈ s ∨ x ∈ t
mp₁ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₂ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₃ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₄ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp₅ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mpr : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → x ∈ s ∨ x ∈ t
mp₁ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₂ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₃ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₄ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₅ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp₆ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mpr : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → x ∈ s ∨ x ∈ t
mp₁ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₂ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₃ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₄ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₅ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₆ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp₇ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mpr : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → x ∈ s ∨ x ∈ t
mp₁ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₂ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₃ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₄ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₅ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₆ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
mp₇ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp₈ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mpr : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → x ∈ s ∨ x ∈ t
mp₁ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₂ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₃ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₄ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₅ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₆ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
mp₇ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₈ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mpr₁ : x ∈ s → x ∉ t → x ∈ s ∨ x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mpr : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → x ∈ s ∨ x ∈ t
mp₁ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₂ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₃ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₄ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₅ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₆ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
mp₇ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₈ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
mpr₁ : x ∈ s → x ∉ t → x ∈ s ∨ x ∈ t
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mpr₂ : x ∈ t → x ∉ s → x ∈ s ∨ x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mpr : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → x ∈ s ∨ x ∈ t
mp₁ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₂ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₃ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₄ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₅ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₆ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
mp₇ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₈ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
mpr₁ : x ∈ s → x ∉ t → x ∈ s ∨ x ∈ t
mpr₂ : x ∈ t → x ∉ s → x ∈ s ∨ x ∈ t
mpr₃ : x ∈ s → x ∉ t → x ∈ s ∨ x ∈ t
mpr₄ : x ∈ t → x ∉ s → x ∈ s ∨ x ∈ t
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mpr₅ : x ∈ s → x ∉ t → x ∉ s → x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mpr : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → x ∈ s ∨ x ∈ t
mp₁ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₂ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₃ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₄ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₅ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₆ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
mp₇ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₈ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
mpr₁ : x ∈ s → x ∉ t → x ∈ s ∨ x ∈ t
mpr₂ : x ∈ t → x ∉ s → x ∈ s ∨ x ∈ t
mpr₃ : x ∈ s → x ∉ t → x ∈ s ∨ x ∈ t
mpr₄ : x ∈ t → x ∉ s → x ∈ s ∨ x ∈ t
mpr₅ : x ∈ s → x ∉ t → x ∉ s → x ∈ t
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mpr₆ : x ∈ t → x ∉ s → x ∉ s → x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mpr : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → x ∈ s ∨ x ∈ t
mp₁ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₂ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₃ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₄ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₅ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₆ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
mp₇ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₈ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
mpr₁ : x ∈ s → x ∉ t → x ∈ s ∨ x ∈ t
mpr₂ : x ∈ t → x ∉ s → x ∈ s ∨ x ∈ t
mpr₃ : x ∈ s → x ∉ t → x ∈ s ∨ x ∈ t
mpr₄ : x ∈ t → x ∉ s → x ∈ s ∨ x ∈ t
mpr₅ : x ∈ s → x ∉ t → x ∉ s → x ∈ t
mpr₆ : x ∈ t → x ∉ s → x ∉ s → x ∈ t
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp₉ : x ∈ s → x ∉ s → x ∈ t
Tactic: tauto