awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n_1 n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
ih : gaussSum χ ψ ^ (n + 1) = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
succ :
  jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j) =
    gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
succ₁ :
  jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j) =
    gaussSum (χ ^ (n + 1)) ψ * ((∏ k ∈ Ico (Nat.succ 0) n, jacobiSum χ (χ ^ k)) * jacobiSum χ (χ ^ n))
⊢ gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
have succ₂ : (gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)) * jacobiSum χ (χ ^ n) =
  gaussSum (χ ^ (n + 1)) ψ * ((∏ k ∈ Ico (Nat.succ 0) n, jacobiSum χ (χ ^ k)) * jacobiSum χ (χ ^ n))
Tactic: rw [ih, Finset.prod_Ico_succ_top hn, mul_rotate, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n_1 n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
ih : gaussSum χ ψ ^ (n + 1) = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
succ :
  jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j) =
    gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
succ₁ :
  jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j) =
    gaussSum (χ ^ (n + 1)) ψ * ((∏ k ∈ Ico (Nat.succ 0) n, jacobiSum χ (χ ^ k)) * jacobiSum χ (χ ^ n))
succ₂ :
  (gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)) * jacobiSum χ (χ ^ n) =
    gaussSum (χ ^ (n + 1)) ψ * ((∏ k ∈ Ico (Nat.succ 0) n, jacobiSum χ (χ ^ k)) * jacobiSum χ (χ ^ n))
⊢ gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
have succ₃ : gaussSum (χ ^ (n + 1)) ψ * ((∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)) * jacobiSum χ (χ ^ n)) =
  gaussSum (χ ^ (n + 1)) ψ * ((∏ k ∈ Ico (Nat.succ 0) n, jacobiSum χ (χ ^ k)) * jacobiSum χ (χ ^ n))
Tactic: rw [ih, Finset.prod_Ico_succ_top hn, mul_rotate, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n : ℕ
hn₁ : 0 < n
hn₂ : n < orderOf χ
⊢ gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
have base : ∀ (hn₂ : Nat.succ 0 < orderOf χ),
  gaussSum χ ψ ^ Nat.succ 0 = gaussSum (χ ^ Nat.succ 0) ψ * ∏ j ∈ Ico 1 (Nat.succ 0), jacobiSum χ (χ ^ j)
Tactic: induction n, hn₁ using Nat.le_induction with
  | base => simp only [pow_one, le_refl, Ico_eq_empty_of_le, prod_empty, mul_one]
  | succ n hn ih =>
      specialize ih <| lt_trans (Nat.lt_succ_self n) hn₂
      have gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ =
            jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ := by
        have hχn : χ * (χ ^ n) ≠ 1 :=
          pow_succ' χ n ▸ pow_ne_one_of_lt_orderOf n.add_one_ne_zero hn₂
        rw [mul_comm, ← jacobiSum_mul_nontrivial hχn, mul_comm, ← pow_succ']
      apply_fun (· * gaussSum χ ψ) at ih
      rw [mul_right_comm, ← pow_succ, gauss_rw] at ih
      rw [ih, Finset.prod_Ico_succ_top hn, mul_rotate, mul_assoc]
Cleared hypotheses: hn₁, hn₂
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n : ℕ
hn₁ : 0 < n
hn₂ : n < orderOf χ
base :
  ∀ (hn₂ : Nat.succ 0 < orderOf χ),
    gaussSum χ ψ ^ Nat.succ 0 = gaussSum (χ ^ Nat.succ 0) ψ * ∏ j ∈ Ico 1 (Nat.succ 0), jacobiSum χ (χ ^ j)
⊢ gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
have succ : ∀ (n : ℕ) (hn : Nat.succ 0 ≤ n)
  (ih : ∀ (hn₂ : n < orderOf χ), gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j))
  (hn₂ : n + 1 < orderOf χ),
  gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
Tactic: induction n, hn₁ using Nat.le_induction with
  | base => simp only [pow_one, le_refl, Ico_eq_empty_of_le, prod_empty, mul_one]
  | succ n hn ih =>
      specialize ih <| lt_trans (Nat.lt_succ_self n) hn₂
      have gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ =
            jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ := by
        have hχn : χ * (χ ^ n) ≠ 1 :=
          pow_succ' χ n ▸ pow_ne_one_of_lt_orderOf n.add_one_ne_zero hn₂
        rw [mul_comm, ← jacobiSum_mul_nontrivial hχn, mul_comm, ← pow_succ']
      apply_fun (· * gaussSum χ ψ) at ih
      rw [mul_right_comm, ← pow_succ, gauss_rw] at ih
      rw [ih, Finset.prod_Ico_succ_top hn, mul_rotate, mul_assoc]
Cleared hypotheses: hn₁, hn₂
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
⊢ gaussSum χ ψ ^ orderOf χ =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
have this : gaussSum χ ψ ^ (orderOf χ - 1) = gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j)
Tactic: have := gaussSum_pow_eq_prod_jacobiSum_aux χ ψ (n := orderOf χ - 1) (by lia) (by lia)
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
this :
  gaussSum χ ψ ^ (orderOf χ - 1) = gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j)
⊢ gaussSum χ ψ ^ orderOf χ =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
have this₁ : gaussSum χ ψ * gaussSum χ ψ ^ (orderOf χ - 1) =
  gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
Tactic: apply_fun (gaussSum χ ψ * ·) at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
this :
  gaussSum χ ψ * gaussSum χ ψ ^ (orderOf χ - 1) =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
⊢ gaussSum χ ψ ^ orderOf χ =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
have this₁ : gaussSum χ ψ ^ orderOf χ =
  gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
Tactic: rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos (by lia)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
this :
  gaussSum χ ψ ^ orderOf χ =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
⊢ gaussSum χ ψ ^ orderOf χ =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
have hχ₁ : χ ≠ 1
Tactic: have hχ₁ : χ ≠ 1 :=
    fun h ↦ ((orderOf_one (G := MulChar F R) ▸ h ▸ hχ).trans_lt Nat.one_lt_two).false
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
this :
  gaussSum χ ψ ^ orderOf χ =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
hχ₁ : χ ≠ 1
⊢ gaussSum χ ψ ^ orderOf χ =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
have rw : gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j)) =
  HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
    ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
Tactic: rw [this, ← mul_assoc, gaussSum_mul_gaussSum_pow_orderOf_sub_one hχ₁ hψ]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
this :
  gaussSum χ ψ ^ orderOf χ =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
hχ₁ : χ ≠ 1
rw :
  gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j)) =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
⊢ gaussSum χ ψ ^ orderOf χ =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
have rw₁ : gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j) =
  HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
    ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
Tactic: rw [this, ← mul_assoc, gaussSum_mul_gaussSum_pow_orderOf_sub_one hχ₁ hψ]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
this :
  gaussSum χ ψ ^ orderOf χ =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
hχ₁ : χ ≠ 1
rw :
  gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j)) =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
rw₁ :
  gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j) =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
⊢ gaussSum χ ψ ^ orderOf χ =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
have rw₂ : HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
    ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j) =
  HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
    ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
Tactic: rw [this, ← mul_assoc, gaussSum_mul_gaussSum_pow_orderOf_sub_one hχ₁ hψ]
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ Eq (α := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)})
    (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})
have rw : Eq (α := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)})
  (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)})
Tactic: rw [Algebra.adjoin.powerBasis'_minpoly_gen hx']
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (((quotMapEquivQuotQuotMap hx hx').symm :
          (a : (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}) →
            S ⧸ Ideal.map (algebraMap R S) I)
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}) :
            (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})
          (Polynomial.map (Ideal.Quotient.mk I) Q)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
        ((aeval x : (a : R[X]) → S) Q) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
have a : Eq.{u_1 + 1} (α :=
  HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
  ((quotMapEquivQuotQuotMap hx hx' :
        (a : S ⧸ Ideal.map (algebraMap R S) I) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})
      (((quotMapEquivQuotQuotMap hx hx').symm :
          (a : (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}) →
            S ⧸ Ideal.map (algebraMap R S) I)
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}) :
            (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})
          (Polynomial.map (Ideal.Quotient.mk I) Q))) :
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
  ((quotMapEquivQuotQuotMap hx hx' :
        (a : S ⧸ Ideal.map (algebraMap R S) I) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
        ((aeval x : (a : R[X]) → S) Q)) :
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
Tactic: apply (quotMapEquivQuotQuotMap hx hx').injective
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ Eq.{u_2 + 1} (α :=
    HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
    ((((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.symm :
          (a : (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)}) →
            ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)}) :
            (a : (R ⧸ I)[X]) →
              (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)})
          (Polynomial.map (Ideal.Quotient.mk I) Q)) :
      HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
        (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
    (((quotAdjoinEquivQuotMap hx ⋯).symm :
          (a : S ⧸ Ideal.map (algebraMap R S) I) → ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          ((aeval x : (a : R[X]) → S) Q)) :
      HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
        (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
have h : Eq (α :=
  HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
  (((quotAdjoinEquivQuotMap hx sorry).symm :
        (a : S ⧸ Ideal.map (algebraMap R S) I) → ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
        ((aeval x : (a : R[X]) → S) Q)) :
    HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
  ((Ideal.Quotient.mk (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) :
        (a : ↥R[x]) → ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
      ((aeval (adjoin.powerBasis' hx').gen : (a : R[X]) → ↥R[x]) Q) :
    HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
Tactic: convert! (adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap_symm_apply_mk I Q
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ Eq (α :=
    HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
    (((quotAdjoinEquivQuotMap hx ⋯).symm :
          (a : S ⧸ Ideal.map (algebraMap R S) I) → ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          ((aeval x : (a : R[X]) → S) Q)) :
      HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
        (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
    ((Ideal.Quotient.mk (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) :
          (a : ↥R[x]) → ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
        ((aeval (adjoin.powerBasis' hx').gen : (a : R[X]) → ↥R[x]) Q) :
      HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
        (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
have h : Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
  ((quotAdjoinEquivQuotMap hx sorry : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
      (((quotAdjoinEquivQuotMap hx sorry).symm :
          (a : S ⧸ Ideal.map (algebraMap R S) I) → ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          ((aeval x : (a : R[X]) → S) Q))) :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
  ((quotAdjoinEquivQuotMap hx sorry : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
      ((Ideal.Quotient.mk (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) :
          (a : ↥R[x]) → ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
        ((aeval (adjoin.powerBasis' hx').gen : (a : R[X]) → ↥R[x]) Q)) :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
Tactic: apply (quotAdjoinEquivQuotMap hx
    (FaithfulSMul.algebraMap_injective ((adjoin R {x})) S)).injective
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ Equiv.{u_2 + 1, u_1 + 1}
    (↑{J : Ideal S |
          Membership.mem (γ := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I))
            J} :
      Type u_2)
    (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} : Type u_1)
have refine_1 : Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
Tactic: refine (IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx')
    ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
refine_1 : Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
⊢ Equiv.{u_2 + 1, u_1 + 1}
    (↑{J : Ideal S |
          Membership.mem (γ := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I))
            J} :
      Type u_2)
    (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} : Type u_1)
have refine_2 : Ne (α := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}) ⊥
Tactic: refine (IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx')
    ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
refine_1 : Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
refine_2 : Ne (α := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}) ⊥
⊢ Equiv.{u_2 + 1, u_1 + 1}
    (↑{J : Ideal S |
          Membership.mem (γ := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I))
            J} :
      Type u_2)
    (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} : Type u_1)
have refine_3 : (↑{M : Ideal (R ⧸ I)[X] |
        Membership.mem (γ := Multiset (Ideal (R ⧸ I)[X]))
          (normalizedFactors (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})) M} :
    Type u_1) ≃
  (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} : Type u_1)
Tactic: refine (IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx')
    ?_ ?_).trans ?_