awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
x : A
h : x ∈ s
⊢ IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ x ∈ s, r x) x)
have rw : IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ x ∈ s.erase x, r x) (r x • x))
Tactic: rw [← Finset.prod_erase_mul _ _ h, mul_smul]
-- 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)
x : A
h : x ∈ s
⊢ IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ x ∈ s, r x) x)
have classical : IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ x ∈ s.erase x, r x) (r x • x))
Tactic: classical rw [← Finset.prod_erase_mul _ _ h, mul_smul]
-- 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
y : R
hy : ¬IsNilpotent y
h : IsIntegral R (y • z)
⊢ IsAlgebraic R z
have have : ∀ (p : R[X]) (monic : p.Monic) (eval0 : eval₂ (algebraMap R A) (y • z) p = 0), IsAlgebraic R z
Tactic: have ⟨p, monic, eval0⟩ := 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
y : R
hy : ¬IsNilpotent y
h : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
⊢ IsAlgebraic R z
have refine : ∀ (h : p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X) = 0), False
Tactic: refine ⟨p.comp (C y * X), fun h ↦ ?_, by simpa [aeval_comp, Algebra.smul_def] using eval0⟩
-- 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
y : R
hy : ¬IsNilpotent y
h_1 : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X) = 0
⊢ False
have h₁ : (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X)).coeff p.natDegree = coeff 0 p.natDegree
Tactic: apply_fun (coeff · p.natDegree) at h
Cleared hypotheses: h
-- 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
y : R
hy : ¬IsNilpotent y
h_1 : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h :
  (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X)).coeff p.natDegree = coeff 0 p.natDegree
⊢ False
have hy0 : y ≠ 0
Tactic: have hy0 : y ≠ 0 := by rintro rfl; exact hy .zero
-- 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
y : R
hy : ¬IsNilpotent y
h_1 : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h :
  (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X)).coeff p.natDegree = coeff 0 p.natDegree
hy0 : y ≠ 0
⊢ False
have rw : ∀ (h : y ^ p.natDegree = 0) (hy0 : y ≠ 0), False
Tactic: rw [coeff_zero, ← mul_one p.natDegree, ← natDegree_C_mul_X y hy0,
    coeff_comp_degree_mul_degree, monic, one_mul, leadingCoeff_C_mul_X] at h
Cleared hypotheses: h, hy0
-- 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
y : R
hy : ¬IsNilpotent y
h_1 : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h :
  (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X)).coeff p.natDegree = coeff 0 p.natDegree
hy0 : y ≠ 0
rw : ∀ (h : y ^ p.natDegree = 0) (hy0 : y ≠ 0), False
⊢ False
have rw₁ : ∀
  (h :
    (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X)).coeff
        (p.natDegree * (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X).natDegree) =
      0)
  (hy0 : y ≠ 0), (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X).natDegree ≠ 0
Tactic: rw [coeff_zero, ← mul_one p.natDegree, ← natDegree_C_mul_X y hy0,
    coeff_comp_degree_mul_degree, monic, one_mul, leadingCoeff_C_mul_X] at h
Cleared hypotheses: h, hy0
-- 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
y : R
hy : ¬IsNilpotent y
h_1 : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h :
  (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X)).coeff
      (p.natDegree * (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X).natDegree) =
    0
hy0 : y ≠ 0
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X).natDegree ≠ 0
have rw : Ne (α := ℕ) 1 0
Tactic: rw [natDegree_C_mul_X _ hy0]
-- 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
inst_3 : IsReduced R
h : ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
w : R
hy : w ≠ 0
int : IsIntegral R (w • z)
⊢ ¬IsNilpotent w
have rwa : ¬w = 0
Tactic: rwa [isNilpotent_iff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_4
inst_2 : CommRing K
inst_3 : Algebra S K
inst_4 : Algebra R K
inst_5 : IsIntegralClosure S R K
x : K
hx : IsAlgebraic R x
⊢ ∃ (r : R) (s : S), r ≠ 0 ∧ r • x = (algebraMap S K : (a : S) → K) s
have obtain : ∀ (r : R) (hr : r ≠ 0) (h : IsIntegral R (r • x)), ∃ (r : R) (s : S), r ≠ 0 ∧ r • x = (algebraMap S K : (a : S) → K) s
Tactic: obtain ⟨r, hr, h⟩ := hx.exists_integral_multiple
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_4
inst_2 : CommRing K
inst_3 : Algebra S K
inst_4 : Algebra R K
inst_5 : IsIntegralClosure S R K
x : K
hx : IsAlgebraic R x
r : R
hr : r ≠ 0
h : IsIntegral R (r • x)
⊢ ∃ (r : R) (s : S), r ≠ 0 ∧ r • x = (algebraMap S K : (a : S) → K) s
have obtain : ∀ (s : S) (hs : (algebraMap S K : (a : S) → K) s = r • x),
  ∃ (r : R) (s : S), r ≠ 0 ∧ r • x = (algebraMap S K : (a : S) → K) s
Tactic: obtain ⟨s, hs⟩ := IsIntegralClosure.isIntegral_iff (A := S) |>.mp h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra S K
inst_3 : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
⊢ ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s
have obtain : ∀ (a : ℤ) (s : S) (ha : a ≠ 0) (h : a • x = (algebraMap S K : (a : S) → K) s),
  ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s
Tactic: obtain ⟨a, s, ha, h⟩ := hx.exists_smul_eq S
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra S K
inst_3 : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
a : ℤ
s : S
ha : a ≠ 0
h : a • x = (algebraMap S K : (a : S) → K) s
⊢ ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s
have inl : ∀ (n : ℕ) (ha : Ne (α := ℤ) (↑n : ℤ) 0) (h : HSMul.hSMul (α := ℤ) (↑n : ℤ) x = (algebraMap S K : (a : S) → K) s),
  ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s
Tactic: obtain ⟨n, rfl | rfl⟩ := a.eq_nat_or_neg
Cleared hypotheses: a, ha, h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra S K
inst_3 : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
a : ℤ
s : S
ha : a ≠ 0
h : a • x = (algebraMap S K : (a : S) → K) s
inl :
  ∀ (n : ℕ) (ha : Ne (α := ℤ) (↑n : ℤ) 0) (h : HSMul.hSMul (α := ℤ) (↑n : ℤ) x = (algebraMap S K : (a : S) → K) s),
    ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s
⊢ ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s
have inr : ∀ (n : ℕ) (ha : Ne (α := ℤ) (-(↑n : ℤ)) 0) (h : HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x = (algebraMap S K : (a : S) → K) s),
  ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s
Tactic: obtain ⟨n, rfl | rfl⟩ := a.eq_nat_or_neg
Cleared hypotheses: a, ha, h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
⊢ IsAlgebraic R a
have pos : ∀ (hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)), IsAlgebraic R a
Tactic: by_cases hRS : Function.Injective (algebraMap R S)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
pos :
  ∀ (hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)), IsAlgebraic R a
⊢ IsAlgebraic R a
have neg : ∀ (hRS : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)), IsAlgebraic R a
Tactic: by_cases hRS : Function.Injective (algebraMap R S)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsAlgebraic R a
have this : NoZeroDivisors R
Tactic: have := hRS.noZeroDivisors _ (map_zero _) (map_mul _)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
⊢ IsAlgebraic R a
have pos : ∀ (s : S) (hs : s ≠ 0) (int_s : IsIntegral S (s • a)), IsAlgebraic R a
Tactic: have ⟨s, hs, int_s⟩ := h.exists_integral_multiple
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
⊢ IsAlgebraic R a
have pos : Subsingleton R → IsAlgebraic R a
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
pos : Subsingleton R → IsAlgebraic R a
⊢ IsAlgebraic R a
have pos₁ : Nontrivial R → IsAlgebraic R a
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Subsingleton R
⊢ IsAlgebraic R a
have this₁ : Subsingleton S
Tactic: have := Module.subsingleton R S
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Nontrivial R
⊢ IsAlgebraic R a
have pos : ∀ (r : R) (hr : r ≠ 0) (w : S) (e : (algebraMap R S : (a : R) → S) r = s * w), IsAlgebraic R a
Tactic: have ⟨r, hr, _, e⟩ := (int.1 s).isAlgebraic.exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero hs)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Nontrivial R
r : R
hr : r ≠ 0
w : S
e : (algebraMap R S : (a : R) → S) r = s * w
⊢ ¬IsNilpotent r
have rwa : ¬r = 0
Tactic: rwa [isNilpotent_iff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Nontrivial R
r : R
hr : r ≠ 0
w : S
e : (algebraMap R S : (a : R) → S) r = s * w
⊢ IsAlgebraic R a
have pos : IsIntegral R (r • a)
Tactic: refine .of_smul_isIntegral (y := r) (by rwa [isNilpotent_iff_eq_zero]) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Nontrivial R
r : R
hr : r ≠ 0
w : S
e : (algebraMap R S : (a : R) → S) r = s * w
⊢ IsIntegral R (r • a)
have pos : IsIntegral R (w • s • a)
Tactic: rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R S,
    e, ← Algebra.smul_def, mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
⊢ IsAlgebraic R a
have have : ∀ (p : S[X]) (hp : p ≠ 0) (eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)), IsAlgebraic R a
Tactic: have ⟨p, hp, eval0⟩ := h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
⊢ IsAlgebraic R a
have pos : ∀ (hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)), IsAlgebraic R a
Tactic: by_cases hRS : Function.Injective (algebraMap R S)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
pos :
  ∀ (hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)), IsAlgebraic R a
⊢ IsAlgebraic R a
have neg : ∀ (hRS : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)), IsAlgebraic R a
Tactic: by_cases hRS : Function.Injective (algebraMap R S)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsAlgebraic R a
have hRS₁ : FaithfulSMul R S
Tactic: rw [← faithfulSMul_iff_algebraMap_injective] at hRS
Cleared hypotheses: hRS
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : FaithfulSMul R S
⊢ IsAlgebraic R a
have this : NoZeroDivisors R
Tactic: have := NoZeroDivisors.of_faithfulSMul R S
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : FaithfulSMul R S
this : NoZeroDivisors R
⊢ IsAlgebraic R a
have this₁ : Nontrivial R
Tactic: have := Algebra.nontrivial_of_isAlgebraic R S
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this : Nontrivial R
⊢ IsAlgebraic R a
have this₁ : IsDomain R
Tactic: have : IsDomain R := NoZeroDivisors.to_isDomain _
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
⊢ IsAlgebraic R a
have pos : ∀ (r : R) (hr : r ≠ 0) (int : ∀ z ∈ Finset.image p.coeff p.support, IsIntegral R (r • z)), IsAlgebraic R a
Tactic: have ⟨r, hr, int⟩ := Algebra.IsAlgebraic.exists_integral_multiples R (p.support.image (coeff p))
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p.coeff p.support, IsIntegral R (r • z)
s : S
hs : s ∈ (↑(r • p).coeffs : Set S)
⊢ s ∈ (↑(Subalgebra.toSubring (integralClosure R S)) : Set S)
have obtain : ∀ (n : ℕ) (hn : n ∈ (r • p).support) (hs : (r • p).coeff n ∈ (↑(r • p).coeffs : Set S)),
  (r • p).coeff n ∈ (↑(Subalgebra.toSubring (integralClosure R S)) : Set S)
Tactic: obtain ⟨n, hn, rfl⟩ := mem_coeffs_iff.mp hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p_1 : S[X]
hp : p_1 ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p_1 : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p_1.coeff p_1.support, IsIntegral R (r • z)
p : (↥(Subalgebra.toSubring (integralClosure R S)))[X] :=
  (r • p_1).toSubring (Subalgebra.toSubring (integralClosure R S)) ⋯
⊢ IsAlgebraic.{u_2, u_3} (↥(integralClosure R S)) a
have refine_1 : p ≠ 0
Tactic: refine ⟨p, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p_1 : S[X]
hp : p_1 ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p_1 : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p_1.coeff p_1.support, IsIntegral R (r • z)
p : (↥(Subalgebra.toSubring (integralClosure R S)))[X] :=
  (r • p_1).toSubring (Subalgebra.toSubring (integralClosure R S)) ⋯
refine_1 : p ≠ 0
⊢ IsAlgebraic.{u_2, u_3} (↥(integralClosure R S)) a
have refine_2 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)
Tactic: refine ⟨p, ?_, ?_⟩