Theorem: exercise4_3 (LeanCourse/Assignments/Solutions/Solutions4.lean)

State before:
x y z : PosReal
⊢ x * y * z = x * (y * z)
Tactic:
ext
State after:
case h
x y z : PosReal
⊢ ↑(x * y * z) = ↑(x * (y * z))

State before:
case h
x y z : PosReal
⊢ ↑(x * y * z) = ↑(x * (y * z))
Tactic:
apply mul_assoc
State after:
no goals

State before:
⊢ 0 < 1
Tactic:
norm_num
State after:
no goals

State before:
x : PosReal
⊢ 1 * x = x
Tactic:
ext
State after:
case h
x : PosReal
⊢ ↑(1 * x) = ↑x

State before:
case h
x : PosReal
⊢ ↑(1 * x) = ↑x
Tactic:
apply one_mul
State after:
no goals

State before:
x : PosReal
⊢ x * 1 = x
Tactic:
ext
State after:
case h
x : PosReal
⊢ ↑(x * 1) = ↑x

State before:
case h
x : PosReal
⊢ ↑(x * 1) = ↑x
Tactic:
apply mul_one
State after:
no goals

State before:
x : PosReal
⊢ x⁻¹ * x = 1
Tactic:
ext
State after:
case h
x : PosReal
⊢ ↑(x⁻¹ * x) = ↑1

State before:
case h
x : PosReal
⊢ ↑(x⁻¹ * x) = ↑1
Tactic:
apply inv_mul_cancel
State after:
case h.h
x : PosReal
⊢ ↑x ≠ 0

State before:
case h.h
x : PosReal
⊢ ↑x ≠ 0
Tactic:
exact x.2.ne'
State after:
no goals