[GOAL]
n : ℕ
⊢ LeftMoves (powHalf n) = PUnit
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ LeftMoves (powHalf Nat.zero) = PUnit
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ : ℕ
⊢ LeftMoves (powHalf (Nat.succ n✝)) = PUnit
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
i : LeftMoves (powHalf n)
⊢ moveLeft (powHalf n) i = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
i : LeftMoves (powHalf Nat.zero)
⊢ moveLeft (powHalf Nat.zero) i = 0
[PROOFSTEP]
cases i
[GOAL]
case succ
n✝ : ℕ
i : LeftMoves (powHalf (Nat.succ n✝))
⊢ moveLeft (powHalf (Nat.succ n✝)) i = 0
[PROOFSTEP]
cases i
[GOAL]
case zero.unit
⊢ moveLeft (powHalf Nat.zero) PUnit.unit = 0
[PROOFSTEP]
rfl
[GOAL]
case succ.unit
n✝ : ℕ
⊢ moveLeft (powHalf (Nat.succ n✝)) PUnit.unit = 0
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ Unique (LeftMoves (powHalf n))
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ Unique (LeftMoves (powHalf Nat.zero))
[PROOFSTEP]
exact PUnit.unique
[GOAL]
case succ
n✝ : ℕ
⊢ Unique (LeftMoves (powHalf (Nat.succ n✝)))
[PROOFSTEP]
exact PUnit.unique
[GOAL]
⊢ birthday (powHalf 1) = 2
[PROOFSTEP]
rw [birthday_def]
[GOAL]
⊢ max (Ordinal.lsub fun i => birthday (moveLeft (powHalf 1) i))
      (Ordinal.lsub fun i => birthday (moveRight (powHalf 1) i)) =
    2
[PROOFSTEP]
dsimp
[GOAL]
⊢ max (Ordinal.lsub fun i => birthday (moveLeft (powHalf 1) i)) (Ordinal.lsub fun i => birthday 1) = 2
[PROOFSTEP]
simpa using Order.le_succ (1 : Ordinal)
[GOAL]
n : ℕ
⊢ Numeric (powHalf n)
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
⊢ Numeric (powHalf Nat.zero)
[PROOFSTEP]
exact numeric_one
[GOAL]
case succ
n : ℕ
hn : Numeric (powHalf n)
⊢ Numeric (powHalf (Nat.succ n))
[PROOFSTEP]
constructor
[GOAL]
case succ.left
n : ℕ
hn : Numeric (powHalf n)
⊢ ∀ (i j : PUnit), OfNat.ofNat 0 i < (fun x => powHalf n) j
[PROOFSTEP]
simpa using hn.moveLeft_lt default
[GOAL]
case succ.right
n : ℕ
hn : Numeric (powHalf n)
⊢ (∀ (i : PUnit), Numeric (OfNat.ofNat 0 i)) ∧ ∀ (j : PUnit), Numeric ((fun x => powHalf n) j)
[PROOFSTEP]
exact ⟨fun _ => numeric_zero, fun _ => hn⟩
[GOAL]
n : ℕ
⊢ powHalf n ≤ 1
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
⊢ powHalf Nat.zero ≤ 1
[PROOFSTEP]
exact le_rfl
[GOAL]
case succ
n : ℕ
hn : powHalf n ≤ 1
⊢ powHalf (Nat.succ n) ≤ 1
[PROOFSTEP]
exact (powHalf_succ_le_powHalf n).trans hn
[GOAL]
n : ℕ
⊢ 0 < powHalf n
[PROOFSTEP]
rw [← lf_iff_lt numeric_zero (numeric_powHalf n), zero_lf_le]
[GOAL]
n : ℕ
⊢ ∃ i, 0 ≤ moveLeft (powHalf n) i
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n hn
[GOAL]
case h
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n
[PROOFSTEP]
constructor
[GOAL]
case h.left
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf (n + 1) + powHalf (n + 1) ≤ powHalf n
[PROOFSTEP]
rw [le_iff_forall_lf]
[GOAL]
case h.right
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n ≤ powHalf (n + 1) + powHalf (n + 1)
[PROOFSTEP]
rw [le_iff_forall_lf]
[GOAL]
case h.left
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (∀ (i : LeftMoves (powHalf (n + 1) + powHalf (n + 1))), moveLeft (powHalf (n + 1) + powHalf (n + 1)) i ⧏ powHalf n) ∧
    ∀ (j : RightMoves (powHalf n)), powHalf (n + 1) + powHalf (n + 1) ⧏ moveRight (powHalf n) j
[PROOFSTEP]
constructor
[GOAL]
case h.right
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (∀ (i : LeftMoves (powHalf n)), moveLeft (powHalf n) i ⧏ powHalf (n + 1) + powHalf (n + 1)) ∧
    ∀ (j : RightMoves (powHalf (n + 1) + powHalf (n + 1))), powHalf n ⧏ moveRight (powHalf (n + 1) + powHalf (n + 1)) j
[PROOFSTEP]
constructor
[GOAL]
case h.left.left
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (i : LeftMoves (powHalf (n + 1) + powHalf (n + 1))), moveLeft (powHalf (n + 1) + powHalf (n + 1)) i ⧏ powHalf n
[PROOFSTEP]
rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩)
[GOAL]
case h.left.left.inl.unit
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveLeft (powHalf (n + 1) + powHalf (n + 1)) (Sum.inl PUnit.unit) ⧏ powHalf n
[PROOFSTEP]
apply lf_of_lt
[GOAL]
case h.left.left.inr.unit
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveLeft (powHalf (n + 1) + powHalf (n + 1)) (Sum.inr PUnit.unit) ⧏ powHalf n
[PROOFSTEP]
apply lf_of_lt
[GOAL]
case h.left.left.inl.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveLeft (powHalf (n + 1) + powHalf (n + 1)) (Sum.inl PUnit.unit) < powHalf n
[PROOFSTEP]
calc
  0 + powHalf n.succ ≈ powHalf n.succ := zero_add_equiv _
  _ < powHalf n := powHalf_succ_lt_powHalf n
[GOAL]
case h.left.left.inr.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveLeft (powHalf (n + 1) + powHalf (n + 1)) (Sum.inr PUnit.unit) < powHalf n
[PROOFSTEP]
calc
  powHalf n.succ + 0 ≈ powHalf n.succ := add_zero_equiv _
  _ < powHalf n := powHalf_succ_lt_powHalf n
[GOAL]
case h.left.right
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : RightMoves (powHalf n)), powHalf (n + 1) + powHalf (n + 1) ⧏ moveRight (powHalf n) j
[PROOFSTEP]
cases' n with n
[GOAL]
case h.left.right.zero
hn : ∀ (m : ℕ), m < Nat.zero → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : RightMoves (powHalf Nat.zero)),
    powHalf (Nat.zero + 1) + powHalf (Nat.zero + 1) ⧏ moveRight (powHalf Nat.zero) j
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case h.left.right.succ
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : RightMoves (powHalf (Nat.succ n))),
    powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1) ⧏ moveRight (powHalf (Nat.succ n)) j
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case h.left.right.succ.unit
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1) ⧏ moveRight (powHalf (Nat.succ n)) PUnit.unit
[PROOFSTEP]
apply lf_of_moveRight_le
[GOAL]
case h.left.right.succ.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveRight (powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1)) ?h.left.right.succ.unit.j ≤
    moveRight (powHalf (Nat.succ n)) PUnit.unit
case h.left.right.succ.unit.j
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ RightMoves (powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1))
[PROOFSTEP]
swap
[GOAL]
case h.left.right.succ.unit.j
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ RightMoves (powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1))
case h.left.right.succ.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveRight (powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1)) ?h.left.right.succ.unit.j ≤
    moveRight (powHalf (Nat.succ n)) PUnit.unit
[PROOFSTEP]
exact Sum.inl default
[GOAL]
case h.left.right.succ.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveRight (powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1)) (Sum.inl default) ≤
    moveRight (powHalf (Nat.succ n)) PUnit.unit
[PROOFSTEP]
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)
[GOAL]
case h.right.left
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (i : LeftMoves (powHalf n)), moveLeft (powHalf n) i ⧏ powHalf (n + 1) + powHalf (n + 1)
[PROOFSTEP]
simp only [powHalf_moveLeft, forall_const]
[GOAL]
case h.right.left
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ 0 ⧏ powHalf (n + 1) + powHalf (n + 1)
[PROOFSTEP]
apply lf_of_lt
[GOAL]
case h.right.left.h
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ 0 < powHalf (n + 1) + powHalf (n + 1)
[PROOFSTEP]
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 _) _
[GOAL]
case h.right.right
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : RightMoves (powHalf (n + 1) + powHalf (n + 1))), powHalf n ⧏ moveRight (powHalf (n + 1) + powHalf (n + 1)) j
[PROOFSTEP]
rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩)
[GOAL]
case h.right.right.inl.unit
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n ⧏ moveRight (powHalf (n + 1) + powHalf (n + 1)) (Sum.inl PUnit.unit)
[PROOFSTEP]
apply lf_of_lt
[GOAL]
case h.right.right.inr.unit
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n ⧏ moveRight (powHalf (n + 1) + powHalf (n + 1)) (Sum.inr PUnit.unit)
[PROOFSTEP]
apply lf_of_lt
[GOAL]
case h.right.right.inl.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n < moveRight (powHalf (n + 1) + powHalf (n + 1)) (Sum.inl PUnit.unit)
[PROOFSTEP]
calc
  powHalf n ≈ powHalf n + 0 := (Equiv.symm (add_zero_equiv _))
  _ < powHalf n + powHalf n.succ := add_lt_add_left (powHalf_pos _) _
[GOAL]
case h.right.right.inr.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n < moveRight (powHalf (n + 1) + powHalf (n + 1)) (Sum.inr PUnit.unit)
[PROOFSTEP]
calc
  powHalf n ≈ 0 + powHalf n := (Equiv.symm (zero_add_equiv _))
  _ < powHalf n.succ + powHalf n := add_lt_add_right (powHalf_pos _) _
[GOAL]
n : ℕ
⊢ 2 • powHalf (Nat.succ n) = powHalf n
[PROOFSTEP]
rw [two_nsmul]
[GOAL]
n : ℕ
⊢ powHalf (Nat.succ n) + powHalf (Nat.succ n) = powHalf n
[PROOFSTEP]
exact Quotient.sound (PGame.add_powHalf_succ_self_eq_powHalf n)
[GOAL]
n : ℕ
⊢ 2 ^ n • powHalf n = 1
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
⊢ 2 ^ Nat.zero • powHalf Nat.zero = 1
[PROOFSTEP]
simp only [Nat.zero_eq, pow_zero, powHalf_zero, one_smul]
[GOAL]
case succ
n : ℕ
hn : 2 ^ n • powHalf n = 1
⊢ 2 ^ Nat.succ n • powHalf (Nat.succ n) = 1
[PROOFSTEP]
rw [← hn, ← double_powHalf_succ_eq_powHalf n, smul_smul (2 ^ n) 2 (powHalf n.succ), mul_comm, pow_succ]
[GOAL]
n k : ℕ
⊢ 2 ^ n • powHalf (n + k) = powHalf k
[PROOFSTEP]
induction' k with k hk
[GOAL]
case zero
n : ℕ
⊢ 2 ^ n • powHalf (n + Nat.zero) = powHalf Nat.zero
[PROOFSTEP]
simp only [add_zero, Surreal.nsmul_pow_two_powHalf, Nat.zero_eq, eq_self_iff_true, Surreal.powHalf_zero]
[GOAL]
case succ
n k : ℕ
hk : 2 ^ n • powHalf (n + k) = powHalf k
⊢ 2 ^ n • powHalf (n + Nat.succ k) = powHalf (Nat.succ k)
[PROOFSTEP]
rw [← double_powHalf_succ_eq_powHalf (n + k), ← double_powHalf_succ_eq_powHalf k, smul_algebra_smul_comm] at hk 
[GOAL]
case succ
n k : ℕ
hk : 2 • 2 ^ n • powHalf (Nat.succ (n + k)) = 2 • powHalf (Nat.succ k)
⊢ 2 ^ n • powHalf (n + Nat.succ k) = powHalf (Nat.succ k)
[PROOFSTEP]
rwa [← zsmul_eq_zsmul_iff' two_ne_zero]
[GOAL]
m : ℤ
n k : ℕ
⊢ (m * 2 ^ n) • powHalf (n + k) = m • powHalf k
[PROOFSTEP]
rw [mul_zsmul]
[GOAL]
m : ℤ
n k : ℕ
⊢ m • 2 ^ n • powHalf (n + k) = m • powHalf k
[PROOFSTEP]
congr
[GOAL]
case e_a
m : ℤ
n k : ℕ
⊢ 2 ^ n • powHalf (n + k) = powHalf k
[PROOFSTEP]
norm_cast
[GOAL]
case e_a
m : ℤ
n k : ℕ
⊢ 2 ^ n • powHalf (n + k) = powHalf k
[PROOFSTEP]
exact nsmul_pow_two_powHalf' n k
[GOAL]
m₁ m₂ : ℤ
y₁ y₂ : ℕ
h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂
⊢ m₁ • powHalf y₂ = m₂ • powHalf y₁
[PROOFSTEP]
revert m₁ m₂
[GOAL]
y₁ y₂ : ℕ
⊢ ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → m₁ • powHalf y₂ = m₂ • powHalf y₁
[PROOFSTEP]
wlog h : y₁ ≤ y₂
[GOAL]
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₁
[PROOFSTEP]
intro m₁ m₂ aux
[GOAL]
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₁
[PROOFSTEP]
exact (this (le_of_not_le h) aux.symm).symm
[GOAL]
y₁ y₂ : ℕ
h : y₁ ≤ y₂
⊢ ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → m₁ • powHalf y₂ = m₂ • powHalf y₁
[PROOFSTEP]
intro m₁ m₂ h₂
[GOAL]
y₁ y₂ : ℕ
h : y₁ ≤ y₂
m₁ m₂ : ℤ
h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂
⊢ m₁ • powHalf y₂ = m₂ • powHalf y₁
[PROOFSTEP]
obtain ⟨c, rfl⟩ := le_iff_exists_add.mp h
[GOAL]
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₁
[PROOFSTEP]
rw [add_comm, pow_add, ← mul_assoc, mul_eq_mul_right_iff] at h₂ 
[GOAL]
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₁
[PROOFSTEP]
cases' h₂ with h₂ h₂
[GOAL]
case intro.inl
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : m₁ = m₂ * 2 ^ c
⊢ m₁ • powHalf (y₁ + c) = m₂ • powHalf y₁
[PROOFSTEP]
rw [h₂, add_comm, zsmul_pow_two_powHalf m₂ c y₁]
[GOAL]
case intro.inr
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : 2 ^ y₁ = 0
⊢ m₁ • powHalf (y₁ + c) = m₂ • powHalf y₁
[PROOFSTEP]
have := Nat.one_le_pow y₁ 2 Nat.succ_pos'
[GOAL]
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₁
[PROOFSTEP]
norm_cast at h₂ 
[GOAL]
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₁
[PROOFSTEP]
linarith
[GOAL]
x : Localization.Away 2
⊢ ∀ {a c : ℤ} {b d : { x // x ∈ Submonoid.powers 2 }},
    ↑(Localization.r (Submonoid.powers 2)) (a, b) (c, d) → a • powHalf (Submonoid.log b) = c • powHalf (Submonoid.log d)
[PROOFSTEP]
intro m₁ m₂ n₁ n₂ h₁
[GOAL]
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
obtain ⟨⟨n₃, y₃, hn₃⟩, h₂⟩ := Localization.r_iff_exists.mp h₁
[GOAL]
case intro.mk.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h₂ :
  ↑{ val := n₃, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = n₃) } * (↑(m₂, n₂).snd * (m₁, n₁).fst) =
    ↑{ val := n₃, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = n₃) } * (↑(m₁, n₁).snd * (m₂, n₂).fst)
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
simp only [Subtype.coe_mk, mul_eq_mul_left_iff] at h₂ 
[GOAL]
case intro.mk.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h₂ : ↑n₂ * m₁ = ↑n₁ * m₂ ∨ n₃ = 0
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
cases h₂
[GOAL]
case intro.mk.intro.inl
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
obtain ⟨a₁, ha₁⟩ := n₁.prop
[GOAL]
case intro.mk.intro.inl.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : (fun x x_1 => x ^ x_1) 2 a₁ = ↑n₁
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
obtain ⟨a₂, ha₂⟩ := n₂.prop
[GOAL]
case intro.mk.intro.inl.intro.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : (fun x x_1 => x ^ x_1) 2 a₁ = ↑n₁
a₂ : ℕ
ha₂ : (fun x x_1 => x ^ x_1) 2 a₂ = ↑n₂
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
simp only at ha₁ ha₂ ⊢
[GOAL]
case intro.mk.intro.inl.intro.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : 2 ^ a₁ = ↑n₁
a₂ : ℕ
ha₂ : 2 ^ a₂ = ↑n₂
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
have hn₁ : n₁ = Submonoid.pow 2 a₁ := Subtype.ext ha₁.symm
[GOAL]
case intro.mk.intro.inl.intro.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : 2 ^ a₁ = ↑n₁
a₂ : ℕ
ha₂ : 2 ^ a₂ = ↑n₂
hn₁ : n₁ = Submonoid.pow 2 a₁
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
have hn₂ : n₂ = Submonoid.pow 2 a₂ := Subtype.ext ha₂.symm
[GOAL]
case intro.mk.intro.inl.intro.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : 2 ^ a₁ = ↑n₁
a₂ : ℕ
ha₂ : 2 ^ a₂ = ↑n₂
hn₁ : n₁ = Submonoid.pow 2 a₁
hn₂ : n₂ = Submonoid.pow 2 a₂
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
have h₂ : 1 < (2 : ℤ).natAbs := one_lt_two
[GOAL]
case intro.mk.intro.inl.intro.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : 2 ^ a₁ = ↑n₁
a₂ : ℕ
ha₂ : 2 ^ a₂ = ↑n₂
hn₁ : n₁ = Submonoid.pow 2 a₁
hn₂ : n₂ = Submonoid.pow 2 a₂
h₂ : 1 < Int.natAbs 2
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
rw [hn₁, hn₂, Submonoid.log_pow_int_eq_self h₂, Submonoid.log_pow_int_eq_self h₂]
[GOAL]
case intro.mk.intro.inl.intro.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : 2 ^ a₁ = ↑n₁
a₂ : ℕ
ha₂ : 2 ^ a₂ = ↑n₂
hn₁ : n₁ = Submonoid.pow 2 a₁
hn₂ : n₂ = Submonoid.pow 2 a₂
h₂ : 1 < Int.natAbs 2
⊢ m₁ • powHalf a₁ = m₂ • powHalf a₂
[PROOFSTEP]
apply dyadic_aux
[GOAL]
case intro.mk.intro.inl.intro.intro.h₂
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : 2 ^ a₁ = ↑n₁
a₂ : ℕ
ha₂ : 2 ^ a₂ = ↑n₂
hn₁ : n₁ = Submonoid.pow 2 a₁
hn₂ : n₂ = Submonoid.pow 2 a₂
h₂ : 1 < Int.natAbs 2
⊢ m₁ * 2 ^ a₂ = m₂ * 2 ^ a₁
[PROOFSTEP]
rwa [ha₁, ha₂, mul_comm, mul_comm m₂]
[GOAL]
case intro.mk.intro.inr
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : n₃ = 0
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
have : (1 : ℤ) ≤ 2 ^ y₃ := by exact_mod_cast Nat.one_le_pow y₃ 2 Nat.succ_pos'
[GOAL]
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : n₃ = 0
⊢ 1 ≤ 2 ^ y₃
[PROOFSTEP]
exact_mod_cast Nat.one_le_pow y₃ 2 Nat.succ_pos'
[GOAL]
case intro.mk.intro.inr
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : n₃ = 0
this : 1 ≤ 2 ^ y₃
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
linarith
[GOAL]
x y : Localization.Away 2
⊢ ∀ (x y : ℤ × { x // x ∈ Submonoid.powers 2 }),
    ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk x.fst x.snd + Localization.mk y.fst y.snd) =
      ZeroHom.toFun
          {
            toFun := fun x =>
              Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
                (_ :
                  ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                    ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                      m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
            map_zero' :=
              (_ :
                Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                    (_ :
                      ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                        ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                          m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                  0 • powHalf (Submonoid.log 1)) }
          (Localization.mk x.fst x.snd) +
        ZeroHom.toFun
          {
            toFun := fun x =>
              Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
                (_ :
                  ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                    ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                      m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
            map_zero' :=
              (_ :
                Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                    (_ :
                      ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                        ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                          m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                  0 • powHalf (Submonoid.log 1)) }
          (Localization.mk y.fst y.snd)
[PROOFSTEP]
rintro ⟨a, ⟨b, ⟨b', rfl⟩⟩⟩ ⟨c, ⟨d, ⟨d', rfl⟩⟩⟩
[GOAL]
case mk.mk.intro.mk.mk.intro
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
⊢ ZeroHom.toFun
      {
        toFun := fun x =>
          Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
            (_ :
              ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                  m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
        map_zero' :=
          (_ :
            Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                (_ :
                  ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                    ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                      m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
              0 • powHalf (Submonoid.log 1)) }
      (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd +
        Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd) =
    ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd) +
      ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd)
[PROOFSTEP]
have h₂ : 1 < (2 : ℤ).natAbs := one_lt_two
[GOAL]
case mk.mk.intro.mk.mk.intro
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
h₂ : 1 < Int.natAbs 2
⊢ ZeroHom.toFun
      {
        toFun := fun x =>
          Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
            (_ :
              ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                  m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
        map_zero' :=
          (_ :
            Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                (_ :
                  ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                    ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                      m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
              0 • powHalf (Submonoid.log 1)) }
      (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd +
        Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd) =
    ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd) +
      ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd)
[PROOFSTEP]
have hpow₂ := Submonoid.log_pow_int_eq_self h₂
[GOAL]
case mk.mk.intro.mk.mk.intro
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
h₂ : 1 < Int.natAbs 2
hpow₂ : ∀ (m : ℕ), Submonoid.log (Submonoid.pow 2 m) = m
⊢ ZeroHom.toFun
      {
        toFun := fun x =>
          Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
            (_ :
              ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                  m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
        map_zero' :=
          (_ :
            Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                (_ :
                  ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                    ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                      m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
              0 • powHalf (Submonoid.log 1)) }
      (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd +
        Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd) =
    ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd) +
      ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd)
[PROOFSTEP]
simp_rw [Submonoid.pow_apply] at hpow₂ 
[GOAL]
case mk.mk.intro.mk.mk.intro
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
h₂ : 1 < Int.natAbs 2
hpow₂ : ∀ (m : ℕ), Submonoid.log { val := 2 ^ m, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = 2 ^ m) } = m
⊢ ZeroHom.toFun
      {
        toFun := fun x =>
          Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
            (_ :
              ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                  m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
        map_zero' :=
          (_ :
            Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                (_ :
                  ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                    ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                      m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
              0 • powHalf (Submonoid.log 1)) }
      (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd +
        Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd) =
    ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd) +
      ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd)
[PROOFSTEP]
simp_rw [Localization.add_mk, Localization.liftOn_mk, Submonoid.log_mul (Int.pow_right_injective h₂), hpow₂]
[GOAL]
case mk.mk.intro.mk.mk.intro
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
h₂ : 1 < Int.natAbs 2
hpow₂ : ∀ (m : ℕ), Submonoid.log { val := 2 ^ m, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = 2 ^ m) } = m
⊢ (2 ^ b' * c + 2 ^ d' * a) • powHalf (b' + d') = a • powHalf b' + c • powHalf d'
[PROOFSTEP]
calc
  (2 ^ b' * c + 2 ^ d' * a) • powHalf (b' + d') = (c * 2 ^ b') • powHalf (b' + d') + (a * 2 ^ d') • powHalf (d' + b') :=
    by simp only [add_smul, mul_comm, add_comm]
  _ = c • powHalf d' + a • powHalf b' := by simp only [zsmul_pow_two_powHalf]
  _ = a • powHalf b' + c • powHalf d' := add_comm _ _
[GOAL]
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
h₂ : 1 < Int.natAbs 2
hpow₂ : ∀ (m : ℕ), Submonoid.log { val := 2 ^ m, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = 2 ^ m) } = m
⊢ (2 ^ b' * c + 2 ^ d' * a) • powHalf (b' + d') = (c * 2 ^ b') • powHalf (b' + d') + (a * 2 ^ d') • powHalf (d' + b')
[PROOFSTEP]
simp only [add_smul, mul_comm, add_comm]
[GOAL]
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
h₂ : 1 < Int.natAbs 2
hpow₂ : ∀ (m : ℕ), Submonoid.log { val := 2 ^ m, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = 2 ^ m) } = m
⊢ (c * 2 ^ b') • powHalf (b' + d') + (a * 2 ^ d') • powHalf (d' + b') = c • powHalf d' + a • powHalf b'
[PROOFSTEP]
simp only [zsmul_pow_two_powHalf]
[GOAL]
m : ℤ
p : { x // x ∈ Submonoid.powers 2 }
⊢ ↑dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m p) = m • powHalf (Submonoid.log p)
[PROOFSTEP]
rw [← Localization.mk_eq_mk']
[GOAL]
m : ℤ
p : { x // x ∈ Submonoid.powers 2 }
⊢ ↑dyadicMap (Localization.mk m p) = m • powHalf (Submonoid.log p)
[PROOFSTEP]
rfl
[GOAL]
m : ℤ
n : ℕ
⊢ ↑dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m (Submonoid.pow 2 n)) = m • powHalf n
[PROOFSTEP]
rw [dyadicMap_apply, @Submonoid.log_pow_int_eq_self 2 one_lt_two]
[GOAL]
m : ℤ
n : ℕ
⊢ m • powHalf (Submonoid.log (Submonoid.pow 2 n)) = m • powHalf n
[PROOFSTEP]
rw [@Submonoid.log_pow_int_eq_self 2 one_lt_two]
