-- Mathlib/FieldTheory/Separable.lean
theorem _root_.Associated.separable {f g : R[X]}
    (ha : Associated f g) (h : f.Separable) : g.Separable

Proof state:
case intro.mk.intro.intro
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : (a * f + b * derivative f) * (u * v) = 1 * 1
⊢ (a * v + b * derivative v) * g + b * v * derivative g = 1

Tactic:
have h3 := congr(derivative $(h1))

Result:
case intro.mk.intro.intro
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : (a * f + b * derivative f) * (u * v) = 1 * 1
h3 : derivative (u * v) = derivative 1
⊢ (a * v + b * derivative v) * g + b * v * derivative g = 1

Proof state:
case intro.mk.intro.intro
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : (a * f + b * derivative f) * (u * v) = 1 * 1
h3 : derivative (u * v) = derivative 1
⊢ (a * v + b * derivative v) * g + b * v * derivative g = 1

Tactic:
simp only [← ha, derivative_mul, derivative_one] at h3 ⊢

Result:
case intro.mk.intro.intro
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : (a * f + b * derivative f) * (u * v) = 1 * 1
h3 : derivative u * v + u * derivative v = 0
⊢ (a * v + b * derivative v) * (f * u) + b * v * (derivative f * u + f * derivative u) = 1

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
ha : Associated f g
h : f.Separable
⊢ g.Separable

Tactic:
obtain ⟨⟨u, v, h1, h2⟩, ha⟩ := ha

Result:
case intro.mk
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : f.Separable
u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
⊢ g.Separable

Proof state:
case intro.mk
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : f.Separable
u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
⊢ g.Separable

Tactic:
obtain ⟨a, b, h⟩ := h

Result:
case intro.mk.intro.intro
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : a * f + b * derivative f = 1
⊢ g.Separable

Proof state:
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : (a * f + b * derivative f) * (u * v) = 1 * 1
h3 : derivative u * v + u * derivative v = 0
⊢ (a * f + b * derivative f) * (u * v) + b * f * (derivative u * v + u * derivative v) = 1

Tactic:
rw [h, h3]

Result:
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : (a * f + b * derivative f) * (u * v) = 1 * 1
h3 : derivative u * v + u * derivative v = 0
⊢ 1 * 1 + b * f * 0 = 1

Proof state:
case intro.mk.intro.intro
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : (a * f + b * derivative f) * (u * v) = 1 * 1
h3 : derivative u * v + u * derivative v = 0
⊢ (a * v + b * derivative v) * (f * u) + b * v * (derivative f * u + f * derivative u) = 1

Tactic:
calc
  _ = (a * f + b * derivative f) * (u * v)
    + (b * f) * (derivative u * v + u * derivative v) := by ring1
  _ = 1 := by rw [h, h3]; ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : (a * f + b * derivative f) * (u * v) = 1 * 1
h3 : derivative u * v + u * derivative v = 0
⊢ 1 * 1 + b * f * 0 = 1

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : (a * f + b * derivative f) * (u * v) = 1 * 1
h3 : derivative u * v + u * derivative v = 0
⊢ (a * v + b * derivative v) * (f * u) + b * v * (derivative f * u + f * derivative u) =
    (a * f + b * derivative f) * (u * v) + b * f * (derivative u * v + u * derivative v)

Tactic:
ring1

Result:
no goals

Proof state:
case intro.mk.intro.intro
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : a * f + b * derivative f = 1
⊢ g.Separable

Tactic:
refine ⟨a * v + b * derivative v, b * v, ?_⟩

Result:
case intro.mk.intro.intro
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : a * f + b * derivative f = 1
⊢ (a * v + b * derivative v) * g + b * v * derivative g = 1

Proof state:
case intro.mk.intro.intro
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : a * f + b * derivative f = 1
⊢ (a * v + b * derivative v) * g + b * v * derivative g = 1

Tactic:
replace h := congr($h * $(h1))

Result:
case intro.mk.intro.intro
R : Type u
inst✝ : CommSemiring R
f g u v : R[X]
h1 : u * v = 1
h2 : v * u = 1
ha : f * ↑{ val := u, inv := v, val_inv := h1, inv_val := h2 } = g
a b : R[X]
h : (a * f + b * derivative f) * (u * v) = 1 * 1
⊢ (a * v + b * derivative v) * g + b * v * derivative g = 1