awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : MvPolynomial σ R
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → 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 : MvPolynomial σ R) → A) p : A)
Tactic: rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ←
    IsScalarTower.algebraMap_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : MvPolynomial σ R
rw :
  eval₂ (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) p =
    (algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → 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, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ←
    IsScalarTower.algebraMap_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : MvPolynomial σ R
rw :
  eval₂ (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) p =
    (algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → 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) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B)
have rw₂ : Eq.{u_3 + 1} (α := B)
  ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
  ((algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x p) : B)
Tactic: rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ←
    IsScalarTower.algebraMap_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : MvPolynomial σ R
rw :
  eval₂ (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) p =
    (algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → 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₂ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x p) : B)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B)
have rw₃ : Eq.{u_3 + 1} (α := B)
  ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
  ((algebraMap A B : (a : A) → B) ((eval₂Hom (algebraMap R A) x : (a : MvPolynomial σ R) → A) p : A) : B)
Tactic: rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ←
    IsScalarTower.algebraMap_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : MvPolynomial σ R
rw :
  eval₂ (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) p =
    (algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → 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₂ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x p) : B)
rw₃ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((eval₂Hom (algebraMap R A) x : (a : MvPolynomial σ R) → A) p : A) : B)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B)
have rw₄ : Eq.{u_3 + 1} (α := B)
  ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
  ((eval₂Hom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) fun (i : σ) ↦
          (algebraMap A B : (a : A) → B) (x i) :
        (a : MvPolynomial σ R) → B)
      p :
    B)
Tactic: rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ←
    IsScalarTower.algebraMap_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : MvPolynomial σ R
rw :
  eval₂ (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) p =
    (algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → 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₂ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x p) : B)
rw₃ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((eval₂Hom (algebraMap R A) x : (a : MvPolynomial σ R) → A) p : A) : B)
rw₄ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((eval₂Hom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) fun (i : σ) ↦
            (algebraMap A B : (a : A) → B) (x i) :
          (a : MvPolynomial σ R) → B)
        p :
      B)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B)
have rw₅ : Eq.{u_3 + 1} (α := B)
  ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
  ((eval₂Hom (algebraMap R B) fun (i : σ) ↦ (algebraMap A B : (a : A) → B) (x i) : (a : MvPolynomial σ R) → B) p : B)
Tactic: rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ←
    IsScalarTower.algebraMap_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : MvPolynomial σ R
rw :
  eval₂ (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) p =
    (algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → 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₂ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x p) : B)
rw₃ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((eval₂Hom (algebraMap R A) x : (a : MvPolynomial σ R) → A) p : A) : B)
rw₄ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((eval₂Hom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) fun (i : σ) ↦
            (algebraMap A B : (a : A) → B) (x i) :
          (a : MvPolynomial σ R) → B)
        p :
      B)
rw₅ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((eval₂Hom (algebraMap R B) fun (i : σ) ↦ (algebraMap A B : (a : A) → B) (x i) : (a : MvPolynomial σ R) → B) p : B)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B)
have rw₆ : Eq.{u_3 + 1} (α := B)
  ((eval₂Hom (algebraMap R B) fun (x_1 : σ) ↦ (algebraMap A B : (a : A) → B) (x x_1) : (a : MvPolynomial σ R) → B) p :
    B)
  ((eval₂Hom (algebraMap R B) fun (i : σ) ↦ (algebraMap A B : (a : A) → B) (x i) : (a : MvPolynomial σ R) → B) p : B)
Tactic: rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ←
    IsScalarTower.algebraMap_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : Module.IsTorsionFree A B
inst_9 : Nontrivial B
x : σ → A
p : MvPolynomial σ R
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
have rw : Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B) (0 : B) ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → 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.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : Module.IsTorsionFree A B
inst_9 : Nontrivial B
x : σ → A
p : MvPolynomial σ R
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
have rw₁ : HSMul.hSMul.{u_2, u_3, u_3} (α := A) (β := B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) 1 = 0 ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → 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.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : Module.IsTorsionFree A B
inst_9 : Nontrivial B
x : σ → A
p : MvPolynomial σ R
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
rw₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) (β := B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) 1 = 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
have rw₂ : Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A) ∨ Eq.{u_3 + 1} (α := B) 1 0 ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → 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.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : Module.IsTorsionFree A B
inst_9 : Nontrivial B
x : σ → A
p : MvPolynomial σ R
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
rw₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) (β := B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) 1 = 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
rw₂ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A) ∨ Eq.{u_3 + 1} (α := B) 1 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
have rw₃ : Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A) ∨ False ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → 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.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : Module.IsTorsionFree A B
inst_9 : Nontrivial B
x : σ → A
p : MvPolynomial σ R
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
rw₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) (β := B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) 1 = 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
rw₂ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A) ∨ Eq.{u_3 + 1} (α := B) 1 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
rw₃ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A) ∨ False ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
have rw₄ : Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A) ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → 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.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : MvPolynomial σ R
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) : (a : MvPolynomial σ R) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
have rw : Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B) (0 : B) ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
Tactic: rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : MvPolynomial σ R
h : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
have rw₁ : Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B)
    ((algebraMap A B : (a : A) → B) 0 : B) ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
Tactic: rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring 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 : MvPolynomial σ R
h : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
rw₁ :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B)
      ((algebraMap A B : (a : A) → B) 0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
have rw₂ : Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A) ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
Tactic: rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
w : σ → M
p : MvPolynomial σ R
⊢ weightedTotalDegree' w p = ⊥ ↔ p = 0
have simp : (∀ (s : σ →₀ ℕ), coeff s p ≠ 0 → False) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0
Tactic: simp only [weightedTotalDegree', Finset.sup_eq_bot_iff, mem_support_iff, WithBot.coe_ne_bot,
    MvPolynomial.eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : p ≠ 0
⊢ weightedTotalDegree' w p = (↑(weightedTotalDegree w p) : WithBot M)
have hp₁ : ∃ (a : M), (↑a : WithBot M) = weightedTotalDegree' w p
Tactic: rw [Ne, ← weightedTotalDegree'_eq_bot_iff w p, ← Ne, WithBot.ne_bot_iff_exists] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : ∃ (a : M), (↑a : WithBot M) = weightedTotalDegree' w p
⊢ weightedTotalDegree' w p = (↑(weightedTotalDegree w p) : WithBot M)
have obtain : ∀ (m : M) (hm : (↑m : WithBot M) = weightedTotalDegree' w p),
  weightedTotalDegree' w p = (↑(weightedTotalDegree w p) : WithBot M)
Tactic: obtain ⟨m, hm⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : (↑m : WithBot M) = weightedTotalDegree' w p
⊢ weightedTotalDegree' w p = (↑(weightedTotalDegree w p) : WithBot M)
have a : weightedTotalDegree' w p ≤ (↑(weightedTotalDegree w p) : WithBot M)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : (↑m : WithBot M) = weightedTotalDegree' w p
a : weightedTotalDegree' w p ≤ (↑(weightedTotalDegree w p) : WithBot M)
⊢ weightedTotalDegree' w p = (↑(weightedTotalDegree w p) : WithBot M)
have a₁ : (↑(weightedTotalDegree w p) : WithBot M) ≤ weightedTotalDegree' w p
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : (↑m : WithBot M) = weightedTotalDegree' w p
⊢ weightedTotalDegree' w p ≤ (↑(weightedTotalDegree w p) : WithBot M)
have a : ∀ b ∈ p.support,
  LE.le.{u_2} (α := M) ((weight w : (a : σ →₀ ℕ) → M) b : M)
    (p.support.sup fun (s : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) s : M)
Tactic: simp only [weightedTotalDegree, weightedTotalDegree', Finset.sup_le_iff, WithBot.coe_le_coe]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : (↑m : WithBot M) = weightedTotalDegree' w p
⊢ (↑(p.support.sup fun (s : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) s) : WithBot M) ≤ weightedTotalDegree' w p
have hm' : weightedTotalDegree' w p ≤ (↑m : WithBot M)
Tactic: have hm' : weightedTotalDegree' w p ≤ m := le_of_eq hm.symm