awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
refine :
  ∀ (c : Set (Set ((i : ι) → β i))) (hc : c ⊆ sets β) (hcc : IsChain (fun (x1 x2 : Set ((i : ι) → β i)) ↦ x1 ⊆ x2) c)
    (i : ι),
    ∀ x ∈ ⋃₀ c,
      ∀ y ∈ ⋃₀ c,
        ∀ (hi : Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y))
          (p : Set ((i : ι) → β i)) (hpc : p ∈ c) (hxp : x ∈ p) (q : Set ((i : ι) → β i)) (hqc : q ∈ c) (hyq : y ∈ q),
          x = y
⊢ ∃ (s : Set ((i : ι) → β i)), Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s

Tactic:
refine zorn_subset _ fun c hc hcc ↦
      ⟨⋃₀ c, fun i x ⟨p, hpc, hxp⟩ y ⟨q, hqc, hyq⟩ hi ↦ ?_, fun _ ↦ subset_sUnion_of_mem⟩
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
c : Set (Set ((i : ι) → β i))
hc : c ⊆ sets β
hcc : IsChain (fun (x1 x2 : Set ((i : ι) → β i)) ↦ x1 ⊆ x2) c
i : ι
x : (i : ι) → β i
h : x ∈ ⋃₀ c
y : (i : ι) → β i
h_1 : y ∈ ⋃₀ c
hi : Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y)
p : Set ((i : ι) → β i)
hpc : p ∈ c
hxp : x ∈ p
q : Set ((i : ι) → β i)
hqc : q ∈ c
hyq : y ∈ q
⊢ x = y

Tactic:
(hcc.total hpc hqc).elim (fun h ↦ hc hqc i (h hxp) hyq hi)
      fun h ↦ hc hpc i hxp (h hyq) hi

Premises used: Or.elim, IsChain.total
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
c : Set (Set ((i : ι) → β i))
hc : c ⊆ sets β
hcc : IsChain (fun (x1 x2 : Set ((i : ι) → β i)) ↦ x1 ⊆ x2) c
i : ι
x : (i : ι) → β i
h : x ∈ ⋃₀ c
y : (i : ι) → β i
h_1 : y ∈ ⋃₀ c
hi : Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y)
p : Set ((i : ι) → β i)
hpc : p ∈ c
hxp : x ∈ p
q : Set ((i : ι) → β i)
hqc : q ∈ c
hyq : y ∈ q
⊢ x = y

Tactic:
exact (hcc.total hpc hqc).elim (fun h ↦ hc hqc i (h hxp) hyq hi)
      fun h ↦ hc hpc i hxp (h hyq) hi

Premises used: Or.elim, IsChain.total
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
⊢ ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y

Tactic:
simpa [Surjective] using h

Premises used: Function.Surjective
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x : (i : ι) → β i
hx : x ∈ insert f s
y : (i : ι) → β i
hy : y ∈ insert f s
inl :
  ∀ (hx : x = f), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
inr :
  ∀ (hx : x ∈ s), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y

Tactic:
rcases hx with hx | hx
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x = f
inl :
  ∀ (hy : y = f), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
inl₁ :
  ∀ (hy : y ∈ s), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y

Tactic:
rcases hy with hy | hy
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x ∈ s
inr :
  ∀ (hy : y = f), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
inr₁ :
  ∀ (hy : y ∈ s), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y

Tactic:
rcases hy with hy | hy
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y = f
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y

Tactic:
simp [hx, hy]
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
inl : Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) f) ((fun (x : (i : ι) → β i) ↦ x i) y) → f = y
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y

Tactic:
subst x
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
y : (i : ι) → β i
hy : y ∈ s
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) f) ((fun (x : (i : ι) → β i) ↦ x i) y) → f = y

Tactic:
fun e => (hf i y hy e.symm).elim

Premises used: False.elim, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
y : (i : ι) → β i
hy : y ∈ s
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) f) ((fun (x : (i : ι) → β i) ↦ x i) y) → f = y

Tactic:
exact fun e => (hf i y hy e.symm).elim

Premises used: False.elim
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
inr : Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) f) → x = f
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y

Tactic:
subst y
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x : (i : ι) → β i
hx : x ∈ s
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) f) → x = f

Tactic:
fun e => (hf i x hx e).elim

Premises used: False.elim
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x : (i : ι) → β i
hx : x ∈ s
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) f) → x = f

Tactic:
exact fun e => (hf i x hx e).elim

Premises used: False.elim
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y

Tactic:
hs.prop i hx hy

Premises used: Maximal.prop
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y

Tactic:
exact hs.prop i hx hy

Premises used: Maximal.prop
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
⊢ Nonempty (α ↪ β) ∨ Nonempty (β ↪ α)

Tactic:
match @min_injective Bool (fun b => cond b (ULift α) (ULift.{max u v, v} β)) ⟨true⟩
    with
  | ⟨true, ⟨h⟩⟩ =>
    let ⟨f, hf⟩ := h false
    Or.inl ⟨Embedding.congr Equiv.ulift Equiv.ulift ⟨f, hf⟩⟩
  | ⟨false, ⟨h⟩⟩ =>
    let ⟨f, hf⟩ := h true
    Or.inr ⟨Embedding.congr Equiv.ulift Equiv.ulift ⟨f, hf⟩⟩

Premises used: cond, _private.0.Function.Embedding.total.match_2, ULift, Function.Embedding.mk, Equiv.ulift, _private.0.Function.Embedding.total.match_3, Nonempty.intro, Function.Embedding, _private.0.Function.Embedding.total.match_1, Bool.true, Function.Embedding.min_injective, Nonempty, Function.Embedding.congr, Or.inl, Or, Bool.false, Or.inr
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
x y : WType (Operands s)
⊢ WType.elim (β := Operands s) (↥(closure s)) (operate s)
      (WType.mk (β := Operands s) (Sum.inl 1) fun (t : Bool) ↦
        Bool.rec (motive := fun (x : Bool) ↦ WType (Operands s)) x y t) =
    HMul.hMul (α := ↥(closure s)) (WType.elim (β := Operands s) (↥(closure s)) (operate s) x)
      (WType.elim (β := Operands s) (↥(closure s)) (operate s) y)

Tactic:
rfl
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
x y : WType (Operands s)
⊢ Membership.mem (γ := Set ↥(closure s)) (Set.range (WType.elim (β := Operands s) (↥(closure s)) (operate s)))
    (HMul.hMul (α := ↥(closure s)) (WType.elim (β := Operands s) (↥(closure s)) (operate s) x)
      (WType.elim (β := Operands s) (↥(closure s)) (operate s) y))

Tactic:
exact ⟨WType.mk (.inl 1) (Bool.rec x y), by rfl⟩
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
x y : WType (Operands s)
⊢ WType.elim (β := Operands s) (↥(closure s)) (operate s)
      (WType.mk (β := Operands s) (Sum.inl 0) fun (t : Bool) ↦
        Bool.rec (motive := fun (x : Bool) ↦ WType (Operands s)) x y t) =
    HAdd.hAdd (α := ↥(closure s)) (WType.elim (β := Operands s) (↥(closure s)) (operate s) x)
      (WType.elim (β := Operands s) (↥(closure s)) (operate s) y)

Tactic:
rfl
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
x y : WType (Operands s)
⊢ Membership.mem (γ := Set ↥(closure s)) (Set.range (WType.elim (β := Operands s) (↥(closure s)) (operate s)))
    (HAdd.hAdd (α := ↥(closure s)) (WType.elim (β := Operands s) (↥(closure s)) (operate s) x)
      (WType.elim (β := Operands s) (↥(closure s)) (operate s) y))

Tactic:
exact ⟨WType.mk (.inl 0) (Bool.rec x y), by rfl⟩
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
x : WType (Operands s)
⊢ Membership.mem (γ := Set ↥(closure s)) (Set.range (WType.elim (β := Operands s) (↥(closure s)) (operate s)))
    (-WType.elim (β := Operands s) (↥(closure s)) (operate s) x)

Tactic:
⟨WType.mk (.inl 2) fun _ ↦ x, rfl⟩

Premises used: Set.Mem, setOf, Sum.inl, WType.mk, Exists.intro, Set.range, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
x : WType (Operands s)
⊢ Membership.mem (γ := Set ↥(closure s)) (Set.range (WType.elim (β := Operands s) (↥(closure s)) (operate s)))
    (-WType.elim (β := Operands s) (↥(closure s)) (operate s) x)

Tactic:
exact ⟨WType.mk (.inl 2) fun _ ↦ x, rfl⟩
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
x : WType (Operands s)
⊢ Membership.mem (γ := Set ↥(closure s)) (Set.range (WType.elim (β := Operands s) (↥(closure s)) (operate s)))
    (WType.elim (β := Operands s) (↥(closure s)) (operate s) x)⁻¹

Tactic:
⟨WType.mk (.inl 3) fun _ ↦ x, rfl⟩

Premises used: Set.Mem, setOf, Sum.inl, WType.mk, Exists.intro, Set.range, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
x : WType (Operands s)
⊢ Membership.mem (γ := Set ↥(closure s)) (Set.range (WType.elim (β := Operands s) (↥(closure s)) (operate s)))
    (WType.elim (β := Operands s) (↥(closure s)) (operate s) x)⁻¹

Tactic:
exact ⟨WType.mk (.inl 3) fun _ ↦ x, rfl⟩
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
a : ↥(closure s)
h : Membership.mem (γ := Subfield ↥(closure s)) ⊤ a
rw :
  (↑a : α) ∈
    Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Subfield α) (closure s) x) ''
      (↑(rangeOfWType s) : Set ↥(closure s))
⊢ Membership.mem (γ := Subfield ↥(closure s)) (rangeOfWType s) a

Tactic:
rw [← SetLike.mem_coe, ← Subtype.val_injective.mem_set_image]

Premises used: Subtype.val_injective, SetLike.mem_coe, Function.Injective.mem_set_image
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
a : ↥(closure s)
h : Membership.mem (γ := Subfield ↥(closure s)) ⊤ a
change : Membership.mem (γ := Subfield α) (map (subtype (closure s)) (rangeOfWType s)) (↑a : α)
⊢ (↑a : α) ∈
    Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Subfield α) (closure s) x) ''
      (↑(rangeOfWType s) : Set ↥(closure s))

Tactic:
change ↑a ∈ map (closure s).subtype _

Premises used: Subfield.subtype, Subfield.closure, Subfield.map
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
a : ↥(closure s)
h : Membership.mem (γ := Subfield ↥(closure s)) ⊤ a
⊢ Membership.mem (γ := Subfield α) (map (subtype (closure s)) (rangeOfWType s)) (↑a : α)

Tactic:
closure_le.mpr (fun a ha ↦ ?_) a.prop

Premises used: Iff.mpr, Subfield.closure_le, Subtype.prop
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
a : ↥(closure s)
h : Membership.mem (γ := Subfield ↥(closure s)) ⊤ a
refine : ∀ (a : α) (ha : a ∈ s), a ∈ (↑(map (subtype (closure s)) (rangeOfWType s)) : Set α)
⊢ Membership.mem (γ := Subfield α) (map (subtype (closure s)) (rangeOfWType s)) (↑a : α)

Tactic:
refine closure_le.mpr (fun a ha ↦ ?_) a.prop

Premises used: Iff.mpr, Subfield.closure_le, Subtype.prop
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
a_1 : ↥(closure s)
h : Membership.mem (γ := Subfield ↥(closure s)) ⊤ a_1
a : α
ha : a ∈ s
⊢ a ∈ (↑(map (subtype (closure s)) (rangeOfWType s)) : Set α)

Tactic:
⟨⟨a, subset_closure ha⟩, ⟨WType.mk (.inr ⟨a, ha⟩) Empty.rec, rfl⟩, rfl⟩

Premises used: WType, Set.Mem, setOf, Subtype.mk, WType.mk, Sum.inr, And.intro, Exists.intro, _private.0.Subfield.Operands, Set.image, Subfield.subset_closure, rfl, Empty.rec
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
a_1 : ↥(closure s)
h : Membership.mem (γ := Subfield ↥(closure s)) ⊤ a_1
a : α
ha : a ∈ s
⊢ a ∈ (↑(map (subtype (closure s)) (rangeOfWType s)) : Set α)

Tactic:
exact ⟨⟨a, subset_closure ha⟩, ⟨WType.mk (.inr ⟨a, ha⟩) Empty.rec, rfl⟩, rfl⟩
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
rw : Eq (α := Set ↥(closure s)) (Set.range (WType.elim (β := Operands s) (↥(closure s)) (operate s))) Set.univ
⊢ Function.Surjective (β := ↥(closure s)) (WType.elim (β := Operands s) (↥(closure s)) (operate s))

Tactic:
rw [← Set.range_eq_univ]

Premises used: Set.range_eq_univ
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ Eq (α := Set ↥(closure s)) (Set.range (WType.elim (β := Operands s) (↥(closure s)) (operate s))) Set.univ

Tactic:
SetLike.coe_set_eq.mpr (rangeOfWType_eq_top s)

Premises used: Iff.mpr, Set.univ, _private.0.Subfield.rangeOfWType_eq_top, setOf, SetLike.coe_set_eq, Set.range
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ Eq (α := Set ↥(closure s)) (Set.range (WType.elim (β := Operands s) (↥(closure s)) (operate s))) Set.univ

Tactic:
exact SetLike.coe_set_eq.mpr (rangeOfWType_eq_top s)

Premises used: Iff.mpr, _private.0.Subfield.rangeOfWType_eq_top, SetLike.coe_set_eq
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ #(WType (Operands s)) ≤ max (lift.{0, u} #(Fin 6 ⊕ (↑s : Type u))) ℵ₀

Tactic:
WType.cardinalMk_le_max_aleph0_of_finite'

Premises used: WType.cardinalMk_le_max_aleph0_of_finite'
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
h : max #(↑s : Type u) ℵ₀ = max (lift.{0, u} #(Fin 6 ⊕ (↑s : Type u))) ℵ₀
convert_3 : ∀ (a : Fin 6 ⊕ (↑s : Type u)), Finite (Operands s a)
⊢ #(WType (Operands s)) ≤ max #(↑s : Type u) ℵ₀

Tactic:
convert! WType.cardinalMk_le_max_aleph0_of_finite' using 1

Premises used: WType.cardinalMk_le_max_aleph0_of_finite'
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
h : max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
⊢ max #(↑s : Type u) ℵ₀ = max (lift.{0, u} #(Fin 6 ⊕ (↑s : Type u))) ℵ₀

Tactic:
rw [lift_uzero, mk_sum, lift_uzero]

Premises used: Cardinal.lift_uzero, Cardinal.mk_sum
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ lift.{u, 0} #(Fin 6) < ℵ₀

Tactic:
have : lift.{u, 0} #(Fin 6) < ℵ₀ := lift_lt_aleph0.mpr (lt_aleph0_of_finite _)
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ∀ (h : #(↑s : Type u) < ℵ₀), max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
h₁ : ∀ (h : ℵ₀ ≤ #(↑s : Type u)), max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
⊢ max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀

Tactic:
obtain h | h := lt_or_ge #s ℵ₀

Premises used: Cardinal.mk, Set.Elem, Cardinal.aleph0, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #(↑s : Type u) < ℵ₀
h₁ : lift.{u, 0} #(Fin 6) + #(↑s : Type u) ≤ ℵ₀
⊢ max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀

Tactic:
rw [max_eq_right h.le, max_eq_right]

Premises used: LT.lt.le, max_eq_right
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #(↑s : Type u) < ℵ₀
⊢ lift.{u, 0} #(Fin 6) + #(↑s : Type u) ≤ ℵ₀

Tactic:
(add_lt_aleph0 this h).le

Premises used: LT.lt.le, Cardinal.add_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #(↑s : Type u) < ℵ₀
⊢ lift.{u, 0} #(Fin 6) + #(↑s : Type u) ≤ ℵ₀

Tactic:
exact (add_lt_aleph0 this h).le

Premises used: LT.lt.le, Cardinal.add_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ℵ₀ ≤ #(↑s : Type u)
h₁ : #(↑s : Type u) = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
h₂ : #(↑s : Type u) = max #(↑s : Type u) ℵ₀
h₃ h₄ : #(↑s : Type u) = #(↑s : Type u)
⊢ max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀

Tactic:
rw [max_eq_left h, add_eq_right h (this.le.trans h), max_eq_left h]

Premises used: LT.lt.le, max_eq_left, LE.le.trans, Cardinal.add_eq_right
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
n : Fin 6
convert_3 : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩)))
convert_3₁ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩)))
convert_3₂ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩)))
convert_3₃ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩)))
convert_3₄ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩)))
convert_3₅ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨5, ⋯⟩)))
⊢ Finite (Operands s (Sum.inl n))

Tactic:
fin_cases n
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨0, ⋯⟩))

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨1, ⋯⟩))

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨2, ⋯⟩))

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨3, ⋯⟩))

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨4, ⋯⟩))

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨5, ⋯⟩))

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
val : (↑s : Type u)
⊢ Finite (Operands s (Sum.inr val))

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Cardinal.Subfield
Goal:
α : Type u
s : Set α
inst : DivisionRing α
inst_1 : Infinite.{u + 1} (↑s : Type u)
⊢ #↥(closure s) = #(↑s : Type u)

Tactic:
((cardinalMk_closure_le_max s).trans_eq <| max_eq_left <| aleph0_le_mk s).antisymm
    (mk_le_mk_of_subset subset_closure)

Premises used: LE.le.trans_eq, Subfield.cardinalMk_closure_le_max, LE.le.antisymm, Set.Elem, max_eq_left, Cardinal.mk_le_mk_of_subset, Subfield.subset_closure, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
a : Cardinal.{u_1}
⊢ ENat.toNat ((toENat : (a : Cardinal.{u_1}) → ℕ∞) a) = (toNat : (a : Cardinal.{u_1}) → ℕ) a

Tactic:
rfl

Premises used: dite, Function.extend, ENat.toNat, WithTop.untopD, WithTop.recTopCoe, rfl, Cardinal.toENatAux
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
n : ℕ∞
⊢ (toNat : (a : Cardinal.{u_1}) → ℕ) (↑n : Cardinal.{u_1}) = n.toNat

Tactic:
congr_arg ENat.toNat <| toENat_ofENat n

Premises used: Cardinal.toENat_ofENat, congr_arg, ENat.toNat, WithTop.untopD, WithTop.recTopCoe