awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
⊢ motive s hs
have refine : ∀ {a : α} {s_1 : Set α},
  a ∉ s_1 →
    ∀ (hs_1 : s_1.Finite),
      (fun (t : Set α) (x : t.Finite) ↦ ∀ (hts : t ⊆ s), motive t sorry) s_1 hs_1 →
        (fun (t : Set α) (x : t.Finite) ↦ ∀ (hts : t ⊆ s), motive t sorry) (Insert.insert a s_1) sorry
Tactic: refine Set.Finite.induction_on (motive := fun t _ => ∀ hts : t ⊆ s, motive t (hs.subset hts)) s hs
    (fun _ => empty) ?_ .rfl
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (hypothesis)
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s_1 : Set α
hs : s_1.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s_1 → ∀ (hts : t ⊆ s_1), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs_1 : s.Finite
hCs : ∀ (hts : s ⊆ s_1), motive s ⋯
haS : Insert.insert a s ⊆ s_1
⊢ motive (Insert.insert a s) ⋯
have haS₁ : a ∈ s_1 ∧ s ⊆ s_1
Tactic: rw [insert_subset_iff] at haS
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (hypothesis)
Goal:
γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), t.Finite → ∃ (c : γ), P c t
⊢ ∃ (u : ℕ → γ), ∀ (n : ℕ), P (u n) (u '' Iio n)
have this : Nonempty γ
Tactic: haveI : Nonempty γ := (h ∅ finite_empty).nonempty
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), t.Finite → ∃ (c : γ), P c t
this : Nonempty γ
⊢ ∃ (u : ℕ → γ), ∀ (n : ℕ), P (u n) (u '' Iio n)
have choose! : ∀ (c : (t : Set γ) → γ) (hc : ∀ (t : Set γ), t.Finite → P (c t) t), ∃ (u : ℕ → γ), ∀ (n : ℕ), P (u n) (u '' Iio n)
Tactic: choose! c hc using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : (t : Set γ) → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → (g : (m : ℕ) → m < n → γ) → γ :=
  fun (n : ℕ) (g : (m : ℕ) → m < n → γ) ↦ c (range fun (k : (↑(Iio n) : Type)) ↦ g (↑k : ℕ) ⋯)
u : ℕ → γ := fun (n : ℕ) ↦ n.strongRecOn' (P := fun (x : ℕ) ↦ γ) f
⊢ ∃ (u : ℕ → γ), ∀ (n : ℕ), P (u n) (u '' Iio n)
have refine : ∀ (n : ℕ), P (u n) (u '' Iio n)
Tactic: refine ⟨u, fun n => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : (t : Set γ) → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → (g : (m : ℕ) → m < n → γ) → γ :=
  fun (n : ℕ) (g : (m : ℕ) → m < n → γ) ↦ c (range fun (k : (↑(Iio n) : Type)) ↦ g (↑k : ℕ) ⋯)
u : ℕ → γ := fun (n : ℕ) ↦ n.strongRecOn' (P := fun (x : ℕ) ↦ γ) f
n : ℕ
⊢ P (u n) (u '' Iio n)
have h : u n = c (u '' Iio n)
Tactic: convert! hc (u '' Iio n) ((finite_lt_nat _).image _)
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : (t : Set γ) → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → (g : (m : ℕ) → m < n → γ) → γ :=
  fun (n : ℕ) (g : (m : ℕ) → m < n → γ) ↦ c (range fun (k : (↑(Iio n) : Type)) ↦ g (↑k : ℕ) ⋯)
u : ℕ → γ := fun (n : ℕ) ↦ n.strongRecOn' (P := fun (x : ℕ) ↦ γ) f
n : ℕ
⊢ u n = c (u '' Iio n)
have h : u n = c (range fun (x : (↑(Iio n) : Type)) ↦ u (↑x : ℕ))
Tactic: rw [image_eq_range]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
a : α
s : Set α
inst : Fintype (↑s : Type u)
h : a ∉ s
d : Fintype (↑(insert a s) : Type u)
⊢ Fintype.card.{u} (↑(insert a s) : Type u) = Fintype.card.{u} (↑s : Type u) + 1
have rw : Fintype.card.{u} (↑(insert a s) : Type u) = Fintype.card.{u} (↑(insert a s) : Type u)
Tactic: rw [← card_fintypeInsertOfNotMem s h]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
inst : Fintype α
a : α
inst_1 : Fintype (↑{x : α | x ≠ a} : Type u)
⊢ Fintype.card.{u} (↑{x : α | x ≠ a} : Type u) = Fintype.card α - 1
have haveI : ∀ (this : DecidableEq α), Fintype.card.{u} (↑{x : α | x ≠ a} : Type u) = Fintype.card α - 1
Tactic: haveI := Classical.decEq α
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
inst : Fintype α
a : α
inst_1 : Fintype (↑{x : α | x ≠ a} : Type u)
this : DecidableEq α
⊢ Fintype.card.{u} (↑{x : α | x ≠ a} : Type u) = Fintype.card α - 1
have rw : Finset.card.{u} (α := α) (toFinset {x : α | x ≠ a}) = Fintype.card α - 1
Tactic: rw [← toFinset_card, toFinset_setOf, Finset.filter_ne',
    Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
inst : Fintype α
a : α
inst_1 : Fintype (↑{x : α | x ≠ a} : Type u)
this : DecidableEq α
rw : Finset.card.{u} (α := α) (toFinset {x : α | x ≠ a}) = Fintype.card α - 1
⊢ Fintype.card.{u} (↑{x : α | x ≠ a} : Type u) = Fintype.card α - 1
have rw₁ : Finset.card.{u} (α := α) {x : α | x ≠ a} = Fintype.card α - 1
Tactic: rw [← toFinset_card, toFinset_setOf, Finset.filter_ne',
    Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
inst : Fintype α
a : α
inst_1 : Fintype (↑{x : α | x ≠ a} : Type u)
this : DecidableEq α
rw : Finset.card.{u} (α := α) (toFinset {x : α | x ≠ a}) = Fintype.card α - 1
rw₁ : Finset.card.{u} (α := α) {x : α | x ≠ a} = Fintype.card α - 1
⊢ Fintype.card.{u} (↑{x : α | x ≠ a} : Type u) = Fintype.card α - 1
have rw₂ : (Finset.erase Finset.univ a).card = Fintype.card α - 1
Tactic: rw [← toFinset_card, toFinset_setOf, Finset.filter_ne',
    Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
inst : Fintype α
a : α
inst_1 : Fintype (↑{x : α | x ≠ a} : Type u)
this : DecidableEq α
rw : Finset.card.{u} (α := α) (toFinset {x : α | x ≠ a}) = Fintype.card α - 1
rw₁ : Finset.card.{u} (α := α) {x : α | x ≠ a} = Fintype.card α - 1
rw₂ : (Finset.erase Finset.univ a).card = Fintype.card α - 1
⊢ Fintype.card.{u} (↑{x : α | x ≠ a} : Type u) = Fintype.card α - 1
have rw₃ : Finset.card.{u} (α := α) Finset.univ - 1 = Fintype.card α - 1
Tactic: rw [← toFinset_card, toFinset_setOf, Finset.filter_ne',
    Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
inst : Fintype α
a : α
inst_1 : Fintype (↑{x : α | x ≠ a} : Type u)
this : DecidableEq α
rw : Finset.card.{u} (α := α) (toFinset {x : α | x ≠ a}) = Fintype.card α - 1
rw₁ : Finset.card.{u} (α := α) {x : α | x ≠ a} = Fintype.card α - 1
rw₂ : (Finset.erase Finset.univ a).card = Fintype.card α - 1
rw₃ : Finset.card.{u} (α := α) Finset.univ - 1 = Fintype.card α - 1
⊢ Fintype.card.{u} (↑{x : α | x ≠ a} : Type u) = Fintype.card α - 1
have rw₄ : Fintype.card α - 1 = Fintype.card α - 1
Tactic: rw [← toFinset_card, toFinset_setOf, Finset.filter_ne',
    Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
⊢ Set.Infinite.{u} (α := α) univ ↔ Infinite α
have rw : ¬Set.Finite.{u} (α := α) univ ↔ Infinite α
Tactic: rw [Set.Infinite, finite_univ_iff, not_finite_iff_infinite]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
rw : ¬Set.Finite.{u} (α := α) univ ↔ Infinite α
⊢ Set.Infinite.{u} (α := α) univ ↔ Infinite α
have rw₁ : ¬Finite α ↔ Infinite α
Tactic: rw [Set.Infinite, finite_univ_iff, not_finite_iff_infinite]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
rw : ¬Set.Finite.{u} (α := α) univ ↔ Infinite α
rw₁ : ¬Finite α ↔ Infinite α
⊢ Set.Infinite.{u} (α := α) univ ↔ Infinite α
have rw₂ : Infinite α ↔ Infinite α
Tactic: rw [Set.Infinite, finite_univ_iff, not_finite_iff_infinite]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s t : Set α
hs : s.Infinite
ht : t.Finite
⊢ ∃ a ∈ s, a ∉ t
have by_contra! : ∀ (h : ∀ (a : α) (_ : a ∈ s), a ∈ t), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
s : Set α
inst : Infinite α
hs : s.Finite
⊢ ∃ (a : α), a ∉ s
have by_contra! : ∀ (h : ∀ (a : α), a ∈ s), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
s : Set α
t : Set β
f : α → β
hs : s.Infinite
hf : MapsTo f s t
ht : t.Finite
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
have contrapose! : ∀ (ht : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y), t.Infinite
Tactic: contrapose! ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Infinite α
f : α → β
hi : Injective f
⊢ (range f).Infinite
have rw : Set.Infinite.{u} (α := α) univ
Tactic: rw [← image_univ, infinite_image_iff hi.injOn]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (hypothesis)
Goal:
α : Type u
β : Type v
inst : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : ∀ (x : α), f x ∈ s
⊢ s.Infinite
have hf₁ : range f ⊆ s
Tactic: rw [← range_subset_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
⊢ ¬InjOn f s
have this : Finite.{v + 1} (↑(f '' s) : Type v)
Tactic: have : Finite (f '' s) := finite_coe_iff.mpr h_fin
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this : Finite.{v + 1} (↑(f '' s) : Type v)
⊢ ¬InjOn f s
have this₁ : Infinite.{u + 1} (↑s : Type u)
Tactic: have : Infinite s := infinite_coe_iff.mpr h_inf
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this_1 : Finite.{v + 1} (↑(f '' s) : Type v)
this : Infinite.{u + 1} (↑s : Type u)
⊢ ¬InjOn f s
have h : ¬Injective (β := (↑(f '' s) : Type v)) (codRestrict (s.restrict (π := fun (a : α) ↦ β) f) (f '' s) sorry)
Tactic: have h := not_injective_infinite_finite
            ((f '' s).codRestrict (s.restrict f) fun x => ⟨x, x.property, rfl⟩)
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this_1 : Finite.{v + 1} (↑(f '' s) : Type v)
this : Infinite.{u + 1} (↑s : Type u)
h : ¬Injective (β := (↑(f '' s) : Type v)) (codRestrict (s.restrict (π := fun (a : α) ↦ β) f) (f '' s) ⋯)
⊢ ¬InjOn f s
have contrapose : ∀ (h : InjOn f s), Injective (β := (↑(f '' s) : Type v)) (codRestrict (s.restrict (π := fun (a : α) ↦ β) f) (f '' s) sorry)
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this_1 : Finite.{v + 1} (↑(f '' s) : Type v)
this : Infinite.{u + 1} (↑s : Type u)
h : InjOn f s
⊢ Injective (β := (↑(f '' s) : Type v)) (codRestrict (s.restrict (π := fun (a : α) ↦ β) f) (f '' s) ⋯)
have rwa : Injective (s.restrict (π := fun (a : α) ↦ β) f)
Tactic: rwa [injective_codRestrict, ← injOn_iff_injective]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
inst : Infinite α
n : ℕ
⊢ ∃ (s : Finset α), #s = n + 1
have obtain : ∀ (s : Finset α), ∃ (s_1 : Finset α), #s_1 = #s + 1
Tactic: obtain ⟨s, rfl⟩ := exists_card_eq n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
inst : Infinite α
s : Finset α
⊢ ∃ (s_1 : Finset α), #s_1 = #s + 1
have obtain : ∀ (a : α) (ha : a ∉ s), ∃ (s_1 : Finset α), #s_1 = #s + 1
Tactic: obtain ⟨a, ha⟩ := s.exists_notMem
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
inst : Infinite α
n : ℕ
⊢ ∃ (s : Finset α), #s = n + 1
have obtain : ∀ (s : Finset α), ∃ (s_1 : Finset α), #s_1 = #s + 1
Tactic: classical
    obtain ⟨s, rfl⟩ := exists_card_eq n
    obtain ⟨a, ha⟩ := s.exists_notMem
    exact ⟨insert a s, card_insert_of_notMem ha⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
inst : Infinite α
n : ℕ
obtain : ∀ (s : Finset α), ∃ (s_1 : Finset α), #s_1 = #s + 1
⊢ ∃ (s : Finset α), #s = n + 1
have obtain₁ : ∀ (s : Finset α) (a : α) (ha : a ∉ s), ∃ (s_1 : Finset α), #s_1 = #s + 1
Tactic: classical
    obtain ⟨s, rfl⟩ := exists_card_eq n
    obtain ⟨a, ha⟩ := s.exists_notMem
    exact ⟨insert a s, card_insert_of_notMem ha⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s (↑t : Set β)
⊢ ∃ (u : Finset α), (↑u : Set α) ⊆ s ∧ InjOn f (↑u : Set α) ∧ image f u = t
have obtain : ∀ (u : Set α) (hus : u ⊆ s) (hf : InjOn f u) (himg : f '' u = (↑t : Set β)),
  ∃ (u : Finset α), (↑u : Set α) ⊆ s ∧ InjOn f (↑u : Set α) ∧ image f u = t
Tactic: obtain ⟨u, hus, hf, himg⟩ := hfs.exists_subset_injOn_image_eq
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s (↑t : Set β)
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = (↑t : Set β)
⊢ ∃ (u : Finset α), (↑u : Set α) ⊆ s ∧ InjOn f (↑u : Set α) ∧ image f u = t
have refine : image f (sorry.toFinset (s := u)) = t
Tactic: refine ⟨(Finite.of_finite_image (by simp [himg]) hf).toFinset, by simpa, by simpa, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (hypothesis)
Goal:
α : Type u
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
⊢ Finite α
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
h_1 : Nontrivial α
⊢ Finite α
have rcases : ∀ (x y : α) (hne : x ≠ y), Finite α
Tactic: rcases exists_pair_ne α with ⟨x, y, hne⟩
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
h_1 : Nontrivial α
x y : α
hne : x ≠ y
⊢ Finite α
have refine : ∀ (z : α), Membership.mem (γ := Finset α) {x, y} z
Tactic: refine @Finite.of_fintype α ⟨{x, y}, fun z => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : DecidableEq α
s : Set (Set α)
inst_1 : Fintype (↑s : Type u)
H : (t : (↑s : Type u)) → Fintype (↑(↑t : Set α) : Type u)
⊢ Fintype (↑(⋃₀ s) : Type u)
have rw : Fintype (↑(⋃ (i : (↑s : Type u)), (↑i : Set α)) : Type u)
Tactic: rw [sUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
β : Type v
inst : Fintype β
inst_1 : DecidableEq α
f : β → Set α
inst_2 : (w : β) → Fintype (↑(f w) : Type u)
⊢ Eq.{u + 1} (α := Finset α) (toFinset (⋃ (x : β), f x)) (Finset.biUnion Finset.univ fun (x : β) ↦ (f x).toFinset)
have h : ∀ (v : α),
  Membership.mem (γ := Finset α) (toFinset (⋃ (x : β), f x)) v ↔
    Membership.mem (γ := Finset α) (Finset.biUnion Finset.univ fun (x : β) ↦ (f x).toFinset) v
Tactic: ext v
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : Finite ι
f : ι → Set α
inst_1 : ∀ (i : ι), Finite.{u + 1} (↑(f i) : Type u)
⊢ Finite.{u + 1} (↑(⋃ (i : ι), f i) : Type u)
have have : ∀ (this : Fintype (PLift ι)), Finite.{u + 1} (↑(⋃ (i : ι), f i) : Type u)
Tactic: have : Fintype (PLift ι) := Fintype.ofFinite _
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : Finite ι
f : ι → Set α
inst_1 : ∀ (i : ι), Finite.{u + 1} (↑(f i) : Type u)
this : Fintype (PLift ι)
⊢ Finite.{u + 1} (↑(⋃ (i : ι), f i) : Type u)
have have : ∀ (this : (i : ι) → Fintype (↑(f i) : Type u)), Finite.{u + 1} (↑(⋃ (i : ι), f i) : Type u)
Tactic: have : ∀ i, Fintype (f i) := fun i => Fintype.ofFinite _
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
inst : Finite.{u + 1} (↑s : Type u)
H : ∀ (t : (↑s : Type u)), Finite.{u + 1} (↑(↑t : Set α) : Type u)
⊢ Finite.{u + 1} (↑(⋃₀ s) : Type u)
have rw : Finite.{u + 1} (↑(⋃ (i : (↑s : Type u)), (↑i : Set α)) : Type u)
Tactic: rw [sUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : Set ι
inst : Finite.{u_1 + 1} (↑s : Type u_1)
t : ι → Set α
H : ∀ i ∈ s, Finite.{u + 1} (↑(t i) : Type u)
⊢ Finite.{u + 1} (↑(⋃ x ∈ s, t x) : Type u)
have rw : Finite.{u + 1} (↑(⋃ (x : (↑s : Type u_1)), t (↑x : ι)) : Type u)
Tactic: rw [biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u
ι : Type u_1
s : Set ι
inst : Finite.{u_1 + 1} (↑s : Type u_1)
t : ι → Set α
H : ∀ i ∈ s, Finite.{u + 1} (↑(t i) : Type u)
⊢ Finite.{u + 1} (↑(⋃ (x : (↑s : Type u_1)), t (↑x : ι)) : Type u)
have this : ∀ (i : (↑s : Type u_1)), Finite.{u + 1} (↑(t (↑i : ι)) : Type u)
Tactic: haveI : ∀ i : s, Finite (t i) := fun i => H i i.property
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
⊢ Set.Finite.{u} (α := α) (⋃ (i : ι), ⋃ (h : i ∈ s), t i h)
have this : Finite.{u_1 + 1} (↑s : Type u_1)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ Set.Finite.{u} (α := α) (⋃ (i : ι), ⋃ (h : i ∈ s), t i h)
have rw : Set.Finite.{u} (α := α) (⋃ (x : (↑s : Type u_1)), t (↑x : ι) sorry)
Tactic: rw [biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
⊢ Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
have suffices : Subset.{u} (α := Set α) (⋃ (i : ι), s i) (⋃ i ∈ t, s i)
Tactic: suffices ⋃ i, s i ⊆ ⋃ i ∈ t, s i by exact (ht.biUnion hs).subset this
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
⊢ Subset.{u} (α := Set α) (⋃ (i : ι), s i) (⋃ i ∈ t, s i)
have refine : ∀ (i : ι) (x : α) (hx : x ∈ s i), Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x
Tactic: refine iUnion_subset fun i x hx => ?_
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
⊢ Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x
have pos : ∀ (hi : i ∈ t), Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x
Tactic: by_cases hi : i ∈ t
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
pos : ∀ (hi : i ∈ t), Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x
⊢ Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x
have neg : ∀ (hi : i ∉ t), Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x
Tactic: by_cases hi : i ∈ t
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∉ t
⊢ Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x
have hx₁ : False
Tactic: rw [he i hi, mem_empty_iff_false] at hx
Cleared hypotheses: hx, hi
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
⊢ (∀ (i : ι), (s i).Finite) ∧ Set.Finite.{u_1} (α := ι) {i : ι | (s i).Nonempty}
have refine : Set.Finite.{u_1} (α := ι) {i : ι | (s i).Nonempty}
Tactic: refine ⟨fun i ↦ h.subset <| subset_iUnion _ _, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} i
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} j
hij :
  u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) =
    u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj)
⊢ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi =
    Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj
have a : (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) : ι) =
  (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj) : ι)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} i
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} j
hij :
  u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) =
    u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj)
⊢ (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) : ι) =
    (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj) : ι)
have a : (↑(u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi)) : α) ∈
  s (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj) : ι)
Tactic: refine hs.eq <| not_disjoint_iff.2 ⟨u ⟨i, hi⟩, hi.choose_spec, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} i
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} j
hij :
  u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) =
    u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj)
⊢ (↑(u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi)) : α) ∈
    s (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj) : ι)
have a : (↑(u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj)) : α) ∈
  s (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj) : ι)
Tactic: rw [hij]