awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_6
B : Type u_7
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
x : A
⊢ IsIntegral.{u_1, u_7} R (A := B) ((f : (a : A) → B) x : B) ↔ IsIntegral R x

Tactic:
simp [IsIntegral, ← RingHom.IsIntegralElem.map_iff (g := (f : A →+* B)) hf]

Premises used: IsIntegral, RingHom.IsIntegralElem.map_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
h : Nontrivial A
hf : Monic.{u_6} (R := R) 1
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) 1 : A) (0 : A)
⊢ False

Tactic:
simp [one_ne_zero' A] at hfx

Premises used: one_ne_zero'
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
⊢ f ≠ 1

Tactic:
have hf1 : f ≠ 1 := by rintro rfl; simp [one_ne_zero' A] at hfx
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
⊢ Eq (α := Submodule R A) (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x])

Tactic:
(span_le.mpr fun s hs ↦ ?_).antisymm fun r hr ↦ ?_

Premises used: Iff.mpr, LE.le.antisymm, Submodule.span_le
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
refine_1 :
  ∀ (s : A) (hs : s ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)),
    s ∈ (↑((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x] : Submodule R A) : Set A)
refine_2 :
  ∀ (r : A)
    (hr :
      Membership.mem (γ := Submodule R A)
        ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x] : Submodule R A) r),
    Membership.mem (γ := Submodule R A)
      (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)) r
⊢ Eq (α := Submodule R A) (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x])

Tactic:
refine (span_le.mpr fun s hs ↦ ?_).antisymm fun r hr ↦ ?_

Premises used: Iff.mpr, LE.le.antisymm, Submodule.span_le
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
s : A
hs : s ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)
refine_1 :
  ∀ (k : ℕ) (hs : x ^ k ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)),
    x ^ k ∈ (↑((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x] : Submodule R A) : Set A)
⊢ s ∈ (↑((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x] : Submodule R A) : Set A)

Tactic:
rcases Finset.mem_image.1 (SetLike.mem_coe.mp hs) with ⟨k, -, rfl⟩

Premises used: Finset.mem_image, SetLike.mem_coe, Iff.mp, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
k : ℕ
hs : x ^ k ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)
⊢ x ^ k ∈ (↑((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x] : Submodule R A) : Set A)

Tactic:
(Algebra.adjoin R {x}).pow_mem (Algebra.subset_adjoin rfl) k

Premises used: iInf, Set.Mem, Set.iInter, Algebra.subset_adjoin, setOf, Algebra.adjoin, Subalgebra.pow_mem, Singleton.singleton, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
k : ℕ
hs : x ^ k ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)
⊢ x ^ k ∈ (↑((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x] : Submodule R A) : Set A)

Tactic:
exact (Algebra.adjoin R {x}).pow_mem (Algebra.subset_adjoin rfl) k

Premises used: Algebra.subset_adjoin, Algebra.adjoin, Subalgebra.pow_mem, Singleton.singleton, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
r : A
hr :
  Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x] : Submodule R A) r
⊢ Membership.mem (γ := Subalgebra R A) (AlgHom.range (aeval x)) r

Tactic:
rw [Subalgebra.mem_toSubmodule, Algebra.adjoin_singleton_eq_range_aeval] at hr

Premises used: Subalgebra.mem_toSubmodule, Algebra.adjoin_singleton_eq_range_aeval
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
r : A
hr : Membership.mem (γ := Subalgebra R A) (AlgHom.range (aeval x)) r
refine_2 :
  ∀ (p : R[X])
    (hr : Membership.mem (α := A) (γ := Subalgebra R A) (AlgHom.range (aeval x)) ((aeval x : (a : R[X]) → A) p : A)),
    Membership.mem (α := A) (γ := Submodule R A)
      (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
      ((aeval x : (a : R[X]) → A) p : A)
⊢ Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)) r

Tactic:
rcases (aeval x).mem_range.mp hr with ⟨p, rfl⟩

Premises used: AlgHom.mem_range, Iff.mp, Polynomial.aeval, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : Membership.mem (α := A) (γ := Subalgebra R A) (AlgHom.range (aeval x)) ((aeval x : (a : R[X]) → A) p : A)
refine_2 :
  Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    (∑ n ∈ (p %ₘ f).support,
      eval₂ (algebraMap R A) x
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((p %ₘ f).coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)))
⊢ Membership.mem (α := A) (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    ((aeval x : (a : R[X]) → A) p : A)

Tactic:
rw [← modByMonic_add_div p f, map_add, map_mul, hfx,
      zero_mul, add_zero, ← sum_C_mul_X_pow_eq (p %ₘ f), aeval_def, eval₂_sum, sum_def]

Premises used: MulZeroClass.zero_mul, Polynomial.eval₂_sum, Polynomial.sum_C_mul_X_pow_eq, map_add, Polynomial.aeval_def, map_mul, Polynomial.modByMonic, Polynomial.sum_def, Polynomial.modByMonic_add_div, add_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : Membership.mem (α := A) (γ := Subalgebra R A) (AlgHom.range (aeval x)) ((aeval x : (a : R[X]) → A) p : A)
⊢ Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    (∑ n ∈ (p %ₘ f).support,
      eval₂ (algebraMap R A) x
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((p %ₘ f).coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)))

Tactic:
sum_mem fun k hkq ↦ ?_

Premises used: sum_mem
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : Membership.mem (α := A) (γ := Subalgebra R A) (AlgHom.range (aeval x)) ((aeval x : (a : R[X]) → A) p : A)
refine_2 :
  ∀ (k : ℕ) (hkq : k ∈ (p %ₘ f).support),
    Membership.mem (γ := Submodule R A)
      (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
      (eval₂ (algebraMap R A) x
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((p %ₘ f).coeff k) : R[X]) (HPow.hPow (α := R[X]) X k)))
⊢ Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    (∑ n ∈ (p %ₘ f).support,
      eval₂ (algebraMap R A) x
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((p %ₘ f).coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)))

Tactic:
refine sum_mem fun k hkq ↦ ?_

Premises used: sum_mem
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : Membership.mem (α := A) (γ := Subalgebra R A) (AlgHom.range (aeval x)) ((aeval x : (a : R[X]) → A) p : A)
k : ℕ
hkq : k ∈ (p %ₘ f).support
refine_2 :
  Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)) ((p %ₘ f).coeff k • x ^ k)
⊢ Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    (eval₂ (algebraMap R A) x
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((p %ₘ f).coeff k) : R[X]) (HPow.hPow (α := R[X]) X k)))

Tactic:
rw [C_mul_X_pow_eq_monomial, eval₂_monomial, ← Algebra.smul_def]

Premises used: Polynomial.eval₂_monomial, Polynomial.C_mul_X_pow_eq_monomial, Algebra.smul_def
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : Membership.mem (α := A) (γ := Subalgebra R A) (AlgHom.range (aeval x)) ((aeval x : (a : R[X]) → A) p : A)
k : ℕ
hkq : k ∈ (p %ₘ f).support
⊢ Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)) ((p %ₘ f).coeff k • x ^ k)

Tactic:
smul_mem _ _ (subset_span <| Finset.mem_image_of_mem _ <| Finset.mem_range.mpr <|
    (le_natDegree_of_mem_supp _ hkq).trans_lt <| natDegree_modByMonic_lt p hf hf1)

Premises used: Iff.mpr, Polynomial.le_natDegree_of_mem_supp, Set.Mem, Polynomial.natDegree_modByMonic_lt, Finset.mem_range, Submodule.subset_span, Finset.mem_image_of_mem, LE.le.trans_lt, Submodule.smul_mem
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : Membership.mem (α := A) (γ := Subalgebra R A) (AlgHom.range (aeval x)) ((aeval x : (a : R[X]) → A) p : A)
k : ℕ
hkq : k ∈ (p %ₘ f).support
⊢ Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)) ((p %ₘ f).coeff k • x ^ k)

Tactic:
exact smul_mem _ _ (subset_span <| Finset.mem_image_of_mem _ <| Finset.mem_range.mpr <|
    (le_natDegree_of_mem_supp _ hkq).trans_lt <| natDegree_modByMonic_lt p hf hf1)

Premises used: Iff.mpr, Polynomial.le_natDegree_of_mem_supp, Polynomial.natDegree_modByMonic_lt, Finset.mem_range, Submodule.subset_span, Finset.mem_image_of_mem, LE.le.trans_lt, Submodule.smul_mem
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
hx : IsIntegral R x
rcases :
  ∀ (f : R[X]) (hfm : f.Monic) (hfx : eval₂ (algebraMap R B) x f = 0),
    FG.{u_1, u_3} (R := R) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])
⊢ FG.{u_1, u_3} (R := R) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])

Tactic:
rcases hx with ⟨f, hfm, hfx⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
f : R[X]
hfm : f.Monic
hfx : eval₂ (algebraMap R B) x f = 0
h :
  Eq (α := Submodule R B) (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set B))
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])
⊢ FG.{u_1, u_3} (R := R) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])

Tactic:
use (Finset.range <| f.natDegree).image (x ^ ·)

Premises used: Finset.range, HPow.hPow, Polynomial.natDegree, Finset.image
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
f : R[X]
hfm : f.Monic
hfx rwa rwa₁ rwa₂ rwa₃ : eval₂ (algebraMap R B) x f = 0
⊢ Eq.{u_3 + 1} (α := B) ((aeval x : (a : R[X]) → B) f : B) (0 : B)

Tactic:
rwa [aeval_def]

Premises used: Polynomial.aeval_def
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
f : R[X]
hfm : f.Monic
hfx : eval₂ (algebraMap R B) x f = 0
⊢ Eq (α := Submodule R B) (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set B))
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])

Tactic:
exact span_range_natDegree_eq_adjoin hfm (by rwa [aeval_def])

Premises used: Submodule.span_range_natDegree_eq_adjoin
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
hx : IsIntegral R x
rcases :
  ∀ (f : R[X]) (hfm : f.Monic) (hfx : eval₂ (algebraMap R B) x f = 0),
    FG.{u_1, u_3} (R := R) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])
h :
  ∀ (f : R[X]) (hfm : f.Monic) (hfx : eval₂ (algebraMap R B) x f = 0),
    Eq (α := Submodule R B) (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set B))
      ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])
⊢ FG.{u_1, u_3} (R := R) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])

Tactic:
classical
  rcases hx with ⟨f, hfm, hfx⟩
  use (Finset.range <| f.natDegree).image (x ^ ·)
  exact span_range_natDegree_eq_adjoin hfm (by rwa [aeval_def])
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
f : R →+* B
⊢ f.IsIntegralElem 0

Tactic:
f.map_zero ▸ f.isIntegralElem_map

Premises used: Eq.rec, RingHom.isIntegralElem_map, RingHom.map_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
⊢ IsIntegral.{u_1, u_3} R (A := B) 0

Tactic:
(algebraMap R B).isIntegralElem_zero

Premises used: Algebra.algebraMap, IsIntegral, RingHom.isIntegralElem_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
f : R →+* B
⊢ f.IsIntegralElem 1

Tactic:
f.map_one ▸ f.isIntegralElem_map

Premises used: RingHom.map_one, Eq.rec, RingHom.isIntegralElem_map
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
⊢ IsIntegral.{u_1, u_3} R (A := B) 1

Tactic:
(algebraMap R B).isIntegralElem_one

Premises used: Algebra.algebraMap, RingHom.isIntegralElem_one, IsIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
n : ℕ
hn : 0 < n
hx : IsIntegral R (x ^ n)
p : R[X]
hmonic : p.Monic
heval : eval₂ (algebraMap R B) (x ^ n) p = 0
rwa : Eq.{u_3 + 1} (α := B) ((aeval x : (a : R[X]) → B) ((expand R n : (a : R[X]) → R[X]) p : R[X]) : B) (0 : B)
rwa₁ rwa₂ rwa₃ rwa₄ : Eq.{u_3 + 1} (α := B) ((aeval (x ^ n) : (a : R[X]) → B) p : B) (0 : B)
⊢ eval₂ (algebraMap R B) x ((expand R n : (a : R[X]) → R[X]) p) = 0

Tactic:
rwa [← aeval_def, expand_aeval]

Premises used: Polynomial.aeval_def, Polynomial.expand_aeval
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : A
p_1 : R[X]
monic : p_1.Monic
deg : p_1.natDegree ≠ 0
hx : IsIntegral.{u_1, u_2} R (A := A) ((aeval x : (a : R[X]) → A) p_1 : A)
p : R[X]
hmonic : p.Monic
heval : eval₂ (algebraMap R A) ((aeval x : (a : R[X]) → A) p_1) p = 0
rwa : eval₂ (algebraMap R A) (eval₂ (algebraMap R A) x p_1) p = 0
rwa₁ rwa₂ rwa₃ rwa₄ : eval₂ (algebraMap R A) ((aeval x : (a : R[X]) → A) p_1) p = 0
⊢ eval₂ (algebraMap R A) x (p.comp p_1) = 0

Tactic:
rwa [eval₂_comp, ← aeval_def x]

Premises used: Polynomial.aeval_def, Polynomial.eval₂_comp
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Ring U
inst_4 : Algebra R S
inst_5 : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
rw :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap T U) (Polynomial.map φ p)) : U) (0 : U)
rw₁ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (RingHom.comp (algebraMap T U) φ) p) : U) (0 : U)
rw₂ : Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (ψ.comp (algebraMap R S)) p) : U) (0 : U)
rw₃ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map ψ (Polynomial.map (algebraMap R S) p)) : U) (0 : U)
rw₄ : eval₂ ψ ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap R S) p) = 0
rw₅ : Eq.{u_8 + 1} (α := U) ((ψ : (a : S) → U) (eval a (Polynomial.map (algebraMap R S) p)) : U) (0 : U)
rw₆ : Eq.{u_8 + 1} (α := U) ((ψ : (a : S) → U) (eval₂ (algebraMap R S) a p) : U) (0 : U)
rw₇ : Eq.{u_8 + 1} (α := U) ((ψ : (a : S) → U) 0 : U) (0 : U)
rw₈ rw₉ : Eq.{u_8 + 1} (α := U) 0 0
⊢ eval₂ (algebraMap T U) ((ψ : (a : S) → U) a) (Polynomial.map φ p) = 0

Tactic:
rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]

Premises used: Polynomial.eval_map, RingHom.map_zero, And.right, Polynomial.eval₂_at_apply, Polynomial.map_map
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_5
B : Type u_6
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A ≃ₐ[R] B
x : A
h : IsIntegral.{u_1, u_6} R (A := B) ((f : (a : A) → B) x : B)
⊢ IsIntegral R x

Tactic:
simpa using h.map f.symm

Premises used: AlgEquiv.symm, IsIntegral.map
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
x : B
hx : IsIntegral R x
p : R[X]
hp : p.Monic
hpx : eval₂ (algebraMap R B) x p = 0
rw : Eq.{u_3 + 1} (α := B) ((aeval x : (a : A[X]) → B) (Polynomial.map (algebraMap R A) p) : B) (0 : B)
rw₁ : Eq.{u_3 + 1} (α := B) ((aeval x : (a : R[X]) → B) p : B) (0 : B)
rw₂ : eval₂ (algebraMap R B) x p = 0
rw₃ rw₄ : Eq.{u_3 + 1} (α := B) 0 0
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap R A) p) = 0

Tactic:
rw [← aeval_def, aeval_map_algebraMap, aeval_def, hpx]

Premises used: Polynomial.aeval_map_algebraMap, Polynomial.aeval_def
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra T S
φ : R ≃+* T
h : Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ.toRingHom) (algebraMap R S)
a : S
mp : IsIntegral R a → IsIntegral T a
mpr : IsIntegral T a → IsIntegral R a
⊢ IsIntegral R a ↔ IsIntegral T a

Tactic:
constructor
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra T S
φ : R ≃+* T
h : Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ.toRingHom) (algebraMap R S)
a : S
ha : IsIntegral R a
this : Algebra R T := φ.toRingHom.toAlgebra
r : R
t : T
s : S
simp :
  HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) ((algebraMap R T : (a : R) → T) r : T) : S)
      (HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) t : S) s) =
    HMul.hMul (α := S) ((RingHom.comp (algebraMap T S) φ.toRingHom : (a : R) → S) r : S)
      (HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) t : S) s)
⊢ (r • t) • s = r • t • s

Tactic:
simp only [Algebra.smul_def, map_mul, ← h, mul_assoc]

Premises used: mul_assoc, map_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra T S
φ : R ≃+* T
h : Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ.toRingHom) (algebraMap R S)
a : S
ha : IsIntegral R a
this : Algebra R T := φ.toRingHom.toAlgebra
r : R
t : T
s : S
⊢ HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) ((algebraMap R T : (a : R) → T) r : T) : S)
      (HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) t : S) s) =
    HMul.hMul (α := S) ((RingHom.comp (algebraMap T S) φ.toRingHom : (a : R) → S) r : S)
      (HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) t : S) s)

Tactic:
rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra T S
φ : R ≃+* T
h : Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ.toRingHom) (algebraMap R S)
a : S
ha : IsIntegral R a
this_1 : Algebra R T := φ.toRingHom.toAlgebra
this : IsScalarTower R T S := ⋯
⊢ IsIntegral T a

Tactic:
IsIntegral.tower_top ha

Premises used: IsIntegral.tower_top
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra T S
φ : R ≃+* T
h : Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ.toRingHom) (algebraMap R S)
a : S
ha : IsIntegral R a
this_1 : Algebra R T := φ.toRingHom.toAlgebra
this : IsScalarTower R T S := ⋯
⊢ IsIntegral T a

Tactic:
exact IsIntegral.tower_top ha

Premises used: IsIntegral.tower_top