case inl
R : Type u_3
inst✝⁸ : CommRing R
A : Type ?u.578634
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module A M
inst✝³ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a b : A
K : Type u_1
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
⊢ ↑D 0⁻¹ = -0⁻¹ ^ 2 • ↑D 0

case inr
R : Type u_3
inst✝⁸ : CommRing R
A : Type ?u.578634
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module A M
inst✝³ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b : A
K : Type u_1
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
ha : a ≠ 0
⊢ ↑D a⁻¹ = -a⁻¹ ^ 2 • ↑D a
R : Type u_3
inst✝⁸ : CommRing R
A : Type ?u.578634
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module A M
inst✝³ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b : A
K : Type u_1
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
⊢ ↑D a⁻¹ = -a⁻¹ ^ 2 • ↑D a
rcases eq_or_ne a 0 with (rfl | ha)
no goals
case inl
R : Type u_3
inst✝⁸ : CommRing R
A : Type ?u.578634
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module A M
inst✝³ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a b : A
K : Type u_1
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
⊢ ↑D 0⁻¹ = -0⁻¹ ^ 2 • ↑D 0
simp
no goals
case inr
R : Type u_3
inst✝⁸ : CommRing R
A : Type ?u.578634
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module A M
inst✝³ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b : A
K : Type u_1
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
ha : a ≠ 0
⊢ ↑D a⁻¹ = -a⁻¹ ^ 2 • ↑D a
exact D.leibniz_of_mul_eq_one (inv_mul_cancel ha)