awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
pos : ∀ (h' : a ∈ s₁), lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁
⊢ lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁
have neg : ∀ (h' : a ∉ s₁), lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁
Tactic: by_cases h' : a ∈ s₁
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∈ s₁
⊢ lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁
have pos : lookup (β := β) a s₁ = lookup (β := β) a s₁
Tactic: rw [lookup_union_left h']
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
⊢ lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁
have neg : lookup (β := β) a s₂ = lookup (β := β) a s₁
Tactic: rw [lookup_union_right h', lookup_eq_none.mpr h, lookup_eq_none.mpr h']
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
neg : lookup (β := β) a s₂ = lookup (β := β) a s₁
⊢ lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁
have neg₁ : none = lookup (β := β) a s₁
Tactic: rw [lookup_union_right h', lookup_eq_none.mpr h, lookup_eq_none.mpr h']
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
neg : lookup (β := β) a s₂ = lookup (β := β) a s₁
neg₁ : none = lookup (β := β) a s₁
⊢ lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁
have neg₂ : Eq.{v + 1} (α := Option (β a)) none none
Tactic: rw [lookup_union_right h', lookup_eq_none.mpr h, lookup_eq_none.mpr h']
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup (β := β) a s = some b
x : α
⊢ lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s
have pos : ∀ (h' : x = a), lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s
Tactic: by_cases h' : x = a
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup (β := β) a s = some b
x : α
pos : ∀ (h' : x = a), lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s
⊢ lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s
have neg : ∀ (h' : ¬x = a), lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s
Tactic: by_cases h' : x = a
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup (β := β) a s = some b
x : α
h' : x = a
⊢ lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s
have pos : ∀ (b : β x) (h : lookup (β := β) x s = some b),
  lookup (β := β) x (erase (β := β) x s ∪ singleton (β := β) x b) = lookup (β := β) x s
Tactic: subst a
Cleared hypotheses: a, b, h, h'
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup (β := β) x s = some b
⊢ lookup (β := β) x (erase (β := β) x s ∪ singleton (β := β) x b) = lookup (β := β) x s
have pos : lookup (β := β) x (singleton (β := β) x b) = lookup (β := β) x s
Tactic: rw [lookup_union_right notMem_erase_self, lookup_singleton_eq, h]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup (β := β) x s = some b
pos : lookup (β := β) x (singleton (β := β) x b) = lookup (β := β) x s
⊢ lookup (β := β) x (erase (β := β) x s ∪ singleton (β := β) x b) = lookup (β := β) x s
have pos₁ : some b = lookup (β := β) x s
Tactic: rw [lookup_union_right notMem_erase_self, lookup_singleton_eq, h]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup (β := β) x s = some b
pos : lookup (β := β) x (singleton (β := β) x b) = lookup (β := β) x s
pos₁ : some b = lookup (β := β) x s
⊢ lookup (β := β) x (erase (β := β) x s ∪ singleton (β := β) x b) = lookup (β := β) x s
have pos₂ : some b = some b
Tactic: rw [lookup_union_right notMem_erase_self, lookup_singleton_eq, h]
-- Lean 4 proof step from Mathlib.Data.Finmap (hypothesis)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup (β := β) a s = some b
x : α
h' : ¬x = a
⊢ lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s
have this : x ∉ singleton (β := β) a b
Tactic: have : x ∉ singleton a b := by rwa [mem_singleton]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup (β := β) a s = some b
x : α
h' : ¬x = a
this : x ∉ singleton (β := β) a b
⊢ lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s
have neg : lookup (β := β) x (erase (β := β) a s) = lookup (β := β) x s
Tactic: rw [lookup_union_left_of_not_in this, lookup_erase_ne h']
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup (β := β) a s = some b
x : α
h' : ¬x = a
this : x ∉ singleton (β := β) a b
neg : lookup (β := β) x (erase (β := β) a s) = lookup (β := β) x s
⊢ lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s
have neg₁ : lookup (β := β) x s = lookup (β := β) x s
Tactic: rw [lookup_union_left_of_not_in this, lookup_erase_ne h']
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
x y z : Finmap β
⊢ x.Disjoint (β := β) (y ∪ z) ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
have rw : (y ∪ z).Disjoint (β := β) x ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
Tactic: rw [Disjoint.symm_iff, disjoint_union_left, Disjoint.symm_iff _ x, Disjoint.symm_iff _ x]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
x y z : Finmap β
rw : (y ∪ z).Disjoint (β := β) x ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
⊢ x.Disjoint (β := β) (y ∪ z) ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
have rw₁ : y.Disjoint (β := β) x ∧ z.Disjoint (β := β) x ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
Tactic: rw [Disjoint.symm_iff, disjoint_union_left, Disjoint.symm_iff _ x, Disjoint.symm_iff _ x]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
x y z : Finmap β
rw : (y ∪ z).Disjoint (β := β) x ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
rw₁ : y.Disjoint (β := β) x ∧ z.Disjoint (β := β) x ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
⊢ x.Disjoint (β := β) (y ∪ z) ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
have rw₂ : x.Disjoint (β := β) y ∧ z.Disjoint (β := β) x ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
Tactic: rw [Disjoint.symm_iff, disjoint_union_left, Disjoint.symm_iff _ x, Disjoint.symm_iff _ x]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
x y z : Finmap β
rw : (y ∪ z).Disjoint (β := β) x ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
rw₁ : y.Disjoint (β := β) x ∧ z.Disjoint (β := β) x ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
rw₂ : x.Disjoint (β := β) y ∧ z.Disjoint (β := β) x ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
⊢ x.Disjoint (β := β) (y ∪ z) ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
have rw₃ : x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
Tactic: rw [Disjoint.symm_iff, disjoint_union_left, Disjoint.symm_iff _ x, Disjoint.symm_iff _ x]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
⊢ s₁ = s₂
have a : ∀ (x : α), lookup (β := β) x s₁ = lookup (β := β) x s₂
Tactic: apply ext_lookup
-- Lean 4 proof step from Mathlib.Data.Finmap (hypothesis)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂
have this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
Tactic: have : (s₁ ∪ s₃).lookup x = (s₂ ∪ s₃).lookup x := h'' ▸ rfl
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂
have pos : ∀ (hs₁ : x ∈ s₁), lookup (β := β) x s₁ = lookup (β := β) x s₂
Tactic: by_cases hs₁ : x ∈ s₁
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
pos : ∀ (hs₁ : x ∈ s₁), lookup (β := β) x s₁ = lookup (β := β) x s₂
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂
have neg : ∀ (hs₁ : x ∉ s₁), lookup (β := β) x s₁ = lookup (β := β) x s₂
Tactic: by_cases hs₁ : x ∈ s₁
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
hs₁ : x ∈ s₁
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂
have pos : ∀ (this : lookup (β := β) x s₁ = lookup (β := β) x (s₂ ∪ s₃)) (hs₁ : x ∈ s₁),
  lookup (β := β) x s₁ = lookup (β := β) x s₂
Tactic: rwa [lookup_union_left hs₁, lookup_union_left_of_not_in (h _ hs₁)] at this
Cleared hypotheses: this, hs₁
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
hs₁ : x ∈ s₁
pos :
  ∀ (this : lookup (β := β) x s₁ = lookup (β := β) x (s₂ ∪ s₃)) (hs₁ : x ∈ s₁),
    lookup (β := β) x s₁ = lookup (β := β) x s₂
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂
have pos₁ : ∀ (this : lookup (β := β) x s₁ = lookup (β := β) x s₂) (hs₁ : x ∈ s₁), lookup (β := β) x s₁ = lookup (β := β) x s₂
Tactic: rwa [lookup_union_left hs₁, lookup_union_left_of_not_in (h _ hs₁)] at this
Cleared hypotheses: this, hs₁
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂
have pos : ∀ (hs₂ : x ∈ s₂), lookup (β := β) x s₁ = lookup (β := β) x s₂
Tactic: by_cases hs₂ : x ∈ s₂
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
pos : ∀ (hs₂ : x ∈ s₂), lookup (β := β) x s₁ = lookup (β := β) x s₂
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂
have neg : ∀ (hs₂ : x ∉ s₂), lookup (β := β) x s₁ = lookup (β := β) x s₂
Tactic: by_cases hs₂ : x ∈ s₂
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∈ s₂
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂
have pos : ∀ (this : lookup (β := β) x s₁ = lookup (β := β) x (s₂ ∪ s₃)) (hs₁ : x ∉ s₁) (hs₂ : x ∈ s₂),
  lookup (β := β) x s₁ = lookup (β := β) x s₂
Tactic: rwa [lookup_union_left_of_not_in (h' _ hs₂), lookup_union_left hs₂] at this
Cleared hypotheses: this, hs₁, hs₂
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∈ s₂
pos :
  ∀ (this : lookup (β := β) x s₁ = lookup (β := β) x (s₂ ∪ s₃)) (hs₁ : x ∉ s₁) (hs₂ : x ∈ s₂),
    lookup (β := β) x s₁ = lookup (β := β) x s₂
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂
have pos₁ : ∀ (this : lookup (β := β) x s₁ = lookup (β := β) x s₂) (hs₁ : x ∉ s₁) (hs₂ : x ∈ s₂),
  lookup (β := β) x s₁ = lookup (β := β) x s₂
Tactic: rwa [lookup_union_left_of_not_in (h' _ hs₂), lookup_union_left hs₂] at this
Cleared hypotheses: this, hs₁, hs₂
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∉ s₂
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂
have neg : none = lookup (β := β) x s₂
Tactic: rw [lookup_eq_none.mpr hs₁, lookup_eq_none.mpr hs₂]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∉ s₂
neg : none = lookup (β := β) x s₂
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂
have neg₁ : Eq.{v + 1} (α := Option (β x)) none none
Tactic: rw [lookup_eq_none.mpr hs₁, lookup_eq_none.mpr hs₂]
-- Lean 4 proof step from Mathlib.Data.Finset.Attach (goal)
Goal:
α : Type u_1
s : Finset α
⊢ (↑s.attach : Set ↥s) = Set.univ
have h : ∀ (x : ↥s), x ∈ (↑s.attach : Set ↥s) ↔ Membership.mem (γ := Set ↥s) Set.univ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ Disjoint s t ∨ (s ∩ t).Nonempty
have rw : Disjoint s t ∨ ¬Disjoint s t
Tactic: rw [← not_disjoint_iff_nonempty_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ (s.erase a).Nonempty ↔ s.Nontrivial
have simp : (∃ x ∈ s, x ≠ a) ↔ s.Nontrivial
Tactic: simp only [Finset.Nonempty, mem_erase, and_comm (b := _ ∈ _)]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ (∃ x ∈ s, x ≠ a) ↔ s.Nontrivial
have refine : (∃ x ∈ s, x ≠ a) → s.Nontrivial
Tactic: refine ⟨?_, fun hs ↦ hs.exists_ne a⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ s.erase a ⊆ (insert a s).erase a
have grw : s.erase a ⊆ s.erase a
Tactic: grw [← subset_insert]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ s ⊆ insert a t ↔ s ⊆ t
have rw : s.erase a ⊆ t ↔ s ⊆ t
Tactic: rw [subset_insert_iff, erase_eq_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
rw : s.erase a ⊆ t ↔ s ⊆ t
⊢ s ⊆ insert a t ↔ s ⊆ t
have rw₁ : s ⊆ t ↔ s ⊆ t
Tactic: rw [subset_insert_iff, erase_eq_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
h : a ∈ t
⊢ s.erase a ⊆ t ↔ s ⊆ t
have rw : s ⊆ insert a t ↔ s ⊆ t
Tactic: rw [← subset_insert_iff, insert_eq_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
h : a ∈ t
rw : s ⊆ insert a t ↔ s ⊆ t
⊢ s.erase a ⊆ t ↔ s ⊆ t
have rw₁ : s ⊆ t ↔ s ⊆ t
Tactic: rw [← subset_insert_iff, insert_eq_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
hs : Membership.mem (γ := Set (Finset α)) {s : Finset α | a ∈ s} s
t : Finset α
ht : Membership.mem (γ := Set (Finset α)) {s : Finset α | a ∈ s} t
h : s.erase a = (fun (s : Finset α) ↦ s.erase a) t
⊢ s = t
have rw : insert a (s.erase a) = t
Tactic: rw [← insert_erase hs, ← insert_erase ht, h]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
hs : Membership.mem (γ := Set (Finset α)) {s : Finset α | a ∈ s} s
t : Finset α
ht : Membership.mem (γ := Set (Finset α)) {s : Finset α | a ∈ s} t
h : s.erase a = (fun (s : Finset α) ↦ s.erase a) t
rw : insert a (s.erase a) = t
⊢ s = t
have rw₁ : insert a (s.erase a) = insert a (t.erase a)
Tactic: rw [← insert_erase hs, ← insert_erase ht, h]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
hs : Membership.mem (γ := Set (Finset α)) {s : Finset α | a ∈ s} s
t : Finset α
ht : Membership.mem (γ := Set (Finset α)) {s : Finset α | a ∈ s} t
h : s.erase a = (fun (s : Finset α) ↦ s.erase a) t
rw : insert a (s.erase a) = t
rw₁ : insert a (s.erase a) = insert a (t.erase a)
⊢ s = t
have rw₂ : insert a ((fun (s : Finset α) ↦ s.erase a) t) = insert a (t.erase a)
Tactic: rw [← insert_erase hs, ← insert_erase ht, h]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nontrivial
⊢ ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
have obtain : ∀ (a : α) (ha : a ∈ (↑s : Set α)) (b : α) (hb : b ∈ (↑s : Set α)) (hab : a ≠ b),
  ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) sorry = s
Tactic: obtain ⟨a, ha, b, hb, hab⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (hypothesis)
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
⊢ ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
have this : b ∈ s.erase a
Tactic: have : b ∈ s.erase a := mem_erase.2 ⟨hab.symm, hb⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
this : b ∈ s.erase a
⊢ ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
have refine_1 : a ∉ (s.erase a).erase b
Tactic: refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
this : b ∈ s.erase a
refine_1 : a ∉ (s.erase a).erase b
⊢ ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
have refine_2 : b ∉ (s.erase a).erase b
Tactic: refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
this : b ∈ s.erase a
refine_1 : a ∉ (s.erase a).erase b
refine_2 : b ∉ (s.erase a).erase b
⊢ ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
have refine_3 : ¬a = b
Tactic: refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
this : b ∈ s.erase a
refine_1 : a ∉ (s.erase a).erase b
refine_2 : b ∉ (s.erase a).erase b
refine_3 : ¬a = b
⊢ ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
have refine_4 : cons a (cons b ((s.erase a).erase b) sorry) sorry = s
Tactic: refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nontrivial
⊢ ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
have obtain : ∀ (a : α) (ha : a ∈ (↑s : Set α)) (b : α) (hb : b ∈ (↑s : Set α)) (hab : a ≠ b),
  ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) sorry = s
Tactic: classical
  obtain ⟨a, ha, b, hb, hab⟩ := hs
  have : b ∈ s.erase a := mem_erase.2 ⟨hab.symm, hb⟩
  refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩ <;> simp [insert_erase ha, *]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nontrivial
obtain :
  ∀ (a : α) (ha : a ∈ (↑s : Set α)) (b : α) (hb : b ∈ (↑s : Set α)) (hab : a ≠ b),
    ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
⊢ ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
have obtain₁ : ∀ (a : α) (ha : a ∈ (↑s : Set α)) (b : α) (hb : b ∈ (↑s : Set α)) (hab : a ≠ b) (this : b ∈ s.erase a),
  ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) sorry = s
Tactic: classical
  obtain ⟨a, ha, b, hb, hab⟩ := hs
  have : b ∈ s.erase a := mem_erase.2 ⟨hab.symm, hb⟩
  refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩ <;> simp [insert_erase ha, *]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
hb : b ∈ s
⊢ s.erase a \ s.erase b = {b}
have h : ∀ (a_1 : α), a_1 ∈ s.erase a \ s.erase b ↔ Membership.mem (γ := Finset α) {b} a_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)
have simp_rw : Disjoint (s \ {a}) t ↔ Disjoint s (t \ {a})
Tactic: simp_rw [erase_eq, disjoint_sdiff_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
⊢ Disjoint (s.erase a) (insert a t) ↔ Disjoint s t
have rw : Disjoint s ((insert a t).erase a) ↔ Disjoint s t
Tactic: rw [disjoint_erase_comm, erase_insert ha]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
rw : Disjoint s ((insert a t).erase a) ↔ Disjoint s t
⊢ Disjoint (s.erase a) (insert a t) ↔ Disjoint s t
have rw₁ : Disjoint s t ↔ Disjoint s t
Tactic: rw [disjoint_erase_comm, erase_insert ha]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ Disjoint (insert a s) (t.erase a) ↔ Disjoint s t
have rw : Disjoint ((insert a s).erase a) t ↔ Disjoint s t
Tactic: rw [← disjoint_erase_comm, erase_insert ha]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
rw : Disjoint ((insert a s).erase a) t ↔ Disjoint s t
⊢ Disjoint (insert a s) (t.erase a) ↔ Disjoint s t
have rw₁ : Disjoint s t ↔ Disjoint s t
Tactic: rw [← disjoint_erase_comm, erase_insert ha]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ Disjoint s t
have rw : a ∉ s.erase a ∧ Disjoint (s.erase a) t
Tactic: rw [← erase_insert ha, ← disjoint_erase_comm, disjoint_insert_right]
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
⊢ Disjoint s t
have rw : a ∉ t.erase a ∧ Disjoint s (t.erase a)
Tactic: rw [← erase_insert ha, disjoint_erase_comm, disjoint_insert_left]