awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
i : ℕ
⊢ (p.toSubring T hp).coeff i = 0 ↔ p.coeff i = 0
have h : (p.toSubring T hp).coeff i = 0 ↔ (↑((p.toSubring T hp).coeff i) : R) = 0
Tactic: conv_rhs => rw [← coeff_toSubring p T hp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
i : ℕ
H : (p.toSubring T hp).coeff i = 0
⊢ (↑((p.toSubring T hp).coeff i) : R) = 0
have rw : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
Tactic: rw [H, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
i : ℕ
H : (p.toSubring T hp).coeff i = 0
rw : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
⊢ (↑((p.toSubring T hp).coeff i) : R) = 0
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [H, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
⊢ (p.toSubring T hp).Monic ↔ p.Monic
have simp_rw : (p.toSubring T hp).coeff p.natDegree = 1 ↔ (↑((p.toSubring T hp).coeff p.natDegree) : R) = 1
Tactic: simp_rw [Monic, leadingCoeff, natDegree_toSubring, ← coeff_toSubring p T hp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
H : (p.toSubring T hp).coeff p.natDegree = 1
⊢ (↑((p.toSubring T hp).coeff p.natDegree) : R) = 1
have rw : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
Tactic: rw [H, OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
H : (p.toSubring T hp).coeff p.natDegree = 1
rw : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
⊢ (↑((p.toSubring T hp).coeff p.natDegree) : R) = 1
have rw₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [H, OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
⊢ toSubring 0 T ⋯ = 0
have a : ∀ (i : ℕ), (↑((toSubring 0 T sorry).coeff i) : R) = (↑(coeff 0 i) : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
i : ℕ
⊢ (↑((toSubring 1 T ⋯).coeff i) : R) = (↑(coeff 1 i) : R)
have rw : Eq.{u_1 + 1} (α := R) (coeff 1 i) (↑(coeff 1 i) : R)
Tactic: rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero,
      OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
i : ℕ
rw : Eq.{u_1 + 1} (α := R) (coeff 1 i) (↑(coeff 1 i) : R)
⊢ (↑((toSubring 1 T ⋯).coeff i) : R) = (↑(coeff 1 i) : R)
have rw₁ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (↑(coeff 1 i) : R)
Tactic: rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero,
      OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
i : ℕ
rw : Eq.{u_1 + 1} (α := R) (coeff 1 i) (↑(coeff 1 i) : R)
rw₁ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (↑(coeff 1 i) : R)
⊢ (↑((toSubring 1 T ⋯).coeff i) : R) = (↑(coeff 1 i) : R)
have rw₂ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (↑(if i = 0 then 1 else 0) : R)
Tactic: rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero,
      OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
i : ℕ
rw : Eq.{u_1 + 1} (α := R) (coeff 1 i) (↑(coeff 1 i) : R)
rw₁ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (↑(coeff 1 i) : R)
rw₂ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (↑(if i = 0 then 1 else 0) : R)
⊢ (↑((toSubring 1 T ⋯).coeff i) : R) = (↑(coeff 1 i) : R)
have rw₃ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (if i = 0 then (↑1 : R) else (↑0 : R))
Tactic: rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero,
      OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
i : ℕ
rw : Eq.{u_1 + 1} (α := R) (coeff 1 i) (↑(coeff 1 i) : R)
rw₁ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (↑(coeff 1 i) : R)
rw₂ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (↑(if i = 0 then 1 else 0) : R)
rw₃ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (if i = 0 then (↑1 : R) else (↑0 : R))
⊢ (↑((toSubring 1 T ⋯).coeff i) : R) = (↑(coeff 1 i) : R)
have rw₄ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (if i = 0 then (↑1 : R) else 0)
Tactic: rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero,
      OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
i : ℕ
rw : Eq.{u_1 + 1} (α := R) (coeff 1 i) (↑(coeff 1 i) : R)
rw₁ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (↑(coeff 1 i) : R)
rw₂ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (↑(if i = 0 then 1 else 0) : R)
rw₃ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (if i = 0 then (↑1 : R) else (↑0 : R))
rw₄ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (if i = 0 then (↑1 : R) else 0)
⊢ (↑((toSubring 1 T ⋯).coeff i) : R) = (↑(coeff 1 i) : R)
have rw₅ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (if i = 0 then 1 else 0)
Tactic: rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero,
      OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
⊢ map T.subtype (p.toSubring T hp) = p
have a : ∀ (n : ℕ), (map T.subtype (p.toSubring T hp)).coeff n = p.coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
⊢ (ofSubring T p).coeff n = (↑(p.coeff n) : R)
have simp : p.coeff n = 0 → 0 = (↑(p.coeff n) : R)
Tactic: simp only [ofSubring, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, Classical.not_not, ite_eq_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
h : p.coeff n = 0
⊢ 0 = (↑(p.coeff n) : R)
have rw : Eq.{u_1 + 1} (α := R) 0 (↑0 : R)
Tactic: rw [h, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
h : p.coeff n = 0
rw : Eq.{u_1 + 1} (α := R) 0 (↑0 : R)
⊢ 0 = (↑(p.coeff n) : R)
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [h, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (hypothesis)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
i : R
hi : i ∈ (↑(ofSubring T p).coeffs : Set R)
⊢ i ∈ (↑T : Set R)
have hi₁ : ∃ (x : ℕ), ¬(ofSubring T p).coeff x = 0 ∧ (ofSubring T p).coeff x = i
Tactic: simp only [coeffs, Set.mem_image, mem_support_iff, Ne, Finset.mem_coe,
    (Finset.coe_image)] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
i : R
hi : ∃ (x : ℕ), ¬(ofSubring T p).coeff x = 0 ∧ (ofSubring T p).coeff x = i
⊢ i ∈ (↑T : Set R)
have rcases : ∀ (n : ℕ), ¬(ofSubring T p).coeff n = 0 → ∀ (h'n : (ofSubring T p).coeff n = i), i ∈ (↑T : Set R)
Tactic: rcases hi with ⟨n, _, h'n⟩
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
i : R
n : ℕ
left : ¬(ofSubring T p).coeff n = 0
h'n : (ofSubring T p).coeff n = i
⊢ i ∈ (↑T : Set R)
have rw : (↑(p.coeff n) : R) ∈ (↑T : Set R)
Tactic: rw [← h'n, coeff_ofSubring]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
⊢ (↑(ofSubring T p).coeffs : Set R) ⊆ (↑T : Set R)
have intro : ∀ ⦃i : R⦄, i ∈ (↑(ofSubring T p).coeffs : Set R) → i ∈ (↑T : Set R)
Tactic: classical
  intro i hi
  simp only [coeffs, Set.mem_image, mem_support_iff, Ne, Finset.mem_coe,
    (Finset.coe_image)] at hi
  rcases hi with ⟨n, _, h'n⟩
  rw [← h'n, coeff_ofSubring]
  exact Subtype.mem (coeff p n : T)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
intro intro₁ : ∀ ⦃i : R⦄ (hi : i ∈ (↑(ofSubring T p).coeffs : Set R)), i ∈ (↑T : Set R)
⊢ (↑(ofSubring T p).coeffs : Set R) ⊆ (↑T : Set R)
have intro₂ : ∀ ⦃i : R⦄ (hi : ∃ (x : ℕ), ¬(ofSubring T p).coeff x = 0 ∧ (ofSubring T p).coeff x = i), i ∈ (↑T : Set R)
Tactic: classical
  intro i hi
  simp only [coeffs, Set.mem_image, mem_support_iff, Ne, Finset.mem_coe,
    (Finset.coe_image)] at hi
  rcases hi with ⟨n, _, h'n⟩
  rw [← h'n, coeff_ofSubring]
  exact Subtype.mem (coeff p n : T)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
intro intro₁ : ∀ ⦃i : R⦄ (hi : i ∈ (↑(ofSubring T p).coeffs : Set R)), i ∈ (↑T : Set R)
intro₂ : ∀ ⦃i : R⦄ (hi : ∃ (x : ℕ), ¬(ofSubring T p).coeff x = 0 ∧ (ofSubring T p).coeff x = i), i ∈ (↑T : Set R)
⊢ (↑(ofSubring T p).coeffs : Set R) ⊆ (↑T : Set R)
have intro₃ : ∀ ⦃i : R⦄ (n : ℕ), ¬(ofSubring T p).coeff n = 0 → ∀ (h'n : (ofSubring T p).coeff n = i), i ∈ (↑T : Set R)
Tactic: classical
  intro i hi
  simp only [coeffs, Set.mem_image, mem_support_iff, Ne, Finset.mem_coe,
    (Finset.coe_image)] at hi
  rcases hi with ⟨n, _, h'n⟩
  rw [← h'n, coeff_ofSubring]
  exact Subtype.mem (coeff p n : T)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
intro intro₁ : ∀ ⦃i : R⦄ (hi : i ∈ (↑(ofSubring T p).coeffs : Set R)), i ∈ (↑T : Set R)
intro₂ : ∀ ⦃i : R⦄ (hi : ∃ (x : ℕ), ¬(ofSubring T p).coeff x = 0 ∧ (ofSubring T p).coeff x = i), i ∈ (↑T : Set R)
intro₃ : ∀ ⦃i : R⦄ (n : ℕ), ¬(ofSubring T p).coeff n = 0 → ∀ (h'n : (ofSubring T p).coeff n = i), i ∈ (↑T : Set R)
⊢ (↑(ofSubring T p).coeffs : Set R) ⊆ (↑T : Set R)
have intro₄ : ∀ ⦃i : R⦄ (n : ℕ),
  ¬(ofSubring T p).coeff n = 0 → ∀ (h'n : (ofSubring T p).coeff n = i), (↑(p.coeff n) : R) ∈ (↑T : Set R)
Tactic: classical
  intro i hi
  simp only [coeffs, Set.mem_image, mem_support_iff, Ne, Finset.mem_coe,
    (Finset.coe_image)] at hi
  rcases hi with ⟨n, _, h'n⟩
  rw [← h'n, coeff_ofSubring]
  exact Subtype.mem (coeff p n : T)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : B
p : R[X]
⊢ Eq.{u_3 + 1} (α := B) ((aeval x : (a : A[X]) → B) (map (algebraMap R A) p) : B) ((aeval x : (a : R[X]) → B) p : B)
have rw : eval₂ (algebraMap A B) x (map (algebraMap R A) p) = (aeval x : (a : R[X]) → B) p
Tactic: rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : B
p : R[X]
rw : eval₂ (algebraMap A B) x (map (algebraMap R A) p) = (aeval x : (a : R[X]) → B) p
⊢ Eq.{u_3 + 1} (α := B) ((aeval x : (a : A[X]) → B) (map (algebraMap R A) p) : B) ((aeval x : (a : R[X]) → B) p : B)
have rw₁ : eval₂ (algebraMap A B) x (map (algebraMap R A) p) = eval₂ (algebraMap R B) x p
Tactic: rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : B
p : R[X]
rw : eval₂ (algebraMap A B) x (map (algebraMap R A) p) = (aeval x : (a : R[X]) → B) p
rw₁ : eval₂ (algebraMap A B) x (map (algebraMap R A) p) = eval₂ (algebraMap R B) x p
⊢ Eq.{u_3 + 1} (α := B) ((aeval x : (a : A[X]) → B) (map (algebraMap R A) p) : B) ((aeval x : (a : R[X]) → B) p : B)
have rw₂ : eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p =
  eval₂ (algebraMap R B) x p
Tactic: rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : B
p : R[X]
rw : eval₂ (algebraMap A B) x (map (algebraMap R A) p) = (aeval x : (a : R[X]) → B) p
rw₁ : eval₂ (algebraMap A B) x (map (algebraMap R A) p) = eval₂ (algebraMap R B) x p
rw₂ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p =
    eval₂ (algebraMap R B) x p
⊢ Eq.{u_3 + 1} (α := B) ((aeval x : (a : A[X]) → B) (map (algebraMap R A) p) : B) ((aeval x : (a : R[X]) → B) p : B)
have rw₃ : eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p =
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p
Tactic: rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
p : R[X]
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
have rw : eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
  (algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A)
Tactic: rw [aeval_def, aeval_def, hom_eval₂, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
p : R[X]
rw :
  eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
    (algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A)
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
have rw₁ : eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
  (algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x p)
Tactic: rw [aeval_def, aeval_def, hom_eval₂, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
p : R[X]
rw :
  eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
    (algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A)
rw₁ :
  eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
    (algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x p)
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
have rw₂ : eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A))
    ((algebraMap A B : (a : A) → B) x) p
Tactic: rw [aeval_def, aeval_def, hom_eval₂, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
p : R[X]
rw :
  eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
    (algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A)
rw₁ :
  eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
    (algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x p)
rw₂ :
  eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
    eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A))
      ((algebraMap A B : (a : A) → B) x) p
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
have rw₃ : eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
  eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p
Tactic: rw [aeval_def, aeval_def, hom_eval₂, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
inst_7 : IsDomain A
inst_8 : IsTorsionFree A B
inst_9 : Nontrivial B
x : A
p : R[X]
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
have rw : Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B) (0 : B) ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
Tactic: rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
    iff_false_intro (one_ne_zero' B), or_false]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
inst_7 : IsDomain A
inst_8 : IsTorsionFree A B
inst_9 : Nontrivial B
x : A
p : R[X]
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
have rw₁ : HSMul.hSMul.{u_2, u_3, u_3} (α := A) (β := B) ((aeval x : (a : R[X]) → A) p : A) 1 = 0 ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
Tactic: rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
    iff_false_intro (one_ne_zero' B), or_false]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
inst_7 : IsDomain A
inst_8 : IsTorsionFree A B
inst_9 : Nontrivial B
x : A
p : R[X]
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rw₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) (β := B) ((aeval x : (a : R[X]) → A) p : A) 1 = 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
have rw₂ : Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) ∨ Eq.{u_3 + 1} (α := B) 1 0 ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
Tactic: rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
    iff_false_intro (one_ne_zero' B), or_false]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
inst_7 : IsDomain A
inst_8 : IsTorsionFree A B
inst_9 : Nontrivial B
x : A
p : R[X]
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rw₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) (β := B) ((aeval x : (a : R[X]) → A) p : A) 1 = 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rw₂ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) ∨ Eq.{u_3 + 1} (α := B) 1 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
have rw₃ : Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) ∨ False ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
Tactic: rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
    iff_false_intro (one_ne_zero' B), or_false]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
inst_7 : IsDomain A
inst_8 : IsTorsionFree A B
inst_9 : Nontrivial B
x : A
p : R[X]
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rw₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) (β := B) ((aeval x : (a : R[X]) → A) p : A) 1 = 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rw₂ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) ∨ Eq.{u_3 + 1} (α := B) 1 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rw₃ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) ∨ False ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
have rw₄ : Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
Tactic: rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
    iff_false_intro (one_ne_zero' B), or_false]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
p : R[X]
h : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
have rw : Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B) (0 : B) ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
Tactic: rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]