-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem add_powHalf_succ_self_eq_powHalf (n) : powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n

Proof state:
case h.left.right.zero
hn : ∀ m < 0, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : (powHalf 0).RightMoves), powHalf (0 + 1) + powHalf (0 + 1) ⧏ (powHalf 0).moveRight j

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
case h.right.left
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (i : (powHalf n).LeftMoves), (powHalf n).moveLeft i ⧏ powHalf (n + 1) + powHalf (n + 1)

Tactic:
simp only [powHalf_moveLeft, forall_const]

Result:
case h.right.left
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ 0 ⧏ powHalf (n + 1) + powHalf (n + 1)

Proof state:
case h.left.left.inl.unit.h
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (powHalf (n + 1) + powHalf (n + 1)).moveLeft (Sum.inl PUnit.unit) < powHalf n

Tactic:
calc
  0 + powHalf n.succ ≈ powHalf n.succ := zero_add_equiv _
  _ < powHalf n := powHalf_succ_lt_powHalf n

Result:
no goals

Proof state:
case h.left.right
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : (powHalf n).RightMoves), powHalf (n + 1) + powHalf (n + 1) ⧏ (powHalf n).moveRight j

Tactic:
rcases n with - | n

Result:
case h.left.right.zero
hn : ∀ m < 0, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : (powHalf 0).RightMoves), powHalf (0 + 1) + powHalf (0 + 1) ⧏ (powHalf 0).moveRight j

case h.left.right.succ
n : ℕ
hn : ∀ m < n + 1, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : (powHalf (n + 1)).RightMoves), powHalf (n + 1 + 1) + powHalf (n + 1 + 1) ⧏ (powHalf (n + 1)).moveRight j

Proof state:
case h
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n

Tactic:
constructor <;> rw [le_iff_forall_lf] <;> constructor

Result:
case h.left.left
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (i : (powHalf (n + 1) + powHalf (n + 1)).LeftMoves), (powHalf (n + 1) + powHalf (n + 1)).moveLeft i ⧏ powHalf n

case h.left.right
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : (powHalf n).RightMoves), powHalf (n + 1) + powHalf (n + 1) ⧏ (powHalf n).moveRight j

case h.right.left
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (i : (powHalf n).LeftMoves), (powHalf n).moveLeft i ⧏ powHalf (n + 1) + powHalf (n + 1)

case h.right.right
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : (powHalf (n + 1) + powHalf (n + 1)).RightMoves), powHalf n ⧏ (powHalf (n + 1) + powHalf (n + 1)).moveRight j

Proof state:
case h.left.right.succ.unit
n : ℕ
hn : ∀ m < n + 1, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf (n + 1 + 1) + powHalf (n + 1 + 1) ⧏ (powHalf (n + 1)).moveRight PUnit.unit

Tactic:
apply lf_of_moveRight_le

Result:
case h.left.right.succ.unit.h
n : ℕ
hn : ∀ m < n + 1, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (powHalf (n + 1 + 1) + powHalf (n + 1 + 1)).moveRight ?h.left.right.succ.unit.j ≤
    (powHalf (n + 1)).moveRight PUnit.unit

case h.left.right.succ.unit.j
n : ℕ
hn : ∀ m < n + 1, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (powHalf (n + 1 + 1) + powHalf (n + 1 + 1)).RightMoves

Proof state:
case h.left.right.succ.unit.j
n : ℕ
hn : ∀ m < n + 1, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (powHalf (n + 1 + 1) + powHalf (n + 1 + 1)).RightMoves

Tactic:
exact Sum.inl default

Result:
no goals

Proof state:
case h.left.left
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (i : (powHalf (n + 1) + powHalf (n + 1)).LeftMoves), (powHalf (n + 1) + powHalf (n + 1)).moveLeft i ⧏ powHalf n

Tactic:
rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩) <;> apply lf_of_lt

Result:
case h.left.left.inl.unit.h
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (powHalf (n + 1) + powHalf (n + 1)).moveLeft (Sum.inl PUnit.unit) < powHalf n

case h.left.left.inr.unit.h
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (powHalf (n + 1) + powHalf (n + 1)).moveLeft (Sum.inr PUnit.unit) < powHalf n

Proof state:
case h.left.right.succ
n : ℕ
hn : ∀ m < n + 1, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : (powHalf (n + 1)).RightMoves), powHalf (n + 1 + 1) + powHalf (n + 1 + 1) ⧏ (powHalf (n + 1)).moveRight j

Tactic:
rintro ⟨⟩

Result:
case h.left.right.succ.unit
n : ℕ
hn : ∀ m < n + 1, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf (n + 1 + 1) + powHalf (n + 1 + 1) ⧏ (powHalf (n + 1)).moveRight PUnit.unit

Proof state:
n : ℕ
⊢ powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n

Tactic:
induction' n using Nat.strong_induction_on with n hn

Result:
case h
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n

Proof state:
case h.right.right.inr.unit.h
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n < (powHalf (n + 1) + powHalf (n + 1)).moveRight (Sum.inr PUnit.unit)

Tactic:
calc
  powHalf n ≈ 0 + powHalf n := Equiv.symm (zero_add_equiv _)
  _ < powHalf n.succ + powHalf n := add_lt_add_right (powHalf_pos _) _

Result:
no goals

Proof state:
case h.right.left.h
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ 0 < powHalf (n + 1) + powHalf (n + 1)

Tactic:
calc
  0 ≈ 0 + 0 := Equiv.symm (add_zero_equiv 0)
  _ ≤ powHalf n.succ + 0 := add_le_add_right (zero_le_powHalf _) _
  _ < powHalf n.succ + powHalf n.succ := add_lt_add_left (powHalf_pos _) _

Result:
no goals

Proof state:
case h.left.right.succ.unit.h
n : ℕ
hn : ∀ m < n + 1, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (powHalf (n + 1 + 1) + powHalf (n + 1 + 1)).moveRight (Sum.inl default) ≤ (powHalf (n + 1)).moveRight PUnit.unit

Tactic:
calc
  powHalf n.succ + powHalf (n.succ + 1) ≤ powHalf n.succ + powHalf n.succ :=
    add_le_add_left (powHalf_succ_le_powHalf _) _
  _ ≈ powHalf n := hn _ (Nat.lt_succ_self n)

Result:
no goals

Proof state:
case h.right.right.inl.unit.h
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n < (powHalf (n + 1) + powHalf (n + 1)).moveRight (Sum.inl PUnit.unit)

Tactic:
calc
  powHalf n ≈ powHalf n + 0 := Equiv.symm (add_zero_equiv _)
  _ < powHalf n + powHalf n.succ := add_lt_add_left (powHalf_pos _) _

Result:
no goals

Proof state:
case h.left.left.inr.unit.h
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (powHalf (n + 1) + powHalf (n + 1)).moveLeft (Sum.inr PUnit.unit) < powHalf n

Tactic:
calc
  powHalf n.succ + 0 ≈ powHalf n.succ := add_zero_equiv _
  _ < powHalf n := powHalf_succ_lt_powHalf n

Result:
no goals

Proof state:
case h.right.left
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ 0 ⧏ powHalf (n + 1) + powHalf (n + 1)

Tactic:
apply lf_of_lt

Result:
case h.right.left.h
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ 0 < powHalf (n + 1) + powHalf (n + 1)

Proof state:
case h.left.right.succ.unit.h
n : ℕ
hn : ∀ m < n + 1, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (powHalf (n + 1 + 1) + powHalf (n + 1 + 1)).moveRight ?h.left.right.succ.unit.j ≤
    (powHalf (n + 1)).moveRight PUnit.unit

case h.left.right.succ.unit.j
n : ℕ
hn : ∀ m < n + 1, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (powHalf (n + 1 + 1) + powHalf (n + 1 + 1)).RightMoves

Tactic:
swap

Result:
case h.left.right.succ.unit.j
n : ℕ
hn : ∀ m < n + 1, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (powHalf (n + 1 + 1) + powHalf (n + 1 + 1)).RightMoves

case h.left.right.succ.unit.h
n : ℕ
hn : ∀ m < n + 1, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (powHalf (n + 1 + 1) + powHalf (n + 1 + 1)).moveRight ?h.left.right.succ.unit.j ≤
    (powHalf (n + 1)).moveRight PUnit.unit