awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type v
κ : ι → Sort w
inst : Nonempty ((a : ι) → κ a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
suffices suffices₁ suffices₂ suffices₃ :
  ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
⊢ Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
have suffices₄ : ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α) (this : Finite.{v + 1} (↑s : Type v)),
  Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
Tactic: classical
  suffices h : ∀ {κ : ι → Type w} [Nonempty (Π a, κ a)] (f : Π a, κ a → α),
      ⨅ a ∈ s, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a ∈ s, f a (g a) by
    haveI : Nonempty (Π a, PLift (κ a)) := (Equiv.piCongrRight fun _ => Equiv.plift).nonempty
    simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.piCongrRight fun _ => Equiv.plift).symm.iSup_comp]
      using h (κ := fun a => PLift (κ a)) fun a b => f a b.down
  intro κ _ f
  haveI := hs.to_subtype
  haveI : Nonempty (Π a : { a // a ∉ s }, κ ↑a) := ‹Nonempty (Π a, κ a)›.map fun f a ↦ f a
  simp [← iInf_subtype'', iInf_iSup_eq_of_finite (ι := s),
    ← Equiv.piEquivPiSubtypeProd (· ∈ s) _ |>.symm.iSup_comp, iSup_prod, iSup_const]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
ι : Type v
κ : ι → Sort w
inst : Nonempty ((a : ι) → κ a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
suffices suffices₁ suffices₂ suffices₃ :
  ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
suffices₄ :
  ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α) (this : Finite.{v + 1} (↑s : Type v)),
    Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
⊢ Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
have suffices₅ : ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α) (this : Finite.{v + 1} (↑s : Type v))
  (this : Nonempty ((a : { a : ι // a ∉ s }) → κ (↑a : ι))),
  Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
Tactic: classical
  suffices h : ∀ {κ : ι → Type w} [Nonempty (Π a, κ a)] (f : Π a, κ a → α),
      ⨅ a ∈ s, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a ∈ s, f a (g a) by
    haveI : Nonempty (Π a, PLift (κ a)) := (Equiv.piCongrRight fun _ => Equiv.plift).nonempty
    simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.piCongrRight fun _ => Equiv.plift).symm.iSup_comp]
      using h (κ := fun a => PLift (κ a)) fun a b => f a b.down
  intro κ _ f
  haveI := hs.to_subtype
  haveI : Nonempty (Π a : { a // a ∉ s }, κ ↑a) := ‹Nonempty (Π a, κ a)›.map fun f a ↦ f a
  simp [← iInf_subtype'', iInf_iSup_eq_of_finite (ι := s),
    ← Equiv.piEquivPiSubtypeProd (· ∈ s) _ |>.symm.iSup_comp, iSup_prod, iSup_const]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
I : Set β
S : β → Set α
H : I.Finite
⊢ BddAbove.{u} (α := α) (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i)
have empty : BddAbove.{u} (α := α) (⋃ (i : β), ⋃ (_ : Membership.mem (γ := Set β) ∅ i), S i) ↔
  ∀ (i : β), Membership.mem (γ := Set β) ∅ i → BddAbove (S i)
Tactic: induction I, H using Set.Finite.induction_on with
  | empty => simp only [biUnion_empty, bddAbove_empty, forall_mem_empty]
  | insert _ _ hs => simp only [biUnion_insert, forall_mem_insert, bddAbove_union, hs]
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
I : Set β
S : β → Set α
H : I.Finite
empty :
  BddAbove.{u} (α := α) (⋃ (i : β), ⋃ (_ : Membership.mem (γ := Set β) ∅ i), S i) ↔
    ∀ (i : β), Membership.mem (γ := Set β) ∅ i → BddAbove (S i)
⊢ BddAbove.{u} (α := α) (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i)
have insert : ∀ {a : β} {s : Set β},
  a ∉ s →
    s.Finite →
      ∀ (hs : BddAbove.{u} (α := α) (⋃ i ∈ s, S i) ↔ ∀ i ∈ s, BddAbove (S i)),
        BddAbove.{u} (α := α) (⋃ i ∈ insert a s, S i) ↔ ∀ i ∈ insert a s, BddAbove (S i)
Tactic: induction I, H using Set.Finite.induction_on with
  | empty => simp only [biUnion_empty, bddAbove_empty, forall_mem_empty]
  | insert _ _ hs => simp only [biUnion_insert, forall_mem_insert, bddAbove_union, hs]
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : Nonempty ι
f : ι → Set α
h : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ∀ (hs : (↑t : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑t : Set α) ⊆ f i
hs : (↑(Finset.cons b t hbt) : Set α) ⊆ ⋃ (i : ι), f i
⊢ ∃ (i : ι), (↑(Finset.cons b t hbt) : Set α) ⊆ f i
have cons : ∀ (hs : (∃ (i : ι), b ∈ f i) ∧ (↑t : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), b ∈ f i ∧ (↑t : Set α) ⊆ f i
Tactic: simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : Nonempty ι
f : ι → Set α
h : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ∀ (hs : (↑t : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑t : Set α) ⊆ f i
hs : (∃ (i : ι), b ∈ f i) ∧ (↑t : Set α) ⊆ ⋃ (i : ι), f i
⊢ ∃ (i : ι), b ∈ f i ∧ (↑t : Set α) ⊆ f i
have cons : ∀ (i : ι) (hi : b ∈ f i) (j : ι) (hj : (↑t : Set α) ⊆ f j), ∃ (i : ι), b ∈ f i ∧ (↑t : Set α) ⊆ f i
Tactic: rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : Nonempty ι
f : ι → Set α
h : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ∀ (hs : (↑t : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑t : Set α) ⊆ f i
hs : (∃ (i : ι), b ∈ f i) ∧ (↑t : Set α) ⊆ ⋃ (i : ι), f i
i : ι
hi : b ∈ f i
j : ι
hj : (↑t : Set α) ⊆ f j
⊢ ∃ (i : ι), b ∈ f i ∧ (↑t : Set α) ⊆ f i
have cons : ∀ (k : ι) (hik : f i ⊆ f k) (hjk : f j ⊆ f k), ∃ (i : ι), b ∈ f i ∧ (↑t : Set α) ⊆ f i
Tactic: rcases h i j with ⟨k, hik, hjk⟩
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : Nonempty ι
f : ι → Set α
h : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
s : Finset α
hs : (↑s : Set α) ⊆ ⋃ (i : ι), f i
⊢ ∃ (i : ι), (↑s : Set α) ⊆ f i
have empty : ∀ (hs : (↑∅ : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑∅ : Set α) ⊆ f i
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons b t hbt iht =>
    simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢
    rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩
    rcases h i j with ⟨k, hik, hjk⟩
    exact ⟨k, hik hi, hj.trans hjk⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : Nonempty ι
f : ι → Set α
h : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
s : Finset α
hs : (↑s : Set α) ⊆ ⋃ (i : ι), f i
empty : ∀ (hs : (↑∅ : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑∅ : Set α) ⊆ f i
⊢ ∃ (i : ι), (↑s : Set α) ⊆ f i
have cons : ∀ (b : α) (t : Finset α) (hbt : b ∉ t) (iht : ∀ (hs : (↑t : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑t : Set α) ⊆ f i)
  (hs : (↑(Finset.cons b t hbt) : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑(Finset.cons b t hbt) : Set α) ⊆ f i
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons b t hbt iht =>
    simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢
    rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩
    rcases h i j with ⟨k, hik, hjk⟩
    exact ⟨k, hik hi, hj.trans hjk⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun (i j : ι) ↦ f i ⊆ f j) c
s : Finset α
hs : (↑s : Set α) ⊆ ⋃ i ∈ c, f i
⊢ ∃ i ∈ c, (↑s : Set α) ⊆ f i
have hs₁ : (↑s : Set α) ⊆ ⋃ (x : (↑c : Type u_2)), f (↑x : ι)
Tactic: rw [Set.biUnion_eq_iUnion] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun (i j : ι) ↦ f i ⊆ f j) c
s : Finset α
hs : (↑s : Set α) ⊆ ⋃ (x : (↑c : Type u_2)), f (↑x : ι)
⊢ ∃ i ∈ c, (↑s : Set α) ⊆ f i
have this : Nonempty.{u_2 + 1} (↑c : Type u_2)
Tactic: haveI := hn.coe_sort
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : s ⊆ ⋃₀ c
⊢ ∃ t ∈ c, s ⊆ t
have hsc₁ : (↑(hs.toFinset (s := s)) : Set α) ⊆ ⋃ i ∈ c, i
Tactic: rw [← hs.coe_toFinset, sUnion_eq_biUnion] at hsc
Cleared hypotheses: hsc
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lattice (hypothesis)
Goal:
α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : (↑(hs.toFinset (s := s)) : Set α) ⊆ ⋃ i ∈ c, i
⊢ ∃ t ∈ c, s ⊆ t
have this : ∃ i ∈ c, (↑(hs.toFinset (s := s)) : Set α) ⊆ i
Tactic: have := DirectedOn.exists_mem_subset_of_finset_subset_biUnion hn hc hsc
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lemmas (goal)
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
⊢ C S
have have : ∀ (this : Finite.{u + 1} (↑S : Type u)), C S
Tactic: have : Finite S := Finite.to_subtype h
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lemmas (hypothesis)
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this : Finite.{u + 1} (↑S : Type u)
⊢ C S
have this₁ : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
Tactic: have : Finite {T : Set α // T ⊆ S} := Finite.of_equiv (Set S) (Equiv.Set.powerset S).symm
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lemmas (goal)
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
⊢ C S
have rw : C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S sorry : { x : Set α // x ⊆ S }) : Set α)
Tactic: rw [← Subtype.coe_mk (p := (· ⊆ S)) _ le_rfl]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lemmas (hypothesis)
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
⊢ C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S ⋯ : { x : Set α // x ⊆ S }) : Set α)
have H0₁ : C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S0 hS0) : Set α)
Tactic: rw [← Subtype.coe_mk (p := (· ⊆ S)) _ hS0] at H0
Cleared hypotheses: H0, H1, this_1, this
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lemmas (goal)
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S0 hS0) : Set α)
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
⊢ C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S ⋯ : { x : Set α // x ⊆ S }) : Set α)
have refine : ∀ (s : { x : Set α // x ⊆ S })
  (hs : (↑s : Set α) ≠ (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S sorry : { x : Set α // x ⊆ S }) : Set α))
  (hs' : C (↑s : Set α)), ∃ (c : { x : Set α // x ⊆ S }), s < c ∧ C (↑c : Set α)
Tactic: refine Finite.to_wellFoundedGT.wf.induction_bot' (fun s hs hs' ↦ ?_) H0
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lemmas (goal)
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S0 hS0) : Set α)
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
s : { x : Set α // x ⊆ S }
hs : (↑s : Set α) ≠ (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S ⋯ : { x : Set α // x ⊆ S }) : Set α)
hs' : C (↑s : Set α)
⊢ ∃ (c : { x : Set α // x ⊆ S }), s < c ∧ C (↑c : Set α)
have obtain : ∀ (a : α) (ha' : C (insert a (↑s : Set α))) (ha1 : a ∈ S) (ha2 : a ∉ (↑s : Set α)),
  ∃ (c : { x : Set α // x ⊆ S }), s < c ∧ C (↑c : Set α)
Tactic: obtain ⟨a, ⟨ha1, ha2⟩, ha'⟩ := H1 s (ssubset_of_ne_of_subset hs s.2) hs'
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lemmas (goal)
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : LinearOrder β
s : Set α
f : α → β
h : s.Finite
⊢ ∃ (a : α), ∀ b ∈ s, f a ≤ f b
have inl : ∀ (h : Set.Finite.{u} (α := α) ∅), ∃ (a : α), ∀ (b : α), Membership.mem (γ := Set α) ∅ b → f a ≤ f b
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lemmas (goal)
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : LinearOrder β
s : Set α
f : α → β
h : s.Finite
inl : ∀ (h : Set.Finite.{u} (α := α) ∅), ∃ (a : α), ∀ (b : α), Membership.mem (γ := Set α) ∅ b → f a ≤ f b
⊢ ∃ (a : α), ∀ b ∈ s, f a ≤ f b
have inr : ∀ (hs : s.Nonempty), ∃ (a : α), ∀ b ∈ s, f a ≤ f b
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Lemmas (goal)
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : LinearOrder β
s : Set α
f : α → β
h : s.Finite
hs : s.Nonempty
⊢ ∃ (a : α), ∀ b ∈ s, f a ≤ f b
have inr : ∀ x₀ ∈ s, ∀ (hx₀ : ∀ b ∈ s, f x₀ ≤ f b), ∃ (a : α), ∀ b ∈ s, f a ≤ f b
Tactic: rcases Set.exists_min_image s f h hs with ⟨x₀, _, hx₀⟩
-- Lean 4 proof step from Mathlib.Data.Set.Finite.List (goal)
Goal:
α : Type u_1
inst : Finite α
n : ℕ
⊢ Set.Finite.{u_1} (α := List α) {l : List α | l.length < n}
have h : Eq.{u_1 + 1} (α := Set (List α)) {l : List α | l.length < n}
  (⋃ i ∈ (↑(Finset.range n) : Set ℕ), {l : List α | l.length = i})
Tactic: convert! (Finset.range n).finite_toSet.biUnion fun i _ ↦ finite_length_eq α i
-- Lean 4 proof step from Mathlib.Data.Set.Finite.List (goal)
Goal:
α : Type u_1
inst : Finite α
n : ℕ
⊢ Eq.{u_1 + 1} (α := Set (List α)) {l : List α | l.length < n}
    (⋃ i ∈ (↑(Finset.range n) : Set ℕ), {l : List α | l.length = i})
have h : ∀ (x : List α),
  Membership.mem (γ := Set (List α)) {l : List α | l.length < n} x ↔
    Membership.mem (γ := Set (List α)) (⋃ i ∈ (↑(Finset.range n) : Set ℕ), {l : List α | l.length = i}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Monad (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : DecidableEq β
f : Set (α → β)
s : Set α
inst_1 : Fintype (↑f : Type (max u v))
inst_2 : Fintype (↑s : Type u)
⊢ Fintype (↑(f.seq s) : Type v)
have rw : Fintype (↑(⋃ f_1 ∈ f, f_1 '' s) : Type v)
Tactic: rw [seq_def]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Monad (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
inst : Finite (↑f : Type (max u v))
inst_1 : Finite.{u + 1} (↑s : Type u)
⊢ Finite.{v + 1} (↑(f.seq s) : Type v)
have rw : Finite.{v + 1} (↑(⋃ f_1 ∈ f, f_1 '' s) : Type v)
Tactic: rw [seq_def]
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Powerset (goal)
Goal:
α : Type u
a : Set α
h : a.Finite
⊢ Set.Finite.{u} (α := Set α) {b : Set α | b ⊆ a}
have h₁ : {b : Set α | b ⊆ a} =
  (↑(Finset.map
        (RelEmbedding.toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Set α) ↦ x1 ≤ x2)
          Finset.coeEmb)
        h.toFinset (s := a).powerset) :
    Set (Set α))
Tactic: convert! ((Finset.powerset h.toFinset).map Finset.coeEmb.1).finite_toSet
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Powerset (goal)
Goal:
α : Type u
a : Set α
h : a.Finite
⊢ {b : Set α | b ⊆ a} =
    (↑(Finset.map
          (RelEmbedding.toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Set α) ↦ x1 ≤ x2)
            Finset.coeEmb)
          h.toFinset (s := a).powerset) :
      Set (Set α))
have h₁ : ∀ (s : Set α),
  Membership.mem (γ := Set (Set α)) {b : Set α | b ⊆ a} s ↔
    s ∈
      (↑(Finset.map
            (RelEmbedding.toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Set α) ↦ x1 ≤ x2)
              Finset.coeEmb)
            h.toFinset (s := a).powerset) :
        Set (Set α))
Tactic: ext s
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Range (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : ι → α
inst : Finite ι
⊢ Finite.{u + 1} (↑(range f) : Type u)
have haveI : ∀ (this : Fintype (PLift ι)), Finite.{u + 1} (↑(range f) : Type u)
Tactic: haveI := Fintype.ofFinite (PLift ι)
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Range (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : ι → α
inst : Finite ι
⊢ Finite.{u + 1} (↑(range f) : Type u)
have haveI : ∀ (this : Fintype (PLift ι)), Finite.{u + 1} (↑(range f) : Type u)
Tactic: classical
  haveI := Fintype.ofFinite (PLift ι)
  infer_instance
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Range (hypothesis)
Goal:
α : Type u
β : Type v
s : Set α
hs : s.Finite
F : (i : α) → i ∈ s → β
⊢ Set.Finite.{v} (α := β) {y : β | ∃ (x : α) (hx : x ∈ s), F x hx = y}
have this : Finite.{u + 1} (↑s : Type u)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Range (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
hsu : u ⊆ f '' s
⊢ ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u
have this : Finite.{v + 1} (↑u : Type v)
Tactic: have : Finite u := Finite.to_subtype hu
-- Lean 4 proof step from Mathlib.Data.Set.Finite.Range (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
hsu : u ⊆ f '' s
this : Finite.{v + 1} (↑u : Type v)
⊢ ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u
have choose : ∀ (g : ⦃a : β⦄ → a ∈ u → α) (hg : ∀ ⦃a : β⦄ (a_1 : a ∈ u), g a_1 ∈ s) (hg' : ∀ ⦃a : β⦄ (a_1 : a ∈ u), f (g a_1) = a),
  ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u
Tactic: choose g hg hg' using hsu
Cleared hypotheses: hsu
-- Lean 4 proof step from Mathlib.Data.Set.FiniteExhaustion (goal)
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
⊢ s.FiniteExhaustion
have a : Nonempty.{u_1 + 1} s.FiniteExhaustion
Tactic: apply Classical.choice
-- Lean 4 proof step from Mathlib.Data.Set.FiniteExhaustion (goal)
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion
have pos : ∀ (h : Nonempty.{u_1 + 1} (↑s : Type u_1)), Nonempty.{u_1 + 1} s.FiniteExhaustion
Tactic: by_cases h : Nonempty s
-- Lean 4 proof step from Mathlib.Data.Set.FiniteExhaustion (goal)
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
pos : ∀ (h : Nonempty.{u_1 + 1} (↑s : Type u_1)), Nonempty.{u_1 + 1} s.FiniteExhaustion
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion
have neg : ∀ (h : ¬Nonempty.{u_1 + 1} (↑s : Type u_1)), Nonempty.{u_1 + 1} s.FiniteExhaustion
Tactic: by_cases h : Nonempty s
-- Lean 4 proof step from Mathlib.Data.Set.FiniteExhaustion (goal)
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion
have pos : ∀ (f : ℕ → (↑s : Type u_1)) (hf : Function.Surjective f), Nonempty.{u_1 + 1} s.FiniteExhaustion
Tactic: obtain ⟨f, hf⟩ := @exists_surjective_nat s h hs
-- Lean 4 proof step from Mathlib.Data.Set.FiniteExhaustion (goal)
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty.{u_1 + 1} (↑s : Type u_1)
f : ℕ → (↑s : Type u_1)
hf : Function.Surjective f
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion
have pos : ∀ (n : ℕ),
  Finite.{u_1 + 1} (↑((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) n) : Type u_1)
Tactic: refine ⟨fun n ↦ (Subtype.val ∘ f) '' {i | i ≤ n}, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.FiniteExhaustion (goal)
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty.{u_1 + 1} (↑s : Type u_1)
f : ℕ → (↑s : Type u_1)
hf : Function.Surjective f
pos :
  ∀ (n : ℕ),
    Finite.{u_1 + 1} (↑((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) n) : Type u_1)
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion
have pos₁ : ∀ (n : ℕ),
  Subset.{u_1} (α := Set α) ((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) n)
    ((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) (n + 1))
Tactic: refine ⟨fun n ↦ (Subtype.val ∘ f) '' {i | i ≤ n}, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.FiniteExhaustion (goal)
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty.{u_1 + 1} (↑s : Type u_1)
f : ℕ → (↑s : Type u_1)
hf : Function.Surjective f
pos :
  ∀ (n : ℕ),
    Finite.{u_1 + 1} (↑((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) n) : Type u_1)
pos₁ :
  ∀ (n : ℕ),
    Subset.{u_1} (α := Set α) ((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) n)
      ((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) (n + 1))
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion
have pos₂ : ⋃ (n : ℕ), (fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) n = s
Tactic: refine ⟨fun n ↦ (Subtype.val ∘ f) '' {i | i ≤ n}, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.FiniteExhaustion (goal)
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion
have neg : ⋃ (n : ℕ), (fun (x : ℕ) ↦ (∅ : Set α)) n = s
Tactic: refine ⟨fun _ ↦ ∅, by simp [Finite.to_subtype], fun n ↦ by simp, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.FiniteExhaustion (goal)
Goal:
α : Type u_1
s : Set α
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion ↔ s.Countable
have refine : Nonempty.{u_1 + 1} s.FiniteExhaustion → ∀ (K : s.FiniteExhaustion), s.Countable
Tactic: refine ⟨fun ⟨K⟩ ↦ ?_, fun h ↦ ⟨h.finiteExhaustion⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.FiniteExhaustion (goal)
Goal:
α : Type u_1
s : Set α
h : Nonempty.{u_1 + 1} s.FiniteExhaustion
K : s.FiniteExhaustion
⊢ s.Countable
have rw : Set.Countable.{u_1} (α := α) (⋃ (n : ℕ), (K : (a : ℕ) → Set α) n)
Tactic: rw [← K.iUnion_eq]
-- Lean 4 proof step from Mathlib.Data.Set.FiniteExhaustion (goal)
Goal:
α : Type u_1
s : Set α
K : s.FiniteExhaustion
β : Type u_2
t : Set β
K' : t.FiniteExhaustion
⊢ ⋃ (n : ℕ),
      SProd.sprod (α := Set α) (β := Set β) ((K : (a : ℕ) → Set α) n : Set α) ((K' : (a : ℕ) → Set β) n : Set β) =
    s ×ˢ t
have rw : SProd.sprod (α := Set α) (β := Set β) (⋃ (x : ℕ), (K : (a : ℕ) → Set α) x) (⋃ (x : ℕ), (K' : (a : ℕ) → Set β) x) =
  s ×ˢ t
Tactic: rw [Set.iUnion_prod_of_monotone (OrderHomClass.mono K) (OrderHomClass.mono K'),
          K.iUnion_eq, K'.iUnion_eq]
-- Lean 4 proof step from Mathlib.Data.Set.FiniteExhaustion (goal)
Goal:
α : Type u_1
s : Set α
K : s.FiniteExhaustion
β : Type u_2
t : Set β
K' : t.FiniteExhaustion
rw :
  SProd.sprod (α := Set α) (β := Set β) (⋃ (x : ℕ), (K : (a : ℕ) → Set α) x) (⋃ (x : ℕ), (K' : (a : ℕ) → Set β) x) =
    s ×ˢ t
⊢ ⋃ (n : ℕ),
      SProd.sprod (α := Set α) (β := Set β) ((K : (a : ℕ) → Set α) n : Set α) ((K' : (a : ℕ) → Set β) n : Set β) =
    s ×ˢ t
have rw₁ : SProd.sprod (β := Set β) s (⋃ (x : ℕ), (K' : (a : ℕ) → Set β) x) = s ×ˢ t
Tactic: rw [Set.iUnion_prod_of_monotone (OrderHomClass.mono K) (OrderHomClass.mono K'),
          K.iUnion_eq, K'.iUnion_eq]