mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case pos.«_@».Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff.4094078725._hygCtx._hyg.105.«0»
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ M.charpoly.coeff 0 = (X ^ 2 - C M.trace * X + C M.det).coeff 0

pp: case pos.«_@».Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff.4094078725._hygCtx._hyg.105.«1»
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ M.charpoly.coeff 1 = (X ^ 2 - C M.trace * X + C M.det).coeff 1

pp: case pos.«_@».Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff.4094078725._hygCtx._hyg.105.«2»
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ M.charpoly.coeff 2 = (X ^ 2 - C M.trace * X + C M.det).coeff 2

Tactic:
· simp [det_eq_sign_charpoly_coeff, hn]

Goal state after:
case pos.«_@».Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff.4094078725._hygCtx._hyg.105.«1»
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ M.charpoly.coeff 1 = (X ^ 2 - C M.trace * X + C M.det).coeff 1

case pos.«_@».Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff.4094078725._hygCtx._hyg.105.«2»
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ M.charpoly.coeff 2 = (X ^ 2 - C M.trace * X + C M.det).coeff 2
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
hp : toLaurentAlg M.charpoly = p
hq : toLaurentAlg M.charpolyRev = q
this : t_inv ^ Fintype.card n * p = invert q
⊢ invert (toLaurentAlg M.charpoly) * T ↑M.charpoly.natDegree = toLaurentAlg M.charpolyRev

Tactic:
hp,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
hp : toLaurentAlg M.charpoly = p
hq : toLaurentAlg M.charpolyRev = q
this : t_inv ^ Fintype.card n * p = invert q
⊢ invert p * T ↑M.charpoly.natDegree = toLaurentAlg M.charpolyRev
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ r • x ∈ S[x]

Tactic:
rw [← algebraMap_smul S]

Goal state after:
B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ (algebraMap R S) r • x ∈ S[x]
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : IsEmpty n
⊢ IsNilpotent M.trace

pp: case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : Nonempty n
⊢ IsNilpotent M.trace

Tactic:
· simp

Goal state after:
case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : Nonempty n
⊢ IsNilpotent M.trace
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ (if n + k - k = n then ↑((n + k).choose k) * f.coeff (n + k) else 0) = ↑((n + k).choose k) * f.coeff (n + k)

pp: case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ∀ b ∈ f.support, b ≠ n + k → ((monomial (b - k)) (↑(b.choose k) * f.coeff b)).coeff n = 0

pp: case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ n + k ∉ f.support → ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0

Tactic:
· simp

Goal state after:
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ∀ b ∈ f.support, b ≠ n + k → ((monomial (b - k)) (↑(b.choose k) * f.coeff b)).coeff n = 0

case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ n + k ∉ f.support → ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (taylor 0) f = f

Tactic:
by rw [taylor_apply, C_0, add_zero, comp_X]

Goal state after:
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max 0 (max 0 0) = max 0 0

Tactic:
· simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : p = 0
⊢ ((taylor r) p).degree = p.degree

Tactic:
hp,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : p = 0
⊢ ((taylor r) 0).degree = degree 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ (compHom (D k)).comp Φ = ∑ x ∈ antidiagonal k, (compHom.comp ((compHom Φ) (D x.1))).flip (D x.2)

Tactic:
ext m r n s : 4

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
⊢ (((((compHom (D k)).comp Φ).comp (monomial m).toAddMonoidHom) r).comp (monomial n).toAddMonoidHom) s =
    ((((∑ x ∈ antidiagonal k, (compHom.comp ((compHom Φ) (D x.1))).flip (D x.2)).comp (monomial m).toAddMonoidHom)
            r).comp
        (monomial n).toAddMonoidHom)
      s
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : p = 0
⊢ (p.scaleRoots s).degree = p.degree

Tactic:
hp,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : p = 0
⊢ (scaleRoots 0 s).degree = degree 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝ : CommSemiring R
r : R
h✝ : Nontrivial R
hp : Splits 0
⊢ (Polynomial.scaleRoots 0 r).Splits

pp: case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
⊢ (p.scaleRoots r).Splits

Tactic:
· simp

Goal state after:
case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
⊢ (p.scaleRoots r).Splits
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝ : CommRing R
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
⊢ rootMultiplicity (r * a) (scaleRoots 0 r) = rootMultiplicity a 0

pp: case inr.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

Tactic:
· simp

Goal state after:
case inr.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
b : R
hf : (C 0 * X + C b).natDegree ≤ 1
h : Invertible (C 0 * X + C b).leadingCoeff
⊢ (C 0 * X + C b).Splits

pp: case inr
R : Type u_1
inst✝ : Semiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
h : Invertible (C a * X + C b).leadingCoeff
ha : a ≠ 0
⊢ (C a * X + C b).Splits

Tactic:
· simp

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
h : Invertible (C a * X + C b).leadingCoeff
ha : a ≠ 0
⊢ (C a * X + C b).Splits
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).coeff (p.toSubring T hp).natDegree = 1 ↔ p.coeff p.natDegree = 1

Tactic:
natDegree_toSubring,

Goal state after:
R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).coeff p.natDegree = 1 ↔ p.coeff p.natDegree = 1
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inr.hp
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ (X - C a).leadingCoeff ^ rootMultiplicity a p ≠ 0

pp: case inr.inr.h
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ ((X - C a) ^ rootMultiplicity a p).leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
· simp

Goal state after:
case inr.inr.h
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ ((X - C a) ^ rootMultiplicity a p).leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
hmg : mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)
⊢ (Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)).prod.Monic

Tactic:
hmg

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
hmg : mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)
⊢ (Multiset.map (fun x ↦ X + C x) (Multiset.map j (Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)))).prod.Monic
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ ((C a).comp (-X)).Splits

pp: case inr
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ ((X + C a).comp (-X)).Splits

Tactic:
· simp

Goal state after:
case inr
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ ((X + C a).comp (-X)).Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ (-(X - C a)).Splits

Tactic:
exact (X_sub_C a).neg

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : f p.leadingCoeff = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
hp,

Goal state after:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : f p.leadingCoeff = 0
⊢ f.IsIntegralElem (0 * x)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case mpr
A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
p : K[X]
hp : p ≠ 0
px : (aeval x) p = 0
⊢ IsAlgebraic A x

Tactic:
exact
      ⟨integerNormalization _ p, mt integerNormalization_eq_zero_iff.mp hp,
        integerNormalization_aeval_eq_zero _ p px⟩

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case mpr
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ ⊤ → g ∈ S[(Ideal.Quotient.mkₐ S I) X]

Tactic:
intro _
      obtain ⟨g', hg⟩ := Ideal.Quotient.mkₐ_surjective S I g
      have : g = (Polynomial.aeval ((Ideal.Quotient.mkₐ S I) X)) g' := by
        nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _),
          as_sum_range_C_mul_X_pow g', map_sum]
        simp only [Polynomial.C_mul', ← map_pow, map_smul]
      exact this ▸ (aeval_mem_adjoin_singleton S ((Ideal.Quotient.mk I) Polynomial.X))

Goal state after:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
hg : natDegree 0 ≤ 1
⊢ (f.comp 0).Splits

pp: case inr
R : Type u_1
inst✝ : Field R
f g : R[X]
hf : f.Splits
hg : g.natDegree ≤ 1
hg0 : g ≠ 0
⊢ (f.comp g).Splits

Tactic:
· simp

Goal state after:
case inr
R : Type u_1
inst✝ : Field R
f g : R[X]
hf : f.Splits
hg : g.natDegree ≤ 1
hg0 : g ≠ 0
⊢ (f.comp g).Splits
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
⊢ IsUnit a

Tactic:
obtain ⟨p, p_monic, hp⟩ := hf (ha.unit⁻¹ : _)

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹) p = 0
⊢ IsUnit a
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹) p = 0
⊢ -(eval a X * eval a p.reverse.divX) = 1

Tactic:
← eval_mul,

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹) p = 0
⊢ -eval a (X * p.reverse.divX) = 1
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case inl
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
h✝ : Subsingleton Rₘ
⊢ ∃ m, IsIntegral R (m • x)

pp: case inr
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
nontriv : Nontrivial Rₘ
⊢ ∃ m, IsIntegral R (m • x)

Tactic:
· have := (algebraMap Rₘ S).codomain_trivial
    exact ⟨1, Polynomial.X, Polynomial.monic_X, Subsingleton.elim _ _⟩

Goal state after:
case inr
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
nontriv : Nontrivial Rₘ
⊢ ∃ m, IsIntegral R (m • x)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h✝ : Nontrivial R
r : R
hr : r ≠ 0
w✝ : S
e : (algebraMap R S) r = s * w✝
⊢ IsIntegral R ((algebraMap R A) r * a)

Tactic:
IsScalarTower.algebraMap_apply R S,

Goal state after:
case pos.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h✝ : Nontrivial R
r : R
hr : r ≠ 0
w✝ : S
e : (algebraMap R S) r = s * w✝
⊢ IsIntegral R ((algebraMap S A) ((algebraMap R S) r) * a)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this✝ : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
i : ℕ
hi₁ : i ∈ q.support
hi₂ : i ≠ q.natDegree
this : N + i < q.natDegree + N
⊢ (q.coeff i).natDegree < q.natDegree + N - i

Tactic:
by grind

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
⊢ IsAlgebraic R a

Tactic:
by
  cases subsingleton_or_nontrivial A
  · have := Algebra.IsAlgebraic.nontrivial R S
    exact Subsingleton.elim a 0 ▸ isAlgebraic_zero
  · have := Module.nontrivial S A
    exact h.isAlgebraic.restrictScalars _

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral K (mk' L x s)

Tactic:
IsLocalization.mk'_eq_mul_mk'_one

Goal state after:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral K ((algebraMap S L) x * mk' L 1 s)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u_1
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FaithfullyFlat R M
⊢ FaithfullyFlat S (S ⊗[R] M)

Tactic:
rw [Module.FaithfullyFlat.iff_flat_and_rTensor_reflects_triviality]
  refine ⟨inferInstance, fun N _ _ hN ↦ ?_⟩
  let _ : Module R N := Module.compHom N (algebraMap R S)
  have : IsScalarTower R S N := IsScalarTower.of_algebraMap_smul fun r ↦ congrFun rfl
  have := (AlgebraTensorModule.cancelBaseChange R S S N M).symm.subsingleton
  exact FaithfullyFlat.rTensor_reflects_triviality R M N

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case tmul
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : (algebraMap R T) s ∉ J
e : c * (algebraMap R T) s * x₂ = c * (algebraMap R T) y
⊢ 1 ⊗ₜ[R] ((algebraMap R T) s * c) * x₁ ⊗ₜ[R] x₂ = (y • x₁) ⊗ₜ[R] c

Tactic:
rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e,
      TensorProduct.smul_tmul, Algebra.smul_def, mul_comm]

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
this✝ : q.IsPrime
this : comap f q ≤ p
⊢ p = comap f q

Tactic:
exact (H.2 ⟨inferInstance, Ideal.comap_mono hq.le⟩ this).antisymm this

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S) ↔ p ∈ Set.range (comap (algebraMap R S))

Tactic:
let k := p.asIdeal.ResidueField
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨m, hm⟩ := Ideal.exists_maximal (k ⊗[R] S)
    use PrimeSpectrum.comap (Algebra.TensorProduct.includeRight).toRingHom ⟨m, hm.isPrime⟩
    ext : 1
    rw [← PrimeSpectrum.comap_comp_apply,
      ← Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap, comap_comp_apply]
    simp [Ideal.eq_bot_of_prime, k, ← RingHom.ker_eq_comap_bot]
  · obtain ⟨q, rfl⟩ := h
    let f : k ⊗[R] S →ₐ[R] q.asIdeal.ResidueField :=
      Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ _ _ (Algebra.ofId _ _) rfl)
        (IsScalarTower.toAlgHom _ _ _) (fun _ _ ↦ Commute.all ..)
    exact RingHom.domain_nontrivial f.toRingHom

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mpr.refine_1
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
⊢ p.IsPrime

pp: case mpr.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
⊢ ∀ ⦃y : Ideal A⦄, (fun q ↦ q.IsPrime ∧ Ideal.map (algebraMap R A) J ≤ q) y → y ≤ p → p ≤ y

Tactic:
· rw [IsLocalization.isPrime_iff_isPrime_disjoint S A, IsLocalization.disjoint_under_iff S]
      refine ⟨hp.isPrime, ?_⟩
      rintro rfl
      exact hp.isPrime.ne_top rfl

Goal state after:
case mpr.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
⊢ ∀ ⦃y : Ideal A⦄, (fun q ↦ q.IsPrime ∧ Ideal.map (algebraMap R A) J ≤ q) y → y ≤ p → p ≤ y
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ ⊤ ∈ L

Tactic:
simpa using compl_mem L.bot_mem

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
h : ¬∀ t ∈ s, IsOpen[inst✝¹] t
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
⊢ s ⊆ a ∪ b

Tactic:
by grind

Goal state after: