awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH : ∀ (q : R[X]), q.resultant q = HPow.hPow (α := R) 0 q.natDegree
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
surjective : (map φ f').resultant (map φ f') = HPow.hPow (α := S) 0 (map φ f').natDegree
surjective₁ :
  (φ : (a : R) → S) (f'.resultant f' (map φ f').natDegree (map φ f').natDegree) =
    HPow.hPow (α := S) 0 (map φ f').natDegree
surjective₂ : (φ : (a : R) → S) (f'.resultant f' f.natDegree f.natDegree) = HPow.hPow (α := S) 0 f.natDegree
surjective₃ : (φ : (a : R) → S) (f'.resultant f') = HPow.hPow (α := S) 0 f'.natDegree
⊢ f.resultant f = HPow.hPow (α := S) 0 f.natDegree
have surjective₄ : (φ : (a : R) → S) (HPow.hPow (α := R) 0 f'.natDegree) = HPow.hPow (α := S) 0 f'.natDegree
Tactic: rw [← hf', resultant_map_map, hf', ← natDegree_eq_natDegree e, IH f', map_pow, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH : ∀ (q : R[X]), q.resultant q = HPow.hPow (α := R) 0 q.natDegree
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
surjective : (map φ f').resultant (map φ f') = HPow.hPow (α := S) 0 (map φ f').natDegree
surjective₁ :
  (φ : (a : R) → S) (f'.resultant f' (map φ f').natDegree (map φ f').natDegree) =
    HPow.hPow (α := S) 0 (map φ f').natDegree
surjective₂ : (φ : (a : R) → S) (f'.resultant f' f.natDegree f.natDegree) = HPow.hPow (α := S) 0 f.natDegree
surjective₃ : (φ : (a : R) → S) (f'.resultant f') = HPow.hPow (α := S) 0 f'.natDegree
surjective₄ : (φ : (a : R) → S) (HPow.hPow (α := R) 0 f'.natDegree) = HPow.hPow (α := S) 0 f'.natDegree
⊢ f.resultant f = HPow.hPow (α := S) 0 f.natDegree
have surjective₅ : HPow.hPow (α := S) ((φ : (a : R) → S) 0 : S) f'.natDegree = HPow.hPow (α := S) 0 f'.natDegree
Tactic: rw [← hf', resultant_map_map, hf', ← natDegree_eq_natDegree e, IH f', map_pow, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH : ∀ (q : R[X]), q.resultant q = HPow.hPow (α := R) 0 q.natDegree
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
surjective : (map φ f').resultant (map φ f') = HPow.hPow (α := S) 0 (map φ f').natDegree
surjective₁ :
  (φ : (a : R) → S) (f'.resultant f' (map φ f').natDegree (map φ f').natDegree) =
    HPow.hPow (α := S) 0 (map φ f').natDegree
surjective₂ : (φ : (a : R) → S) (f'.resultant f' f.natDegree f.natDegree) = HPow.hPow (α := S) 0 f.natDegree
surjective₃ : (φ : (a : R) → S) (f'.resultant f') = HPow.hPow (α := S) 0 f'.natDegree
surjective₄ : (φ : (a : R) → S) (HPow.hPow (α := R) 0 f'.natDegree) = HPow.hPow (α := S) 0 f'.natDegree
surjective₅ : HPow.hPow (α := S) ((φ : (a : R) → S) 0 : S) f'.natDegree = HPow.hPow (α := S) 0 f'.natDegree
⊢ f.resultant f = HPow.hPow (α := S) 0 f.natDegree
have surjective₆ : HPow.hPow (α := S) 0 f'.natDegree = HPow.hPow (α := S) 0 f'.natDegree
Tactic: rw [← hf', resultant_map_map, hf', ← natDegree_eq_natDegree e, IH f', map_pow, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ f.resultant f = HPow.hPow (α := R) 0 f.natDegree
have Splits : ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hf : f.Splits), f.resultant f = HPow.hPow (α := R) 0 f.natDegree
Tactic: induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hf =>
    by_cases h : f.natDegree = 0
    · obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp h; simp
    rw [resultant_eq_prod_eval _ _ _ le_rfl hf]
    simp [zero_pow h, h, hf.exists_eval_eq_zero (degree_ne_of_natDegree_ne h), eq_or_ne f]
  | injective R S φ hφ f IH =>
    apply hφ
    simpa only [resultant_map_map, natDegree_map_eq_of_injective hφ, map_zero, map_pow] using IH
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    rw [← hf', resultant_map_map, hf', ← natDegree_eq_natDegree e, IH f', map_pow, map_zero]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
Splits : ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hf : f.Splits), f.resultant f = HPow.hPow (α := R) 0 f.natDegree
⊢ f.resultant f = HPow.hPow (α := R) 0 f.natDegree
have injective : ∀ (R S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
  (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (f : R[X])
  (IH : (map φ f).resultant (map φ f) = HPow.hPow (α := S) 0 (map φ f).natDegree),
  f.resultant f = HPow.hPow (α := R) 0 f.natDegree
Tactic: induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hf =>
    by_cases h : f.natDegree = 0
    · obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp h; simp
    rw [resultant_eq_prod_eval _ _ _ le_rfl hf]
    simp [zero_pow h, h, hf.exists_eval_eq_zero (degree_ne_of_natDegree_ne h), eq_or_ne f]
  | injective R S φ hφ f IH =>
    apply hφ
    simpa only [resultant_map_map, natDegree_map_eq_of_injective hφ, map_zero, map_pow] using IH
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    rw [← hf', resultant_map_map, hf', ← natDegree_eq_natDegree e, IH f', map_pow, map_zero]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
Splits : ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hf : f.Splits), f.resultant f = HPow.hPow (α := R) 0 f.natDegree
injective :
  ∀ (R S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (f : R[X])
    (IH : (map φ f).resultant (map φ f) = HPow.hPow (α := S) 0 (map φ f).natDegree),
    f.resultant f = HPow.hPow (α := R) 0 f.natDegree
⊢ f.resultant f = HPow.hPow (α := R) 0 f.natDegree
have surjective : ∀ (R S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
  (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (f : S[X])
  (IH : ∀ (q : R[X]), q.resultant q = HPow.hPow (α := R) 0 q.natDegree),
  f.resultant f = HPow.hPow (α := S) 0 f.natDegree
Tactic: induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hf =>
    by_cases h : f.natDegree = 0
    · obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp h; simp
    rw [resultant_eq_prod_eval _ _ _ le_rfl hf]
    simp [zero_pow h, h, hf.exists_eval_eq_zero (degree_ne_of_natDegree_ne h), eq_or_ne f]
  | injective R S φ hφ f IH =>
    apply hφ
    simpa only [resultant_map_map, natDegree_map_eq_of_injective hφ, map_zero, map_pow] using IH
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    rw [← hf', resultant_map_map, hf', ← natDegree_eq_natDegree e, IH f', map_pow, map_zero]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have inl : ∀ (H : IsCoprime 0 g), ∃ (n : ℕ), resultant 0 g ∣ HPow.hPow (α := R) (leadingCoeff 0) n
Tactic: obtain rfl | hf := eq_or_ne f 0
Cleared hypotheses: f, H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
inl : ∀ (H : IsCoprime 0 g), ∃ (n : ℕ), resultant 0 g ∣ HPow.hPow (α := R) (leadingCoeff 0) n
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have inr : ∀ (hf : f ≠ 0), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
Tactic: obtain rfl | hf := eq_or_ne f 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
H : IsCoprime 0 g
⊢ ∃ (n : ℕ), resultant 0 g ∣ HPow.hPow (α := R) (leadingCoeff 0) n
have H₁ : ∃ (r : R), IsUnit r ∧ (C : (a : R) → R[X]) r = g
Tactic: simp only [isCoprime_zero_left, isUnit_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have inr : ∀ (H : IsCoprime f 0), ∃ (n : ℕ), f.resultant 0 ∣ f.leadingCoeff ^ n
Tactic: obtain rfl | hg := eq_or_ne g 0
Cleared hypotheses: g, H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
inr : ∀ (H : IsCoprime f 0), ∃ (n : ℕ), f.resultant 0 ∣ f.leadingCoeff ^ n
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have inr₁ : ∀ (hg : g ≠ 0), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
Tactic: obtain rfl | hg := eq_or_ne g 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
hf : f ≠ 0
H : IsCoprime f 0
⊢ ∃ (n : ℕ), f.resultant 0 ∣ f.leadingCoeff ^ n
have H₁ : ∃ (r : R), IsUnit r ∧ (C : (a : R) → R[X]) r = f
Tactic: simp only [isCoprime_zero_right, isUnit_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have inr : ∀ (a b : R[X]) (e : a * f + b * g = 1), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
Tactic: have ⟨a, b, e⟩ := H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have inr : ∀ (e : 0 * f + b * g = 1), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a, e
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
inr : ∀ (e : 0 * f + b * g = 1), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have inr₁ : ∀ (ha : a ≠ 0), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
b : R[X]
e : 0 * f + b * g = 1
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have inr : ∀ (r : R) (hr : IsUnit r) (H : IsCoprime f ((C : (a : R) → R[X]) r))
  (hg : Ne (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]))
  (e : 0 * f + HMul.hMul (β := R[X]) b ((C : (a : R) → R[X]) r : R[X]) = 1),
  ∃ (n : ℕ), f.resultant ((C : (a : R) → R[X]) r) ∣ f.leadingCoeff ^ n
Tactic: obtain ⟨r, hr, rfl⟩ := isUnit_iff.mp (.of_mul_eq_one_right b (by simpa using e))
Cleared hypotheses: g, H, hg, e
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have inr : ∀ (e : a * f + 0 * g = 1), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b, e
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
inr : ∀ (e : a * f + 0 * g = 1), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have inr₁ : ∀ (hb : b ≠ 0), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a : R[X]
ha : a ≠ 0
e : a * f + 0 * g = 1
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have inr : ∀ (r : R) (hr : IsUnit r) (H : IsCoprime ((C : (a : R) → R[X]) r) g)
  (hf : Ne (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]))
  (e : HMul.hMul (β := R[X]) a ((C : (a : R) → R[X]) r : R[X]) + 0 * g = 1),
  ∃ (n : ℕ), resultant ((C : (a : R) → R[X]) r) g ∣ HPow.hPow (α := R) (leadingCoeff ((C : (a : R) → R[X]) r)) n
Tactic: obtain ⟨r, hr, rfl⟩ := isUnit_iff.mp (.of_mul_eq_one_right a (by simpa using e))
Cleared hypotheses: f, H, hf, e
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
Tactic: have := resultant_mul_right f b g _ le_rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have inr : ∀ (this : f.coeff f.natDegree ^ (b.natDegree + g.natDegree) = f.resultant b * f.resultant g),
  ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
Tactic: rw [← resultant_add_mul_right _ _ a _ _ _ le_rfl, add_comm, mul_comm f, e,
    resultant_one_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
inr :
  ∀ (this : f.coeff f.natDegree ^ (b.natDegree + g.natDegree) = f.resultant b * f.resultant g),
    ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
have rw : a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree
Tactic: rw [← resultant_add_mul_right _ _ a _ _ _ le_rfl, add_comm, mul_comm f, e,
    resultant_one_right] at this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree
have by_contra! : ∀ (H : b.natDegree + g.natDegree < a.natDegree + f.natDegree), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H_1 : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
H : b.natDegree + g.natDegree < a.natDegree + f.natDegree
⊢ False
have H₁ : (b * g).natDegree < (a * f).natDegree
Tactic: rw [← natDegree_mul ha hf, ← natDegree_mul hb hg] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H_1 : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
H : (b * g).natDegree < (a * f).natDegree
⊢ False
have this₁ : (a * f + b * g).natDegree = (a * f).natDegree
Tactic: have := natDegree_add_eq_left_of_natDegree_lt H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H_1 : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this_1 : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
H : (b * g).natDegree < (a * f).natDegree
this : (a * f + b * g).natDegree = (a * f).natDegree
⊢ False
have this₁ : 0 = (a * f).natDegree
Tactic: simp only [e, natDegree_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
⊢ f.resultant g ≠ 0
have inl : ∀ (H : IsCoprime 0 g), resultant 0 g ≠ 0
Tactic: obtain rfl | hf := eq_or_ne f 0
Cleared hypotheses: f, H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
inl : ∀ (H : IsCoprime 0 g), resultant 0 g ≠ 0
⊢ f.resultant g ≠ 0
have inr : ∀ (hf : f ≠ 0), f.resultant g ≠ 0
Tactic: obtain rfl | hf := eq_or_ne f 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
H : IsCoprime 0 g
⊢ resultant 0 g ≠ 0
have H₁ : ∃ (r : R), IsUnit r ∧ (C : (a : R) → R[X]) r = g
Tactic: simp only [isCoprime_zero_left, isUnit_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
f : ι → R[X]
g : R[X]
n : ℕ
hn : g.natDegree ≤ n
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∀ (hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0),
    resultant (∏ i ∈ s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ s, f i)) n =
      ∏ i ∈ s, (f i).resultant g (f i).natDegree n
hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ insert a s, (f i).leadingCoeff) 0
⊢ resultant (∏ i ∈ insert a s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ insert a s, f i)) n =
    ∏ i ∈ insert a s, (f i).resultant g (f i).natDegree n
have hf' : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
Tactic: have hf' : ∏ i ∈ s, (f i).leadingCoeff ≠ 0 := by aesop
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
f : ι → R[X]
g : R[X]
n : ℕ
hn : g.natDegree ≤ n
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∀ (hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0),
    resultant (∏ i ∈ s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ s, f i)) n =
      ∏ i ∈ s, (f i).resultant g (f i).natDegree n
hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ insert a s, (f i).leadingCoeff) 0
hf' : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
⊢ resultant (∏ i ∈ insert a s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ insert a s, f i)) n =
    ∏ i ∈ insert a s, (f i).resultant g (f i).natDegree n
have insert : (f a * ∏ x ∈ s, f x).resultant g (f a * ∏ x ∈ s, f x).natDegree n =
  ∏ i ∈ insert a s, (f i).resultant g (f i).natDegree n
Tactic: rw [Finset.prod_insert has, natDegree_mul' (by simpa [*, leadingCoeff_prod'] using hf),
      resultant_mul_left _ _ _ _ hn, IH hf', Finset.prod_insert has]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
f : ι → R[X]
g : R[X]
n : ℕ
hn : g.natDegree ≤ n
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∀ (hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0),
    resultant (∏ i ∈ s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ s, f i)) n =
      ∏ i ∈ s, (f i).resultant g (f i).natDegree n
hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ Insert.insert a s, (f i).leadingCoeff) 0
hf' : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
insert :
  (f a * ∏ x ∈ s, f x).resultant g (f a * ∏ x ∈ s, f x).natDegree n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
⊢ resultant (∏ i ∈ Insert.insert a s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ Insert.insert a s, f i)) n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
have insert₁ : (f a * ∏ x ∈ s, f x).resultant g ((f a).natDegree + natDegree.{u_1} (R := R) (∏ x ∈ s, f x)) n =
  ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
Tactic: rw [Finset.prod_insert has, natDegree_mul' (by simpa [*, leadingCoeff_prod'] using hf),
      resultant_mul_left _ _ _ _ hn, IH hf', Finset.prod_insert has]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
f : ι → R[X]
g : R[X]
n : ℕ
hn : g.natDegree ≤ n
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∀ (hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0),
    resultant (∏ i ∈ s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ s, f i)) n =
      ∏ i ∈ s, (f i).resultant g (f i).natDegree n
hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ Insert.insert a s, (f i).leadingCoeff) 0
hf' : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
insert :
  (f a * ∏ x ∈ s, f x).resultant g (f a * ∏ x ∈ s, f x).natDegree n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
insert₁ :
  (f a * ∏ x ∈ s, f x).resultant g ((f a).natDegree + natDegree.{u_1} (R := R) (∏ x ∈ s, f x)) n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
⊢ resultant (∏ i ∈ Insert.insert a s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ Insert.insert a s, f i)) n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
have insert₂ : (f a).resultant g (f a).natDegree n * resultant (∏ x ∈ s, f x) g (natDegree.{u_1} (R := R) (∏ x ∈ s, f x)) n =
  ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
Tactic: rw [Finset.prod_insert has, natDegree_mul' (by simpa [*, leadingCoeff_prod'] using hf),
      resultant_mul_left _ _ _ _ hn, IH hf', Finset.prod_insert has]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
f : ι → R[X]
g : R[X]
n : ℕ
hn : g.natDegree ≤ n
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∀ (hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0),
    resultant (∏ i ∈ s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ s, f i)) n =
      ∏ i ∈ s, (f i).resultant g (f i).natDegree n
hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ Insert.insert a s, (f i).leadingCoeff) 0
hf' : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
insert :
  (f a * ∏ x ∈ s, f x).resultant g (f a * ∏ x ∈ s, f x).natDegree n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
insert₁ :
  (f a * ∏ x ∈ s, f x).resultant g ((f a).natDegree + natDegree.{u_1} (R := R) (∏ x ∈ s, f x)) n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
insert₂ :
  (f a).resultant g (f a).natDegree n * resultant (∏ x ∈ s, f x) g (natDegree.{u_1} (R := R) (∏ x ∈ s, f x)) n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
⊢ resultant (∏ i ∈ Insert.insert a s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ Insert.insert a s, f i)) n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
have insert₃ : (f a).resultant g (f a).natDegree n * ∏ i ∈ s, (f i).resultant g (f i).natDegree n =
  ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
Tactic: rw [Finset.prod_insert has, natDegree_mul' (by simpa [*, leadingCoeff_prod'] using hf),
      resultant_mul_left _ _ _ _ hn, IH hf', Finset.prod_insert has]