awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
a_1 : R[X]
a :
  ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₁ :
  (Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₂ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₃ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₄ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₅ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₆ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₇ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₈ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₉ : a_1 = 0 → ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₁₀ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₁₁ : a_1 = 0 → ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₁₂ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → False
a₁₃ : a_1 = 0 → a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → False
⊢ ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) ↔
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
have a₁₄ : a_1 = 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
a_1 : R[X]
a :
  ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₁ :
  (Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₂ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₃ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₄ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₅ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₆ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₇ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₈ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₉ : a_1 = 0 → ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₁₀ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₁₁ : a_1 = 0 → ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₁₂ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → False
a₁₃ : a_1 = 0 → a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → False
a₁₄ a₁₅ a₁₆ : a_1 = 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₁₇ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
⊢ ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) ↔
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
have a₁₈ : ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
  a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
a_1 : R[X]
a :
  ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₁ :
  (Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₂ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₃ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₄ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₅ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₆ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₇ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₈ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₉ : a_1 = 0 → ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₁₀ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₁₁ : a_1 = 0 → ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₁₂ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → False
a₁₃ : a_1 = 0 → a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → False
a₁₄ a₁₅ a₁₆ : a_1 = 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₁₇ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₁₈ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → False
⊢ ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) ↔
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
have a₁₉ : a_1 = 0 → a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Algebra.IsAlgebraic R A
⊢ Nontrivial R
have obtain : ∀ (p : R[X]) (hp : p ≠ 0), Nontrivial R
Tactic: obtain ⟨p, hp, -⟩ := Algebra.IsAlgebraic.isAlgebraic (R := R) (0 : A)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ (∀ x ∈ S, IsAlgebraic R x) ↔ Algebra.IsAlgebraic.{u, v} R ↥S
have rw : (∀ (x : ↥S), IsAlgebraic R (↑x : A)) ↔ ∀ (x : ↥S), IsAlgebraic R x
Tactic: rw [Subtype.forall', Algebra.isAlgebraic_def]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : ↥S), IsAlgebraic R (↑x : A)) ↔ ∀ (x : ↥S), IsAlgebraic R x
have refine : ∀ (x : ↥S) (p : R[X]),
  Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
    Eq.{v + 1} (α := ↥S) ((aeval x : (a : R[X]) → ↥S) p : ↥S) (0 : ↥S)
Tactic: refine forall_congr' fun x => exists_congr fun p => and_congr Iff.rfl ?_
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
⊢ Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
    Eq.{v + 1} (α := ↥S) ((aeval x : (a : R[X]) → ↥S) p : ↥S) (0 : ↥S)
have h : Function.Injective (α := ↥S) (β := A) (⇑S.val : (a : ↥S) → A)
Tactic: have h : Function.Injective S.val := Subtype.val_injective
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective (α := ↥S) (β := A) (⇑S.val : (a : ↥S) → A)
| Eq.{v + 1} (α := ↥S) ((aeval x : (a : R[X]) → ↥S) p : ↥S) (0 : ↥S)
have rw : Eq (α := A) ((S.val : (a : ↥S) → A) ((aeval x : (a : R[X]) → ↥S) p : ↥S) : A) (0 : A)
Tactic: rw [← h.eq_iff, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective (α := ↥S) (β := A) (⇑S.val : (a : ↥S) → A)
⊢ Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
    Eq.{v + 1} (α := ↥S) ((aeval x : (a : R[X]) → ↥S) p : ↥S) (0 : ↥S)
have conv_rhs : Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
  Eq (α := A) ((S.val : (a : ↥S) → A) ((aeval x : (a : R[X]) → ↥S) p : ↥S) : A) (0 : A)
Tactic: conv_rhs => rw [← h.eq_iff, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective (α := ↥S) (β := A) (⇑S.val : (a : ↥S) → A)
⊢ Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
    Eq (α := A) ((S.val : (a : ↥S) → A) ((aeval x : (a : R[X]) → ↥S) p : ↥S) : A) (0 : A)
have rw : Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
  Eq.{v + 1} (α := A) (((aeval ((S.val : (a : ↥S) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
Tactic: rw [← aeval_algHom_apply, S.val_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective (α := ↥S) (β := A) (⇑S.val : (a : ↥S) → A)
rw :
  Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
    Eq.{v + 1} (α := A) (((aeval ((S.val : (a : ↥S) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
    Eq (α := A) ((S.val : (a : ↥S) → A) ((aeval x : (a : R[X]) → ↥S) p : ↥S) : A) (0 : A)
have rw₁ : Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
  Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A)
Tactic: rw [← aeval_algHom_apply, S.val_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
x : A
⊢ IsAlgebraic K x ↔ IsIntegral K x
have refine : IsAlgebraic K x → IsIntegral K x
Tactic: refine ⟨?_, IsIntegral.isAlgebraic⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : Eq.{v + 1} (α := A) ((aeval x : (a : K[X]) → A) p : A) (0 : A)
⊢ IsIntegral K x
have refine : eval₂ (algebraMap K A) x (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) = 0
Tactic: refine ⟨_, monic_mul_leadingCoeff_inv hp, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : Eq.{v + 1} (α := A) ((aeval x : (a : K[X]) → A) p : A) (0 : A)
⊢ eval₂ (algebraMap K A) x (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) = 0
have rw : Eq.{v + 1} (α := A)
  ((aeval x : (a : K[X]) → A) (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) : A) (0 : A)
Tactic: rw [← aeval_def, map_mul, hpx, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : Eq.{v + 1} (α := A) ((aeval x : (a : K[X]) → A) p : A) (0 : A)
rw :
  Eq.{v + 1} (α := A)
    ((aeval x : (a : K[X]) → A) (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) : A) (0 : A)
⊢ eval₂ (algebraMap K A) x (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) = 0
have rw₁ : HMul.hMul (α := A) (β := A) ((aeval x : (a : K[X]) → A) p : A)
    ((aeval x : (a : K[X]) → A) ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X]) : A) =
  0
Tactic: rw [← aeval_def, map_mul, hpx, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : Eq.{v + 1} (α := A) ((aeval x : (a : K[X]) → A) p : A) (0 : A)
rw :
  Eq.{v + 1} (α := A)
    ((aeval x : (a : K[X]) → A) (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) : A) (0 : A)
rw₁ :
  HMul.hMul (α := A) (β := A) ((aeval x : (a : K[X]) → A) p : A)
      ((aeval x : (a : K[X]) → A) ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X]) : A) =
    0
⊢ eval₂ (algebraMap K A) x (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) = 0
have rw₂ : HMul.hMul (α := A) (β := A) (0 : A) ((aeval x : (a : K[X]) → A) ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X]) : A) = 0
Tactic: rw [← aeval_def, map_mul, hpx, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : Eq.{v + 1} (α := A) ((aeval x : (a : K[X]) → A) p : A) (0 : A)
rw :
  Eq.{v + 1} (α := A)
    ((aeval x : (a : K[X]) → A) (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) : A) (0 : A)
rw₁ :
  HMul.hMul (α := A) (β := A) ((aeval x : (a : K[X]) → A) p : A)
      ((aeval x : (a : K[X]) → A) ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X]) : A) =
    0
rw₂ :
  HMul.hMul (α := A) (β := A) (0 : A) ((aeval x : (a : K[X]) → A) ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X]) : A) =
    0
⊢ eval₂ (algebraMap K A) x (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) = 0
have rw₃ : Eq.{v + 1} (α := A) 0 0
Tactic: rw [← aeval_def, map_mul, hpx, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
⊢ Algebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A
have rw : (∀ (x : A), IsAlgebraic K x) ↔ Algebra.IsIntegral K A
Tactic: rw [Algebra.isAlgebraic_def, Algebra.isIntegral_def,
      forall_congr' fun _ ↦ isAlgebraic_iff_isIntegral]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
rw : (∀ (x : A), IsAlgebraic K x) ↔ Algebra.IsIntegral K A
⊢ Algebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A
have rw₁ : (∀ (x : A), IsAlgebraic K x) ↔ ∀ (x : A), IsIntegral K x
Tactic: rw [Algebra.isAlgebraic_def, Algebra.isIntegral_def,
      forall_congr' fun _ ↦ isAlgebraic_iff_isIntegral]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
rw : (∀ (x : A), IsAlgebraic K x) ↔ Algebra.IsIntegral K A
rw₁ : (∀ (x : A), IsAlgebraic K x) ↔ ∀ (x : A), IsIntegral K x
⊢ Algebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A
have rw₂ : (∀ (a : A), IsIntegral K a) ↔ ∀ (x : A), IsIntegral K x
Tactic: rw [Algebra.isAlgebraic_def, Algebra.isIntegral_def,
      forall_congr' fun _ ↦ isAlgebraic_iff_isIntegral]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
K : Type u_1
A : Type u_4
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
r : A
f : K[X]
⊢ Transcendental.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A) ↔ Transcendental K r ∧ Transcendental K f
have refine : ∀ (h : Transcendental.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)), Transcendental K r
Tactic: refine ⟨fun h ↦ ⟨?_, h.of_aeval⟩, fun ⟨h1, h2⟩ ↦ h1.aeval_of_transcendental h2⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
K : Type u_1
A : Type u_4
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
r : A
f : K[X]
h : Transcendental.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)
⊢ Transcendental K r
have h₁ : ¬IsAlgebraic.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)
Tactic: rw [Transcendental] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
K : Type u_1
A : Type u_4
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
r : A
f : K[X]
h : ¬IsAlgebraic.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)
⊢ ¬IsAlgebraic K r
have contrapose : ∀ (h : IsAlgebraic K r), IsAlgebraic.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
K : Type u_1
A : Type u_4
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
r : A
f : K[X]
h : IsAlgebraic K r
⊢ IsAlgebraic.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)
have rw : ∀ (h : IsIntegral K r), IsIntegral.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)
Tactic: rw [isAlgebraic_iff_isIntegral] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
have pos : ∀ (inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)),
  ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
Tactic: by_cases inj : Function.Injective (algebraMap R A)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
pos :
  ∀ (inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)),
    ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
have neg : ∀ (inj : ¬Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)),
  ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
Tactic: by_cases inj : Function.Injective (algebraMap R A)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
have inj₁ : ¬∀ (a : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) a : A) (0 : A) → a = 0
Tactic: rw [injective_iff_map_eq_zero] at inj
Cleared hypotheses: inj
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬∀ (a : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) a : A) (0 : A) → a = 0
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
have inj₁ : ∃ (a : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) a : A) (0 : A) ∧ a ≠ 0
Tactic: push Not at inj
Cleared hypotheses: inj
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ (a : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) a : A) (0 : A) ∧ a ≠ 0
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
have neg : ∀ (r : R) (eq : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) (0 : A)) (ne : r ≠ 0),
  ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
Tactic: have ⟨r, eq, ne⟩ := inj
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
have pos : ∀ (p : R[X]) (p_ne_zero : p ≠ 0) (px : Eq.{u_3 + 1} (α := A) ((aeval z : (a : R[X]) → A) p : A) (0 : A)),
  ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
Tactic: have ⟨p, p_ne_zero, px⟩ := hz
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p : R[X]
p_ne_zero : p ≠ 0
px : Eq.{u_3 + 1} (α := A) ((aeval z : (a : R[X]) → A) p : A) (0 : A)
a : R := p.leadingCoeff
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
have a_ne_zero : a ≠ 0
Tactic: have a_ne_zero : a ≠ 0 := mt Polynomial.leadingCoeff_eq_zero.mp p_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p : R[X]
p_ne_zero : p ≠ 0
px : Eq.{u_3 + 1} (α := A) ((aeval z : (a : R[X]) → A) p : A) (0 : A)
a : R := p.leadingCoeff
a_ne_zero : a ≠ 0
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
have x_integral : IsIntegral R (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) a : A) z)
Tactic: have x_integral : IsIntegral R (algebraMap R A a * z) :=
    ⟨p.integralNormalization, monic_integralNormalization p_ne_zero,
      integralNormalization_aeval_eq_zero px fun _ ↦ (map_eq_zero_iff _ inj).mp⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
⊢ ∃ (y : R), y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)
have this : Nontrivial R
Tactic: have := Algebra.IsAlgebraic.nontrivial R A
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
⊢ ∃ (y : R), y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)
have choose : ∀ (r : (x : A) → R) (hr : ∀ (x : A), r x ≠ 0) (int : ∀ (x : A), IsIntegral R (r x • x)),
  ∃ (y : R), y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)
Tactic: choose r hr int using fun x ↦ (alg.1 x).exists_integral_multiple
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : (x : A) → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
⊢ ∃ (y : R), y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)
have refine : ∀ (x : A) (h : x ∈ s), IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ x ∈ s, r x) x)
Tactic: refine ⟨∏ x ∈ s, r x, Finset.prod_ne_zero_iff.mpr fun _ _ ↦ hr _, fun _ h ↦ ?_⟩