awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
mp₉ : x ∈ s → x ∉ s → x ∈ t
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp₁₀ : 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
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
mp₉ : x ∈ s → x ∉ s → x ∈ t
mp₁₀ mp₁₁ mp₁₂ : 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 ∉ s → False
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
mp₉ : x ∈ s → x ∉ s → x ∈ t
mp₁₀ mp₁₁ mp₁₂ : x ∈ s → ¬x ∉ t → x ∈ t
mp₁₃ : x ∈ s → x ∈ s → x ∉ s → False
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp₁₄ : x ∈ s → x ∈ s → ¬x ∉ t → False
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
mp₉ : x ∈ s → x ∉ s → x ∈ t
mp₁₀ mp₁₁ mp₁₂ : x ∈ s → ¬x ∉ t → x ∈ t
mp₁₃ : x ∈ s → x ∈ s → x ∉ s → False
mp₁₄ mp₁₅ mp₁₆ : x ∈ s → x ∈ s → ¬x ∉ t → False
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp₁₇ : x ∈ t → x ∈ s → x ∉ s → False
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
mp₉ : x ∈ s → x ∉ s → x ∈ t
mp₁₀ mp₁₁ mp₁₂ : x ∈ s → ¬x ∉ t → x ∈ t
mp₁₃ : x ∈ s → x ∈ s → x ∉ s → False
mp₁₄ mp₁₅ mp₁₆ : x ∈ s → x ∈ s → ¬x ∉ t → False
mp₁₇ : x ∈ t → x ∈ s → x ∉ s → False
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp₁₈ : x ∈ t → x ∈ s → ¬x ∉ t → False
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
mp₉ : x ∈ s → x ∉ s → x ∈ t
mp₁₀ mp₁₁ mp₁₂ : x ∈ s → ¬x ∉ t → x ∈ t
mp₁₃ : x ∈ s → x ∈ s → x ∉ s → False
mp₁₄ mp₁₅ mp₁₆ : x ∈ s → x ∈ s → ¬x ∉ t → False
mp₁₇ : x ∈ t → x ∈ s → x ∉ s → False
mp₁₈ mp₁₉ mp₂₀ : x ∈ t → x ∈ s → ¬x ∉ t → False
mpr₇ : x ∈ s → x ∉ t → x ∉ s → x ∈ t
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp₂₁ : 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
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
mp₉ : x ∈ s → x ∉ s → x ∈ t
mp₁₀ mp₁₁ mp₁₂ : x ∈ s → ¬x ∉ t → x ∈ t
mp₁₃ : x ∈ s → x ∈ s → x ∉ s → False
mp₁₄ mp₁₅ mp₁₆ : x ∈ s → x ∈ s → ¬x ∉ t → False
mp₁₇ : x ∈ t → x ∈ s → x ∉ s → False
mp₁₈ mp₁₉ mp₂₀ : x ∈ t → x ∈ s → ¬x ∉ t → False
mpr₇ : x ∈ s → x ∉ t → x ∉ s → x ∈ t
mp₂₁ mp₂₂ mp₂₃ : 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 → False
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
mp₉ : x ∈ s → x ∉ s → x ∈ t
mp₁₀ mp₁₁ mp₁₂ : x ∈ s → ¬x ∉ t → x ∈ t
mp₁₃ : x ∈ s → x ∈ s → x ∉ s → False
mp₁₄ mp₁₅ mp₁₆ : x ∈ s → x ∈ s → ¬x ∉ t → False
mp₁₇ : x ∈ t → x ∈ s → x ∉ s → False
mp₁₈ mp₁₉ mp₂₀ : x ∈ t → x ∈ s → ¬x ∉ t → False
mpr₇ : x ∈ s → x ∉ t → x ∉ s → x ∈ t
mp₂₁ mp₂₂ mp₂₃ : x ∈ s → x ∈ t → x ∈ t
mp₂₄ mp₂₅ mp₂₆ : x ∈ s → x ∈ s → x ∈ t → False
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have mp₂₇ : x ∈ t → x ∈ s → x ∈ t → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finset.Basic (hypothesis)
Goal:
α : Type u_4
H : ∀ (s : Finset α), s = ∅
a : α
⊢ False
have H₁ : Eq (α := Finset α) {a} ∅
Tactic: specialize H {a}
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
⊢ Finset.Nonempty.{u_1} (α := α) univ ↔ Nonempty α
have rw : (↑univ : Set α).Nonempty ↔ Nonempty α
Tactic: rw [← coe_nonempty, coe_univ, Set.nonempty_iff_univ_nonempty]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
rw : (↑univ : Set α).Nonempty ↔ Nonempty α
⊢ Finset.Nonempty.{u_1} (α := α) univ ↔ Nonempty α
have rw₁ : Set.Nonempty.{u_1} (α := α) Set.univ ↔ Nonempty α
Tactic: rw [← coe_nonempty, coe_univ, Set.nonempty_iff_univ_nonempty]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
rw : (↑univ : Set α).Nonempty ↔ Nonempty α
rw₁ : Set.Nonempty.{u_1} (α := α) Set.univ ↔ Nonempty α
⊢ Finset.Nonempty.{u_1} (α := α) univ ↔ Nonempty α
have rw₂ : Set.Nonempty.{u_1} (α := α) Set.univ ↔ Set.Nonempty.{u_1} (α := α) Set.univ
Tactic: rw [← coe_nonempty, coe_univ, Set.nonempty_iff_univ_nonempty]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
⊢ Eq.{u_1 + 1} (α := Finset α) univ ∅ ↔ IsEmpty α
have contrapose! : Finset.Nonempty.{u_1} (α := α) univ ↔ Nonempty α
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
⊢ Finset.Nontrivial.{u_1} (α := α) univ ↔ Nontrivial α
have rw : (↑univ : Set α).Nontrivial ↔ Nontrivial α
Tactic: rw [Finset.Nontrivial, Finset.coe_univ, Set.nontrivial_univ_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
rw : (↑univ : Set α).Nontrivial ↔ Nontrivial α
⊢ Finset.Nontrivial.{u_1} (α := α) univ ↔ Nontrivial α
have rw₁ : Set.Nontrivial.{u_1} (α := α) Set.univ ↔ Nontrivial α
Tactic: rw [Finset.Nontrivial, Finset.coe_univ, Set.nontrivial_univ_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
rw : (↑univ : Set α).Nontrivial ↔ Nontrivial α
rw₁ : Set.Nontrivial.{u_1} (α := α) Set.univ ↔ Nontrivial α
⊢ Finset.Nontrivial.{u_1} (α := α) univ ↔ Nontrivial α
have rw₂ : Nontrivial α ↔ Nontrivial α
Tactic: rw [Finset.Nontrivial, Finset.coe_univ, Set.nontrivial_univ_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nontrivial α
a : α
⊢ Ne (α := Finset α) {a} univ
have apply : (↑{a} : Set α) ≠ (↑univ : Set α)
Tactic: apply SetLike.coe_ne_coe.1
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
⊢ a ∉ sᶜ ↔ a ∈ s
have rw : ¬a ∉ s ↔ a ∈ s
Tactic: rw [mem_compl, not_not]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
rw : ¬a ∉ s ↔ a ∈ s
⊢ a ∉ sᶜ ↔ a ∈ s
have rw₁ : a ∈ s ↔ a ∈ s
Tactic: rw [mem_compl, not_not]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
⊢ s ⊆ {a}ᶜ ↔ a ∉ s
have rw : {a} ⊆ sᶜ ↔ a ∉ s
Tactic: rw [subset_compl_comm, singleton_subset_iff, mem_compl]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
rw : {a} ⊆ sᶜ ↔ a ∉ s
⊢ s ⊆ {a}ᶜ ↔ a ∉ s
have rw₁ : a ∈ sᶜ ↔ a ∉ s
Tactic: rw [subset_compl_comm, singleton_subset_iff, mem_compl]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
rw : {a} ⊆ sᶜ ↔ a ∉ s
rw₁ : a ∈ sᶜ ↔ a ∉ s
⊢ s ⊆ {a}ᶜ ↔ a ∉ s
have rw₂ : a ∉ s ↔ a ∉ s
Tactic: rw [subset_compl_comm, singleton_subset_iff, mem_compl]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
⊢ (s.erase a)ᶜ = insert a sᶜ
have h : ∀ (a_1 : α), a_1 ∈ (s.erase a)ᶜ ↔ a_1 ∈ insert a sᶜ
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
⊢ (insert a s)ᶜ = sᶜ.erase a
have h : ∀ (a_1 : α), a_1 ∈ (insert a s)ᶜ ↔ a_1 ∈ sᶜ.erase a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
ha : a ∉ s
⊢ insert a (insert a s)ᶜ = sᶜ
have simp_rw : insert a (sᶜ.erase a) = sᶜ
Tactic: simp_rw [compl_insert, insert_erase (mem_compl.2 ha)]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
⊢ Eq (α := Finset α) (insert x {x}ᶜ) univ
have rw : (erase {x} x)ᶜ = univ
Tactic: rw [← compl_erase, erase_singleton, compl_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
rw : (erase {x} x)ᶜ = univ
⊢ Eq (α := Finset α) (insert x {x}ᶜ) univ
have rw₁ : Eq.{u_1 + 1} (α := Finset α) ∅ᶜ univ
Tactic: rw [← compl_erase, erase_singleton, compl_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
rw : (erase {x} x)ᶜ = univ
rw₁ : Eq.{u_1 + 1} (α := Finset α) ∅ᶜ univ
⊢ Eq (α := Finset α) (insert x {x}ᶜ) univ
have rw₂ : Eq.{u_1 + 1} (α := Finset α) univ univ
Tactic: rw [← compl_erase, erase_singleton, compl_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a : α
⊢ {a}ᶜ = erase univ a
have rw : univ \ {a} = erase univ a
Tactic: rw [compl_eq_univ_sdiff, sdiff_singleton_eq_erase]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a : α
rw : univ \ {a} = erase univ a
⊢ {a}ᶜ = erase univ a
have rw₁ : erase univ a = erase univ a
Tactic: rw [compl_eq_univ_sdiff, sdiff_singleton_eq_erase]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ Set.InjOn (β := Finset α) (fun (a : α) ↦ insert a s) (↑sᶜ : Set α)
have rw : Set.InjOn (β := Finset α) (fun (a : α) ↦ insert a s) (↑s : Set α)ᶜ
Tactic: rw [coe_compl]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ univ ∩ s = s
have h : ∀ (a : α), a ∈ univ ∩ s ↔ a ∈ s
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ s ∩ univ = s
have rw : univ ∩ s = s
Tactic: rw [inter_comm, univ_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
rw : univ ∩ s = s
⊢ s ∩ univ = s
have rw₁ : s = s
Tactic: rw [inter_comm, univ_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Subsingleton α
a : α
⊢ Eq (α := Finset α) {a} univ
have h : ∀ (b : α), Membership.mem (γ := Finset α) {a} b ↔ Membership.mem (γ := Finset α) univ b
Tactic: ext b
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
f : α → β
inst_1 : Fintype β
inst_2 : DecidablePred fun (y : β) ↦ ∃ (x : α), f x = y
inst_3 : DecidableEq β
⊢ {y : β | ∃ (x : α), f x = y} = image f univ
have h : ∀ (a : β), Membership.mem (γ := Finset β) {y : β | ∃ (x : α), f x = y} a ↔ a ∈ image f univ
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype { a : α // p a }
⊢ map (Embedding.subtype p) univ = filter p univ
have rw : map (Embedding.subtype p) univ = map (Embedding.subtype p) (Finset.subtype p univ)
Tactic: rw [← subtype_map, subtype_univ]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype { a : α // p a }
rw : map (Embedding.subtype p) univ = map (Embedding.subtype p) (Finset.subtype p univ)
⊢ map (Embedding.subtype p) univ = filter p univ
have rw₁ : map (Embedding.subtype p) univ = map (Embedding.subtype p) univ
Tactic: rw [← subtype_map, subtype_univ]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype { a : α // p a }
⊢ Multiset.map (α := { a : α // p a }) (Subtype.val (p := fun (a : α) ↦ p a)) (val univ) = (filter p univ).val
have apply : (map (Embedding.subtype p) univ).val = (filter p univ).val
Tactic: apply (map_val (Function.Embedding.subtype p) univ).symm.trans
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype { a : α // p a }
⊢ (map (Embedding.subtype p) univ).val = (filter p univ).val
have h : map (Embedding.subtype p) univ = filter p univ
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
f : α → β
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype { a : α // p a }
⊢ Multiset.map (Subtype.restrict (β := fun (x : α) ↦ β) p f) (val univ) = Multiset.map f (filter p univ).val
have rw : Multiset.map (Subtype.restrict (β := fun (x : α) ↦ β) p f) (val univ) =
  Multiset.map f (Multiset.map (α := { a : α // p a }) (Subtype.val (p := fun (a : α) ↦ p a)) (val univ))
Tactic: rw [← univ_val_map_subtype_val, Multiset.map_map, Subtype.restrict_def]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
f : α → β
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype { a : α // p a }
rw :
  Multiset.map (Subtype.restrict (β := fun (x : α) ↦ β) p f) (val univ) =
    Multiset.map f (Multiset.map (α := { a : α // p a }) (Subtype.val (p := fun (a : α) ↦ p a)) (val univ))
⊢ Multiset.map (Subtype.restrict (β := fun (x : α) ↦ β) p f) (val univ) = Multiset.map f (filter p univ).val
have rw₁ : Multiset.map (Subtype.restrict (β := fun (x : α) ↦ β) p f) (val univ) =
  Multiset.map (α := { a : α // p a }) (f ∘ Subtype.val (p := fun (a : α) ↦ p a)) (val univ)
Tactic: rw [← univ_val_map_subtype_val, Multiset.map_map, Subtype.restrict_def]
-- Lean 4 proof step from Mathlib.Data.Finset.BooleanAlgebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
f : α → β
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype { a : α // p a }
rw :
  Multiset.map (Subtype.restrict (β := fun (x : α) ↦ β) p f) (val univ) =
    Multiset.map f (Multiset.map (α := { a : α // p a }) (Subtype.val (p := fun (a : α) ↦ p a)) (val univ))
rw₁ :
  Multiset.map (Subtype.restrict (β := fun (x : α) ↦ β) p f) (val univ) =
    Multiset.map (α := { a : α // p a }) (f ∘ Subtype.val (p := fun (a : α) ↦ p a)) (val univ)
⊢ Multiset.map (Subtype.restrict (β := fun (x : α) ↦ β) p f) (val univ) = Multiset.map f (filter p univ).val
have rw₂ : Multiset.map (α := Subtype p) (f ∘ fun (a : Subtype p) ↦ (↑a : α)) (val univ) =
  Multiset.map (α := { a : α // p a }) (f ∘ Subtype.val (p := fun (a : α) ↦ p a)) (val univ)
Tactic: rw [← univ_val_map_subtype_val, Multiset.map_map, Subtype.restrict_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
h : a ∈ s
⊢ #(insert a s) = #s
have rw : #s = #s
Tactic: rw [insert_eq_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
⊢ s.toList.length = #s
have rw : s.val.toList.length = #s
Tactic: rw [toList, ← Multiset.coe_card, Multiset.coe_toList, card_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
rw : s.val.toList.length = #s
⊢ s.toList.length = #s
have rw₁ : (↑s.val.toList : Multiset α).card = #s
Tactic: rw [toList, ← Multiset.coe_card, Multiset.coe_toList, card_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
rw : s.val.toList.length = #s
rw₁ : (↑s.val.toList : Multiset α).card = #s
⊢ s.toList.length = #s
have rw₂ : s.val.card = #s
Tactic: rw [toList, ← Multiset.coe_card, Multiset.coe_toList, card_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
rw : s.val.toList.length = #s
rw₁ : (↑s.val.toList : Multiset α).card = #s
rw₂ : s.val.card = #s
⊢ s.toList.length = #s
have rw₃ : s.val.card = s.val.card
Tactic: rw [toList, ← Multiset.coe_card, Multiset.coe_toList, card_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
H : #(image f s) = #s
⊢ Set.InjOn f (↑s : Set α)
have H₁ : { val := (Multiset.map f s.val).dedup, nodup := sorry : Finset β }.val.card = s.val.card
Tactic: rw [card_def, card_def, image, toFinset] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ (Multiset.map f s.val).dedup = Multiset.map f s.val
have refine : (Multiset.map f s.val).card ≤ (Multiset.map f s.val).dedup.card
Tactic: refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Card (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ Set.InjOn f (↑s : Set α)
have this : (Multiset.map f s.val).dedup = Multiset.map f s.val
Tactic: have : (s.1.map f).dedup = s.1.map f := by
    refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
    simp only [H, Multiset.card_map, le_rfl]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
this : (Multiset.map f s.val).dedup = Multiset.map f s.val
⊢ Set.InjOn f (↑s : Set α)
have this₁ : (Multiset.map f s.val).Nodup
Tactic: rw [Multiset.dedup_eq_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
y : β
⊢ #({x ∈ s | f x = y}) ≠ 0 ↔ y ∈ image f s
have rw : 0 < #({x ∈ s | f x = y}) ↔ y ∈ image f s
Tactic: rw [← Nat.pos_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
y : β
rw : 0 < #({x ∈ s | f x = y}) ↔ y ∈ image f s
⊢ #({x ∈ s | f x = y}) ≠ 0 ↔ y ∈ image f s
have rw₁ : {x ∈ s | f x = y}.Nonempty ↔ y ∈ image f s
Tactic: rw [← Nat.pos_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image]