mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
hr : IsRegular r
inst✝ : Flat R M
h : Function.Injective ⇑(rTensor M (toSpanSingleton R R r))
h2 : (fun x ↦ r • x) = ⇑(↑(TensorProduct.lid R M) ∘ₗ rTensor M (toSpanSingleton R R r) ∘ₗ ↑(TensorProduct.lid R M).symm)
⊢ Function.Injective ⇑(↑(TensorProduct.lid R M) ∘ₗ rTensor M (toSpanSingleton R R r) ∘ₗ ↑(TensorProduct.lid R M).symm)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
hr : IsRegular r
inst✝ : Flat R M
h : Function.Injective ⇑(rTensor M (toSpanSingleton R R r))
h2 : (fun x ↦ r • x) = ⇑(↑(TensorProduct.lid R M) ∘ₗ rTensor M (toSpanSingleton R R r) ∘ₗ ↑(TensorProduct.lid R M).symm)
⊢ Function.Injective ⇑(↑(TensorProduct.lid R M) ∘ₗ rTensor M (toSpanSingleton R R r) ∘ₗ ↑(TensorProduct.lid R M).symm)
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Flat R M
⊢ torsion R M ≤ ⊥

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Flat R M
⊢ torsion R M ≤ ⊥
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
pX : R[X]
hpX : pX ∈ P
hp0 : map (Ideal.Quotient.mk (comap C P)) pX ≠ 0
a : R ⧸ P' := (map (Ideal.Quotient.mk P') pX).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hP'_prime : P'.IsPrime
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
⊢ (algebraMap (R[X] ⧸ P) (Localization M')).comp φ = (algebraMap (R[X] ⧸ P) (Localization M')).comp φ

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
⊢ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(lift (lsmul R M ∘ₗ Submodule.subtype I))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
⊢ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(lift (lsmul R M ∘ₗ Submodule.subtype I))
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
⊢ P = P ⊔ comap f ⊥

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
⊢ P = P ⊔ comap f ⊥
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
⊢ ¬I = ⊥

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
⊢ ¬I = ⊥
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
hPJ : P = comap f (Ideal.map f P)
⊢ (((Ideal.Quotient.mk (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P)).comp C).comp
      (Ideal.Quotient.mk (comap C P))).IsIntegral

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
hPJ : P = comap f (Ideal.map f P)
⊢ (((Ideal.Quotient.mk (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P)).comp C).comp
      (Ideal.Quotient.mk (comap C P))).IsIntegral
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this✝ : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
hPJ : P = comap f (Ideal.map f P)
this : (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P).IsMaximal
z : R
hx : C ((Ideal.Quotient.mk P') z) ∈ Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P
⊢ C ((Ideal.Quotient.mk P') z) ∈ Ideal.map f P

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this✝ : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
hPJ : P = comap f (Ideal.map f P)
this : (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P).IsMaximal
z : R
hx : C ((Ideal.Quotient.mk P') z) ∈ Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P
⊢ C ((Ideal.Quotient.mk P') z) ∈ Ideal.map f P
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective (⇑((lsmul R M) (IsPrincipal.generator I)) ∘ ⇑(lift (lsmul R M)))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective (⇑((lsmul R M) (IsPrincipal.generator I)) ∘ ⇑(lift (lsmul R M)))
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
⊢ (comap ((Ideal.Quotient.mk P).comp C) ⊥).IsMaximal

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
⊢ (comap ((Ideal.Quotient.mk P).comp C) ⊥).IsMaximal
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ (g.comp ((Ideal.Quotient.mk (RingHom.ker f)).comp C)).IsIntegral

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ (g.comp ((Ideal.Quotient.mk (RingHom.ker f)).comp C)).IsIntegral
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective (⇑((lsmul R M) (IsPrincipal.generator I)) ∘ ⇑(lift (lsmul R M)))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective (⇑((lsmul R M) (IsPrincipal.generator I)) ∘ ⇑(lift (lsmul R M)))
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hf : Function.Surjective (⇑g ∘ ⇑(Ideal.Quotient.mk (RingHom.ker f)))
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ Function.Surjective ⇑g

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hf : Function.Surjective (⇑g ∘ ⇑(Ideal.Quotient.mk (RingHom.ker f)))
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ Function.Surjective ⇑g
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case intro
R : Type u_1
inst✝² : CommRing R
ι : Type u_2
inst✝¹ : _root_.Finite ι
inst✝ : IsJacobsonRing R
val✝ : Fintype ι
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
⊢ IsJacobsonRing (MvPolynomial (Fin (Fintype.card ι)) R)

Tactic:
]

Goal state after:
case intro
R : Type u_1
inst✝² : CommRing R
ι : Type u_2
inst✝¹ : _root_.Finite ι
inst✝ : IsJacobsonRing R
val✝ : Fintype ι
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
⊢ IsJacobsonRing (MvPolynomial (Fin (Fintype.card ι)) R)
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective (⇑(lift (lsmul R M)) ∘ ⇑(TensorProduct.lid R M).symm.toEquiv)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective (⇑(lift (lsmul R M)) ∘ ⇑(TensorProduct.lid R M).symm.toEquiv)
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], ValuationRing (Localization P.primeCompl)
h : IsTorsionFree R M
P : Ideal R
hP : P.IsMaximal
⊢ Flat R (LocalizedModule P.primeCompl M)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], ValuationRing (Localization P.primeCompl)
h : IsTorsionFree R M
P : Ideal R
hP : P.IsMaximal
⊢ Flat R (LocalizedModule P.primeCompl M)
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], ValuationRing (Localization P.primeCompl)
h : IsTorsionFree R M
P : Ideal R
hP : P.IsMaximal
⊢ IsTorsionFree (Localization P.primeCompl) (LocalizedModule P.primeCompl M)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], ValuationRing (Localization P.primeCompl)
h : IsTorsionFree R M
P : Ideal R
hP : P.IsMaximal
⊢ IsTorsionFree (Localization P.primeCompl) (LocalizedModule P.primeCompl M)
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : IsTorsionFree R M
⊢ IsTorsionFree R M

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : IsTorsionFree R M
⊢ IsTorsionFree R M
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
⊢ (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))).IsIntegral

Tactic:
]

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
⊢ (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))).IsIntegral
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
this : w'.toRingHom = quotientMap Q Polynomial.C ⋯
⊢ (quotientMap Q Polynomial.C ⋯).IsIntegral

Tactic:
]

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
this : w'.toRingHom = quotientMap Q Polynomial.C ⋯
⊢ (quotientMap Q Polynomial.C ⋯).IsIntegral
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
this : w'.toRingHom = quotientMap Q Polynomial.C ⋯
⊢ ((Ideal.Quotient.mk Q).comp Polynomial.C).IsIntegral

Tactic:
]

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
this : w'.toRingHom = quotientMap Q Polynomial.C ⋯
⊢ ((Ideal.Quotient.mk Q).comp Polynomial.C).IsIntegral
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ (g.comp ((Ideal.Quotient.mk (ker f')).comp C)).IsIntegral

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ (g.comp ((Ideal.Quotient.mk (ker f')).comp C)).IsIntegral
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
hf' : Function.Surjective (⇑g ∘ ⇑(Ideal.Quotient.mk (ker f')))
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ Function.Surjective ⇑g

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
hf' : Function.Surjective (⇑g ∘ ⇑(Ideal.Quotient.mk (ker f')))
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ Function.Surjective ⇑g
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (f.comp ((renameEquiv R e).toRingEquiv.toRingHom.comp C)).IsIntegral
⊢ (f.comp C).IsIntegral

Tactic:
]

Goal state after:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (f.comp ((renameEquiv R e).toRingEquiv.toRingHom.comp C)).IsIntegral
⊢ (f.comp C).IsIntegral
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i : ι
⊢ ↑2 = ↑2

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
S✝ : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i j : ι
S : Type u_6
inst✝² : CommRing S
inst✝¹ : Algebra S R
inst✝ : P.IsValuedIn S
⊢ ∀ (b a : ι), ∃ s, (algebraMap S R) s = P.flip.pairing a b

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
S✝ : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i j : ι
S : Type u_6
inst✝² : CommRing S
inst✝¹ : Algebra S R
inst✝ : P.IsValuedIn S
⊢ ∀ (b a : ι), ∃ s, (algebraMap S R) s = P.flip.pairing a b
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ ((↑f).comp (algebraMap R (MvPolynomial ι R))).IsIntegral

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ ((↑f).comp (algebraMap R (MvPolynomial ι R))).IsIntegral
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
⊢ span K (range ⇑(P.restrictScalars' K).root) = span K {x | ↑x ∈ range ⇑P.root}

Tactic:
]

Goal state after:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
⊢ span K (range ⇑(P.restrictScalars' K).root) = span K {x | ↑x ∈ range ⇑P.root}
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
⊢ span K (range ⇑(P.restrictScalars' K).coroot) = span K {x | ↑x ∈ range ⇑P.coroot}

Tactic:
]

Goal state after:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
⊢ span K (range ⇑(P.restrictScalars' K).coroot) = span K {x | ↑x ∈ range ⇑P.coroot}