Theorem: Real.log_eq_log (CvxLean/Lib/Math/Data/Real.lean)

State before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x = y
⊢ x.log = y.log
Tactic:
rw [h]
State after:
no goals

State before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
⊢ x = y
Tactic:
have hxmem := Set.mem_Ioi.2 hx
State after:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
⊢ x = y

State before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
⊢ x = y
Tactic:
have hymem := Set.mem_Ioi.2 hy
State after:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
⊢ x = y

State before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
⊢ x = y
Tactic:
have heq : Set.restrict (Set.Ioi 0) log ⟨x, hxmem⟩ =
  Set.restrict (Set.Ioi 0) log ⟨y, hymem⟩ := by
  simp [h]
State after:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
heq : (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
⊢ x = y

State before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
heq : (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
⊢ x = y
Tactic:
have h := log_injOn_pos.injective heq
State after:
x y : ℝ
hx : 0 < x
hy : 0 < y
h✝ : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
heq : (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
h : ⟨x, hxmem⟩ = ⟨y, hymem⟩
⊢ x = y

State before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h✝ : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
heq : (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
h : ⟨x, hxmem⟩ = ⟨y, hymem⟩
⊢ x = y
Tactic:
simp [Subtype.eq] at h
State after:
x y : ℝ
hx : 0 < x
hy : 0 < y
h✝ : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
heq : (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
h : x = y
⊢ x = y

State before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h✝ : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
heq : (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
h : x = y
⊢ x = y
Tactic:
exact h
State after:
no goals

State before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
⊢ (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
Tactic:
simp [h]
State after:
no goals