awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
B : Type u_3
S : Type u_4
inst : Ring B
inst_1 : CommRing S
R : Type u_5
inst_2 : CommSemiring R
inst_3 : Algebra R B
inst_4 : Algebra S B
inst_5 : Algebra R S
inst_6 : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ Membership.mem (γ := Subalgebra S B) S[x] x

Tactic:
Algebra.subset_adjoin rfl

Premises used: Algebra.subset_adjoin, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
B : Type u_3
S : Type u_4
inst : Ring B
inst_1 : CommRing S
R : Type u_5
inst_2 : CommSemiring R
inst_3 : Algebra R B
inst_4 : Algebra S B
inst_5 : Algebra R S
inst_6 : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ Membership.mem (γ := Subalgebra S B) S[x] x

Tactic:
exact Algebra.subset_adjoin rfl

Premises used: Algebra.subset_adjoin, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
a : A
⊢ Membership.mem (γ := Subalgebra R A) (integralClosure R A) a ↔ IsIntegral R a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, RingHom.IsIntegralElem, IsIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A_1 : Type u_2
B_1 : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing A_1
inst_2 : Ring B_1
inst_3 : CommRing S
inst_4 : Algebra R A_1
inst_5 : Algebra R B_1
f_1 : R →+* S
f_2 : R →+* B_1
f : R →+* S
A : Type u_5
B : Type u_6
inst_6 : Ring A
inst_7 : Algebra R A
inst_8 : Ring B
inst_9 : Algebra R B
inst_10 : Algebra.IsIntegral R A
inst_11 : Algebra.IsIntegral R B
⊢ Algebra.IsIntegral R (A × B)

Tactic:
Algebra.isIntegral_def.mpr fun x ↦
    (Algebra.isIntegral_def.mp ‹_› x.1).pair (Algebra.isIntegral_def.mp ‹_› x.2)

Premises used: Iff.mpr, IsIntegral.pair, Algebra.isIntegral_def, Prod.fst, Iff.mp, Prod.snd
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.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
x : A
y : B
h : IsIntegral R y
rw : IsIntegral A (HSMul.hSMul (β := A ⊗[R] B) x (1 ⊗ₜ[R] y))
⊢ IsIntegral A (A := A ⊗[R] B) (x ⊗ₜ[R] y)

Tactic:
rw [← mul_one x, ← smul_eq_mul, ← smul_tmul']

Premises used: TensorProduct.smul_tmul', smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.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
x : A
y : B
h : IsIntegral R y
⊢ IsIntegral A (HSMul.hSMul (β := A ⊗[R] B) x (1 ⊗ₜ[R] y))

Tactic:
smul _ (h.map_of_comp_eq (algebraMap R A)
    (Algebra.TensorProduct.includeRight (R := R) (A := A) (B := B)).toRingHom
    Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap)

Premises used: Algebra.algebraMap, Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap, IsIntegral.smul, IsIntegral.map_of_comp_eq, AlgHom.toRingHom, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.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
x : A
y : B
h : IsIntegral R y
⊢ IsIntegral A (HSMul.hSMul (β := A ⊗[R] B) x (1 ⊗ₜ[R] y))

Tactic:
exact smul _ (h.map_of_comp_eq (algebraMap R A)
    (Algebra.TensorProduct.includeRight (R := R) (A := A) (B := B)).toRingHom
    Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap)

Premises used: Algebra.algebraMap, Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap, IsIntegral.smul, IsIntegral.map_of_comp_eq, AlgHom.toRingHom, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g h : G
x : ↥(integralClosure R K)
a : (↑((g * h) • x) : K) = (↑(g • h • x) : K)
⊢ (g * h) • x = g • h • x

Tactic:
ext
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g h : G
x : ↥(integralClosure R K)
⊢ (↑((g * h) • x) : K) = (↑(g • h • x) : K)

Tactic:
mul_smul g h (x : K)

Premises used: Subtype.val, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g h : G
x : ↥(integralClosure R K)
⊢ (↑((g * h) • x) : K) = (↑(g • h • x) : K)

Tactic:
exact mul_smul g h (x : K)

Premises used: Subtype.val, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
x : ↥(integralClosure R K)
a : (↑(HSMul.hSMul.{u_1, u_3, u_3} (α := G) 1 x) : K) = (↑x : K)
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := G) 1 x = x

Tactic:
ext
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
x : ↥(integralClosure R K)
⊢ (↑(HSMul.hSMul.{u_1, u_3, u_3} (α := G) 1 x) : K) = (↑x : K)

Tactic:
one_smul G (x : K)

Premises used: one_smul, Subtype.val
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
x : ↥(integralClosure R K)
⊢ (↑(HSMul.hSMul.{u_1, u_3, u_3} (α := G) 1 x) : K) = (↑x : K)

Tactic:
exact one_smul G (x : K)

Premises used: one_smul, Subtype.val
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
a : (↑(HSMul.hSMul (β := ↥(integralClosure R K)) g 0) : K) = (↑0 : K)
⊢ HSMul.hSMul (β := ↥(integralClosure R K)) g 0 = 0

Tactic:
ext
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
⊢ (↑(HSMul.hSMul (β := ↥(integralClosure R K)) g 0) : K) = (↑0 : K)

Tactic:
smul_zero g

Premises used: smul_zero
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
⊢ (↑(HSMul.hSMul (β := ↥(integralClosure R K)) g 0) : K) = (↑0 : K)

Tactic:
exact smul_zero g

Premises used: smul_zero
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
a : (↑(g • (x + y)) : K) = (↑(g • x + g • y) : K)
⊢ g • (x + y) = g • x + g • y

Tactic:
ext
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ (↑(g • (x + y)) : K) = (↑(g • x + g • y) : K)

Tactic:
smul_add g (x : K) (y : K)

Premises used: Subtype.val, smul_add
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ (↑(g • (x + y)) : K) = (↑(g • x + g • y) : K)

Tactic:
exact smul_add g (x : K) (y : K)

Premises used: Subtype.val, smul_add
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
a : (↑(HSMul.hSMul (β := ↥(integralClosure R K)) g 1) : K) = (↑1 : K)
⊢ HSMul.hSMul (β := ↥(integralClosure R K)) g 1 = 1

Tactic:
ext
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
⊢ (↑(HSMul.hSMul (β := ↥(integralClosure R K)) g 1) : K) = (↑1 : K)

Tactic:
smul_one g

Premises used: MulDistribMulAction.smul_one
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
⊢ (↑(HSMul.hSMul (β := ↥(integralClosure R K)) g 1) : K) = (↑1 : K)

Tactic:
exact smul_one g

Premises used: MulDistribMulAction.smul_one
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
a : (↑(g • (x * y)) : K) = (↑(g • x * g • y) : K)
⊢ g • (x * y) = g • x * g • y

Tactic:
ext
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ (↑(g • (x * y)) : K) = (↑(g • x * g • y) : K)

Tactic:
smul_mul' g (x : K) (y : K)

Premises used: Subtype.val, smul_mul'
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ (↑(g • (x * y)) : K) = (↑(g • x * g • y) : K)

Tactic:
exact smul_mul' g (x : K) (y : K)

Premises used: Subtype.val, smul_mul'
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
k : ↥(integralClosure R K)
⊢ (↑(g • k) : K) = g • (↑k : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Defs
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
⊢ Algebra.IsIntegral R A ↔ ∀ (x : A), IsIntegral R x

Tactic:
⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Premises used: Iff.intro, _private.0.Algebra.isIntegral_def.match_1, Algebra.IsIntegral.mk
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Defs
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
⊢ RingHom.IsIntegral (algebraMap R A) ↔ Algebra.IsIntegral R A

Tactic:
(Algebra.isIntegral_iff ..).symm

Premises used: IsIntegral, RingHom.IsIntegral, Iff.symm, Algebra.isIntegral_iff
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P x : R[X]
hx :
  Membership.mem (γ := Set R[X])
    {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x} x
i : ℕ
mem : ∀ (r : R) (hrI : r ∈ I), (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X).coeff i ∈ I ^ i
⊢ x.coeff i ∈ I ^ i

Tactic:
obtain ⟨r, hrI, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P : R[X]
i : ℕ
r : R
hrI : r ∈ I
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X).coeff i ∈ I ^ i

Tactic:
simp +contextual [coeff_X, apply_ite, hrI, @eq_comm _ 1]

Premises used: apply_ite, eq_comm, Polynomial.coeff_X
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P : R[X]
r : R
i : ℕ
⊢ coeff ((algebraMap R R[X] : (a : R) → R[X]) r) i ∈ I ^ i

Tactic:
simp +contextual [coeff_C, apply_ite]

Premises used: apply_ite, Polynomial.coeff_C
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P x y : R[X]
hx :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) x
hy :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) y
h : ∀ (i : ℕ), x.coeff i ∈ I ^ i
h_1 : ∀ (i : ℕ), y.coeff i ∈ I ^ i
i : ℕ
⊢ (x + y).coeff i ∈ I ^ i

Tactic:
aesop
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P x y : R[X]
hx_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) x
hy_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) y
hx : ∀ (i : ℕ), x.coeff i ∈ I ^ i
hy : ∀ (i : ℕ), y.coeff i ∈ I ^ i
i : ℕ
mul : ∑ x_1 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, x.coeff x_1.1 * y.coeff x_1.2 ∈ I ^ i
⊢ (x * y).coeff i ∈ I ^ i

Tactic:
rw [coeff_mul]

Premises used: Polynomial.coeff_mul
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P x y : R[X]
hx_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) x
hy_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) y
hx : ∀ (i : ℕ), x.coeff i ∈ I ^ i
hy : ∀ (i : ℕ), y.coeff i ∈ I ^ i
i : ℕ
⊢ ∑ x_1 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, x.coeff x_1.1 * y.coeff x_1.2 ∈ I ^ i

Tactic:
sum_mem fun ⟨j₁, j₂⟩ hj ↦ ?_

Premises used: HMul.hMul, Membership.mem, Prod.fst, Polynomial.coeff, HPow.hPow, _private.0.Polynomial.coeff_mem_pow_of_mem_adjoin_C_mul_X.match_2, Prod.snd, sum_mem
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P x y : R[X]
hx_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) x
hy_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) y
hx : ∀ (i : ℕ), x.coeff i ∈ I ^ i
hy : ∀ (i : ℕ), y.coeff i ∈ I ^ i
i : ℕ
mul :
  ∀ (x_1 : ℕ × ℕ) (j₁ j₂ : ℕ) (hj : (j₁, j₂) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i),
    x.coeff (j₁, j₂).1 * y.coeff (j₁, j₂).2 ∈ I ^ i
⊢ ∑ x_1 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, x.coeff x_1.1 * y.coeff x_1.2 ∈ I ^ i

Tactic:
refine sum_mem fun ⟨j₁, j₂⟩ hj ↦ ?_

Premises used: sum_mem
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P x y : R[X]
hx_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) x
hy_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) y
hx : ∀ (i : ℕ), x.coeff i ∈ I ^ i
hy : ∀ (i : ℕ), y.coeff i ∈ I ^ i
i : ℕ
x_1 : ℕ × ℕ
j₁ j₂ : ℕ
hj : (j₁, j₂) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
⊢ j₁ + j₂ = i

Tactic:
simpa using hj
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P x y : R[X]
hx_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) x
hy_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) y
hx : ∀ (i : ℕ), x.coeff i ∈ I ^ i
hy : ∀ (i : ℕ), y.coeff i ∈ I ^ i
i : ℕ
x_1 : ℕ × ℕ
j₁ j₂ : ℕ
hj : (j₁, j₂) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
mul :
  ∀ (hj : (j₁, j₂) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (j₁ + j₂)),
    x.coeff (j₁, j₂).1 * y.coeff (j₁, j₂).2 ∈ I ^ (j₁ + j₂)
⊢ x.coeff (j₁, j₂).1 * y.coeff (j₁, j₂).2 ∈ I ^ i

Tactic:
obtain rfl : j₁ + j₂ = i := by simpa using hj

Premises used: rfl
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P x y : R[X]
hx_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) x
hy_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) y
hx : ∀ (i : ℕ), x.coeff i ∈ I ^ i
hy : ∀ (i : ℕ), y.coeff i ∈ I ^ i
x_1 : ℕ × ℕ
j₁ j₂ : ℕ
hj : (j₁, j₂) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (j₁ + j₂)
⊢ x.coeff (j₁, j₂).1 * y.coeff (j₁, j₂).2 ∈ I ^ (j₁ + j₂)

Tactic:
pow_add I j₁ j₂ ▸ Ideal.mul_mem_mul (hx _) (hy _)

Premises used: Set.Mem, pow_add, Eq.rec, Ideal.mul_mem_mul, Eq.symm
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P x y : R[X]
hx_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) x
hy_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) y
hx : ∀ (i : ℕ), x.coeff i ∈ I ^ i
hy : ∀ (i : ℕ), y.coeff i ∈ I ^ i
x_1 : ℕ × ℕ
j₁ j₂ : ℕ
hj : (j₁, j₂) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (j₁ + j₂)
⊢ x.coeff (j₁, j₂).1 * y.coeff (j₁, j₂).2 ∈ I ^ (j₁ + j₂)

Tactic:
exact pow_add I j₁ j₂ ▸ Ideal.mul_mem_mul (hx _) (hy _)
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P : R[X]
hP :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) P
i : ℕ
mem :
  ∀ (x : R[X])
    (hx :
      Membership.mem (γ := Set R[X])
        {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x} x)
    (i : ℕ), x.coeff i ∈ I ^ i
algebraMap : ∀ (r : R) (i : ℕ), coeff ((Algebra.algebraMap R R[X] : (a : R) → R[X]) r) i ∈ I ^ i
add :
  ∀ (x y : R[X])
    (hx :
      Membership.mem (γ := Subalgebra R R[X])
        (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x})
        x)
    (hy :
      Membership.mem (γ := Subalgebra R R[X])
        (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x})
        y),
    (∀ (i : ℕ), x.coeff i ∈ I ^ i) → (∀ (i : ℕ), y.coeff i ∈ I ^ i) → ∀ (i : ℕ), (x + y).coeff i ∈ I ^ i
mul :
  ∀ (x y : R[X]),
    Membership.mem (γ := Subalgebra R R[X])
        (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x})
        x →
      Membership.mem (γ := Subalgebra R R[X])
          (Algebra.adjoin R
            {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x})
          y →
        ∀ (hx : ∀ (i : ℕ), x.coeff i ∈ I ^ i) (hy : ∀ (i : ℕ), y.coeff i ∈ I ^ i) (i : ℕ), (x * y).coeff i ∈ I ^ i
⊢ P.coeff i ∈ I ^ i

Tactic:
induction hP using Algebra.adjoin_induction generalizing i with
  | mem x hx =>
    obtain ⟨r, hrI, rfl⟩ := hx
    simp +contextual [coeff_X, apply_ite, hrI, @eq_comm _ 1]
  | algebraMap r => simp +contextual [coeff_C, apply_ite]
  | add x y hx hy _ _ => aesop
  | mul x y _ _ hx hy =>
    rw [coeff_mul]
    refine sum_mem fun ⟨j₁, j₂⟩ hj ↦ ?_
    obtain rfl : j₁ + j₂ = i := by simpa using hj
    exact pow_add I j₁ j₂ ▸ Ideal.mul_mem_mul (hx _) (hy _)

Premises used: Algebra.algebraMap, apply_ite, Polynomial.coeff_mul, eq_comm, Polynomial.coeff_C, Polynomial.coeff_X, sum_mem, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
x : S
hx :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
inl :
  Subsingleton R →
    ∃ (p : R[X]),
      p.Monic ∧
        Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
inr :
  Nontrivial R →
    ∃ (p : R[X]),
      p.Monic ∧
        Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
x : S
hx :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
h_1 : Subsingleton R
h :
  Monic.{u_1} (R := R) 0 ∧
    Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) 0 : S) (0 : S) ∧
      ∀ (i : ℕ), coeff 0 i ∈ I ^ (natDegree.{u_1} (R := R) 0 - i)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)

Tactic:
use 0
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
x : S
hx :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
h : Subsingleton R
⊢ Monic.{u_1} (R := R) 0 ∧
    Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) 0 : S) (0 : S) ∧
      ∀ (i : ℕ), coeff 0 i ∈ I ^ (natDegree.{u_1} (R := R) 0 - i)

Tactic:
simp [Monic, Subsingleton.elim (α := R) 0 1]

Premises used: Polynomial.Monic, Subsingleton.elim, OfNat.ofNat