Theorem: coe_mul_inv_eq_one'' (AlgebraI/Subgroups.lean)

State before:
n : ℕ
x : ℤ
h : IsCoprime x ↑n
⊢ ↑x * (↑x)⁻¹ = 1
Tactic:
cases n with
| zero =>
  simp [isCoprime_zero_right] at h
  rw [ZMod.mul_inv_eq_gcd, Nat.gcd_zero_right, Nat.cast_eq_one]
  simp only [ZMod.val]
  rw [Int.cast_id, Int.IsUnit.natAbs_eq h]
| succ n =>
  haveI := n.succ_pos
  rw [← Int.gcd_eq_one_iff_coprime, Int.gcd_comm, Int.gcd_val] at h
  rw [ZMod.mul_inv_eq_gcd, ← Int.coe_nat_gcd, ZMod.val_int_cast, h, Nat.cast_one]
State after:
no goals

State before:
case zero
x : ℤ
h : IsCoprime x ↑Nat.zero
⊢ ↑x * (↑x)⁻¹ = 1
Tactic:
simp [isCoprime_zero_right] at h
State after:
case zero
x : ℤ
h : IsUnit x
⊢ ↑x * (↑x)⁻¹ = 1

State before:
case zero
x : ℤ
h : IsUnit x
⊢ ↑x * (↑x)⁻¹ = 1
Tactic:
rw [ZMod.mul_inv_eq_gcd, Nat.gcd_zero_right, Nat.cast_eq_one]
State after:
case zero
x : ℤ
h : IsUnit x
⊢ ZMod.val ↑x = 1

State before:
case zero
x : ℤ
h : IsUnit x
⊢ ZMod.val ↑x = 1
Tactic:
simp only [ZMod.val]
State after:
case zero
x : ℤ
h : IsUnit x
⊢ Int.natAbs ↑x = 1

State before:
case zero
x : ℤ
h : IsUnit x
⊢ Int.natAbs ↑x = 1
Tactic:
rw [Int.cast_id, Int.IsUnit.natAbs_eq h]
State after:
no goals

State before:
case succ
x : ℤ
n : ℕ
h : IsCoprime x ↑(Nat.succ n)
⊢ ↑x * (↑x)⁻¹ = 1
Tactic:
haveI := n.succ_pos
State after:
case succ
x : ℤ
n : ℕ
h : IsCoprime x ↑(Nat.succ n)
this : 0 < Nat.succ n
⊢ ↑x * (↑x)⁻¹ = 1

State before:
case succ
x : ℤ
n : ℕ
h : IsCoprime x ↑(Nat.succ n)
this : 0 < Nat.succ n
⊢ ↑x * (↑x)⁻¹ = 1
Tactic:
rw [← Int.gcd_eq_one_iff_coprime, Int.gcd_comm, Int.gcd_val] at h
State after:
case succ
x : ℤ
n : ℕ
h : Int.gcd (x % ↑(Nat.succ n)) ↑(Nat.succ n) = 1
this : 0 < Nat.succ n
⊢ ↑x * (↑x)⁻¹ = 1

State before:
case succ
x : ℤ
n : ℕ
h : Int.gcd (x % ↑(Nat.succ n)) ↑(Nat.succ n) = 1
this : 0 < Nat.succ n
⊢ ↑x * (↑x)⁻¹ = 1
Tactic:
rw [ZMod.mul_inv_eq_gcd, ← Int.coe_nat_gcd, ZMod.val_int_cast, h, Nat.cast_one]
State after:
no goals