-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_mul_eq_iff (g : F[X]) :
    (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ (f = 0 ∧ g = 0) ∨ IsCoprime f g

Proof state:
case pos.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : f = 0 ∨ g = 0
this :
  ∀ (f g : F[X]),
    f = 0 ∨ g = 0 → f = 0 → ((f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g)
hf : ¬f = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
simpa only [mul_comm, add_comm, and_comm,
  isCoprime_comm] using this g f h.symm (h.resolve_left hf)

Result:
no goals

Proof state:
case neg.refine_2.inl.intro
F : Type u
inst✝ : Field F
h : ¬0 = 0 ∧ ¬0 = 0
⊢ ∀ (a : AlgebraicClosure F), 0 ≠ 0 ∧ (aeval a) 0 = 0 → ∀ (b : AlgebraicClosure F), 0 ≠ 0 ∧ (aeval b) 0 = 0 → a ≠ b

Tactic:
exact (h.1 rfl).elim

Result:
no goals

Proof state:
case neg.refine_2.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
hc : IsCoprime f g
⊢ ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b

Tactic:
rintro x hf _ hg rfl

Result:
case neg.refine_2.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
hc : IsCoprime f g
x : AlgebraicClosure F
hf : f ≠ 0 ∧ (aeval x) f = 0
hg : g ≠ 0 ∧ (aeval x) g = 0
⊢ False

Proof state:
case neg.refine_1.intro
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H : ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b
u : F[X]
hu : Irreducible u
x✝¹ : u ∣ f
x✝ : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
x : AlgebraicClosure F
hx : (aeval x) u = 0
⊢ False

Tactic:
exact H x ⟨h.1, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)⟩
  x ⟨h.2, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hg)⟩ rfl

Result:
no goals

Proof state:
case pos
F : Type u
inst✝ : Field F
f g : F[X]
h : f * g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
rw [mul_eq_zero] at h

Result:
case pos
F : Type u
inst✝ : Field F
f g : F[X]
h : f = 0 ∨ g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Proof state:
case neg.refine_2
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
⊢ f = 0 ∧ g = 0 ∨ IsCoprime f g →
    ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b

Tactic:
rintro (⟨rfl, rfl⟩ | hc)

Result:
case neg.refine_2.inl.intro
F : Type u
inst✝ : Field F
h : ¬0 = 0 ∧ ¬0 = 0
⊢ ∀ (a : AlgebraicClosure F), 0 ≠ 0 ∧ (aeval a) 0 = 0 → ∀ (b : AlgebraicClosure F), 0 ≠ 0 ∧ (aeval b) 0 = 0 → a ≠ b

case neg.refine_2.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
hc : IsCoprime f g
⊢ ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b

Proof state:
case refine_2.inr.intro.intro
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x : F
h : C x = g
⊢ ∃ x, C x = g

Tactic:
exact ⟨x, h⟩

Result:
no goals

Proof state:
case neg.refine_2.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
hc : IsCoprime f g
x : AlgebraicClosure F
hf : f ≠ 0 ∧ (aeval x) f = 0
hg : g ≠ 0 ∧ (aeval x) g = 0
⊢ False

Tactic:
obtain ⟨u, v, hfg⟩ := hc

Result:
case neg.refine_2.inr.intro.intro
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
x : AlgebraicClosure F
hf : f ≠ 0 ∧ (aeval x) f = 0
hg : g ≠ 0 ∧ (aeval x) g = 0
u v : F[X]
hfg : u * f + v * g = 1
⊢ False

Proof state:
case refine_2.inl.intro
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
h : g = 0
⊢ ∃ x, C x = g

Tactic:
exact ⟨0, by rw [h, map_zero]⟩

Result:
no goals

Proof state:
case neg
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x✝ : ∃ x, C x = g
x : F
h : C x = g
hx : ¬x = 0
⊢ 0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g

Tactic:
exact .inr ⟨x, Ne.isUnit hx, h⟩

Result:
no goals

Proof state:
case neg.refine_1
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H : ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b
u : F[X]
hu : Irreducible u
x✝¹ : u ∣ f
x✝ : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
⊢ False

Tactic:
obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero
  (AlgebraicClosure F) _ (degree_pos_of_irreducible hu).ne'

Result:
case neg.refine_1.intro
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H : ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b
u : F[X]
hu : Irreducible u
x✝¹ : u ∣ f
x✝ : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
x : AlgebraicClosure F
hx : (aeval x) u = 0
⊢ False

Proof state:
case neg.refine_2.inr.intro.intro
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
x : AlgebraicClosure F
hf : f ≠ 0 ∧ (aeval x) f = 0
hg : g ≠ 0 ∧ (aeval x) g = 0
u v : F[X]
hfg : u * f + v * g = 1
⊢ False

Tactic:
simpa only [map_add, map_mul, map_one, hf.2, hg.2, mul_zero, add_zero,
  zero_ne_one] using congr(aeval x $hfg)

Result:
no goals

Proof state:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add,
  Finset.card_union_eq_card_add_card, Finset.disjoint_iff_ne, Multiset.mem_toFinset, mem_aroots]

Result:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g

Proof state:
case pos
F : Type u
inst✝ : Field F
f g : F[X]
h : f = 0 ∨ g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
wlog hf : f = 0 generalizing f g

Result:
case pos.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : f = 0 ∨ g = 0
this :
  ∀ (f g : F[X]),
    f = 0 ∨ g = 0 → f = 0 → ((f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g)
hf : ¬f = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Proof state:
F : Type u
inst✝ : Field F
f g : F[X]
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
by_cases h : f * g = 0

Result:
case pos
F : Type u
inst✝ : Field F
f g : F[X]
h : f * g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Proof state:
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
rw [hf, zero_mul, natSepDegree_zero, zero_add, isCoprime_zero_left, isUnit_iff, eq_comm,
  natSepDegree_eq_zero_iff, natDegree_eq_zero]

Result:
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ (∃ x, C x = g) ↔ 0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g

Proof state:
case refine_2
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ (0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g) → ∃ x, C x = g

Tactic:
rintro (⟨-, h⟩ | ⟨x, -, h⟩)

Result:
case refine_2.inl.intro
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
h : g = 0
⊢ ∃ x, C x = g

case refine_2.inr.intro.intro
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x : F
h : C x = g
⊢ ∃ x, C x = g