awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Set α
f : α → ℕ
⊢ s.EquitableOn f ↔ ∃ (b : ℕ), ∀ a ∈ s, f a = b ∨ f a = b + 1
have simp_rw : (∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1) ↔ ∃ (b : ℕ), ∀ a ∈ s, f a = b ∨ f a = b + 1
Tactic: simp_rw [equitableOn_iff_exists_le_le_add_one, Nat.le_and_le_add_one_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
s : Set α
hs : s.Subsingleton
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f i ≤ f j + 1
have rw : f j ≤ f j + 1
Tactic: rw [hs hi hj]
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ (↑s : Set α).EquitableOn f ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
have rw : (∃ (b : ℕ), ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1) ↔
  ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
Tactic: rw [Set.equitableOn_iff_exists_le_le_add_one]
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ (∃ (b : ℕ), ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1) ↔
    ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
have refine : (∃ (b : ℕ), ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1) →
  ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
Tactic: refine ⟨?_, fun h => ⟨_, h⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
have pos : ∀ (h : ∀ a ∈ s, f a = b + 1), ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
Tactic: by_cases! h : ∀ a ∈ s, f a = b + 1
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
pos : ∀ (h : ∀ a ∈ s, f a = b + 1), ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
have neg : ∀ (h : ∃ a ∈ s, f a ≠ b + 1), ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
Tactic: by_cases! h : ∀ a ∈ s, f a = b + 1
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
h : ∀ a ∈ s, f a = b + 1
a : α
ha : a ∈ s
⊢ (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
have pos : b + 1 ≤ b + 1 ∧ b + 1 ≤ b + 1 + 1
Tactic: rw [h _ ha, sum_const_nat h, Nat.mul_div_cancel_left _ (card_pos.2 ⟨a, ha⟩)]
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
h : ∃ a ∈ s, f a ≠ b + 1
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
have neg : ∀ (x : α) (hx₁ : x ∈ s) (hx₂ : f x ≠ b + 1), ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
Tactic: obtain ⟨x, hx₁, hx₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
h : b = (∑ i ∈ s, f i) / #s
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
have simp_rw : ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
Tactic: simp_rw [← h]
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
have neg : b = (∑ i ∈ s, f i) / #s
Tactic: suffices h : b = (∑ i ∈ s, f i) / s.card by
    simp_rw [← h]
    apply hb
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ b = (∑ i ∈ s, f i) / #s
have neg : (∑ i ∈ s, f i) / #s = b
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ (∑ i ∈ s, f i) / #s = b
have neg : ∑ i ∈ s, (b + 1) ≤ (b + 1) * #s
Tactic: refine
    Nat.div_eq_of_lt_le (le_trans (by simp [mul_comm]) (sum_le_sum fun a ha => (hb a ha).1))
      ((sum_lt_sum (fun a ha => (hb a ha).2) ⟨_, hx₁, (hb _ hx₁).2.lt_of_ne hx₂⟩).trans_le ?_)
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∑ i ∈ s, (b + 1) ≤ (b + 1) * #s
have neg : ∀ x ∈ s, b + 1 = b + 1
Tactic: rw [mul_comm, sum_const_nat]
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ (↑s : Set α).EquitableOn f ↔ ∀ a ∈ s, f a = (∑ i ∈ s, f i) / #s ∨ f a = (∑ i ∈ s, f i) / #s + 1
have simp_rw : (∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1) ↔
  ∀ a ∈ s, f a = (∑ i ∈ s, f i) / #s ∨ f a = (∑ i ∈ s, f i) / #s + 1
Tactic: simp_rw [equitableOn_iff_le_le_add_one, Nat.le_and_le_add_one_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
inst : Fintype (↑s : Type u)
h : s.Finite
⊢ h.toFinset (s := s) = s.toFinset
have rw : s.toFinset = s.toFinset
Tactic: rw [Finite.toFinset, Subsingleton.elim h.fintype]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
inst : Fintype (↑s : Type u)
h : s.Finite
rw : s.toFinset = s.toFinset
⊢ h.toFinset (s := s) = s.toFinset
have rw₁ : s.toFinset = s.toFinset
Tactic: rw [Finite.toFinset, Subsingleton.elim h.fintype]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
h : s.Finite
⊢ ∃ (s' : Finset α), ∀ (a : α), a ∈ s' ↔ a ∈ s
have intro : ∀ (val : Fintype (↑s : Type u)), ∃ (s' : Finset α), ∀ (a : α), a ∈ s' ↔ a ∈ s
Tactic: cases h.nonempty_fintype
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
h : s.Finite
⊢ ∃ (s' : Finset α), (↑s' : Set α) = s
have intro : ∀ (val : Fintype (↑s : Type u)), ∃ (s' : Finset α), (↑s' : Set α) = s
Tactic: cases h.nonempty_fintype
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
hs : s.Finite
⊢ hs.toFinset (s := s).Nonempty ↔ s.Nonempty
have rw : (↑(hs.toFinset (s := s)) : Set α).Nonempty ↔ s.Nonempty
Tactic: rw [← Finset.coe_nonempty, Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
hs : s.Finite
rw : (↑(hs.toFinset (s := s)) : Set α).Nonempty ↔ s.Nonempty
⊢ hs.toFinset (s := s).Nonempty ↔ s.Nonempty
have rw₁ : s.Nonempty ↔ s.Nonempty
Tactic: rw [← Finset.coe_nonempty, Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
hs : s.Finite
⊢ ↥(hs.toFinset (s := s)) = (↑s : Type u)
have rw : (↑(↑(hs.toFinset (s := s)) : Set α) : Type u) = (↑s : Type u)
Tactic: rw [← Finset.coe_sort_coe _, hs.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
hs : s.Finite
rw : (↑(↑(hs.toFinset (s := s)) : Set α) : Type u) = (↑s : Type u)
⊢ ↥(hs.toFinset (s := s)) = (↑s : Type u)
have rw₁ : (↑s : Type u) = (↑s : Type u)
Tactic: rw [← Finset.coe_sort_coe _, hs.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
hs : s.Finite
t : Finset α
⊢ hs.toFinset (s := s) ⊆ t ↔ s ⊆ (↑t : Set α)
have rw : (↑(hs.toFinset (s := s)) : Set α) ⊆ (↑t : Set α) ↔ s ⊆ (↑t : Set α)
Tactic: rw [← Finset.coe_subset, Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
hs : s.Finite
t : Finset α
rw : (↑(hs.toFinset (s := s)) : Set α) ⊆ (↑t : Set α) ↔ s ⊆ (↑t : Set α)
⊢ hs.toFinset (s := s) ⊆ t ↔ s ⊆ (↑t : Set α)
have rw₁ : s ⊆ (↑t : Set α) ↔ s ⊆ (↑t : Set α)
Tactic: rw [← Finset.coe_subset, Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
hs : s.Finite
t : Finset α
⊢ hs.toFinset (s := s) ⊂ t ↔ s ⊂ (↑t : Set α)
have rw : (↑(hs.toFinset (s := s)) : Set α) ⊂ (↑t : Set α) ↔ s ⊂ (↑t : Set α)
Tactic: rw [← Finset.coe_ssubset, Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
hs : s.Finite
t : Finset α
rw : (↑(hs.toFinset (s := s)) : Set α) ⊂ (↑t : Set α) ↔ s ⊂ (↑t : Set α)
⊢ hs.toFinset (s := s) ⊂ t ↔ s ⊂ (↑t : Set α)
have rw₁ : s ⊂ (↑t : Set α) ↔ s ⊂ (↑t : Set α)
Tactic: rw [← Finset.coe_ssubset, Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
t : Set α
ht : t.Finite
s : Finset α
⊢ s ⊆ ht.toFinset (s := t) ↔ (↑s : Set α) ⊆ t
have rw : (↑s : Set α) ⊆ (↑(ht.toFinset (s := t)) : Set α) ↔ (↑s : Set α) ⊆ t
Tactic: rw [← Finset.coe_subset, Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
t : Set α
ht : t.Finite
s : Finset α
rw : (↑s : Set α) ⊆ (↑(ht.toFinset (s := t)) : Set α) ↔ (↑s : Set α) ⊆ t
⊢ s ⊆ ht.toFinset (s := t) ↔ (↑s : Set α) ⊆ t
have rw₁ : (↑s : Set α) ⊆ t ↔ (↑s : Set α) ⊆ t
Tactic: rw [← Finset.coe_subset, Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
t : Set α
ht : t.Finite
s : Finset α
⊢ s ⊂ ht.toFinset (s := t) ↔ (↑s : Set α) ⊂ t
have rw : (↑s : Set α) ⊂ (↑(ht.toFinset (s := t)) : Set α) ↔ (↑s : Set α) ⊂ t
Tactic: rw [← Finset.coe_ssubset, Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
t : Set α
ht : t.Finite
s : Finset α
rw : (↑s : Set α) ⊂ (↑(ht.toFinset (s := t)) : Set α) ↔ (↑s : Set α) ⊂ t
⊢ s ⊂ ht.toFinset (s := t) ↔ (↑s : Set α) ⊂ t
have rw₁ : (↑s : Set α) ⊂ t ↔ (↑s : Set α) ⊂ t
Tactic: rw [← Finset.coe_ssubset, Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s t : Set α
inst : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∩ t).Finite
⊢ h.toFinset (s := s ∩ t) = hs.toFinset (s := s) ∩ ht.toFinset (s := t)
have h₁ : ∀ (a : α), a ∈ h.toFinset (s := s ∩ t) ↔ a ∈ hs.toFinset (s := s) ∩ ht.toFinset (s := t)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s t : Set α
inst : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∪ t).Finite
⊢ h.toFinset (s := s ∪ t) = hs.toFinset (s := s) ∪ ht.toFinset (s := t)
have h₁ : ∀ (a : α), a ∈ h.toFinset (s := s ∪ t) ↔ a ∈ hs.toFinset (s := s) ∪ ht.toFinset (s := t)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s t : Set α
inst : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s \ t).Finite
⊢ h.toFinset (s := s \ t) = hs.toFinset (s := s) \ ht.toFinset (s := t)
have h₁ : ∀ (a : α), a ∈ h.toFinset (s := s \ t) ↔ a ∈ hs.toFinset (s := s) \ ht.toFinset (s := t)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s t : Set α
inst : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∆ t).Finite
⊢ h.toFinset (s := s ∆ t) = hs.toFinset (s := s) ∆ ht.toFinset (s := t)
have h₁ : ∀ (a : α), a ∈ h.toFinset (s := s ∆ t) ↔ a ∈ hs.toFinset (s := s) ∆ ht.toFinset (s := t)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
inst : DecidableEq α
inst_1 : Fintype α
hs : s.Finite
h : sᶜ.Finite
⊢ h.toFinset (s := sᶜ) = (hs.toFinset (s := s))ᶜ
have h₁ : ∀ (a : α), a ∈ h.toFinset (s := sᶜ) ↔ a ∈ (hs.toFinset (s := s))ᶜ
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
s : Set α
inst : DecidableEq β
f : α → β
hs : s.Finite
h : (f '' s).Finite
⊢ h.toFinset (s := f '' s) = Finset.image f (hs.toFinset (s := s))
have h₁ : ∀ (a : β), a ∈ h.toFinset (s := f '' s) ↔ a ∈ Finset.image f (hs.toFinset (s := s))
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Fintype β
f : β → α
h : (range f).Finite
⊢ h.toFinset (s := range f) = Finset.image f Finset.univ
have h₁ : ∀ (a : α), a ∈ h.toFinset (s := range f) ↔ a ∈ Finset.image f Finset.univ
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
h : s.Finite
⊢ h.toFinset (s := s).Nontrivial ↔ s.Nontrivial
have rw : (↑(h.toFinset (s := s)) : Set α).Nontrivial ↔ s.Nontrivial
Tactic: rw [Finset.Nontrivial, h.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
h : s.Finite
rw : (↑(h.toFinset (s := s)) : Set α).Nontrivial ↔ s.Nontrivial
⊢ h.toFinset (s := s).Nontrivial ↔ s.Nontrivial
have rw₁ : s.Nontrivial ↔ s.Nontrivial
Tactic: rw [Finset.Nontrivial, h.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Fintype (↑s : Type u)
inst_1 : DecidablePred fun (x : α) ↦ x ∈ t
h : t ⊆ s
⊢ Fintype (↑t : Type u)
have rw : Fintype (↑(s ∩ t) : Type u)
Tactic: rw [← inter_eq_self_of_subset_right h]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Finset α
⊢ ⋯.toFinset (s := (↑s : Set α)) = s
have rw : (↑s : Set α).toFinset = s
Tactic: rw [toFinite_toFinset, toFinset_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Finset α
rw : (↑s : Set α).toFinset = s
⊢ ⋯.toFinset (s := (↑s : Set α)) = s
have rw₁ : s = s
Tactic: rw [toFinite_toFinset, toFinset_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
inst : DecidableEq α
s : Multiset α
⊢ ⋯.toFinset (s := {x : α | x ∈ s}) = s.toFinset
have h : ∀ (x : α), x ∈ sorry.toFinset (s := {x : α | x ∈ s}) ↔ x ∈ s.toFinset
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Finite.{u + 1} (↑s : Type u)
inst_1 : Finite.{u + 1} (↑t : Type u)
⊢ Finite.{u + 1} (↑(s ∪ t) : Type u)
have intro : ∀ (val : Fintype (↑s : Type u)), Finite.{u + 1} (↑(s ∪ t) : Type u)
Tactic: cases nonempty_fintype s
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Finite.{u + 1} (↑s : Type u)
inst_1 : Finite.{u + 1} (↑t : Type u)
val : Fintype (↑s : Type u)
⊢ Finite.{u + 1} (↑(s ∪ t) : Type u)
have intro : ∀ (val : Fintype (↑t : Type u)), Finite.{u + 1} (↑(s ∪ t) : Type u)
Tactic: cases nonempty_fintype t
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst : Finite.{u + 1} (↑s : Type u)
⊢ Finite.{u + 1} (↑{a : α | a ∈ s ∧ p a} : Type u)
have intro : ∀ (val : Fintype (↑s : Type u)), Finite.{u + 1} (↑{a : α | a ∈ s ∧ p a} : Type u)
Tactic: cases nonempty_fintype s
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s t : Set α
inst : Finite.{u + 1} (↑s : Type u)
h : t ⊆ s
⊢ Finite.{u + 1} (↑t : Type u)
have rw : Finite.{u + 1} (↑{x : α | x ∈ s ∧ x ∈ t} : Type u)
Tactic: rw [← sep_eq_of_subset h]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
inst : Finite.{u + 1} (↑s : Type u)
⊢ Finite.{v + 1} (↑(f '' s) : Type v)
have intro : ∀ (val : Fintype (↑s : Type u)), Finite.{v + 1} (↑(f '' s) : Type v)
Tactic: cases nonempty_fintype s
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (hypothesis)
Goal:
α : Type u
s : Set α
hs : s.Finite
t : Set α
ht : t ⊆ s
⊢ t.Finite
have this : Finite.{u + 1} (↑s : Type u)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (hypothesis)
Goal:
α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).Finite
have hs₁ : Finite.{u + 1} (↑s : Type u)
Tactic: rw [Set.Finite] at hs ht
Cleared hypotheses: hs, ht
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (hypothesis)
Goal:
α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
hs₁ : Finite.{u + 1} (↑s : Type u)
⊢ (s ∪ t).Finite
have ht₁ : Finite.{u + 1} (↑t : Type u)
Tactic: rw [Set.Finite] at hs ht
Cleared hypotheses: hs, ht
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ Finite α
have rw : (s ∪ sᶜ).Finite
Tactic: rw [← finite_univ_iff, ← union_compl_self s]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (hypothesis)
Goal:
α : Type u
β : Type v
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).Finite
have this : Finite.{u + 1} (↑s : Type u)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
⊢ s.Finite
have rw : (f '' f ⁻¹' s).Finite
Tactic: rw [← image_preimage_eq_of_subset hs]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
⊢ SurjOn f s s ↔ BijOn f s s
have refine : ∀ (h : SurjOn f s s), InjOn f s
Tactic: refine ⟨fun h ↦ ⟨hm, ?_, h⟩, BijOn.surjOn⟩
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (hypothesis)
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : SurjOn f s s
⊢ InjOn f s
have this : Finite.{u + 1} (↑s : Type u)
Tactic: have : Finite s := finite_coe_iff.mpr hs
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
⊢ InjOn f s ↔ BijOn f s s
have refine : ∀ (h : InjOn f s), SurjOn f s s
Tactic: refine ⟨fun h ↦ ⟨hm, h, ?_⟩, BijOn.injOn⟩
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (hypothesis)
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : InjOn f s
⊢ SurjOn f s s
have this : Finite.{u + 1} (↑s : Type u)
Tactic: have : Finite s := finite_coe_iff.mpr hs
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)
have simp_rw : (∃ (s_1 : Finset β), (∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ Finset.image f s' = s_1) ∧ p (↑s_1 : Set β)) ↔
  ∃ (s_1 : Finset α), (↑s_1 : Set α) ⊆ s ∧ p (f '' (↑s_1 : Set α))
Tactic: simp_rw [@and_comm (_ ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
    Finset.subset_set_image_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)
have simp_rw : (∃ (t : Set β), (t.Finite ∧ p t) ∧ t ⊆ f '' s) ↔ ∃ (t : Set α), (t.Finite ∧ p (f '' t)) ∧ t ⊆ s
Tactic: classical
  simp_rw [@and_comm (_ ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
    Finset.subset_set_image_iff]
  aesop
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
simp_rw : (∃ (t : Set β), (t.Finite ∧ p t) ∧ t ⊆ f '' s) ↔ ∃ (t : Set α), (t.Finite ∧ p (f '' t)) ∧ t ⊆ s
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)
have simp_rw₁ : (∃ (t : Set β), t.Finite ∧ p t ∧ t ⊆ f '' s) ↔ ∃ (t : Set α), t.Finite ∧ p (f '' t) ∧ t ⊆ s
Tactic: classical
  simp_rw [@and_comm (_ ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
    Finset.subset_set_image_iff]
  aesop
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
simp_rw : (∃ (t : Set β), (t.Finite ∧ p t) ∧ t ⊆ f '' s) ↔ ∃ (t : Set α), (t.Finite ∧ p (f '' t)) ∧ t ⊆ s
simp_rw₁ : (∃ (t : Set β), t.Finite ∧ p t ∧ t ⊆ f '' s) ↔ ∃ (t : Set α), t.Finite ∧ p (f '' t) ∧ t ⊆ s
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)
have simp_rw₂ : (∃ (s_1 : Finset β), p (↑s_1 : Set β) ∧ (↑s_1 : Set β) ⊆ f '' s) ↔
  ∃ (s_1 : Finset α), p (f '' (↑s_1 : Set α)) ∧ (↑s_1 : Set α) ⊆ s
Tactic: classical
  simp_rw [@and_comm (_ ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
    Finset.subset_set_image_iff]
  aesop
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
simp_rw : (∃ (t : Set β), (t.Finite ∧ p t) ∧ t ⊆ f '' s) ↔ ∃ (t : Set α), (t.Finite ∧ p (f '' t)) ∧ t ⊆ s
simp_rw₁ : (∃ (t : Set β), t.Finite ∧ p t ∧ t ⊆ f '' s) ↔ ∃ (t : Set α), t.Finite ∧ p (f '' t) ∧ t ⊆ s
simp_rw₂ :
  (∃ (s_1 : Finset β), p (↑s_1 : Set β) ∧ (↑s_1 : Set β) ⊆ f '' s) ↔
    ∃ (s_1 : Finset α), p (f '' (↑s_1 : Set α)) ∧ (↑s_1 : Set α) ⊆ s
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)
have simp_rw₃ : (∃ (s_1 : Finset β), (↑s_1 : Set β) ⊆ f '' s ∧ p (↑s_1 : Set β)) ↔
  ∃ (s_1 : Finset α), (↑s_1 : Set α) ⊆ s ∧ p (f '' (↑s_1 : Set α))
Tactic: classical
  simp_rw [@and_comm (_ ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
    Finset.subset_set_image_iff]
  aesop
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
simp_rw : (∃ (t : Set β), (t.Finite ∧ p t) ∧ t ⊆ f '' s) ↔ ∃ (t : Set α), (t.Finite ∧ p (f '' t)) ∧ t ⊆ s
simp_rw₁ : (∃ (t : Set β), t.Finite ∧ p t ∧ t ⊆ f '' s) ↔ ∃ (t : Set α), t.Finite ∧ p (f '' t) ∧ t ⊆ s
simp_rw₂ :
  (∃ (s_1 : Finset β), p (↑s_1 : Set β) ∧ (↑s_1 : Set β) ⊆ f '' s) ↔
    ∃ (s_1 : Finset α), p (f '' (↑s_1 : Set α)) ∧ (↑s_1 : Set α) ⊆ s
simp_rw₃ :
  (∃ (s_1 : Finset β), (↑s_1 : Set β) ⊆ f '' s ∧ p (↑s_1 : Set β)) ↔
    ∃ (s_1 : Finset α), (↑s_1 : Set α) ⊆ s ∧ p (f '' (↑s_1 : Set α))
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)
have simp_rw₄ : (∃ (s_1 : Finset β), (∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ Finset.image f s' = s_1) ∧ p (↑s_1 : Set β)) ↔
  ∃ (s_1 : Finset α), (↑s_1 : Set α) ⊆ s ∧ p (f '' (↑s_1 : Set α))
Tactic: classical
  simp_rw [@and_comm (_ ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
    Finset.subset_set_image_iff]
  aesop
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
⊢ motive s hs
have lift : ∀ (s : Finset α) (hs : (↑s : Set α).Finite), motive (↑s : Set α) hs
Tactic: lift s to Finset α using hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
s : Finset α
hs : (↑s : Set α).Finite
⊢ motive (↑s : Set α) hs
have empty₁ : ∀ (hs : (↑∅ : Set α).Finite), motive (↑∅ : Set α) hs
Tactic: induction s using Finset.cons_induction_on with
  | empty => simpa
  | cons a s ha ih => simpa using @insert a s ha (Set.toFinite _) (ih _)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
s : Finset α
hs : (↑s : Set α).Finite
empty₁ : ∀ (hs : (↑∅ : Set α).Finite), motive (↑∅ : Set α) hs
⊢ motive (↑s : Set α) hs
have cons : ∀ (a : α) (s : Finset α) (ha : a ∉ s) (ih : ∀ (hs : (↑s : Set α).Finite), motive (↑s : Set α) hs)
  (hs : (↑(Finset.cons a s ha) : Set α).Finite), motive (↑(Finset.cons a s ha) : Set α) hs
Tactic: induction s using Finset.cons_induction_on with
  | empty => simpa
  | cons a s ha ih => simpa using @insert a s ha (Set.toFinite _) (ih _)
Cleared hypotheses: s, hs