[GOAL]
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α α' : Sort u
β : α → Sort v
β' : α' → Sort v
f : (a : α) → β a
f' : (a : α') → β' a
hα : α = α'
h : ∀ (a : α) (a' : α'), HEq a a' → HEq (f a) (f' a')
⊢ HEq f f'
[PROOFSTEP]
subst hα
[GOAL]
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
⊢ HEq f f'
[PROOFSTEP]
have : ∀ a, HEq (f a) (f' a) := λ a => h a a (HEq.refl a)
[GOAL]
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this : ∀ (a : α), HEq (f a) (f' a)
⊢ HEq f f'
[PROOFSTEP]
have : β = β' := by
  funext a
  exact type_eq_of_heq (this a)
[GOAL]
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this : ∀ (a : α), HEq (f a) (f' a)
⊢ β = β'
[PROOFSTEP]
funext a
[GOAL]
case h
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this : ∀ (a : α), HEq (f a) (f' a)
a : α
⊢ β a = β' a
[PROOFSTEP]
exact type_eq_of_heq (this a)
[GOAL]
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this✝ : ∀ (a : α), HEq (f a) (f' a)
this : β = β'
⊢ HEq f f'
[PROOFSTEP]
subst this
[GOAL]
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f f' : (a : α) → β a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this : ∀ (a : α), HEq (f a) (f' a)
⊢ HEq f f'
[PROOFSTEP]
apply heq_of_eq
[GOAL]
case h
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f f' : (a : α) → β a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this : ∀ (a : α), HEq (f a) (f' a)
⊢ f = f'
[PROOFSTEP]
funext a
[GOAL]
case h.h
α✝ : Sort ?u.774
β✝ : Sort ?u.777
γ : Sort ?u.780
f✝ : α✝ → β✝
α : Sort u
β : α → Sort v
f f' : (a : α) → β a
h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')
this : ∀ (a : α), HEq (f a) (f' a)
a : α
⊢ f a = f' a
[PROOFSTEP]
exact eq_of_heq (this a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Sort ?u.1351
f : α → β
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
I : Injective f
a b : α
⊢ (f a == f b) = (a == b)
[PROOFSTEP]
by_cases h : a == b
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Sort ?u.1351
f : α → β
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
I : Injective f
a b : α
h : (a == b) = true
⊢ (f a == f b) = (a == b)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Sort ?u.1351
f : α → β
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
I : Injective f
a b : α
h : ¬(a == b) = true
⊢ (f a == f b) = (a == b)
[PROOFSTEP]
simp [h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Sort ?u.1351
f : α → β
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
I : Injective f
a b : α
h : (a == b) = true
⊢ f a = f b
[PROOFSTEP]
simpa [I.eq_iff] using h
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Sort ?u.1351
f : α → β
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
I : Injective f
a b : α
h : ¬(a == b) = true
⊢ ¬f a = f b
[PROOFSTEP]
simpa [I.eq_iff] using h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
⊢ Injective fun x => if h : p x then f { val := x, property := h } else f' { val := x, property := h }
[PROOFSTEP]
intros x₁ x₂ h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (fun x => if h : p x then f { val := x, property := h } else f' { val := x, property := h }) x₁ =
    (fun x => if h : p x then f { val := x, property := h } else f' { val := x, property := h }) x₂
⊢ x₁ = x₂
[PROOFSTEP]
dsimp only at h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
⊢ x₁ = x₂
[PROOFSTEP]
by_cases h₁ : p x₁
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
h₁ : p x₁
⊢ x₁ = x₂
[PROOFSTEP]
by_cases h₂ : p x₂
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
h₁ : ¬p x₁
⊢ x₁ = x₂
[PROOFSTEP]
by_cases h₂ : p x₂
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
h₁ : p x₁
h₂ : p x₂
⊢ x₁ = x₂
[PROOFSTEP]
rw [dif_pos h₁, dif_pos h₂] at h
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h₁ : p x₁
h₂ : p x₂
h : f { val := x₁, property := h₁ } = f { val := x₂, property := h₂ }
⊢ x₁ = x₂
[PROOFSTEP]
injection (hf h)
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
h₁ : p x₁
h₂ : ¬p x₂
⊢ x₁ = x₂
[PROOFSTEP]
rw [dif_pos h₁, dif_neg h₂] at h
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h₁ : p x₁
h₂ : ¬p x₂
h : f { val := x₁, property := h₁ } = f' { val := x₂, property := h₂ }
⊢ x₁ = x₂
[PROOFSTEP]
exact (im_disj h).elim
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
h₁ : ¬p x₁
h₂ : p x₂
⊢ x₁ = x₂
[PROOFSTEP]
rw [dif_neg h₁, dif_pos h₂] at h
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h₁ : ¬p x₁
h₂ : p x₂
h : f' { val := x₁, property := h₁ } = f { val := x₂, property := h₂ }
⊢ x₁ = x₂
[PROOFSTEP]
exact (im_disj h.symm).elim
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h :
  (if h : p x₁ then f { val := x₁, property := h } else f' { val := x₁, property := h }) =
    if h : p x₂ then f { val := x₂, property := h } else f' { val := x₂, property := h }
h₁ : ¬p x₁
h₂ : ¬p x₂
⊢ x₁ = x₂
[PROOFSTEP]
rw [dif_neg h₁, dif_neg h₂] at h
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
γ : Sort ?u.3653
f✝ : α → β
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
x₁ x₂ : α
h₁ : ¬p x₁
h₂ : ¬p x₂
h : f' { val := x₁, property := h₁ } = f' { val := x₂, property := h₂ }
⊢ x₁ = x₂
[PROOFSTEP]
injection (hf' h)
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.6624
f : α → β
h : ∀ (g₁ g₂ : β → Prop), g₁ ∘ f = g₂ ∘ f → g₁ = g₂
⊢ Surjective f
[PROOFSTEP]
specialize h (fun y ↦ ∃ x, f x = y) (fun _ ↦ True) (funext fun x ↦ eq_true ⟨_, rfl⟩)
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.6624
f : α → β
h : (fun y => ∃ x, f x = y) = fun x => True
⊢ Surjective f
[PROOFSTEP]
intro y
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.6624
f : α → β
h : (fun y => ∃ x, f x = y) = fun x => True
y : β
⊢ ∃ a, f a = y
[PROOFSTEP]
rw [congr_fun h y]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.6624
f : α → β
h : (fun y => ∃ x, f x = y) = fun x => True
y : β
⊢ True
[PROOFSTEP]
trivial
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.7150
f✝ f : α → β
hf : Bijective f
p : β → Prop
x✝ : ∃! y, p y
y : β
hpy : (fun y => p y) y
hy : ∀ (y_1 : β), (fun y => p y) y_1 → y_1 = y
x : α
hx : f x = y
⊢ (fun x => p (f x)) x
[PROOFSTEP]
simpa [hx]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.7150
f✝ f : α → β
hf : Bijective f
p : β → Prop
x✝ : ∃! x, p (f x)
x : α
hpx : (fun x => p (f x)) x
hx : ∀ (y : α), (fun x => p (f x)) y → y = x
y : β
hy : (fun y => p y) y
z : α
hz : f z = y
⊢ (fun x => p (f x)) z
[PROOFSTEP]
simpa [hz]
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
⊢ ¬Surjective f
[PROOFSTEP]
intro hf
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
⊢ False
[PROOFSTEP]
let T : Type max u v := Sigma f
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
⊢ False
[PROOFSTEP]
cases' hf (Set T) with U hU
[GOAL]
case intro
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
⊢ False
[PROOFSTEP]
let g : Set T → T := fun s ↦ ⟨U, cast hU.symm s⟩
[GOAL]
case intro
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
⊢ False
[PROOFSTEP]
have hg : Injective g := by
  intro s t h
  suffices cast hU (g s).2 = cast hU (g t).2
    by
    simp only [cast_cast, cast_eq] at this
    assumption
  · congr
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
⊢ Injective g
[PROOFSTEP]
intro s t h
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
⊢ s = t
[PROOFSTEP]
suffices cast hU (g s).2 = cast hU (g t).2
  by
  simp only [cast_cast, cast_eq] at this
  assumption
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
this : cast hU (g s).snd = cast hU (g t).snd
⊢ s = t
[PROOFSTEP]
simp only [cast_cast, cast_eq] at this
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
this : s = t
⊢ s = t
[PROOFSTEP]
assumption
[GOAL]
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
⊢ cast hU (g s).snd = cast hU (g t).snd
[PROOFSTEP]
congr
[GOAL]
case intro
α✝ : Sort ?u.8686
β : Sort ?u.8689
γ : Sort ?u.8692
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
hg : Injective g
⊢ False
[PROOFSTEP]
exact cantor_injective g hg
[GOAL]
α : Sort u_2
β : Sort u_1
γ : Sort u_3
f✝ f : α → β
g : β → α
h : β → γ
i : γ → β
hf : LeftInverse f g
hh : LeftInverse h i
a : γ
⊢ h (f (g (i a))) = a
[PROOFSTEP]
rw [hf (i a), hh a]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.11227
f✝ f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ = g₁ ∘ f ∘ g₂
[PROOFSTEP]
rw [h₂.comp_eq_id, comp.right_id]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort ?u.11227
f✝ f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ ∘ f ∘ g₂ = g₂
[PROOFSTEP]
rw [← comp.assoc, h₁.comp_eq_id, comp.left_id]
[GOAL]
α✝ : Sort ?u.11659
β✝ : Sort ?u.11662
γ : Sort ?u.11665
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f a = b
[PROOFSTEP]
rw [hpi, dif_pos h'] at h
[GOAL]
α✝ : Sort ?u.11659
β✝ : Sort ?u.11662
γ : Sort ?u.11665
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : some (Classical.choose h') = some a
⊢ f a = b
[PROOFSTEP]
injection h with h
[GOAL]
α✝ : Sort ?u.11659
β✝ : Sort ?u.11662
γ : Sort ?u.11665
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : Classical.choose h' = a
⊢ f a = b
[PROOFSTEP]
subst h
[GOAL]
α✝ : Sort ?u.11659
β✝ : Sort ?u.11662
γ : Sort ?u.11665
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f (Classical.choose h') = b
[PROOFSTEP]
apply Classical.choose_spec h'
[GOAL]
α✝ : Sort ?u.11659
β✝ : Sort ?u.11662
γ : Sort ?u.11665
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b
[PROOFSTEP]
rw [hpi, dif_neg h'] at h
[GOAL]
α✝ : Sort ?u.11659
β✝ : Sort ?u.11662
γ : Sort ?u.11665
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
h : none = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b
[PROOFSTEP]
contradiction
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
a : α
b : β
h : ∃ a, f a = b
⊢ f (invFun f b) = b
[PROOFSTEP]
simp only [invFun, dif_pos h, h.choose_spec]
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
a : α
b✝ : β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = f (g b)
[PROOFSTEP]
rw [hg b]
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
a : α
b✝ : β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = b
[PROOFSTEP]
exact invFun_eq ⟨g b, hg b⟩
[GOAL]
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
⊢ update f a' b a = if a = a' then b else f a
[PROOFSTEP]
have h2 : (h : a = a') → Eq.rec (motive := λ _ _ => β) b h.symm = b :=
  by
  intro h
  rw [eq_rec_constant]
[GOAL]
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
⊢ ∀ (h : a = a'), (_ : a' = a) ▸ b = b
[PROOFSTEP]
intro h
[GOAL]
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
h : a = a'
⊢ (_ : a' = a) ▸ b = b
[PROOFSTEP]
rw [eq_rec_constant]
[GOAL]
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
h2 : ∀ (h : a = a'), (_ : a' = a) ▸ b = b
⊢ update f a' b a = if a = a' then b else f a
[PROOFSTEP]
have h3 : (λ h : a = a' => Eq.rec (motive := λ _ _ => β) b h.symm) = (λ _ : a = a' => b) := funext h2
[GOAL]
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f : α → β
a' : α
b : β
a : α
h2 : ∀ (h : a = a'), (_ : a' = a) ▸ b = b
h3 : (fun h => (_ : a' = a) ▸ b) = fun x => b
⊢ update f a' b a = if a = a' then b else f a
[PROOFSTEP]
let f := λ x => dite (a = a') x (λ (_ : ¬a = a') => (f a))
[GOAL]
α : Sort u
β✝ : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝¹ g : (a : α) → β✝ a
a✝ : α
b✝ : β✝ a✝
β : Sort u_1
f✝ : α → β
a' : α
b : β
a : α
h2 : ∀ (h : a = a'), (_ : a' = a) ▸ b = b
h3 : (fun h => (_ : a' = a) ▸ b) = fun x => b
f : (a = a' → β) → β := fun x => dite (a = a') x fun x => f✝ a
⊢ update f✝ a' b a = if a = a' then b else f✝ a
[PROOFSTEP]
exact congrArg f h3
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β a
a : α
b : β a
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
⊢ v = v'
[PROOFSTEP]
have := congr_fun h a'
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β a
a : α
b : β a
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
this : update f a' v a' = update f a' v' a'
⊢ v = v'
[PROOFSTEP]
rwa [update_same, update_same] at this
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β a
a✝ : α
b✝ : β a✝
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∀ (x : α), p x (update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
[PROOFSTEP]
rw [← and_forall_ne a, update_same]
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β a
a✝ : α
b✝ : β a✝
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (p a b ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β a
a✝ : α
b✝ : β a✝
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∃ x, p x (update f a b x)) ↔ p a b ∨ ∃ x x_1, p x (f x)
[PROOFSTEP]
rw [← not_forall_not, forall_update_iff f fun a b ↦ ¬p a b]
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f✝ g : (a : α) → β a
a✝ : α
b✝ : β a✝
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ ¬(¬p a b ∧ ∀ (x : α), x ≠ a → ¬p x (f x)) ↔ p a b ∨ ∃ x x_1, p x (f x)
[PROOFSTEP]
simp [-not_and, not_and_or]
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f g : (a : α) → β a
a : α
b : β a
⊢ update f a b = f ↔ b = f a
[PROOFSTEP]
simp [update_eq_iff]
[GOAL]
α : Sort u
β : α → Sort v
α' : Sort w
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f g : (a : α) → β a
a : α
b : β a
⊢ f = update f a b ↔ f a = b
[PROOFSTEP]
simp [eq_update_iff]
[GOAL]
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
⊢ f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
h : j = i
⊢ f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j
[PROOFSTEP]
subst j
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
⊢ f i (update g i v i) = update (fun k => f k (g k)) i (f i v) i
[PROOFSTEP]
simp
[GOAL]
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
h : ¬j = i
⊢ f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j
[PROOFSTEP]
simp [h]
[GOAL]
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
⊢ f j (update g i v j) (update h i w j) = update (fun k => f k (g k) (h k)) i (f i v w) j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h✝ : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
h : j = i
⊢ f j (update g i v j) (update h✝ i w j) = update (fun k => f k (g k) (h✝ k)) i (f i v w) j
[PROOFSTEP]
subst j
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h : (i : ι) → β i
i : ι
v : α i
w : β i
⊢ f i (update g i v i) (update h i w i) = update (fun k => f k (g k) (h k)) i (f i v w) i
[PROOFSTEP]
simp
[GOAL]
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g✝ : (a : α✝) → β✝ a
a : α✝
b : β✝ a
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h✝ : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
h : ¬j = i
⊢ f j (update g i v j) (update h✝ i w j) = update (fun k => f k (g k) (h✝ k)) i (f i v w) j
[PROOFSTEP]
simp [h]
[GOAL]
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
⊢ update (update f a v) b w = update (update f b w) a v
[PROOFSTEP]
funext c
[GOAL]
case h
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
⊢ update (update f a v) b w c = update (update f b w) a v c
[PROOFSTEP]
simp only [update]
[GOAL]
case h
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
by_cases h₁ : c = b
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
by_cases h₂ : c = a
[GOAL]
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : ¬c = b
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
by_cases h₂ : c = a
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
rw [dif_pos h₁, dif_pos h₂]
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : c = a
⊢ (_ : b = c) ▸ w = (_ : a = c) ▸ v
[PROOFSTEP]
cases h (h₂.symm.trans h₁)
[GOAL]
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : ¬c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
rw [dif_pos h₁, dif_pos h₁, dif_neg h₂]
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : ¬c = b
h₂ : c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
rw [dif_neg h₁, dif_neg h₁, dif_pos h₂]
[GOAL]
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : ¬c = b
h₂ : ¬c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
[PROOFSTEP]
rw [dif_neg h₁, dif_neg h₁, dif_neg h₂]
[GOAL]
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
⊢ update (update f a v) a w = update f a w
[PROOFSTEP]
funext b
[GOAL]
case h
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
b : α
⊢ update (update f a v) a w b = update f a w b
[PROOFSTEP]
by_cases h : b = a
[GOAL]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
b : α
h : b = a
⊢ update (update f a v) a w b = update f a w b
[PROOFSTEP]
simp [update, h]
[GOAL]
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
b : α
h : ¬b = a
⊢ update (update f a v) a w b = update f a w b
[PROOFSTEP]
simp [update, h]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f✝ f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b
[PROOFSTEP]
unfold extend
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f✝ f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ (if h : ∃ a, f a = b then g (Classical.choose h) else e' b) =
    if h : ∃ a, f a = b then g (Classical.choose h) else e' b
[PROOFSTEP]
congr
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
⊢ extend f g e' (f a) = g a
[PROOFSTEP]
simp only [extend_def, dif_pos, exists_apply_eq_apply]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
⊢ g (Classical.choose (_ : ∃ a_1, f a_1 = f a)) = g a
[PROOFSTEP]
exact hf (Classical.choose_spec (exists_apply_eq_apply f a))
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ extend f g e' b = e' b
[PROOFSTEP]
simp [Function.extend_def, hb]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
hf : FactorsThrough g f
x : α
⊢ g x = (extend f g (const β (Classical.arbitrary γ)) ∘ f) x
[PROOFSTEP]
simp only [comp_apply, hf.extend_apply]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
h : ∃ e, g = e ∘ f
x✝¹ x✝ : α
hf : f x✝¹ = f x✝
⊢ g x✝¹ = g x✝
[PROOFSTEP]
rw [Classical.choose_spec h, comp_apply, comp_apply, hf]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
by_cases hb : ∃ a, f a = b
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
case neg
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
case pos =>
  rcases hb with ⟨a, ha⟩
  subst b
  rw [hf.extend_apply, FactorsThrough.extend_apply, comp]
  case intro.hf =>
    intro a b h
    simp only [comp_apply]
    apply congr_arg
    exact hf h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
case pos =>
  rcases hb with ⟨a, ha⟩
  subst b
  rw [hf.extend_apply, FactorsThrough.extend_apply, comp]
  case intro.hf =>
    intro a b h
    simp only [comp_apply]
    apply congr_arg
    exact hf h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
rcases hb with ⟨a, ha⟩
[GOAL]
case intro
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
a : α
ha : f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
subst b
[GOAL]
case intro
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a : α
⊢ F (extend f g e' (f a)) = extend f (F ∘ g) (F ∘ e') (f a)
[PROOFSTEP]
rw [hf.extend_apply, FactorsThrough.extend_apply, comp]
[GOAL]
case intro.hf
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a : α
⊢ FactorsThrough (F ∘ g) f
[PROOFSTEP]
case intro.hf =>
  intro a b h
  simp only [comp_apply]
  apply congr_arg
  exact hf h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a : α
⊢ FactorsThrough (F ∘ g) f
[PROOFSTEP]
case intro.hf =>
  intro a b h
  simp only [comp_apply]
  apply congr_arg
  exact hf h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a : α
⊢ FactorsThrough (F ∘ g) f
[PROOFSTEP]
intro a b h
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a✝ a b : α
h : f a = f b
⊢ (F ∘ g) a = (F ∘ g) b
[PROOFSTEP]
simp only [comp_apply]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a✝ a b : α
h : f a = f b
⊢ F (g a) = F (g b)
[PROOFSTEP]
apply congr_arg
[GOAL]
case h
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
a✝ a b : α
h : f a = f b
⊢ g a = g b
[PROOFSTEP]
exact hf h
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
case neg => rw [extend_apply' _ _ _ hb, extend_apply' _ _ _ hb, comp]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
case neg => rw [extend_apply' _ _ _ hb, extend_apply' _ _ _ hb, comp]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
δ : Sort u_4
g : α → γ
hf : FactorsThrough g f
F : γ → δ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
[PROOFSTEP]
rw [extend_apply' _ _ _ hb, extend_apply' _ _ _ hb, comp]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
⊢ Injective fun g => extend f g e'
[PROOFSTEP]
intro g₁ g₂ hg
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
⊢ g₁ = g₂
[PROOFSTEP]
refine' funext fun x ↦ _
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
x : α
⊢ g₁ x = g₂ x
[PROOFSTEP]
have H := congr_fun hg (f x)
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
x : α
H : (fun g => extend f g e') g₁ (f x) = (fun g => extend f g e') g₂ (f x)
⊢ g₁ x = g₂ x
[PROOFSTEP]
simp only [hf.extend_apply] at H
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
x : α
H : g₁ x = g₂ x
⊢ g₁ x = g₂ x
[PROOFSTEP]
exact H
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Bijective f
g : α → γ
⊢ (fun g => g ∘ f) (g ∘ surjInv (_ : Surjective f)) = g
[PROOFSTEP]
simp only [comp.assoc g _ f, (leftInverse_surjInv hf).comp_eq_id, comp.right_id]
[GOAL]
α : Sort u
f : α → α
h : Involutive f
P : Prop
inst✝ : Decidable P
x : α
⊢ f (if P then x else f x) = if ¬P then x else f x
[PROOFSTEP]
rw [apply_ite f, h, ite_not]
[GOAL]
p : Prop
α : Sort u_1
inst✝ : Nonempty α
P : α → Prop
f : p → α
a : p
h : P (f a)
⊢ P (sometimes f)
[PROOFSTEP]
rwa [sometimes_eq]
[GOAL]
α β : Sort u_1
h : α = β
⊢ Bijective (Eq.mp h)
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Sort u_1
⊢ Bijective (Eq.mp (_ : α = α))
[PROOFSTEP]
refine ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩
[GOAL]
α β : Sort u_1
h : α = β
⊢ Bijective (Eq.mpr h)
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Sort u_1
⊢ Bijective (Eq.mpr (_ : α = α))
[PROOFSTEP]
refine ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩
[GOAL]
α β : Sort u_1
h : α = β
⊢ Bijective (cast h)
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Sort u_1
⊢ Bijective (cast (_ : α = α))
[PROOFSTEP]
refine ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩
[GOAL]
α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ HEq (C (g (f a))) (C a)
[PROOFSTEP]
rw [h]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ cast (_ : γ (f (g (f a))) = γ (f a)) (C (g (f a))) = C a
[PROOFSTEP]
rw [cast_eq_iff_heq, h]


[GOAL]
a✝ b✝ c a b : Ordinal.{u}
⊢ a ♯ b = max (blsub a fun a' x => a' ♯ b) (blsub b fun b' x => a ♯ b')
[PROOFSTEP]
rw [nadd]
[GOAL]
a b c : Ordinal.{u}
⊢ a < b ♯ c ↔ (∃ b', b' < b ∧ a ≤ b' ♯ c) ∨ ∃ c', c' < c ∧ a ≤ b ♯ c'
[PROOFSTEP]
rw [nadd_def]
[GOAL]
a b c : Ordinal.{u}
⊢ a < max (blsub b fun a' x => a' ♯ c) (blsub c fun b' x => b ♯ b') ↔
    (∃ b', b' < b ∧ a ≤ b' ♯ c) ∨ ∃ c', c' < c ∧ a ≤ b ♯ c'
[PROOFSTEP]
simp [lt_blsub_iff]
[GOAL]
a b c : Ordinal.{u}
⊢ b ♯ c ≤ a ↔ (∀ (b' : Ordinal.{u}), b' < b → b' ♯ c < a) ∧ ∀ (c' : Ordinal.{u}), c' < c → b ♯ c' < a
[PROOFSTEP]
rw [nadd_def]
[GOAL]
a b c : Ordinal.{u}
⊢ max (blsub b fun a' x => a' ♯ c) (blsub c fun b' x => b ♯ b') ≤ a ↔
    (∀ (b' : Ordinal.{u}), b' < b → b' ♯ c < a) ∧ ∀ (c' : Ordinal.{u}), c' < c → b ♯ c' < a
[PROOFSTEP]
simp [blsub_le_iff]
[GOAL]
a✝ b c : Ordinal.{u}
h : b ≤ c
a : Ordinal.{u}
⊢ a ♯ b ≤ a ♯ c
[PROOFSTEP]
rcases lt_or_eq_of_le h with (h | rfl)
[GOAL]
case inl
a✝ b c : Ordinal.{u}
h✝ : b ≤ c
a : Ordinal.{u}
h : b < c
⊢ a ♯ b ≤ a ♯ c
[PROOFSTEP]
exact (nadd_lt_nadd_left h a).le
[GOAL]
case inr
a✝ b a : Ordinal.{u}
h : b ≤ b
⊢ a ♯ b ≤ a ♯ b
[PROOFSTEP]
exact le_rfl
[GOAL]
a✝ b c : Ordinal.{u}
h : b ≤ c
a : Ordinal.{u}
⊢ b ♯ a ≤ c ♯ a
[PROOFSTEP]
rcases lt_or_eq_of_le h with (h | rfl)
[GOAL]
case inl
a✝ b c : Ordinal.{u}
h✝ : b ≤ c
a : Ordinal.{u}
h : b < c
⊢ b ♯ a ≤ c ♯ a
[PROOFSTEP]
exact (nadd_lt_nadd_right h a).le
[GOAL]
case inr
a✝ b a : Ordinal.{u}
h : b ≤ b
⊢ b ♯ a ≤ b ♯ a
[PROOFSTEP]
exact le_rfl
[GOAL]
a✝ b✝ c : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ a ♯ b = b ♯ a
[PROOFSTEP]
rw [nadd_def, nadd_def, max_comm]
[GOAL]
a✝ b✝ c : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ max (blsub b fun b' x => a ♯ b') (blsub a fun a' x => a' ♯ b) =
    max (blsub b fun a' x => a' ♯ a) (blsub a fun b' x => b ♯ b')
[PROOFSTEP]
congr
[GOAL]
case e_a.e_f
a✝ b✝ c : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ (fun b' x => a ♯ b') = fun a' x => a' ♯ a
[PROOFSTEP]
ext
[GOAL]
case e_a.e_f
a✝ b✝ c : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ (fun a' x => a' ♯ b) = fun b' x => b ♯ b'
[PROOFSTEP]
ext
[GOAL]
case e_a.e_f.h.h
a✝ b✝ c : Ordinal.{u}
a b x✝¹ : Ordinal.{u_1}
x✝ : x✝¹ < b
⊢ a ♯ x✝¹ = x✝¹ ♯ a
[PROOFSTEP]
apply nadd_comm
[GOAL]
case e_a.e_f.h.h
a✝ b✝ c : Ordinal.{u}
a b x✝¹ : Ordinal.{u_1}
x✝ : x✝¹ < a
⊢ x✝¹ ♯ b = b ♯ x✝¹
[PROOFSTEP]
apply nadd_comm
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ blsub (a ♯ b) f =
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
[PROOFSTEP]
apply (blsub_le_iff.2 fun i h => _).antisymm (max_le _ _)
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ ∀ (i : Ordinal.{u}) (h : i < a ♯ b),
    f i h <
      max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b))
        (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) ≤ blsub (a ♯ b) f
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) ≤ blsub (a ♯ b) f
[PROOFSTEP]
intro i h
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
i : Ordinal.{u}
h : i < a ♯ b
⊢ f i h <
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
[PROOFSTEP]
rcases lt_nadd_iff.1 h with (⟨a', ha', hi⟩ | ⟨b', hb', hi⟩)
[GOAL]
case inl.intro.intro
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
i : Ordinal.{u}
h : i < a ♯ b
a' : Ordinal.{u}
ha' : a' < a
hi : i ≤ a' ♯ b
⊢ f i h <
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
[PROOFSTEP]
exact lt_max_of_lt_left ((hf h (nadd_lt_nadd_right ha' b) hi).trans_lt (lt_blsub _ _ ha'))
[GOAL]
case inr.intro.intro
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
i : Ordinal.{u}
h : i < a ♯ b
b' : Ordinal.{u}
hb' : b' < b
hi : i ≤ a ♯ b'
⊢ f i h <
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
[PROOFSTEP]
exact lt_max_of_lt_right ((hf h (nadd_lt_nadd_left hb' a) hi).trans_lt (lt_blsub _ _ hb'))
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) ≤ blsub (a ♯ b) f
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) ≤ blsub (a ♯ b) f
[PROOFSTEP]
all_goals
  apply blsub_le_of_brange_subset.{u, u, v}
  rintro c ⟨d, hd, rfl⟩
  apply mem_brange_self
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) ≤ blsub (a ♯ b) f
[PROOFSTEP]
apply blsub_le_of_brange_subset.{u, u, v}
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (brange a fun a_1 ha => (fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) a_1 ha) ⊆
    brange (a ♯ b) fun a_1 ha => f a_1 ha
[PROOFSTEP]
rintro c ⟨d, hd, rfl⟩
[GOAL]
case intro.intro
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
d : Ordinal.{u}
hd : d < a
⊢ (fun a_1 ha => (fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) a_1 ha) d hd ∈ brange (a ♯ b) fun a_1 ha => f a_1 ha
[PROOFSTEP]
apply mem_brange_self
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) ≤ blsub (a ♯ b) f
[PROOFSTEP]
apply blsub_le_of_brange_subset.{u, u, v}
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (brange b fun a_1 ha => (fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) a_1 ha) ⊆
    brange (a ♯ b) fun a_1 ha => f a_1 ha
[PROOFSTEP]
rintro c ⟨d, hd, rfl⟩
[GOAL]
case intro.intro
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
d : Ordinal.{u}
hd : d < b
⊢ (fun a_1 ha => (fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) a_1 ha) d hd ∈ brange (a ♯ b) fun a_1 ha => f a_1 ha
[PROOFSTEP]
apply mem_brange_self
[GOAL]
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ a ♯ b ♯ c = a ♯ (b ♯ c)
[PROOFSTEP]
rw [nadd_def a (b ♯ c), nadd_def, blsub_nadd_of_mono, blsub_nadd_of_mono, max_assoc]
[GOAL]
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ max (blsub a fun a' ha' => a' ♯ b ♯ c) (max (blsub b fun b' hb' => a ♯ b' ♯ c) (blsub c fun b' x => a ♯ b ♯ b')) =
    max (blsub a fun a' x => a' ♯ (b ♯ c))
      (max (blsub b fun a' ha' => a ♯ (a' ♯ c)) (blsub c fun b' hb' => a ♯ (b ♯ b')))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_f
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ (fun a' ha' => a' ♯ b ♯ c) = fun a' x => a' ♯ (b ♯ c)
[PROOFSTEP]
ext (d hd)
[GOAL]
case e_a.e_a.e_f
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ (fun b' hb' => a ♯ b' ♯ c) = fun a' ha' => a ♯ (a' ♯ c)
[PROOFSTEP]
ext (d hd)
[GOAL]
case e_a.e_a.e_f
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ (fun b' x => a ♯ b ♯ b') = fun b' hb' => a ♯ (b ♯ b')
[PROOFSTEP]
ext (d hd)
[GOAL]
case e_a.e_f.h.h
a✝ b✝ c✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd : d < a
⊢ d ♯ b ♯ c = d ♯ (b ♯ c)
[PROOFSTEP]
apply nadd_assoc
[GOAL]
case e_a.e_a.e_f.h.h
a✝ b✝ c✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd : d < b
⊢ a ♯ d ♯ c = a ♯ (d ♯ c)
[PROOFSTEP]
apply nadd_assoc
[GOAL]
case e_a.e_a.e_f.h.h
a✝ b✝ c✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd : d < c
⊢ a ♯ b ♯ d = a ♯ (b ♯ d)
[PROOFSTEP]
apply nadd_assoc
[GOAL]
case hf
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ ∀ {i j : Ordinal.{u_1}}, i < b ♯ c → j < b ♯ c → i ≤ j → a ♯ i ≤ a ♯ j
[PROOFSTEP]
exact fun _ _ h => nadd_le_nadd_left h a
[GOAL]
case hf
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ ∀ {i j : Ordinal.{u_1}}, i < a ♯ b → j < a ♯ b → i ≤ j → i ♯ c ≤ j ♯ c
[PROOFSTEP]
exact fun _ _ h => nadd_le_nadd_right h c
[GOAL]
a b c : Ordinal.{u}
⊢ a ♯ 0 = a
[PROOFSTEP]
induction' a using Ordinal.induction with a IH
[GOAL]
case h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 0 = k
⊢ a ♯ 0 = a
[PROOFSTEP]
rw [nadd_def, blsub_zero, max_zero_right]
[GOAL]
case h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 0 = k
⊢ (blsub a fun a' x => a' ♯ 0) = a
[PROOFSTEP]
convert blsub_id a
[GOAL]
case h.e'_2.h.e'_2.h.h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 0 = k
x✝¹ : Ordinal.{u}
x✝ : x✝¹ < a
⊢ x✝¹ ♯ 0 = x✝¹
[PROOFSTEP]
rename_i hb
[GOAL]
case h.e'_2.h.e'_2.h.h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 0 = k
x✝ : Ordinal.{u}
hb : x✝ < a
⊢ x✝ ♯ 0 = x✝
[PROOFSTEP]
exact IH _ hb
[GOAL]
a b c : Ordinal.{u}
⊢ 0 ♯ a = a
[PROOFSTEP]
rw [nadd_comm, nadd_zero]
[GOAL]
a b c : Ordinal.{u}
⊢ a ♯ 1 = succ a
[PROOFSTEP]
induction' a using Ordinal.induction with a IH
[GOAL]
case h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 1 = succ k
⊢ a ♯ 1 = succ a
[PROOFSTEP]
rw [nadd_def, blsub_one, nadd_zero, max_eq_right_iff, blsub_le_iff]
[GOAL]
case h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 1 = succ k
⊢ ∀ (i : Ordinal.{u}), i < a → i ♯ 1 < succ a
[PROOFSTEP]
intro i hi
[GOAL]
case h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 1 = succ k
i : Ordinal.{u}
hi : i < a
⊢ i ♯ 1 < succ a
[PROOFSTEP]
rwa [IH i hi, succ_lt_succ_iff]
[GOAL]
a b c : Ordinal.{u}
⊢ 1 ♯ a = succ a
[PROOFSTEP]
rw [nadd_comm, nadd_one]
[GOAL]
a b c : Ordinal.{u}
⊢ a ♯ succ b = succ (a ♯ b)
[PROOFSTEP]
rw [← nadd_one (a ♯ b), nadd_assoc, nadd_one]
[GOAL]
a b c : Ordinal.{u}
⊢ succ a ♯ b = succ (a ♯ b)
[PROOFSTEP]
rw [← one_nadd (a ♯ b), ← nadd_assoc, one_nadd]
[GOAL]
a b c : Ordinal.{u}
n : ℕ
⊢ a ♯ ↑n = a + ↑n
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
a b c : Ordinal.{u}
⊢ a ♯ ↑Nat.zero = a + ↑Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
a b c : Ordinal.{u}
n : ℕ
hn : a ♯ ↑n = a + ↑n
⊢ a ♯ ↑(Nat.succ n) = a + ↑(Nat.succ n)
[PROOFSTEP]
rw [Nat.cast_succ, add_one_eq_succ, nadd_succ, add_succ, hn]
[GOAL]
a b c : Ordinal.{u}
n : ℕ
⊢ ↑n ♯ a = a + ↑n
[PROOFSTEP]
rw [nadd_comm, nadd_nat]
[GOAL]
a b c : Ordinal.{u}
⊢ a + b ≤ a ♯ b
[PROOFSTEP]
induction b using limitRecOn with
| H₁ => simp
| H₂ c h => rwa [add_succ, nadd_succ, succ_le_succ_iff]
| H₃ c hc H =>
  simp_rw [← IsNormal.blsub_eq.{u, u} (add_isNormal a) hc, blsub_le_iff]
  exact fun i hi => (H i hi).trans_lt (nadd_lt_nadd_left hi a)
[GOAL]
a b c : Ordinal.{u}
⊢ a + b ≤ a ♯ b
[PROOFSTEP]
induction b using limitRecOn with
| H₁ => simp
| H₂ c h => rwa [add_succ, nadd_succ, succ_le_succ_iff]
| H₃ c hc H =>
  simp_rw [← IsNormal.blsub_eq.{u, u} (add_isNormal a) hc, blsub_le_iff]
  exact fun i hi => (H i hi).trans_lt (nadd_lt_nadd_left hi a)
[GOAL]
case H₁
a b c : Ordinal.{u}
⊢ a + 0 ≤ a ♯ 0
[PROOFSTEP]

| H₁ => simp
[GOAL]
case H₁
a b c : Ordinal.{u}
⊢ a + 0 ≤ a ♯ 0
[PROOFSTEP]
simp
[GOAL]
case H₂
a b c✝ c : Ordinal.{u}
h : a + c ≤ a ♯ c
⊢ a + succ c ≤ a ♯ succ c
[PROOFSTEP]

| H₂ c h => rwa [add_succ, nadd_succ, succ_le_succ_iff]
[GOAL]
case H₂
a b c✝ c : Ordinal.{u}
h : a + c ≤ a ♯ c
⊢ a + succ c ≤ a ♯ succ c
[PROOFSTEP]
rwa [add_succ, nadd_succ, succ_le_succ_iff]
[GOAL]
case H₃
a b c✝ c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a + o' ≤ a ♯ o'
⊢ a + c ≤ a ♯ c
[PROOFSTEP]

| H₃ c hc H =>
  simp_rw [← IsNormal.blsub_eq.{u, u} (add_isNormal a) hc, blsub_le_iff]
  exact fun i hi => (H i hi).trans_lt (nadd_lt_nadd_left hi a)
[GOAL]
case H₃
a b c✝ c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a + o' ≤ a ♯ o'
⊢ a + c ≤ a ♯ c
[PROOFSTEP]
simp_rw [← IsNormal.blsub_eq.{u, u} (add_isNormal a) hc, blsub_le_iff]
[GOAL]
case H₃
a b c✝ c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a + o' ≤ a ♯ o'
⊢ ∀ (i : Ordinal.{u}), i < c → a + i < a ♯ c
[PROOFSTEP]
exact fun i hi => (H i hi).trans_lt (nadd_lt_nadd_left hi a)
[GOAL]
a b c : NatOrdinal
h : a + b ≤ a + c
⊢ b ≤ c
[PROOFSTEP]
by_contra' h'
[GOAL]
a b c : NatOrdinal
h : a + b ≤ a + c
h' : c < b
⊢ False
[PROOFSTEP]
exact h.not_lt (add_lt_add_left h' a)
[GOAL]
n : ℕ
⊢ ↑toOrdinal ↑n = ↑n
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
⊢ ↑toOrdinal ↑Nat.zero = ↑Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
n : ℕ
hn : ↑toOrdinal ↑n = ↑n
⊢ ↑toOrdinal ↑(Nat.succ n) = ↑(Nat.succ n)
[PROOFSTEP]
change (toOrdinal n) ♯ 1 = n + 1
[GOAL]
case succ
n : ℕ
hn : ↑toOrdinal ↑n = ↑n
⊢ ↑toOrdinal ↑n ♯ 1 = ↑n + 1
[PROOFSTEP]
rw [hn]
[GOAL]
case succ
n : ℕ
hn : ↑toOrdinal ↑n = ↑n
⊢ ↑n ♯ 1 = ↑n + 1
[PROOFSTEP]
exact nadd_one n
[GOAL]
n : ℕ
⊢ ↑toNatOrdinal ↑n = ↑n
[PROOFSTEP]
rw [← toOrdinal_cast_nat n]
[GOAL]
n : ℕ
⊢ ↑toNatOrdinal (↑toOrdinal ↑n) = ↑n
[PROOFSTEP]
rfl
[GOAL]
a b : Ordinal.{u_1}
⊢ a ≤ b ♯ a
[PROOFSTEP]
simpa using nadd_le_nadd_right (Ordinal.zero_le b) a
[GOAL]
a b : Ordinal.{u_1}
⊢ a ≤ a ♯ b
[PROOFSTEP]
simpa using nadd_le_nadd_left (Ordinal.zero_le b) a
[GOAL]
a✝ b✝ c d : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ a ⨳ b = sInf {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
[PROOFSTEP]
rw [nmul]
[GOAL]
a b c d a' b' : Ordinal.{u}
ha : a' < a
hb : b' < b
⊢ a' ⨳ b ♯ a ⨳ b' < a ⨳ b ♯ a' ⨳ b'
[PROOFSTEP]
rw [nmul_def a b]
[GOAL]
a b c d a' b' : Ordinal.{u}
ha : a' < a
hb : b' < b
⊢ a' ⨳ b ♯ a ⨳ b' <
    sInf {c | ∀ (a' : Ordinal.{u}), a' < a → ∀ (b' : Ordinal.{u}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} ♯ a' ⨳ b'
[PROOFSTEP]
exact csInf_mem (nmul_nonempty a b) a' ha b' hb
[GOAL]
a b c d a' b' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
⊢ a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'
[PROOFSTEP]
rcases lt_or_eq_of_le ha with (ha | rfl)
[GOAL]
case inl
a b c d a' b' : Ordinal.{u}
ha✝ : a' ≤ a
hb : b' ≤ b
ha : a' < a
⊢ a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'
[PROOFSTEP]
rcases lt_or_eq_of_le hb with (hb | rfl)
[GOAL]
case inl.inl
a b c d a' b' : Ordinal.{u}
ha✝ : a' ≤ a
hb✝ : b' ≤ b
ha : a' < a
hb : b' < b
⊢ a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'
[PROOFSTEP]
exact (nmul_nadd_lt ha hb).le
[GOAL]
case inl.inr
a c d a' b' : Ordinal.{u}
ha✝ : a' ≤ a
ha : a' < a
hb : b' ≤ b'
⊢ a' ⨳ b' ♯ a ⨳ b' ≤ a ⨳ b' ♯ a' ⨳ b'
[PROOFSTEP]
rw [nadd_comm]
[GOAL]
case inr
b c d a' b' : Ordinal.{u}
hb : b' ≤ b
ha : a' ≤ a'
⊢ a' ⨳ b ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a' ⨳ b'
[PROOFSTEP]
exact le_rfl
[GOAL]
a b c d : Ordinal.{u}
⊢ c < a ⨳ b ↔ ∃ a', a' < a ∧ ∃ b', b' < b ∧ c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
a b c d : Ordinal.{u}
h : c < a ⨳ b
⊢ ∃ a', a' < a ∧ ∃ b', b' < b ∧ c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
[PROOFSTEP]
rw [nmul] at h
[GOAL]
case refine'_1
a b c d : Ordinal.{u}
h : c < sInf {c | ∀ (a' : Ordinal.{u}), a' < a → ∀ (b' : Ordinal.{u}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
⊢ ∃ a', a' < a ∧ ∃ b', b' < b ∧ c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
[PROOFSTEP]
simpa using not_mem_of_lt_csInf h ⟨0, fun _ _ => bot_le⟩
[GOAL]
case refine'_2
a b c d : Ordinal.{u}
⊢ (∃ a', a' < a ∧ ∃ b', b' < b ∧ c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b') → c < a ⨳ b
[PROOFSTEP]
rintro ⟨a', ha, b', hb, h⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
a b c d a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
h : c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
⊢ c < a ⨳ b
[PROOFSTEP]
have := h.trans_lt (nmul_nadd_lt ha hb)
[GOAL]
case refine'_2.intro.intro.intro.intro
a b c d a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
h : c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this : c ♯ a' ⨳ b' < a ⨳ b ♯ a' ⨳ b'
⊢ c < a ⨳ b
[PROOFSTEP]
rwa [nadd_lt_nadd_iff_right] at this
[GOAL]
a b c d : Ordinal.{u}
⊢ a ⨳ b ≤ c ↔ ∀ (a' : Ordinal.{u}), a' < a → ∀ (b' : Ordinal.{u}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
a b c d : Ordinal.{u}
⊢ ¬a ⨳ b ≤ c ↔ ¬∀ (a' : Ordinal.{u}), a' < a → ∀ (b' : Ordinal.{u}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'
[PROOFSTEP]
simp [lt_nmul_iff]
[GOAL]
a✝ b✝ c d : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ a ⨳ b = b ⨳ a
[PROOFSTEP]
rw [nmul, nmul]
[GOAL]
a✝ b✝ c d : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ sInf {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} =
    sInf {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
[PROOFSTEP]
congr
[GOAL]
case e_a
a✝ b✝ c d : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} =
    {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
[PROOFSTEP]
ext x
[GOAL]
case e_a.h
a✝ b✝ c d : Ordinal.{u}
a b x : Ordinal.{u_1}
⊢ x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} ↔
    x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
[PROOFSTEP]
constructor
[GOAL]
case e_a.h.mp
a✝ b✝ c d : Ordinal.{u}
a b x : Ordinal.{u_1}
⊢ x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} →
    x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
[PROOFSTEP]
intro H c hc d hd
[GOAL]
case e_a.h.mpr
a✝ b✝ c d : Ordinal.{u}
a b x : Ordinal.{u_1}
⊢ x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'} →
    x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
[PROOFSTEP]
intro H c hc d hd
[GOAL]
case e_a.h.mp
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < b
d : Ordinal.{u_1}
hd : d < a
⊢ c ⨳ a ♯ b ⨳ d < x ♯ c ⨳ d
[PROOFSTEP]
rw [nadd_comm, ← nmul_comm d b, ← nmul_comm a c, ← nmul_comm d]
[GOAL]
case e_a.h.mp
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < b
d : Ordinal.{u_1}
hd : d < a
⊢ d ⨳ b ♯ a ⨳ c < x ♯ d ⨳ c
[PROOFSTEP]
exact H _ hd _ hc
[GOAL]
case e_a.h.mpr
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
⊢ c ⨳ b ♯ a ⨳ d < x ♯ c ⨳ d
[PROOFSTEP]
rw [nadd_comm, nmul_comm a d, nmul_comm c, nmul_comm c]
[GOAL]
case e_a.h.mpr
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
⊢ d ⨳ a ♯ b ⨳ c < x ♯ d ⨳ c
[PROOFSTEP]
exact H _ hd _ hc
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ a ⨳ 0 = 0
[PROOFSTEP]
rw [← Ordinal.le_zero, nmul_le_iff]
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < 0 → a' ⨳ 0 ♯ a ⨳ b' < 0 ♯ a' ⨳ b'
[PROOFSTEP]
exact fun _ _ a ha => (Ordinal.not_lt_zero a ha).elim
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ 0 ⨳ a = 0
[PROOFSTEP]
rw [nmul_comm, nmul_zero]
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ a ⨳ 1 = a
[PROOFSTEP]
rw [nmul]
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ sInf {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < 1 → a' ⨳ 1 ♯ a ⨳ b' < c ♯ a' ⨳ b'} = a
[PROOFSTEP]
simp only [lt_one_iff_zero, forall_eq, nmul_zero, nadd_zero]
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ sInf {c | ∀ (a' : Ordinal.{u_1}), a' < a → a' ⨳ 1 < c} = a
[PROOFSTEP]
convert csInf_Ici (α := Ordinal)
[GOAL]
case h.e'_2.h.e'_3
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ {c | ∀ (a' : Ordinal.{u_1}), a' < a → a' ⨳ 1 < c} = Set.Ici a
[PROOFSTEP]
ext b
[GOAL]
case h.e'_2.h.e'_3.h
a✝ b✝ c d : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ b ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < a → a' ⨳ 1 < c} ↔ b ∈ Set.Ici a
[PROOFSTEP]
simp only [Set.mem_setOf_eq, Set.mem_Ici]
[GOAL]
case h.e'_2.h.e'_3.h
a✝ b✝ c d : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ (∀ (a' : Ordinal.{u_1}), a' < a → a' ⨳ 1 < b) ↔ a ≤ b
[PROOFSTEP]
refine'
  ⟨fun H => le_of_forall_lt fun c hc => _, fun ha c hc => _⟩
    -- Porting note: had to add arguments to `nmul_one` in the next two lines
      -- for the termination checker.
[GOAL]
case h.e'_2.h.e'_3.h.refine'_1
a✝ b✝ c✝ d : Ordinal.{u}
a b : Ordinal.{u_1}
H : ∀ (a' : Ordinal.{u_1}), a' < a → a' ⨳ 1 < b
c : Ordinal.{u_1}
hc : c < a
⊢ c < b
[PROOFSTEP]
simpa only [nmul_one c] using H c hc
[GOAL]
case h.e'_2.h.e'_3.h.refine'_2
a✝ b✝ c✝ d : Ordinal.{u}
a b : Ordinal.{u_1}
ha : a ≤ b
c : Ordinal.{u_1}
hc : c < a
⊢ c ⨳ 1 < b
[PROOFSTEP]
simpa only [nmul_one c] using hc.trans_le ha
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ 1 ⨳ a = a
[PROOFSTEP]
rw [nmul_comm, nmul_one]
[GOAL]
a b c d : Ordinal.{u}
h₁ : a < b
h₂ : 0 < c
⊢ c ⨳ a ♯ 0 ⨳ a ≤ 0 ⨳ b ♯ c ⨳ a
[PROOFSTEP]
simp
[GOAL]
a b c d : Ordinal.{u}
h₁ : a < b
h₂ : 0 < c
⊢ a ⨳ c ♯ a ⨳ 0 ≤ a ⨳ c ♯ b ⨳ 0
[PROOFSTEP]
simp
[GOAL]
a b c d : Ordinal.{u}
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ c ⨳ a ≤ c ⨳ b
[PROOFSTEP]
rcases lt_or_eq_of_le h₁ with (h₁ | rfl)
[GOAL]
case inl
a b c d : Ordinal.{u}
h₁✝ : a ≤ b
h₂ : 0 ≤ c
h₁ : a < b
⊢ c ⨳ a ≤ c ⨳ b
[PROOFSTEP]
rcases lt_or_eq_of_le h₂ with (h₂ | rfl)
[GOAL]
case inr
a c d : Ordinal.{u}
h₂ : 0 ≤ c
h₁ : a ≤ a
⊢ c ⨳ a ≤ c ⨳ a
[PROOFSTEP]
rcases lt_or_eq_of_le h₂ with (h₂ | rfl)
[GOAL]
case inl.inl
a b c d : Ordinal.{u}
h₁✝ : a ≤ b
h₂✝ : 0 ≤ c
h₁ : a < b
h₂ : 0 < c
⊢ c ⨳ a ≤ c ⨳ b
[PROOFSTEP]
exact (nmul_lt_nmul_of_pos_left h₁ h₂).le
[GOAL]
case inl.inr
a b d : Ordinal.{u}
h₁✝ : a ≤ b
h₁ : a < b
h₂ : 0 ≤ 0
⊢ 0 ⨳ a ≤ 0 ⨳ b
case inr.inl
a c d : Ordinal.{u}
h₂✝ : 0 ≤ c
h₁ : a ≤ a
h₂ : 0 < c
⊢ c ⨳ a ≤ c ⨳ a
case inr.inr a d : Ordinal.{u} h₁ : a ≤ a h₂ : 0 ≤ 0 ⊢ 0 ⨳ a ≤ 0 ⨳ a
[PROOFSTEP]
all_goals simp
[GOAL]
case inl.inr
a b d : Ordinal.{u}
h₁✝ : a ≤ b
h₁ : a < b
h₂ : 0 ≤ 0
⊢ 0 ⨳ a ≤ 0 ⨳ b
[PROOFSTEP]
simp
[GOAL]
case inr.inl
a c d : Ordinal.{u}
h₂✝ : 0 ≤ c
h₁ : a ≤ a
h₂ : 0 < c
⊢ c ⨳ a ≤ c ⨳ a
[PROOFSTEP]
simp
[GOAL]
case inr.inr
a d : Ordinal.{u}
h₁ : a ≤ a
h₂ : 0 ≤ 0
⊢ 0 ⨳ a ≤ 0 ⨳ a
[PROOFSTEP]
simp
[GOAL]
a b c d : Ordinal.{u}
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ a ⨳ c ≤ b ⨳ c
[PROOFSTEP]
rw [nmul_comm, nmul_comm b]
[GOAL]
a b c d : Ordinal.{u}
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ c ⨳ a ≤ c ⨳ b
[PROOFSTEP]
exact nmul_le_nmul_of_nonneg_left h₁ h₂
[GOAL]
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ a ⨳ (b ♯ c) = a ⨳ b ♯ a ⨳ c
[PROOFSTEP]
refine le_antisymm (nmul_le_iff.2 fun a' ha d hd => ?_) (nadd_le_iff.2 ⟨fun d hd => ?_, fun d hd => ?_⟩)
[GOAL]
case refine_1
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd : d < b ♯ c
⊢ a' ⨳ (b ♯ c) ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d
[PROOFSTEP]
rw [nmul_nadd a' b c]
[GOAL]
case refine_1
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd : d < b ♯ c
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d
[PROOFSTEP]
rcases lt_nadd_iff.1 hd with (⟨b', hb, hd⟩ | ⟨c', hc, hd⟩)
[GOAL]
case refine_1.inl.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
b' : Ordinal.{u_1}
hb : b' < b
hd : d ≤ b' ♯ c
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d
[PROOFSTEP]
have :=
  nadd_lt_nadd_of_lt_of_le (nmul_nadd_lt ha hb)
    (nmul_nadd_le ha.le hd)
      -- Porting note: adding arguments to `nmul_nadd` for the termination checker.
[GOAL]
case refine_1.inl.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
b' : Ordinal.{u_1}
hb : b' < b
hd : d ≤ b' ♯ c
this : a' ⨳ b ♯ a ⨳ b' ♯ (a' ⨳ (b' ♯ c) ♯ a ⨳ d) < a ⨳ b ♯ a' ⨳ b' ♯ (a ⨳ (b' ♯ c) ♯ a' ⨳ d)
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d
[PROOFSTEP]
rw [nmul_nadd a' b' c, nmul_nadd a b' c] at this
[GOAL]
case refine_1.inl.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
b' : Ordinal.{u_1}
hb : b' < b
hd : d ≤ b' ♯ c
this : a' ⨳ b ♯ a ⨳ b' ♯ (a' ⨳ b' ♯ a' ⨳ c ♯ a ⨳ d) < a ⨳ b ♯ a' ⨳ b' ♯ (a ⨳ b' ♯ a ⨳ c ♯ a' ⨳ d)
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d
[PROOFSTEP]
simp only [nadd_assoc] at this
[GOAL]
case refine_1.inl.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
b' : Ordinal.{u_1}
hb : b' < b
hd : d ≤ b' ♯ c
this : a' ⨳ b ♯ (a ⨳ b' ♯ (a' ⨳ b' ♯ (a' ⨳ c ♯ a ⨳ d))) < a ⨳ b ♯ (a' ⨳ b' ♯ (a ⨳ b' ♯ (a ⨳ c ♯ a' ⨳ d)))
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d
[PROOFSTEP]
rwa [nadd_left_comm, nadd_left_comm _ (a ⨳ b'), nadd_left_comm (a ⨳ b), nadd_lt_nadd_iff_left, nadd_left_comm (a' ⨳ b),
  nadd_left_comm (a ⨳ b), nadd_lt_nadd_iff_left, ← nadd_assoc, ← nadd_assoc] at this
[GOAL]
case refine_1.inr.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
c' : Ordinal.{u_1}
hc : c' < c
hd : d ≤ b ♯ c'
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d
[PROOFSTEP]
have :=
  nadd_lt_nadd_of_le_of_lt (nmul_nadd_le ha.le hd)
    (nmul_nadd_lt ha hc)
      -- Porting note: adding arguments to `nmul_nadd` for the termination checker.
[GOAL]
case refine_1.inr.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
c' : Ordinal.{u_1}
hc : c' < c
hd : d ≤ b ♯ c'
this : a' ⨳ (b ♯ c') ♯ a ⨳ d ♯ (a' ⨳ c ♯ a ⨳ c') < a ⨳ (b ♯ c') ♯ a' ⨳ d ♯ (a ⨳ c ♯ a' ⨳ c')
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d
[PROOFSTEP]
rw [nmul_nadd a' b c', nmul_nadd a b c'] at this
[GOAL]
case refine_1.inr.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
c' : Ordinal.{u_1}
hc : c' < c
hd : d ≤ b ♯ c'
this : a' ⨳ b ♯ a' ⨳ c' ♯ a ⨳ d ♯ (a' ⨳ c ♯ a ⨳ c') < a ⨳ b ♯ a ⨳ c' ♯ a' ⨳ d ♯ (a ⨳ c ♯ a' ⨳ c')
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d
[PROOFSTEP]
simp only [nadd_assoc] at this
[GOAL]
case refine_1.inr.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
c' : Ordinal.{u_1}
hc : c' < c
hd : d ≤ b ♯ c'
this : a' ⨳ b ♯ (a' ⨳ c' ♯ (a ⨳ d ♯ (a' ⨳ c ♯ a ⨳ c'))) < a ⨳ b ♯ (a ⨳ c' ♯ (a' ⨳ d ♯ (a ⨳ c ♯ a' ⨳ c')))
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d
[PROOFSTEP]
rwa [nadd_left_comm, nadd_comm (a ⨳ c), nadd_left_comm (a' ⨳ d), nadd_left_comm (a ⨳ c'), nadd_left_comm (a ⨳ b),
  nadd_lt_nadd_iff_left, nadd_comm (a' ⨳ c), nadd_left_comm (a ⨳ d), nadd_left_comm (a' ⨳ b), nadd_left_comm (a ⨳ b),
  nadd_lt_nadd_iff_left, nadd_comm (a ⨳ d), nadd_comm (a' ⨳ d), ← nadd_assoc, ← nadd_assoc] at this
[GOAL]
case refine_2
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd : d < a ⨳ b
⊢ d ♯ a ⨳ c < a ⨳ (b ♯ c)
[PROOFSTEP]
rcases lt_nmul_iff.1 hd with ⟨a', ha, b', hb, hd⟩
[GOAL]
case refine_2.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ b
a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
hd : d ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
⊢ d ♯ a ⨳ c < a ⨳ (b ♯ c)
[PROOFSTEP]
have :=
  nadd_lt_nadd_of_le_of_lt hd
    (nmul_nadd_lt ha (nadd_lt_nadd_right hb c))
      -- Porting note: adding arguments to `nmul_nadd` for the termination checker.
[GOAL]
case refine_2.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ b
a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
hd : d ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this : d ♯ a' ⨳ b' ♯ (a' ⨳ (b ♯ c) ♯ a ⨳ (b' ♯ c)) < a' ⨳ b ♯ a ⨳ b' ♯ (a ⨳ (b ♯ c) ♯ a' ⨳ (b' ♯ c))
⊢ d ♯ a ⨳ c < a ⨳ (b ♯ c)
[PROOFSTEP]
rw [nmul_nadd a' b c, nmul_nadd a b' c, nmul_nadd a'] at this
[GOAL]
case refine_2.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ b
a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
hd : d ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this : d ♯ a' ⨳ b' ♯ (a' ⨳ b ♯ a' ⨳ c ♯ (a ⨳ b' ♯ a ⨳ c)) < a' ⨳ b ♯ a ⨳ b' ♯ (a ⨳ (b ♯ c) ♯ (a' ⨳ b' ♯ a' ⨳ c))
⊢ d ♯ a ⨳ c < a ⨳ (b ♯ c)
[PROOFSTEP]
simp only [nadd_assoc] at this
[GOAL]
case refine_2.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ b
a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
hd : d ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this : d ♯ (a' ⨳ b' ♯ (a' ⨳ b ♯ (a' ⨳ c ♯ (a ⨳ b' ♯ a ⨳ c)))) < a' ⨳ b ♯ (a ⨳ b' ♯ (a ⨳ (b ♯ c) ♯ (a' ⨳ b' ♯ a' ⨳ c)))
⊢ d ♯ a ⨳ c < a ⨳ (b ♯ c)
[PROOFSTEP]
rwa [nadd_left_comm (a' ⨳ b'), nadd_left_comm, nadd_lt_nadd_iff_left, nadd_left_comm, nadd_left_comm _ (a' ⨳ b'),
  nadd_left_comm (a ⨳ b'), nadd_lt_nadd_iff_left, nadd_left_comm (a' ⨳ c), nadd_left_comm, nadd_lt_nadd_iff_left,
  nadd_left_comm, nadd_comm _ (a' ⨳ c), nadd_lt_nadd_iff_left] at this
[GOAL]
case refine_3
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd : d < a ⨳ c
⊢ a ⨳ b ♯ d < a ⨳ (b ♯ c)
[PROOFSTEP]
rcases lt_nmul_iff.1 hd with ⟨a', ha, c', hc, hd⟩
[GOAL]
case refine_3.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ c
a' : Ordinal.{u_1}
ha : a' < a
c' : Ordinal.{u_1}
hc : c' < c
hd : d ♯ a' ⨳ c' ≤ a' ⨳ c ♯ a ⨳ c'
⊢ a ⨳ b ♯ d < a ⨳ (b ♯ c)
[PROOFSTEP]
have := nadd_lt_nadd_of_lt_of_le (nmul_nadd_lt ha (nadd_lt_nadd_left hc b)) hd
[GOAL]
case refine_3.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ c
a' : Ordinal.{u_1}
ha : a' < a
c' : Ordinal.{u_1}
hc : c' < c
hd : d ♯ a' ⨳ c' ≤ a' ⨳ c ♯ a ⨳ c'
this : a' ⨳ (b ♯ c) ♯ a ⨳ (b ♯ c') ♯ (d ♯ a' ⨳ c') < a ⨳ (b ♯ c) ♯ a' ⨳ (b ♯ c') ♯ (a' ⨳ c ♯ a ⨳ c')
⊢ a ⨳ b ♯ d < a ⨳ (b ♯ c)
[PROOFSTEP]
rw [nmul_nadd a' b c, nmul_nadd a b c', nmul_nadd a'] at this
[GOAL]
case refine_3.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ c
a' : Ordinal.{u_1}
ha : a' < a
c' : Ordinal.{u_1}
hc : c' < c
hd : d ♯ a' ⨳ c' ≤ a' ⨳ c ♯ a ⨳ c'
this : a' ⨳ b ♯ a' ⨳ c ♯ (a ⨳ b ♯ a ⨳ c') ♯ (d ♯ a' ⨳ c') < a ⨳ (b ♯ c) ♯ (a' ⨳ b ♯ a' ⨳ c') ♯ (a' ⨳ c ♯ a ⨳ c')
⊢ a ⨳ b ♯ d < a ⨳ (b ♯ c)
[PROOFSTEP]
simp only [nadd_assoc] at this
[GOAL]
case refine_3.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ c
a' : Ordinal.{u_1}
ha : a' < a
c' : Ordinal.{u_1}
hc : c' < c
hd : d ♯ a' ⨳ c' ≤ a' ⨳ c ♯ a ⨳ c'
this : a' ⨳ b ♯ (a' ⨳ c ♯ (a ⨳ b ♯ (a ⨳ c' ♯ (d ♯ a' ⨳ c')))) < a ⨳ (b ♯ c) ♯ (a' ⨳ b ♯ (a' ⨳ c' ♯ (a' ⨳ c ♯ a ⨳ c')))
⊢ a ⨳ b ♯ d < a ⨳ (b ♯ c)
[PROOFSTEP]
rwa [nadd_left_comm _ (a' ⨳ b), nadd_lt_nadd_iff_left, nadd_left_comm (a' ⨳ c'), nadd_left_comm _ (a' ⨳ c),
  nadd_lt_nadd_iff_left, nadd_left_comm, nadd_comm (a' ⨳ c'), nadd_left_comm _ (a ⨳ c'), nadd_lt_nadd_iff_left,
  nadd_comm _ (a' ⨳ c'), nadd_comm _ (a' ⨳ c'), nadd_left_comm, nadd_lt_nadd_iff_left] at this
[GOAL]
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ (a ♯ b) ⨳ c = a ⨳ c ♯ b ⨳ c
[PROOFSTEP]
rw [nmul_comm, nmul_nadd, nmul_comm, nmul_comm c]
[GOAL]
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
[PROOFSTEP]
simpa only [nadd_nmul, ← nadd_assoc] using nmul_nadd_lt (nmul_nadd_lt ha hb) hc
[GOAL]
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' ≤ a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
[PROOFSTEP]
simpa only [nadd_nmul, ← nadd_assoc] using nmul_nadd_le (nmul_nadd_le ha hb) hc
[GOAL]
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
    a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
[PROOFSTEP]
simp only [nmul_comm _ (_ ⨳ _)]
[GOAL]
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' < b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a
[PROOFSTEP]
convert nmul_nadd_lt₃ hb hc ha using 1
[GOAL]
case h.e'_3
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' = b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b ⨳ c ⨳ a' ♯ b' ⨳ c' ⨳ a'
[PROOFSTEP]
simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]
[GOAL]
case h.e'_3
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a')) =
    ↑toOrdinal
      (↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
abel_nf
[GOAL]
case h.e'_4
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a = b ⨳ c ⨳ a ♯ b' ⨳ c' ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a'
[PROOFSTEP]
simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]
[GOAL]
case h.e'_4
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a)) =
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a) + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') +
        ↑toNatOrdinal (b ⨳ c' ⨳ a'))
[PROOFSTEP]
abel_nf
[GOAL]
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') ≤
    a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
[PROOFSTEP]
simp only [nmul_comm _ (_ ⨳ _)]
[GOAL]
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' ≤ b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a
[PROOFSTEP]
convert nmul_nadd_le₃ hb hc ha using 1
[GOAL]
case h.e'_3
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' = b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b ⨳ c ⨳ a' ♯ b' ⨳ c' ⨳ a'
[PROOFSTEP]
simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]
[GOAL]
case h.e'_3
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a')) =
    ↑toOrdinal
      (↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
abel_nf
[GOAL]
case h.e'_4
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a = b ⨳ c ⨳ a ♯ b' ⨳ c' ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a'
[PROOFSTEP]
simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]
[GOAL]
case h.e'_4
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a)) =
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a) + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') +
        ↑toNatOrdinal (b ⨳ c' ⨳ a'))
[PROOFSTEP]
abel_nf
[GOAL]
a b c d : Ordinal.{u}
⊢ d < a ⨳ b ⨳ c ↔
    ∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
constructor
[GOAL]
case mp
a b c d : Ordinal.{u}
⊢ d < a ⨳ b ⨳ c →
    ∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
intro h
[GOAL]
case mp
a b c d : Ordinal.{u}
h : d < a ⨳ b ⨳ c
⊢ ∃ a',
    a' < a ∧
      ∃ b',
        b' < b ∧
          ∃ c',
            c' < c ∧ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
rcases lt_nmul_iff.1 h with ⟨e, he, c', hc, H₁⟩
[GOAL]
case mp.intro.intro.intro.intro
a b c d : Ordinal.{u}
h : d < a ⨳ b ⨳ c
e : Ordinal.{u}
he : e < a ⨳ b
c' : Ordinal.{u}
hc : c' < c
H₁ : d ♯ e ⨳ c' ≤ e ⨳ c ♯ a ⨳ b ⨳ c'
⊢ ∃ a',
    a' < a ∧
      ∃ b',
        b' < b ∧
          ∃ c',
            c' < c ∧ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
rcases lt_nmul_iff.1 he with ⟨a', ha, b', hb, H₂⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro.intro
a b c d : Ordinal.{u}
h : d < a ⨳ b ⨳ c
e : Ordinal.{u}
he : e < a ⨳ b
c' : Ordinal.{u}
hc : c' < c
H₁ : d ♯ e ⨳ c' ≤ e ⨳ c ♯ a ⨳ b ⨳ c'
a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
H₂ : e ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
⊢ ∃ a',
    a' < a ∧
      ∃ b',
        b' < b ∧
          ∃ c',
            c' < c ∧ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
refine' ⟨a', ha, b', hb, c', hc, _⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro.intro
a b c d : Ordinal.{u}
h : d < a ⨳ b ⨳ c
e : Ordinal.{u}
he : e < a ⨳ b
c' : Ordinal.{u}
hc : c' < c
H₁ : d ♯ e ⨳ c' ≤ e ⨳ c ♯ a ⨳ b ⨳ c'
a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
H₂ : e ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
⊢ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
have := nadd_le_nadd H₁ (nmul_nadd_le H₂ hc.le)
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro.intro
a b c d : Ordinal.{u}
h : d < a ⨳ b ⨳ c
e : Ordinal.{u}
he : e < a ⨳ b
c' : Ordinal.{u}
hc : c' < c
H₁ : d ♯ e ⨳ c' ≤ e ⨳ c ♯ a ⨳ b ⨳ c'
a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
H₂ : e ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this :
  d ♯ e ⨳ c' ♯ ((e ♯ a' ⨳ b') ⨳ c ♯ (a' ⨳ b ♯ a ⨳ b') ⨳ c') ≤
    e ⨳ c ♯ a ⨳ b ⨳ c' ♯ ((a' ⨳ b ♯ a ⨳ b') ⨳ c ♯ (e ♯ a' ⨳ b') ⨳ c')
⊢ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
simp only [nadd_nmul, nadd_assoc] at this
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro.intro
a b c d : Ordinal.{u}
h : d < a ⨳ b ⨳ c
e : Ordinal.{u}
he : e < a ⨳ b
c' : Ordinal.{u}
hc : c' < c
H₁ : d ♯ e ⨳ c' ≤ e ⨳ c ♯ a ⨳ b ⨳ c'
a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
H₂ : e ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this :
  d ♯ (e ⨳ c' ♯ (e ⨳ c ♯ (a' ⨳ b' ⨳ c ♯ (a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c')))) ≤
    e ⨳ c ♯ (a ⨳ b ⨳ c' ♯ (a' ⨳ b ⨳ c ♯ (a ⨳ b' ⨳ c ♯ (e ⨳ c' ♯ a' ⨳ b' ⨳ c'))))
⊢ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
rw [nadd_left_comm, nadd_left_comm d, nadd_left_comm, nadd_le_nadd_iff_left, nadd_left_comm (a ⨳ b' ⨳ c),
  nadd_left_comm (a' ⨳ b ⨳ c), nadd_left_comm (a ⨳ b ⨳ c'), nadd_le_nadd_iff_left, nadd_left_comm (a ⨳ b ⨳ c'),
  nadd_left_comm (a ⨳ b ⨳ c')] at this
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro.intro
a b c d : Ordinal.{u}
h : d < a ⨳ b ⨳ c
e : Ordinal.{u}
he : e < a ⨳ b
c' : Ordinal.{u}
hc : c' < c
H₁ : d ♯ e ⨳ c' ≤ e ⨳ c ♯ a ⨳ b ⨳ c'
a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
H₂ : e ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this : d ♯ (a' ⨳ b' ⨳ c ♯ (a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c')) ≤ a' ⨳ b ⨳ c ♯ (a ⨳ b' ⨳ c ♯ (a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'))
⊢ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
simpa only [nadd_assoc]
[GOAL]
case mpr
a b c d : Ordinal.{u}
⊢ (∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧
                d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c') →
    d < a ⨳ b ⨳ c
[PROOFSTEP]
rintro ⟨a', ha, b', hb, c', hc, h⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
h : d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
⊢ d < a ⨳ b ⨳ c
[PROOFSTEP]
have := h.trans_lt (nmul_nadd_lt₃ ha hb hc)
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
h : d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
this : d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
⊢ d < a ⨳ b ⨳ c
[PROOFSTEP]
repeat' rw [nadd_lt_nadd_iff_right] at this
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
h : d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
this : d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
⊢ d < a ⨳ b ⨳ c
[PROOFSTEP]
rw [nadd_lt_nadd_iff_right] at this
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
h : d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
this : d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c'
⊢ d < a ⨳ b ⨳ c
[PROOFSTEP]
rw [nadd_lt_nadd_iff_right] at this
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
h : d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
this : d ♯ a' ⨳ b' ⨳ c < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c
⊢ d < a ⨳ b ⨳ c
[PROOFSTEP]
rw [nadd_lt_nadd_iff_right] at this
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
h : d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
this : d < a ⨳ b ⨳ c
⊢ d < a ⨳ b ⨳ c
[PROOFSTEP]
rw [nadd_lt_nadd_iff_right] at this
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
h : d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
this : d < a ⨳ b ⨳ c
⊢ d < a ⨳ b ⨳ c
[PROOFSTEP]
assumption
[GOAL]
a b c d : Ordinal.{u}
⊢ a ⨳ b ⨳ c ≤ d ↔
    ∀ (a' : Ordinal.{u}),
      a' < a →
        ∀ (b' : Ordinal.{u}),
          b' < b →
            ∀ (c' : Ordinal.{u}),
              c' < c → a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
a b c d : Ordinal.{u}
⊢ ¬a ⨳ b ⨳ c ≤ d ↔
    ¬∀ (a' : Ordinal.{u}),
        a' < a →
          ∀ (b' : Ordinal.{u}),
            b' < b →
              ∀ (c' : Ordinal.{u}),
                c' < c →
                  a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
[PROOFSTEP]
simp [lt_nmul_iff₃]
[GOAL]
a b c d : Ordinal.{u}
⊢ d < a ⨳ (b ⨳ c) ↔
    ∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧
                d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c') ≤
                  a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c')
[PROOFSTEP]
simp only [nmul_comm _ (_ ⨳ _), lt_nmul_iff₃, nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]
[GOAL]
a b c d : Ordinal.{u}
⊢ (∃ a',
      a' < b ∧
        ∃ b',
          b' < c ∧
            ∃ c',
              c' < a ∧
                ↑toOrdinal
                    (↑toNatOrdinal d + ↑toNatOrdinal (a' ⨳ b' ⨳ a) + ↑toNatOrdinal (a' ⨳ c ⨳ c') +
                      ↑toNatOrdinal (b ⨳ b' ⨳ c')) ≤
                  ↑toOrdinal
                    (↑toNatOrdinal (a' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ b' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ c') +
                      ↑toNatOrdinal (a' ⨳ b' ⨳ c'))) ↔
    ∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧
                ↑toOrdinal
                    (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') +
                      ↑toNatOrdinal (b' ⨳ c' ⨳ a)) ≤
                  ↑toOrdinal
                    (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
                      ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
constructor
[GOAL]
case mp
a b c d : Ordinal.{u}
⊢ (∃ a',
      a' < b ∧
        ∃ b',
          b' < c ∧
            ∃ c',
              c' < a ∧
                ↑toOrdinal
                    (↑toNatOrdinal d + ↑toNatOrdinal (a' ⨳ b' ⨳ a) + ↑toNatOrdinal (a' ⨳ c ⨳ c') +
                      ↑toNatOrdinal (b ⨳ b' ⨳ c')) ≤
                  ↑toOrdinal
                    (↑toNatOrdinal (a' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ b' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ c') +
                      ↑toNatOrdinal (a' ⨳ b' ⨳ c'))) →
    ∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧
                ↑toOrdinal
                    (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') +
                      ↑toNatOrdinal (b' ⨳ c' ⨳ a)) ≤
                  ↑toOrdinal
                    (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
                      ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
rintro ⟨b', hb, c', hc, a', ha, h⟩
[GOAL]
case mpr
a b c d : Ordinal.{u}
⊢ (∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧
                ↑toOrdinal
                    (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') +
                      ↑toNatOrdinal (b' ⨳ c' ⨳ a)) ≤
                  ↑toOrdinal
                    (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
                      ↑toNatOrdinal (b' ⨳ c' ⨳ a'))) →
    ∃ a',
      a' < b ∧
        ∃ b',
          b' < c ∧
            ∃ c',
              c' < a ∧
                ↑toOrdinal
                    (↑toNatOrdinal d + ↑toNatOrdinal (a' ⨳ b' ⨳ a) + ↑toNatOrdinal (a' ⨳ c ⨳ c') +
                      ↑toNatOrdinal (b ⨳ b' ⨳ c')) ≤
                  ↑toOrdinal
                    (↑toNatOrdinal (a' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ b' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ c') +
                      ↑toNatOrdinal (a' ⨳ b' ⨳ c'))
[PROOFSTEP]
rintro ⟨b', hb, c', hc, a', ha, h⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro
a b c d b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
a' : Ordinal.{u}
ha : a' < a
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a')) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
⊢ ∃ a',
    a' < a ∧
      ∃ b',
        b' < b ∧
          ∃ c',
            c' < c ∧
              ↑toOrdinal
                  (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') +
                    ↑toNatOrdinal (b' ⨳ c' ⨳ a)) ≤
                ↑toOrdinal
                  (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
                    ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
use a', ha, b', hb, c', hc
[GOAL]
case right
a b c d b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
a' : Ordinal.{u}
ha : a' < a
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a')) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
⊢ ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') + ↑toNatOrdinal (b' ⨳ c' ⨳ a)) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
convert h using 1
[GOAL]
case h.e'_3
a b c d b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
a' : Ordinal.{u}
ha : a' < a
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a')) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
⊢ ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') + ↑toNatOrdinal (b' ⨳ c' ⨳ a)) =
    ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a'))
[PROOFSTEP]
abel_nf
[GOAL]
case h.e'_4
a b c d b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
a' : Ordinal.{u}
ha : a' < a
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a')) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
⊢ ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a')) =
    ↑toOrdinal
      (↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
abel_nf
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d b' : Ordinal.{u}
hb : b' < a
c' : Ordinal.{u}
hc : c' < b
a' : Ordinal.{u}
ha : a' < c
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b') + ↑toNatOrdinal (c' ⨳ a' ⨳ a)) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ b') + ↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b'))
⊢ ∃ a',
    a' < b ∧
      ∃ b',
        b' < c ∧
          ∃ c',
            c' < a ∧
              ↑toOrdinal
                  (↑toNatOrdinal d + ↑toNatOrdinal (a' ⨳ b' ⨳ a) + ↑toNatOrdinal (a' ⨳ c ⨳ c') +
                    ↑toNatOrdinal (b ⨳ b' ⨳ c')) ≤
                ↑toOrdinal
                  (↑toNatOrdinal (a' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ b' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ c') +
                    ↑toNatOrdinal (a' ⨳ b' ⨳ c'))
[PROOFSTEP]
use c', hc, a', ha, b', hb
[GOAL]
case right
a b c d b' : Ordinal.{u}
hb : b' < a
c' : Ordinal.{u}
hc : c' < b
a' : Ordinal.{u}
ha : a' < c
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b') + ↑toNatOrdinal (c' ⨳ a' ⨳ a)) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ b') + ↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b'))
⊢ ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ a' ⨳ a) + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b')) ≤
    ↑toOrdinal
      (↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ b') +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b'))
[PROOFSTEP]
convert h using 1
[GOAL]
case h.e'_3
a b c d b' : Ordinal.{u}
hb : b' < a
c' : Ordinal.{u}
hc : c' < b
a' : Ordinal.{u}
ha : a' < c
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b') + ↑toNatOrdinal (c' ⨳ a' ⨳ a)) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ b') + ↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b'))
⊢ ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ a' ⨳ a) + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b')) =
    ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b') + ↑toNatOrdinal (c' ⨳ a' ⨳ a))
[PROOFSTEP]
abel_nf
[GOAL]
case h.e'_4
a b c d b' : Ordinal.{u}
hb : b' < a
c' : Ordinal.{u}
hc : c' < b
a' : Ordinal.{u}
ha : a' < c
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b') + ↑toNatOrdinal (c' ⨳ a' ⨳ a)) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ b') + ↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b'))
⊢ ↑toOrdinal
      (↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ b') +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b')) =
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ b') + ↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b'))
[PROOFSTEP]
abel_nf
[GOAL]
a b c d : Ordinal.{u}
⊢ a ⨳ (b ⨳ c) ≤ d ↔
    ∀ (a' : Ordinal.{u}),
      a' < a →
        ∀ (b' : Ordinal.{u}),
          b' < b →
            ∀ (c' : Ordinal.{u}),
              c' < c →
                a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
                  d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
a b c d : Ordinal.{u}
⊢ ¬a ⨳ (b ⨳ c) ≤ d ↔
    ¬∀ (a' : Ordinal.{u}),
        a' < a →
          ∀ (b' : Ordinal.{u}),
            b' < b →
              ∀ (c' : Ordinal.{u}),
                c' < c →
                  a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
                    d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
[PROOFSTEP]
simp [lt_nmul_iff₃']
[GOAL]
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ a ⨳ b ⨳ c = a ⨳ (b ⨳ c)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ a ⨳ b ⨳ c ≤ a ⨳ (b ⨳ c)
[PROOFSTEP]
rw [nmul_le_iff₃]
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ ∀ (a' : Ordinal.{u_1}),
    a' < a →
      ∀ (b' : Ordinal.{u_1}),
        b' < b →
          ∀ (c' : Ordinal.{u_1}),
            c' < c →
              a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' <
                a ⨳ (b ⨳ c) ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
[PROOFSTEP]
intro a' ha b' hb c' hc
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
c' : Ordinal.{u_1}
hc : c' < c
⊢ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ (b ⨳ c) ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
[PROOFSTEP]
rw [nmul_assoc a' b c, nmul_assoc a b' c, nmul_assoc a b c', nmul_assoc a' b' c', nmul_assoc a' b' c,
  nmul_assoc a' b c', nmul_assoc a b' c']
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
c' : Ordinal.{u_1}
hc : c' < c
⊢ a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
    a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
[PROOFSTEP]
exact nmul_nadd_lt₃' ha hb hc
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ a ⨳ (b ⨳ c) ≤ a ⨳ b ⨳ c
[PROOFSTEP]
rw [nmul_le_iff₃']
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ ∀ (a' : Ordinal.{u_1}),
    a' < a →
      ∀ (b' : Ordinal.{u_1}),
        b' < b →
          ∀ (c' : Ordinal.{u_1}),
            c' < c →
              a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
                a ⨳ b ⨳ c ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
[PROOFSTEP]
intro a' ha b' hb c' hc
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
c' : Ordinal.{u_1}
hc : c' < c
⊢ a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
    a ⨳ b ⨳ c ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
[PROOFSTEP]
rw [← nmul_assoc a' b c, ← nmul_assoc a b' c, ← nmul_assoc a b c', ← nmul_assoc a' b' c', ← nmul_assoc a' b' c, ←
  nmul_assoc a' b c', ← nmul_assoc a b' c']
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
a b c a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
c' : Ordinal.{u_1}
hc : c' < c
⊢ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
[PROOFSTEP]
exact nmul_nadd_lt₃ ha hb hc
[GOAL]
a b : Ordinal.{u_1}
⊢ a ⨳ succ b = a ⨳ b ♯ a
[PROOFSTEP]
rw [← nadd_one, nmul_nadd_one]
[GOAL]
a b : Ordinal.{u_1}
⊢ succ a ⨳ b = a ⨳ b ♯ b
[PROOFSTEP]
rw [← nadd_one, nadd_one_nmul]
[GOAL]
a b : Ordinal.{u}
⊢ a * b ≤ a ⨳ b
[PROOFSTEP]
refine b.limitRecOn ?_ ?_ ?_
[GOAL]
case refine_1
a b : Ordinal.{u}
⊢ a * 0 ≤ a ⨳ 0
[PROOFSTEP]
simp
[GOAL]
case refine_2
a b : Ordinal.{u}
⊢ ∀ (o : Ordinal.{u}), a * o ≤ a ⨳ o → a * succ o ≤ a ⨳ succ o
[PROOFSTEP]
intro c h
[GOAL]
case refine_2
a b c : Ordinal.{u}
h : a * c ≤ a ⨳ c
⊢ a * succ c ≤ a ⨳ succ c
[PROOFSTEP]
rw [mul_succ, nmul_succ]
[GOAL]
case refine_2
a b c : Ordinal.{u}
h : a * c ≤ a ⨳ c
⊢ a * c + a ≤ a ⨳ c ♯ a
[PROOFSTEP]
exact (add_le_nadd _ a).trans (nadd_le_nadd_right h a)
[GOAL]
case refine_3
a b : Ordinal.{u}
⊢ ∀ (o : Ordinal.{u}), IsLimit o → (∀ (o' : Ordinal.{u}), o' < o → a * o' ≤ a ⨳ o') → a * o ≤ a ⨳ o
[PROOFSTEP]
intro c hc H
[GOAL]
case refine_3
a b c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a * o' ≤ a ⨳ o'
⊢ a * c ≤ a ⨳ c
[PROOFSTEP]
rcases eq_zero_or_pos a with (rfl | ha)
[GOAL]
case refine_3.inl
b c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → 0 * o' ≤ 0 ⨳ o'
⊢ 0 * c ≤ 0 ⨳ c
[PROOFSTEP]
simp
[GOAL]
case refine_3.inr
a b c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a * o' ≤ a ⨳ o'
ha : 0 < a
⊢ a * c ≤ a ⨳ c
[PROOFSTEP]
have := IsNormal.blsub_eq.{u, u} (mul_isNormal ha) hc
[GOAL]
case refine_3.inr
a b c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a * o' ≤ a ⨳ o'
ha : 0 < a
this : (blsub c fun x x_1 => (fun x x_2 => x * x_2) a x) = (fun x x_1 => x * x_1) a c
⊢ a * c ≤ a ⨳ c
[PROOFSTEP]
dsimp at this
[GOAL]
case refine_3.inr
a b c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a * o' ≤ a ⨳ o'
ha : 0 < a
this : (blsub c fun x x_1 => a * x) = a * c
⊢ a * c ≤ a ⨳ c
[PROOFSTEP]
rw [← this, blsub_le_iff]
[GOAL]
case refine_3.inr
a b c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a * o' ≤ a ⨳ o'
ha : 0 < a
this : (blsub c fun x x_1 => a * x) = a * c
⊢ ∀ (i : Ordinal.{u}), i < c → a * i < a ⨳ c
[PROOFSTEP]
exact fun i hi => (H i hi).trans_lt (nmul_lt_nmul_of_pos_left hi ha)