Theorem: Nat.inv_smul_eq_invCast_mul (DividedPowers/RatAlgebra.lean)

State before:
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Tactic:
cases' Nat.eq_zero_or_pos n with hn hn
State after:
case inl
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n = 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a

case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a

State before:
case inl
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n = 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a

case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Tactic:
. simp only [hn, Nat.cast_zero, isUnit_zero_iff, not_false_eq_true, Ring.inverse_non_unit, zero_smul,
  Ring.inverse_zero, zero_mul]
State after:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a

State before:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Tactic:
. suffices hn' : IsUnit (n : ℚ) by
    simp only [Algebra.smul_def, ← map_natCast (algebraMap ℚ A)]
    apply symm
    rw [Ring.inverse_mul_eq_iff_eq_mul _ _ _ (RingHom.isUnit_map _ hn'), ← mul_assoc]
    apply symm
    convert @one_mul A _ _
    simp only [← map_mul, ← map_one (algebraMap ℚ A)]
    apply congr_arg
    apply symm
    rw [Ring.eq_mul_inverse_iff_mul_eq _ _ _ hn', one_mul]
  rw [isUnit_iff_ne_zero, ne_eq, Nat.cast_eq_zero]
  exact Nat.ne_of_gt hn
State after:
no goals

State before:
case inl
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n = 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Tactic:
simp only [hn, Nat.cast_zero, isUnit_zero_iff, not_false_eq_true, Ring.inverse_non_unit, zero_smul,
Ring.inverse_zero, zero_mul]
State after:
no goals

State before:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Tactic:
suffices hn' : IsUnit (n : ℚ) by
  simp only [Algebra.smul_def, ← map_natCast (algebraMap ℚ A)]
  apply symm
  rw [Ring.inverse_mul_eq_iff_eq_mul _ _ _ (RingHom.isUnit_map _ hn'), ← mul_assoc]
  apply symm
  convert @one_mul A _ _
  simp only [← map_mul, ← map_one (algebraMap ℚ A)]
  apply congr_arg
  apply symm
  rw [Ring.eq_mul_inverse_iff_mul_eq _ _ _ hn', one_mul]
State after:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ IsUnit ↑n

State before:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ IsUnit ↑n
Tactic:
rw [isUnit_iff_ne_zero, ne_eq, Nat.cast_eq_zero]
State after:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ ¬n = 0

State before:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ ¬n = 0
Tactic:
exact Nat.ne_of_gt hn
State after:
no goals

State before:
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Tactic:
simp only [Algebra.smul_def, ← map_natCast (algebraMap ℚ A)]
State after:
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) (Ring.inverse ↑n) * a = Ring.inverse ((algebraMap ℚ A) ↑n) * a

State before:
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) (Ring.inverse ↑n) * a = Ring.inverse ((algebraMap ℚ A) ↑n) * a
Tactic:
apply symm
State after:
case a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ Ring.inverse ((algebraMap ℚ A) ↑n) * a = (algebraMap ℚ A) (Ring.inverse ↑n) * a

State before:
case a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ Ring.inverse ((algebraMap ℚ A) ↑n) * a = (algebraMap ℚ A) (Ring.inverse ↑n) * a
Tactic:
rw [Ring.inverse_mul_eq_iff_eq_mul _ _ _ (RingHom.isUnit_map _ hn'), ← mul_assoc]
State after:
case a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ a = (algebraMap ℚ A) ↑n * (algebraMap ℚ A) (Ring.inverse ↑n) * a

State before:
case a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ a = (algebraMap ℚ A) ↑n * (algebraMap ℚ A) (Ring.inverse ↑n) * a
Tactic:
apply symm
State after:
case a.a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) ↑n * (algebraMap ℚ A) (Ring.inverse ↑n) * a = a

State before:
case a.a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) ↑n * (algebraMap ℚ A) (Ring.inverse ↑n) * a = a
Tactic:
convert @one_mul A _ _
State after:
case h.e'_2.h.e'_5
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) ↑n * (algebraMap ℚ A) (Ring.inverse ↑n) = 1

State before:
case h.e'_2.h.e'_5
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) ↑n * (algebraMap ℚ A) (Ring.inverse ↑n) = 1
Tactic:
simp only [← map_mul, ← map_one (algebraMap ℚ A)]
State after:
case h.e'_2.h.e'_5
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) (↑n * Ring.inverse ↑n) = (algebraMap ℚ A) 1

State before:
case h.e'_2.h.e'_5
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) (↑n * Ring.inverse ↑n) = (algebraMap ℚ A) 1
Tactic:
apply congr_arg
State after:
case h.e'_2.h.e'_5.h
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ ↑n * Ring.inverse ↑n = 1

State before:
case h.e'_2.h.e'_5.h
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ ↑n * Ring.inverse ↑n = 1
Tactic:
apply symm
State after:
case h.e'_2.h.e'_5.h.a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ 1 = ↑n * Ring.inverse ↑n

State before:
case h.e'_2.h.e'_5.h.a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ 1 = ↑n * Ring.inverse ↑n
Tactic:
rw [Ring.eq_mul_inverse_iff_mul_eq _ _ _ hn', one_mul]
State after:
no goals