-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem dyadic_aux {m₁ m₂ : ℤ} {y₁ y₂ : ℕ} (h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂) :
    m₁ * powHalf y₂ = m₂ * powHalf y₁

Proof state:
y₁ y₂ : ℕ
⊢ ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁

Tactic:
wlog h : y₁ ≤ y₂

Result:
case inr
y₁ y₂ : ℕ
this : ∀ {y₁ y₂ : ℕ}, y₁ ≤ y₂ → ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁
h : ¬y₁ ≤ y₂
⊢ ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁

y₁ y₂ : ℕ
h : y₁ ≤ y₂
⊢ ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁

Proof state:
case intro.inl
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : m₁ = m₂ * 2 ^ c
⊢ ↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁

Tactic:
rw [h₂, add_comm]

Result:
case intro.inl
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : m₁ = m₂ * 2 ^ c
⊢ ↑(m₂ * 2 ^ c) * powHalf (c + y₁) = ↑m₂ * powHalf y₁

Proof state:
case intro
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : m₁ = m₂ * 2 ^ c ∨ 2 ^ y₁ = 0
⊢ ↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁

Tactic:
rcases h₂ with h₂ | h₂

Result:
case intro.inl
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : m₁ = m₂ * 2 ^ c
⊢ ↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁

case intro.inr
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : 2 ^ y₁ = 0
⊢ ↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁

Proof state:
case intro.inr
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : 2 ^ y₁ = 0
this : 1 ≤ 2 ^ y₁
⊢ ↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁

Tactic:
norm_cast at h₂

Result:
case intro.inr
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
this : 1 ≤ 2 ^ y₁
h₂ : 2 ^ y₁ = 0
⊢ ↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁

Proof state:
case intro.inr
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : 2 ^ y₁ = 0
⊢ ↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁

Tactic:
have := Nat.one_le_pow y₁ 2 Nat.succ_pos'

Result:
case intro.inr
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : 2 ^ y₁ = 0
this : 1 ≤ 2 ^ y₁
⊢ ↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁

Proof state:
y₁ y₂ : ℕ
h : y₁ ≤ y₂
m₁ m₂ : ℤ
h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂
⊢ ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁

Tactic:
obtain ⟨c, rfl⟩ := le_iff_exists_add.mp h

Result:
case intro
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ (y₁ + c)
⊢ ↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁

Proof state:
case inr
y₁ y₂ : ℕ
this : ∀ {y₁ y₂ : ℕ}, y₁ ≤ y₂ → ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁
h : ¬y₁ ≤ y₂
m₁ m₂ : ℤ
aux : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂
⊢ ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁

Tactic:
exact (this (le_of_not_le h) aux.symm).symm

Result:
no goals

Proof state:
case inr
y₁ y₂ : ℕ
this : ∀ {y₁ y₂ : ℕ}, y₁ ≤ y₂ → ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁
h : ¬y₁ ≤ y₂
⊢ ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁

Tactic:
intro m₁ m₂ aux

Result:
case inr
y₁ y₂ : ℕ
this : ∀ {y₁ y₂ : ℕ}, y₁ ≤ y₂ → ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁
h : ¬y₁ ≤ y₂
m₁ m₂ : ℤ
aux : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂
⊢ ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁

Proof state:
case intro.inr
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
this : 1 ≤ 2 ^ y₁
h₂ : 2 ^ y₁ = 0
⊢ ↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁

Tactic:
omega

Result:
no goals

Proof state:
y₁ y₂ : ℕ
h : y₁ ≤ y₂
⊢ ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁

Tactic:
intro m₁ m₂ h₂

Result:
y₁ y₂ : ℕ
h : y₁ ≤ y₂
m₁ m₂ : ℤ
h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂
⊢ ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁

Proof state:
m₁ m₂ : ℤ
y₁ y₂ : ℕ
h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂
⊢ ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁

Tactic:
revert m₁ m₂

Result:
y₁ y₂ : ℕ
⊢ ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → ↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁

Proof state:
case intro.inl
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : m₁ = m₂ * 2 ^ c
⊢ ↑(m₂ * 2 ^ c) * powHalf (c + y₁) = ↑m₂ * powHalf y₁

Tactic:
simp_rw [Int.cast_mul, Int.cast_pow, Int.cast_ofNat, zsmul_pow_two_powHalf m₂ c y₁]

Result:
no goals

Proof state:
case intro
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ (y₁ + c)
⊢ ↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁

Tactic:
rw [add_comm, pow_add, ← mul_assoc, mul_eq_mul_right_iff] at h₂

Result:
case intro
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : m₁ = m₂ * 2 ^ c ∨ 2 ^ y₁ = 0
⊢ ↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁