-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_eq_self {c : Cardinal} (h : ℵ₀ ≤ c) : c * c = c

Proof state:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ c * c

Tactic:
simpa only [mul_one] using mul_le_mul_left' (one_le_aleph0.trans h) c

Result:
no goals

Proof state:
c✝ : Cardinal.{u_1}
h✝¹ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ y < c, Acc (fun x1 x2 => x1 < x2) y
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
e : (#α).ord = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x1 x2 => x1 < x2
g : α × α → α := fun p => p.1 ⊔ p.2
f : α × α ↪ Ordinal.{u_1} × α × α :=
  { toFun := fun p => ((typein fun x1 x2 => x1 < x2).toRelEmbedding (g p), p), inj' := ⋯ }
s : α × α → α × α → Prop :=
  ⇑f ⁻¹'o Prod.Lex (fun x1 x2 => x1 < x2) (Prod.Lex (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2)
this : IsWellOrder (α × α) s
p : α × α
h✝ : (typein s).toRelEmbedding p < type s
q : α × α
h : g q < g p ∨ g q = g p ∧ (q.1 < p.1 ∨ q.1 = p.1 ∧ q.2 < p.2)
⊢ q ∈ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}

Tactic:
exact max_le_iff.1 (le_iff_lt_or_eq.2 <| h.imp_right And.left)

Result:
no goals

Proof state:
case intro.intro.intro
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ y < c, Acc (fun x1 x2 => x1 < x2) y
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
e : (#α).ord = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x1 x2 => x1 < x2
g : α × α → α := fun p => p.1 ⊔ p.2
f : α × α ↪ Ordinal.{u_1} × α × α :=
  { toFun := fun p => ((typein fun x1 x2 => x1 < x2).toRelEmbedding (g p), p), inj' := ⋯ }
s : α × α → α × α → Prop :=
  ⇑f ⁻¹'o Prod.Lex (fun x1 x2 => x1 < x2) (Prod.Lex (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2)
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
⊢ (typein s).toRelEmbedding p < type r

Tactic:
rw [← e, lt_ord]

Result:
case intro.intro.intro
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ y < c, Acc (fun x1 x2 => x1 < x2) y
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
e : (#α).ord = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x1 x2 => x1 < x2
g : α × α → α := fun p => p.1 ⊔ p.2
f : α × α ↪ Ordinal.{u_1} × α × α :=
  { toFun := fun p => ((typein fun x1 x2 => x1 < x2).toRelEmbedding (g p), p), inj' := ⋯ }
s : α × α → α × α → Prop :=
  ⇑f ⁻¹'o Prod.Lex (fun x1 x2 => x1 < x2) (Prod.Lex (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2)
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
⊢ ((typein s).toRelEmbedding p).card < #α

Proof state:
case intro.intro.intro.refine_2.inl
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ y < c, Acc (fun x1 x2 => x1 < x2) y
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
e : (#α).ord = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x1 x2 => x1 < x2
g : α × α → α := fun p => p.1 ⊔ p.2
f : α × α ↪ Ordinal.{u_1} × α × α :=
  { toFun := fun p => ((typein fun x1 x2 => x1 < x2).toRelEmbedding (g p), p), inj' := ⋯ }
s : α × α → α × α → Prop :=
  ⇑f ⁻¹'o Prod.Lex (fun x1 x2 => x1 < x2) (Prod.Lex (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2)
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
qo : (succ ((typein fun x1 x2 => x1 < x2).toRelEmbedding (g p))).card < ℵ₀
⊢ (succ ((typein fun x1 x2 => x1 < x2).toRelEmbedding (g p))).card *
      (succ ((typein fun x1 x2 => x1 < x2).toRelEmbedding (g p))).card <
    #α

Tactic:
exact (mul_lt_aleph0 qo qo).trans_le ol

Result:
no goals

Proof state:
case intro.intro
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ y < c, Acc (fun x1 x2 => x1 < x2) y
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
e : (#α).ord = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x1 x2 => x1 < x2
g : α × α → α := fun p => p.1 ⊔ p.2
f : α × α ↪ Ordinal.{u_1} × α × α :=
  { toFun := fun p => ((typein fun x1 x2 => x1 < x2).toRelEmbedding (g p), p), inj' := ⋯ }
s : α × α → α × α → Prop :=
  ⇑f ⁻¹'o Prod.Lex (fun x1 x2 => x1 < x2) (Prod.Lex (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2)
this : IsWellOrder (α × α) s
o : Ordinal.{u_1}
h : o < type s
⊢ o < type r

Tactic:
rcases typein_surj s h with ⟨p, rfl⟩

Result:
case intro.intro.intro
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ y < c, Acc (fun x1 x2 => x1 < x2) y
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
e : (#α).ord = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x1 x2 => x1 < x2
g : α × α → α := fun p => p.1 ⊔ p.2
f : α × α ↪ Ordinal.{u_1} × α × α :=
  { toFun := fun p => ((typein fun x1 x2 => x1 < x2).toRelEmbedding (g p), p), inj' := ⋯ }
s : α × α → α × α → Prop :=
  ⇑f ⁻¹'o Prod.Lex (fun x1 x2 => x1 < x2) (Prod.Lex (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2)
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
⊢ (typein s).toRelEmbedding p < type r

Proof state:
case intro.intro.intro.refine_1
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ y < c, Acc (fun x1 x2 => x1 < x2) y
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
e : (#α).ord = type r
this✝² : LinearOrder α := linearOrderOfSTO r
this✝¹ : IsWellOrder α fun x1 x2 => x1 < x2
g : α × α → α := fun p => p.1 ⊔ p.2
f : α × α ↪ Ordinal.{u_1} × α × α :=
  { toFun := fun p => ((typein fun x1 x2 => x1 < x2).toRelEmbedding (g p), p), inj' := ⋯ }
s : α × α → α × α → Prop :=
  ⇑f ⁻¹'o Prod.Lex (fun x1 x2 => x1 < x2) (Prod.Lex (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2)
this✝ : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
this : {q | s q p} ⊆ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
⊢ ↑(insert (g p) {x | r x (g p)}) ≃ ↑{x | r x (g p)} ⊕ PUnit.{u_1 + 1}

Tactic:
refine (Equiv.Set.insert ?_).trans ((Equiv.refl _).sumCongr punitEquivPUnit)

Result:
case intro.intro.intro.refine_1
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ y < c, Acc (fun x1 x2 => x1 < x2) y
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
e : (#α).ord = type r
this✝² : LinearOrder α := linearOrderOfSTO r
this✝¹ : IsWellOrder α fun x1 x2 => x1 < x2
g : α × α → α := fun p => p.1 ⊔ p.2
f : α × α ↪ Ordinal.{u_1} × α × α :=
  { toFun := fun p => ((typein fun x1 x2 => x1 < x2).toRelEmbedding (g p), p), inj' := ⋯ }
s : α × α → α × α → Prop :=
  ⇑f ⁻¹'o Prod.Lex (fun x1 x2 => x1 < x2) (Prod.Lex (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2)
this✝ : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
this : {q | s q p} ⊆ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
⊢ g p ∉ {x | r x (g p)}

Proof state:
case intro.intro
c✝ : Cardinal.{u_1}
h : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ y < c, Acc (fun x1 x2 => x1 < x2) y
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
e : (#α).ord = type r
this✝ : LinearOrder α := linearOrderOfSTO r
this : IsWellOrder α fun x1 x2 => x1 < x2
⊢ #α * #α ≤ #α

Tactic:
let g : α × α → α := fun p => max p.1 p.2

Result:
case intro.intro
c✝ : Cardinal.{u_1}
h : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ y < c, Acc (fun x1 x2 => x1 < x2) y
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
e : (#α).ord = type r
this✝ : LinearOrder α := linearOrderOfSTO r
this : IsWellOrder α fun x1 x2 => x1 < x2
g : α × α → α := fun p => p.1 ⊔ p.2
⊢ #α * #α ≤ #α