awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_6
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
f g : AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1) →ₐ[R] S
rw :
  HMul.hMul (α := S) (β := S)
      ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
          ((algebraMap R (AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
                (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
              r :
            AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
        S)
      ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
        S) =
    1
rw₁ :
  Eq.{u_6 + 1} (α := S)
    ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
        (HMul.hMul (α := AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          ((algebraMap R (AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
                (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
              r :
            AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))) :
      S)
    (1 : S)
rw₂ :
  Eq.{u_6 + 1} (α := S)
    ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
        (HMul.hMul (α := AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          ((of (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1) :
                (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
              r :
            AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))) :
      S)
    (1 : S)
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r : S)
      ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
        S) =
    1
have rw₃ : Eq.{u_6 + 1} (α := S) ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S) 1 : S) (1 : S)
Tactic: rw [← g.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_6
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
f g : AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1) →ₐ[R] S
rw :
  HMul.hMul (α := S) (β := S)
      ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
          ((algebraMap R (AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
                (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
              r :
            AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
        S)
      ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
        S) =
    1
rw₁ :
  Eq.{u_6 + 1} (α := S)
    ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
        (HMul.hMul (α := AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          ((algebraMap R (AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
                (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
              r :
            AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))) :
      S)
    (1 : S)
rw₂ :
  Eq.{u_6 + 1} (α := S)
    ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
        (HMul.hMul (α := AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          ((of (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1) :
                (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
              r :
            AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))) :
      S)
    (1 : S)
rw₃ : Eq.{u_6 + 1} (α := S) ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S) 1 : S) (1 : S)
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r : S)
      ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
        S) =
    1
have rw₄ : Eq.{u_6 + 1} (α := S) 1 1
Tactic: rw [← g.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
⊢ (map g q r hg).comp (map f p q hf) = map (g.comp f) p r ⋯
have hAlg : ∀ (x : R),
  Eq.{u_3 + 1} (α := AdjoinRoot r)
    ((((map g q r hg).comp (map f p q hf)).comp (of p) : (a : R) → AdjoinRoot r) x : AdjoinRoot r)
    (((map (g.comp f) p r sorry).comp (of p) : (a : R) → AdjoinRoot r) x : AdjoinRoot r)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
hAlg :
  ∀ (x : R),
    Eq.{u_3 + 1} (α := AdjoinRoot r)
      ((((map g q r hg).comp (map f p q hf)).comp (of p) : (a : R) → AdjoinRoot r) x : AdjoinRoot r)
      (((map (g.comp f) p r ⋯).comp (of p) : (a : R) → AdjoinRoot r) x : AdjoinRoot r)
⊢ (map g q r hg).comp (map f p q hf) = map (g.comp f) p r ⋯
have hRoot : Eq.{u_3 + 1} (α := AdjoinRoot r)
  (((map g q r hg).comp (map f p q hf) : (a : AdjoinRoot p) → AdjoinRoot r) (root p) : AdjoinRoot r)
  ((map (g.comp f) p r sorry : (a : AdjoinRoot p) → AdjoinRoot r) (root p) : AdjoinRoot r)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
⊢ (map (↑f : R →+* S) p q ⋯).comp (map (↑f.symm : S →+* R) q p ⋯) = RingHom.id (AdjoinRoot q)
have hAlg : ∀ (x : S),
  Eq (α := AdjoinRoot q)
    ((((map (↑f : R →+* S) p q sorry).comp (map (↑f.symm : S →+* R) q p sorry)).comp (of q) : (a : S) → AdjoinRoot q) x :
      AdjoinRoot q)
    ((RingHom.comp (RingHom.id (AdjoinRoot q)) (of q) : (a : S) → AdjoinRoot q) x : AdjoinRoot q)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
hAlg :
  ∀ (x : S),
    Eq (α := AdjoinRoot q)
      ((((map (↑f : R →+* S) p q ⋯).comp (map (↑f.symm : S →+* R) q p ⋯)).comp (of q) : (a : S) → AdjoinRoot q) x :
        AdjoinRoot q)
      ((RingHom.comp (RingHom.id (AdjoinRoot q)) (of q) : (a : S) → AdjoinRoot q) x : AdjoinRoot q)
⊢ (map (↑f : R →+* S) p q ⋯).comp (map (↑f.symm : S →+* R) q p ⋯) = RingHom.id (AdjoinRoot q)
have hRoot : Eq (α := AdjoinRoot q)
  (((map (↑f : R →+* S) p q sorry).comp (map (↑f.symm : S →+* R) q p sorry) : (a : AdjoinRoot q) → AdjoinRoot q) (root q) :
    AdjoinRoot q)
  ((RingHom.id (AdjoinRoot q) : (a : AdjoinRoot q) → AdjoinRoot q) (root q) : AdjoinRoot q)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
⊢ (map (↑f.symm : S →+* R) q p ⋯).comp (map (↑f : R →+* S) p q ⋯) = RingHom.id (AdjoinRoot p)
have hAlg : ∀ (x : R),
  Eq (α := AdjoinRoot p)
    ((((map (↑f.symm : S →+* R) q p sorry).comp (map (↑f : R →+* S) p q sorry)).comp (of p) : (a : R) → AdjoinRoot p) x :
      AdjoinRoot p)
    ((RingHom.comp (RingHom.id (AdjoinRoot p)) (of p) : (a : R) → AdjoinRoot p) x : AdjoinRoot p)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
hAlg :
  ∀ (x : R),
    Eq (α := AdjoinRoot p)
      ((((map (↑f.symm : S →+* R) q p ⋯).comp (map (↑f : R →+* S) p q ⋯)).comp (of p) : (a : R) → AdjoinRoot p) x :
        AdjoinRoot p)
      ((RingHom.comp (RingHom.id (AdjoinRoot p)) (of p) : (a : R) → AdjoinRoot p) x : AdjoinRoot p)
⊢ (map (↑f.symm : S →+* R) q p ⋯).comp (map (↑f : R →+* S) p q ⋯) = RingHom.id (AdjoinRoot p)
have hRoot : Eq (α := AdjoinRoot p)
  (((map (↑f.symm : S →+* R) q p sorry).comp (map (↑f : R →+* S) p q sorry) : (a : AdjoinRoot p) → AdjoinRoot p) (root p) :
    AdjoinRoot p)
  ((RingHom.id (AdjoinRoot p) : (a : AdjoinRoot p) → AdjoinRoot p) (root p) : AdjoinRoot p)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
⊢ Eq (α := S →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.toRingEquiv.symm : T →+* S) (↑f : S →+* T))
    (RingHom.id S)
have a₁ : ∀ (x : S),
  Eq (α := S)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.toRingEquiv.symm : T →+* S) (↑f : S →+* T) : (a : S) → S)
        x :
      S)
    ((RingHom.id S : (a : S) → S) x : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
⊢ p ∣ Polynomial.map (↑(↑f.symm : T →ₐ[R] S) : T →+* S) q
have this : Eq (α := S →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.toRingEquiv.symm : T →+* S) (↑f : S →+* T))
  (RingHom.id S)
Tactic: have : (RingHomClass.toRingHom f.toRingEquiv.symm).comp (RingHomClass.toRingHom f) =
        .id S := by ext; exact f.symm_apply_apply _
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
⊢ (mapAlgHom (↑f : S →ₐ[R] T) p q ⋯).comp (mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯) = AlgHom.id R (AdjoinRoot q)
have hAlg : ∀ (x : T),
  Eq (α := AdjoinRoot q)
    ((((mapAlgHom (↑f : S →ₐ[R] T) p q sorry).comp (mapAlgHom (↑f.symm : T →ₐ[R] S) q p sorry)).comp (ofAlgHom R q) :
          (a : T) → AdjoinRoot q)
        x :
      AdjoinRoot q)
    ((AlgHom.comp (AlgHom.id R (AdjoinRoot q)) (ofAlgHom R q) : (a : T) → AdjoinRoot q) x : AdjoinRoot q)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
hAlg :
  ∀ (x : T),
    Eq (α := AdjoinRoot q)
      ((((mapAlgHom (↑f : S →ₐ[R] T) p q ⋯).comp (mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯)).comp (ofAlgHom R q) :
            (a : T) → AdjoinRoot q)
          x :
        AdjoinRoot q)
      ((AlgHom.comp (AlgHom.id R (AdjoinRoot q)) (ofAlgHom R q) : (a : T) → AdjoinRoot q) x : AdjoinRoot q)
⊢ (mapAlgHom (↑f : S →ₐ[R] T) p q ⋯).comp (mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯) = AlgHom.id R (AdjoinRoot q)
have hRoot : Eq (α := AdjoinRoot q)
  (((mapAlgHom (↑f : S →ₐ[R] T) p q sorry).comp (mapAlgHom (↑f.symm : T →ₐ[R] S) q p sorry) : (a : AdjoinRoot q) → AdjoinRoot q)
      (root q) :
    AdjoinRoot q)
  ((AlgHom.id R (AdjoinRoot q) : (a : AdjoinRoot q) → AdjoinRoot q) (root q) : AdjoinRoot q)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
⊢ (mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯).comp (mapAlgHom (↑f : S →ₐ[R] T) p q ⋯) = AlgHom.id R (AdjoinRoot p)
have hAlg : ∀ (x : S),
  Eq (α := AdjoinRoot p)
    ((((mapAlgHom (↑f.symm : T →ₐ[R] S) q p sorry).comp (mapAlgHom (↑f : S →ₐ[R] T) p q sorry)).comp (ofAlgHom R p) :
          (a : S) → AdjoinRoot p)
        x :
      AdjoinRoot p)
    ((AlgHom.comp (AlgHom.id R (AdjoinRoot p)) (ofAlgHom R p) : (a : S) → AdjoinRoot p) x : AdjoinRoot p)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
hAlg :
  ∀ (x : S),
    Eq (α := AdjoinRoot p)
      ((((mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯).comp (mapAlgHom (↑f : S →ₐ[R] T) p q ⋯)).comp (ofAlgHom R p) :
            (a : S) → AdjoinRoot p)
          x :
        AdjoinRoot p)
      ((AlgHom.comp (AlgHom.id R (AdjoinRoot p)) (ofAlgHom R p) : (a : S) → AdjoinRoot p) x : AdjoinRoot p)
⊢ (mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯).comp (mapAlgHom (↑f : S →ₐ[R] T) p q ⋯) = AlgHom.id R (AdjoinRoot p)
have hRoot : Eq (α := AdjoinRoot p)
  (((mapAlgHom (↑f.symm : T →ₐ[R] S) q p sorry).comp (mapAlgHom (↑f : S →ₐ[R] T) p q sorry) : (a : AdjoinRoot p) → AdjoinRoot p)
      (root p) :
    AdjoinRoot p)
  ((AlgHom.id R (AdjoinRoot p) : (a : AdjoinRoot p) → AdjoinRoot p) (root p) : AdjoinRoot p)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
⊢ Associated (Polynomial.map (↑f.symm : T →+* S) q) p
have this : Eq (α := S →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.toRingEquiv.symm : T →+* S) (↑f : S →+* T))
  (RingHom.id S)
Tactic: have : (RingHomClass.toRingHom f.toRingEquiv.symm).comp (RingHomClass.toRingHom f) =
        .id S := by ext; exact f.symm_apply_apply _
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hfg : Associated f g
⊢ (algEquivOfAssociated R f g hfg : (a : AdjoinRoot f) → AdjoinRoot g) (root f) = root g
have rw : (algHomOfDvd R f g sorry : (a : AdjoinRoot f) → AdjoinRoot g) (root f) = root g
Tactic: rw [coe_algEquivOfAssociated, algHomOfDvd_root]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hfg : Associated f g
rw : (algHomOfDvd R f g ⋯ : (a : AdjoinRoot f) → AdjoinRoot g) (root f) = root g
⊢ (algEquivOfAssociated R f g hfg : (a : AdjoinRoot f) → AdjoinRoot g) (root f) = root g
have rw₁ : root g = root g
Tactic: rw [coe_algEquivOfAssociated, algHomOfDvd_root]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g_1 : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f g : S[X]
hfg : f = g
⊢ Associated f g
have rw : Associated g g
Tactic: rw [hfg]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hfg : f = g
⊢ (algEquivOfEq R f g hfg : (a : AdjoinRoot f) → AdjoinRoot g) (root f) = root g
have rw : (algHomOfDvd R f g sorry : (a : AdjoinRoot f) → AdjoinRoot g) (root f) = root g
Tactic: rw [coe_algEquivOfEq, algHomOfDvd_root]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hfg : f = g
rw : (algHomOfDvd R f g ⋯ : (a : AdjoinRoot f) → AdjoinRoot g) (root f) = root g
⊢ (algEquivOfEq R f g hfg : (a : AdjoinRoot f) → AdjoinRoot g) (root f) = root g
have rw₁ : root g = root g
Tactic: rw [coe_algEquivOfEq, algHomOfDvd_root]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : Field K
f : K[X]
inst_1 : Fact (Irreducible f)
q : ℚ≥0
⊢ (↑q : AdjoinRoot f) = HDiv.hDiv (α := AdjoinRoot f) (↑q.num : AdjoinRoot f) (↑q.den : AdjoinRoot f)
have rw : Eq (α := AdjoinRoot f) (↑q : AdjoinRoot f) ((of f : (a : K) → AdjoinRoot f) (↑q : K))
Tactic: rw [← map_natCast (of f), ← map_natCast (of f), ← map_div₀, ← NNRat.cast_def]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : Field K
f : K[X]
inst_1 : Fact (Irreducible f)
q : ℚ
⊢ (↑q : AdjoinRoot f) = HDiv.hDiv (α := AdjoinRoot f) (↑q.num : AdjoinRoot f) (↑q.den : AdjoinRoot f)
have rw : Eq (α := AdjoinRoot f) (↑q : AdjoinRoot f) ((of f : (a : K) → AdjoinRoot f) (↑q : K))
Tactic: rw [← map_natCast (of f), ← map_intCast (of f), ← map_div₀, ← Rat.cast_def]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
f : AdjoinRoot g
⊢ (mk g : (a : R[X]) → AdjoinRoot g) ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) f) = f
have ih : ∀ (p : R[X]),
  Eq (α := AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g)
        ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) ((mk g : (a : R[X]) → AdjoinRoot g) p)) :
      AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g) p : AdjoinRoot g)
Tactic: induction f using AdjoinRoot.induction_on
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
p : R[X]
⊢ Eq (α := AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g)
        ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) ((mk g : (a : R[X]) → AdjoinRoot g) p)) :
      AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g) p : AdjoinRoot g)
have ih : g ∣ g * (p /ₘ g)
Tactic: rw [modByMonicHom_mk hg, mk_eq_mk, modByMonic_eq_sub_mul_div, sub_sub_cancel_left, dvd_neg]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
f_1 : AdjoinRoot g
f : R[X]
⊢ g ∣
    f -
      ∑ i : Fin g.natDegree,
        (monomial (↑i : ℕ) : (a : R) → R[X])
          ((fun (f : AdjoinRoot g) (i : Fin g.natDegree) ↦
              (coeff ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) f) (↑i : ℕ) : R))
            ((mk g : (a : R[X]) → AdjoinRoot g) f) i)
have simp : g ∣ f - f %ₘ g
Tactic: simp only [modByMonicHom_mk, sum_modByMonic_coeff hg degree_le_natDegree]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
f_1 : AdjoinRoot g
f : R[X]
⊢ g ∣ f - f %ₘ g
have rw : g ∣ g * (f /ₘ g)
Tactic: rw [modByMonic_eq_sub_mul_div, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
⊢ (fun (f : AdjoinRoot g) (i : Fin g.natDegree) ↦
        (coeff ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) f) (↑i : ℕ) : R))
      ((fun (c : Fin g.natDegree → R) ↦
          ((mk g : (a : R[X]) → AdjoinRoot g) (∑ i : Fin g.natDegree, (monomial (↑i : ℕ) : (a : R) → R[X]) (c i)) :
            AdjoinRoot g))
        x)
      i =
    x i
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
h : Nontrivial R
⊢ (fun (f : AdjoinRoot g) (i : Fin g.natDegree) ↦
        (coeff ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) f) (↑i : ℕ) : R))
      ((fun (c : Fin g.natDegree → R) ↦
          ((mk g : (a : R[X]) → AdjoinRoot g) (∑ i : Fin g.natDegree, (monomial (↑i : ℕ) : (a : R) → R[X]) (c i)) :
            AdjoinRoot g))
        x)
      i =
    x i
have simp : ((∑ i : Fin g.natDegree, (monomial (↑i : ℕ) : (a : R) → R[X]) (x i)) %ₘ g).coeff (↑i : ℕ) = x i
Tactic: simp only [modByMonicHom_mk]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
h : Nontrivial R
⊢ ((∑ i : Fin g.natDegree, (monomial (↑i : ℕ) : (a : R) → R[X]) (x i)) %ₘ g).coeff (↑i : ℕ) = x i
have rw : ∑ b : Fin g.natDegree, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (x b)) (↑i : ℕ) = x i
Tactic: rw [(modByMonic_eq_self_iff hg).mpr, finsetSum_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
h : Nontrivial R
rw : ∑ b : Fin g.natDegree, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (x b)) (↑i : ℕ) = x i
⊢ ((∑ i : Fin g.natDegree, (monomial (↑i : ℕ) : (a : R) → R[X]) (x i)) %ₘ g).coeff (↑i : ℕ) = x i
have rw₁ : degree.{u_1} (R := R) (∑ i : Fin g.natDegree, (monomial (↑i : ℕ) : (a : R) → R[X]) (x i)) < g.degree
Tactic: rw [(modByMonic_eq_self_iff hg).mpr, finsetSum_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
h : Nontrivial R
⊢ ∑ b : Fin g.natDegree, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (x b)) (↑i : ℕ) = x i
have simp_rw : (∑ x_1 : Fin g.natDegree, if (↑x_1 : ℕ) = (↑i : ℕ) then x x_1 else 0) = x i
Tactic: simp_rw [coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]