awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : Membership.mem (γ := Submonoid R) R⁰ f.leadingCoeff
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) (((aeval ((aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
⊢ IsAlgebraic R r
have this : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0
Tactic: have : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0 := fun h ↦ h1 <| by
    rwa [coeff_comp_degree_mul_degree hf,
      mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hf' _),
      leadingCoeff_eq_zero] at h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
H : Transcendental R r
f : R[X]
hf : Transcendental R f
⊢ Transcendental.{u, v} R (A := A) ((Polynomial.aeval r : (a : R[X]) → A) f : A)
have rw : ∀ (H : ∀ (p : R[X]), Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) p : A) (0 : A) → p = 0) {f : R[X]}
  (hf : ∀ (p : R[X]), Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X]) → p = 0) (p : R[X]),
  Eq.{v + 1} (α := A)
      (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A) →
    p = 0
Tactic: rw [transcendental_iff] at H hf ⊢
Cleared hypotheses: H, f, hf
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
H : ∀ (p : R[X]), Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) p : A) (0 : A) → p = 0
f : R[X]
hf : ∀ (p : R[X]), Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X]) → p = 0
p : R[X]
hp :
  Eq.{v + 1} (α := A)
    (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A)
    (0 : A)
have rwa : ∀ (hp : Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) (p.comp f) : A) (0 : A)),
  Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A)
    (0 : A)
Tactic: rwa [← aeval_comp, comp_eq_aeval] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
H : ∀ (p : R[X]), Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) p : A) (0 : A) → p = 0
f : R[X]
hf : ∀ (p : R[X]), Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X]) → p = 0
p : R[X]
hp :
  Eq.{v + 1} (α := A)
    (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
rwa :
  ∀ (hp : Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) (p.comp f) : A) (0 : A)),
    Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A)
      (0 : A)
⊢ Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A)
    (0 : A)
have rwa₁ : ∀
  (hp :
    Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A)
      (0 : A)),
  Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A)
    (0 : A)
Tactic: rwa [← aeval_comp, comp_eq_aeval] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
H : Transcendental.{u, v} R (A := A) ((Polynomial.aeval r : (a : R[X]) → A) f : A)
⊢ Transcendental R f
have rw : ∀
  (H :
    ∀ (p : R[X]),
      Eq.{v + 1} (α := A)
          (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A)
          (0 : A) →
        p = 0)
  (p : R[X]), Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X]) → p = 0
Tactic: rw [transcendental_iff] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
H :
  ∀ (p : R[X]),
    Eq.{v + 1} (α := A)
        (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A) →
      p = 0
p : R[X]
hp : Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ Eq.{v + 1} (α := A)
    (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
have rw : Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) (p.comp f) : A) (0 : A)
Tactic: rw [← aeval_comp, comp_eq_aeval, hp, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
H :
  ∀ (p : R[X]),
    Eq.{v + 1} (α := A)
        (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A) →
      p = 0
p : R[X]
hp : Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
rw : Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) (p.comp f) : A) (0 : A)
⊢ Eq.{v + 1} (α := A)
    (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
have rw₁ : Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A)
  (0 : A)
Tactic: rw [← aeval_comp, comp_eq_aeval, hp, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
H :
  ∀ (p : R[X]),
    Eq.{v + 1} (α := A)
        (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A) →
      p = 0
p : R[X]
hp : Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
rw : Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) (p.comp f) : A) (0 : A)
rw₁ :
  Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A)
    (0 : A)
⊢ Eq.{v + 1} (α := A)
    (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
have rw₂ : Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) 0 : A) (0 : A)
Tactic: rw [← aeval_comp, comp_eq_aeval, hp, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
H :
  ∀ (p : R[X]),
    Eq.{v + 1} (α := A)
        (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A) →
      p = 0
p : R[X]
hp : Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
rw : Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) (p.comp f) : A) (0 : A)
rw₁ :
  Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A)
    (0 : A)
rw₂ : Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) 0 : A) (0 : A)
⊢ Eq.{v + 1} (α := A)
    (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
have rw₃ : Eq.{v + 1} (α := A) 0 0
Tactic: rw [← aeval_comp, comp_eq_aeval, hp, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
H : IsAlgebraic.{u, v} R (A := A) ((aeval r : (a : R[X]) → A) f : A)
hf : Transcendental R f
⊢ IsAlgebraic R r
have contrapose : ∀ (H : ¬IsAlgebraic R r), ¬IsAlgebraic.{u, v} R (A := A) ((aeval r : (a : R[X]) → A) f : A)
Tactic: contrapose H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
⊢ Transcendental R x ↔ Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval x)) ⊥
have rw : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑(aeval x) : (a : R[X]) → A) ↔
  Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval x)) ⊥
Tactic: rw [transcendental_iff_injective, RingHom.injective_iff_ker_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
rw :
  Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑(aeval x) : (a : R[X]) → A) ↔
    Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval x)) ⊥
⊢ Transcendental R x ↔ Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval x)) ⊥
have rw₁ : Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval x)) ⊥ ↔
  Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval x)) ⊥
Tactic: rw [transcendental_iff_injective, RingHom.injective_iff_ker_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
h : ¬Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
a : A
inj : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑(aeval a) : (a : R[X]) → A)
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have h₁ : Eq (α := R → A) (⇑(algebraMap R A) : (a : R) → A)
  (Function.comp (β := R[X]) (⇑(aeval a) : (a : R[X]) → A) (⇑C : (a : R) → R[X]))
Tactic: convert! inj.comp C_injective
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
h : ¬Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
a : A
inj : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑(aeval a) : (a : R[X]) → A)
⊢ Eq (α := R → A) (⇑(algebraMap R A) : (a : R) → A)
    (Function.comp (β := R[X]) (⇑(aeval a) : (a : R[X]) → A) (⇑C : (a : R) → R[X]))
have h₁ : ∀ (x : R),
  Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    (Function.comp (β := R[X]) (⇑(aeval a) : (a : R[X]) → A) (⇑C : (a : R) → R[X]) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
h : Algebra.Transcendental R A
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have h₁ : ¬Algebra.IsAlgebraic R A
Tactic: rw [transcendental_iff_not_isAlgebraic] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
h : ¬Algebra.IsAlgebraic R A
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have contrapose : ∀ (h : ¬Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)), Algebra.IsAlgebraic R A
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
x : R
⊢ Eq.{v + 1} (α := A)
    (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) :
      A)
    (0 : A)
have rw : HSub.hSub (α := A) (β := A) (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) X : A)
    (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) ((C : (a : R) → R[X]) x : R[X]) : A) =
  0
Tactic: rw [map_sub, aeval_X, aeval_C, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
x : R
rw :
  HSub.hSub (α := A) (β := A) (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) X : A)
      (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) ((C : (a : R) → R[X]) x : R[X]) :
        A) =
    0
⊢ Eq.{v + 1} (α := A)
    (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) :
      A)
    (0 : A)
have rw₁ : HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A)
    (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) ((C : (a : R) → R[X]) x : R[X]) : A) =
  0
Tactic: rw [map_sub, aeval_X, aeval_C, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
x : R
rw :
  HSub.hSub (α := A) (β := A) (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) X : A)
      (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) ((C : (a : R) → R[X]) x : R[X]) :
        A) =
    0
rw₁ :
  HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A)
      (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) ((C : (a : R) → R[X]) x : R[X]) :
        A) =
    0
⊢ Eq.{v + 1} (α := A)
    (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) :
      A)
    (0 : A)
have rw₂ : HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A) ((algebraMap R A : (a : R) → A) x : A) = 0
Tactic: rw [map_sub, aeval_X, aeval_C, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
x : R
rw :
  HSub.hSub (α := A) (β := A) (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) X : A)
      (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) ((C : (a : R) → R[X]) x : R[X]) :
        A) =
    0
rw₁ :
  HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A)
      (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) ((C : (a : R) → R[X]) x : R[X]) :
        A) =
    0
rw₂ : HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A) ((algebraMap R A : (a : R) → A) x : A) = 0
⊢ Eq.{v + 1} (α := A)
    (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) :
      A)
    (0 : A)
have rw₃ : Eq.{v + 1} (α := A) 0 0
Tactic: rw [map_sub, aeval_X, aeval_C, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
⊢ IsAlgebraic.{u, v} R (A := A) 1
have rw : IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) 1 : A)
Tactic: rw [← map_one (algebraMap R A)]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
n : ℕ
⊢ IsAlgebraic.{u, v} R (A := A) (↑n : A)
have rw : IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) (↑n : R) : A)
Tactic: rw [← map_natCast (_ : R →+* A) n]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
n : ℕ
rw : IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) (↑n : R) : A)
⊢ IsAlgebraic.{u, v} R (A := A) (↑n : A)
have rw₁ : R →+* A
Tactic: rw [← map_natCast (_ : R →+* A) n]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
n : ℤ
⊢ IsAlgebraic.{u, v} R (A := A) (↑n : A)
have rw : IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) (↑n : R) : A)
Tactic: rw [← map_intCast (algebraMap R A)]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : DivisionRing A
inst_1 : Field R
inst_2 : Algebra R A
n : ℚ
⊢ IsAlgebraic.{u, v} R (A := A) (↑n : A)
have rw : IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) (↑n : R) : A)
Tactic: rw [← map_ratCast (algebraMap R A)]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
x : S
⊢ IsAlgebraic R x
have inl : IsAlgebraic.{u, u_1} R (A := S) 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
x : S
inl : IsAlgebraic.{u, u_1} R (A := S) 0
⊢ IsAlgebraic R x
have inr : ∀ (hx : x ≠ 0), IsAlgebraic R x
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
x : S
hx : x ≠ 0
⊢ IsAlgebraic R x
have inr : ∀ (r : R) (m : ↥M)
  (h :
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) =
      (algebraMap R S : (a : R) → S) (r, m).1),
  IsAlgebraic R x
Tactic: have ⟨⟨r, m⟩, h⟩ := surj M x
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) (r, m).1
⊢ IsAlgebraic R x
have inr : ∀
  (eq :
    HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
        ((C : (a : R) → R[X]) r : R[X]) =
      0),
  x = 0
Tactic: refine ⟨C m.1 * X - C r, fun eq ↦ hx ?_, by simpa [sub_eq_zero, mul_comm x] using h⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) (r, m).1
eq :
  HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
      ((C : (a : R) → R[X]) r : R[X]) =
    0
⊢ x = 0
have inr : ∀ (h : x = mk' S (r, m).1 (r, m).2)
  (eq :
    HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
        ((C : (a : R) → R[X]) r : R[X]) =
      0),
  x = 0
Tactic: rwa [← eq_mk'_iff_mul_eq, show r = 0 by simpa using congr(coeff $eq 0), mk'_zero] at h
Cleared hypotheses: h, eq
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) (r, m).1
eq :
  HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
      ((C : (a : R) → R[X]) r : R[X]) =
    0
inr :
  ∀ (h : x = mk' S (r, m).1 (r, m).2)
    (eq :
      HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
          ((C : (a : R) → R[X]) r : R[X]) =
        0),
    x = 0
⊢ x = 0
have inr₁ : ∀ (h : x = mk' S (0, m).1 (0, m).2)
  (eq :
    HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
        ((C : (a : R) → R[X]) r : R[X]) =
      0),
  x = 0
Tactic: rwa [← eq_mk'_iff_mul_eq, show r = 0 by simpa using congr(coeff $eq 0), mk'_zero] at h
Cleared hypotheses: h, eq
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) (r, m).1
eq :
  HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
      ((C : (a : R) → R[X]) r : R[X]) =
    0
inr :
  ∀ (h : x = mk' S (r, m).1 (r, m).2)
    (eq :
      HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
          ((C : (a : R) → R[X]) r : R[X]) =
        0),
    x = 0
inr₁ :
  ∀ (h : x = mk' S (0, m).1 (0, m).2)
    (eq :
      HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
          ((C : (a : R) → R[X]) r : R[X]) =
        0),
    x = 0
⊢ x = 0
have inr₂ : ∀ (h : x = 0)
  (eq :
    HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
        ((C : (a : R) → R[X]) r : R[X]) =
      0),
  x = 0
Tactic: rwa [← eq_mk'_iff_mul_eq, show r = 0 by simpa using congr(coeff $eq 0), mk'_zero] at h
Cleared hypotheses: h, eq
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R A
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
a : S
h : IsAlgebraic R a
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_1 + 1} (α := S) ((aeval a : (a : R[X]) → S) f : S) (0 : S)
⊢ Eq.{v + 1} (α := A) (((aeval ((algebraMap S A : (a : S) → A) a) : R[X] →ₐ[R] A) : (a : R[X]) → A) f : A) (0 : A)
have rw : Eq.{v + 1} (α := A) ((algebraMap S A : (a : S) → A) ((aeval a : (a : R[X]) → S) f : S) : A) (0 : A)
Tactic: rw [aeval_algebraMap_apply, hf₂, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R A
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
a : S
h : IsAlgebraic R a
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_1 + 1} (α := S) ((aeval a : (a : R[X]) → S) f : S) (0 : S)
rw : Eq.{v + 1} (α := A) ((algebraMap S A : (a : S) → A) ((aeval a : (a : R[X]) → S) f : S) : A) (0 : A)
⊢ Eq.{v + 1} (α := A) (((aeval ((algebraMap S A : (a : S) → A) a) : R[X] →ₐ[R] A) : (a : R[X]) → A) f : A) (0 : A)
have rw₁ : Eq.{v + 1} (α := A) ((algebraMap S A : (a : S) → A) 0 : A) (0 : A)
Tactic: rw [aeval_algebraMap_apply, hf₂, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R A
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
a : S
h : IsAlgebraic R a
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_1 + 1} (α := S) ((aeval a : (a : R[X]) → S) f : S) (0 : S)
rw : Eq.{v + 1} (α := A) ((algebraMap S A : (a : S) → A) ((aeval a : (a : R[X]) → S) f : S) : A) (0 : A)
rw₁ : Eq.{v + 1} (α := A) ((algebraMap S A : (a : S) → A) 0 : A) (0 : A)
⊢ Eq.{v + 1} (α := A) (((aeval ((algebraMap S A : (a : S) → A) a) : R[X] →ₐ[R] A) : (a : R[X]) → A) f : A) (0 : A)
have rw₂ : Eq.{v + 1} (α := A) 0 0
Tactic: rw [aeval_algebraMap_apply, hf₂, map_zero]