mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝² : Nontrivial α
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : NoZeroDivisors α
h : IsRegular 0
⊢ False

Tactic:
exact not_not.mpr h.left not_isLeftRegular_zero

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
h : P f ∧ Q f
⊢ P (IsLocalization.Away.map R' S' f r) ∧ Q (IsLocalization.Away.map R' S' f r)

Tactic:
exact ⟨hP f r R' S' h.1, hQ f r R' S' h.2⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.MvPolynomial

Goal state before:
pp: m : Type u_1
R : Type u_3
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ (mvPolynomialX m m R).det ≠ 0

Tactic:
intro h_det
  have := congr_arg Matrix.det (mvPolynomialX_mapMatrix_eval (1 : Matrix m m R))
  rw [det_one, ← RingHom.map_det, h_det, map_zero] at this
  exact zero_ne_one this

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
this : X = (monomial 1) 1
⊢ toLaurent X = T 1

Tactic:
simp [this, Polynomial.toLaurent_C_mul_T]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case mk.inl
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
b : n ⊕ p
a : n
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inl a) b =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inl a) b

Tactic:
rcases b with b | b

Goal state after:
case mk.inl.inl
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : n
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inl a) (inl b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inl a) (inl b)

case mk.inl.inr
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a : n
b : p
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inl a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inl a) (inr b)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case mk.inr
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
b : n ⊕ p
a : p
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) b =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) b

Tactic:
rcases b with b | b

Goal state after:
case mk.inr.inl
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a : p
b : n
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inl b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inl b)

case mk.inr.inr
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inr b)
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
⊢ LinearIndependent R fun i ↦ r * ↑s ^ ↑i

Tactic:
suffices ∀ (g : ℕ → R) (x), (∑ i ∈ Finset.range n, g i • (r * s ^ (i + x))) = 0 →
      ∀ i < n, g i = 0 by
    refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_
    simpa only [dif_pos i.prop] using this (fun i ↦ if h : i < n then g ⟨i, h⟩ else 0) 0
      (by simp [← Fin.sum_univ_eq_sum_range, ← hg]) i i.prop

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
⊢ ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_9
n : Type u_10
R : Type u_11
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Fintype m
i : n
j : m
a : R
x : Matrix m n R
⊢ (single i j a * x).trace = a • x j i

Tactic:
by
  simp [trace, mul_apply, single, ite_and]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_9
n : Type u_10
R : Type u_11
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Fintype m
x : Matrix m n R
i : n
j : m
a : R
⊢ (x * single i j a).trace = MulOpposite.op a • x j i

Tactic:
by
  simp [trace, mul_apply, single, ite_and]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
x✝ : α
⊢ (f x✝) 0 = 0

Tactic:
exact map_zero _

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝¹ : Invertible A
inst✝ : Invertible (C + C * V * ⅟A * U * C)
⊢ 1 + U * C * V * ⅟A -
      (A * (⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A) +
        U * C * V * (⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A)) =
    1

Tactic:
rw [add_sub_assoc, add_eq_left, sub_eq_zero]

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝¹ : Invertible A
inst✝ : Invertible (C + C * V * ⅟A * U * C)
⊢ U * C * V * ⅟A =
    A * (⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A) +
      U * C * V * (⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
A : (listTransvecRow M).length = r
⊢ (M * (listTransvecRow M).prod) i (inr ()) = M i (inr ())

Tactic:
rw [← List.take_length (l := listTransvecRow M), A]

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
A : (listTransvecRow M).length = r
⊢ (M * (List.take r (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
H : ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
A : (listTransvecRow M).length = r
⊢ (M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Tactic:
rw [← List.take_length (l := listTransvecRow M), A]

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
H : ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
A : (listTransvecRow M).length = r
⊢ (M * (List.take r (listTransvecRow M)).prod) (inr ()) (inl i) = 0
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹.det = A.det⁻¹ʳ

pp: case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹.det = A.det⁻¹ʳ

Tactic:
· cases h.nonempty_invertible
    let := invertibleOfDetInvertible A
    rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf]

Goal state after:
case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹.det = A.det⁻¹ʳ
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case convert_7
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
⊢ fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
      (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D) =
    ⅟(fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)

Tactic:
· -- unfold the `Invertible` instances to get the raw factors
    change
      _ =
        fromBlocks 1 0 (-(1 * (⅟D * C) * 1)) 1 *
          (fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * 0 * ⅟D)) 0 (⅟D) *
            fromBlocks 1 (-(1 * (B * ⅟D) * 1)) 0 1)
    -- combine into a single block matrix
    simp only [fromBlocks_multiply, Matrix.one_mul, Matrix.mul_one, Matrix.zero_mul,
      Matrix.mul_zero, add_zero, zero_add, neg_zero, Matrix.mul_neg, Matrix.neg_mul, neg_neg, ←
      Matrix.mul_assoc, add_comm (⅟D)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
r : R
inst✝ : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (X ^ n * C r)

Tactic:
rw [commute_X_pow]
  exact isNilpotent_C_mul_pow_X_of_isNilpotent n hnil

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: case insert
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsNilpotent (f i)) → (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ IsNilpotent (∑ i ∈ insert j s, f i)

Tactic:
| insert j s hj ih =>

Goal state after:
case insert
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsNilpotent (f i)) → (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ IsNilpotent (∑ i ∈ insert j s, f i)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_4
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Ring T
f : R →+* S
g : S →+* T
hg : Function.Injective ⇑g
x : S
hx : (g.comp f).IsIntegralElem (g x)
⊢ f.IsIntegralElem x

Tactic:
obtain ⟨p, hp, hx⟩ := hx
  exact ⟨p, hp, hg <| by simp [Polynomial.hom_eval₂, hx]⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1
⊢ (∏ i, (X - C (M i i)) - M.charpoly).degree < ↑(Fintype.card n)

Tactic:
← neg_sub

Goal state after:
case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1
⊢ (-(M.charpoly - ∏ i, (X - C (M i i)))).degree < ↑(Fintype.card n)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case refine_2
R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : (aeval x) p ∈ (aeval x).range
⊢ eval₂ (algebraMap R A) x ((p %ₘ f).sum fun n a ↦ C a * X ^ n) ∈
    span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))

Tactic:
eval₂_sum,

Goal state after:
case refine_2
R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : (aeval x) p ∈ (aeval x).range
⊢ ((p %ₘ f).sum fun n a ↦ eval₂ (algebraMap R A) x (C a * X ^ n)) ∈
    span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R S : Type u
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R ≃+* S
I : Ideal R
⊢ Submodule.spanRank (map f I) = Submodule.spanRank I

Tactic:
simpa using I.lift_spanRank_map_eq_of_ringEquiv f

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
this : Nontrivial R
I : Type u_2
B : Basis I R M
⊢ #I = lift.{u_2, u_2} #I

Tactic:
Cardinal.lift_id _

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
this : Nontrivial R
I : Type u_2
B : Basis I R M
⊢ #I = #I
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
⊢ Module.rank R M ≤ ⊤.spanRank

Tactic:
rw [Module.rank, Submodule.spanRank]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
⊢ ⨆ ι, #↑↑ι ≤ ⨅ s, #↑↑s
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ↑p.coeffs ⊆ Set.range ⇑f
n : ℕ
hn : p.coeff n = 0
⊢ f 0 = p.coeff n

Tactic:
by simp [hn]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : p.degree ≠ ↑i
⊢ p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Tactic:
by
  rw [integralNormalization_coeff, if_neg hi]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
f : R →+* A
p : R[X]
H : f p.leadingCoeff ≠ 0
i : ℕ
⊢ (map f p).integralNormalization.coeff i = (map f p.integralNormalization).coeff i

Tactic:
simp [integralNormalization_coeff, degree_map_eq_of_leadingCoeff_ne_zero _ H, apply_ite f,
    leadingCoeff_map_of_leadingCoeff_ne_zero _ H, natDegree_map_eq_iff.mpr (.inl H)]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: case mul_X
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
p : MvPolynomial σ R
i : σ
h : (aeval fun x ↦ 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (aeval f) p
⊢ (aeval fun x ↦ 1 ⊗ₜ[R] f x) (p * X i) = 1 ⊗ₜ[R] (aeval f) (p * X i)

Tactic:
| mul_X p i h =>

Goal state after:
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
⊢ (C a - X).Splits

Tactic:
← neg_sub

Goal state after:
case inr
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ (-(X - C a)).Splits
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
⊢ (∃ y, (algebraMap (↥(integralClosure R A)) A) y = x) → IsIntegral R x

Tactic:
by rintro ⟨⟨_, h⟩, rfl⟩; exact h

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

Goal state before:
pp: K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
⊢ (∀ (x : A), IsAlgebraic K x) ↔ Algebra.IsIntegral K A

Tactic:
Algebra.isIntegral_def,

Goal state after:
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
⊢ (∀ (x : A), IsAlgebraic K x) ↔ ∀ (x : A), IsIntegral K x
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ a, (algebraMap R A) a = 0 ∧ a ≠ 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
have ⟨r, eq, ne⟩ := inj

Goal state after:
case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ a, (algebraMap R A) a = 0 ∧ a ≠ 0
r : R
eq : (algebraMap R A) r = 0
ne : r ≠ 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
x : S
inst✝ : Away x Sₘ
p : R[X]
hpm : p.Monic
hp : ∃ a, x ^ a * eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R x

Tactic:
obtain ⟨n, hn⟩ := hp

Goal state after:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
x : S
inst✝ : Away x Sₘ
p : R[X]
hpm : p.Monic
n : ℕ
hn : x ^ n * eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R x
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ Set.univ ⊆ zeroLocus s ↔ s ⊆ ↑(nilradical R)

Tactic:
subset_zeroLocus_iff_subset_vanishingIdeal,

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ s ⊆ ↑(vanishingIdeal Set.univ) ↔ s ⊆ ↑(nilradical R)
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
⊢ FaithfullyFlat R M ↔
    ∀ {N1 : Type (max u v)} [inst : AddCommGroup N1] [inst_1 : Module R N1] {N2 : Type (max u v)}
      [inst_2 : AddCommGroup N2] [inst_3 : Module R N2] {N3 : Type (max u v)} [inst_4 : AddCommGroup N3]
      [inst_5 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
      Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23)

Tactic:
by
  simp only [iff_exact_iff_rTensor_exact, LinearMap.rTensor_exact_iff_lTensor_exact]

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

Goal state before:
pp: case inl
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨i, q⟩
⊢ ⟨i, p⟩ = ⟨i, q⟩

Tactic:
congr; ext x
    simpa using congr_arg (Function.update (0 : ∀ i, R i) i x ∈ ·.asIdeal) eq

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

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum S
hp : I ≤ p.asIdeal
a : R
ha : a ∈ Ideal.comap f I
⊢ a ∈ (comap f p).asIdeal

Tactic:
exact hp ha

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
⊢ x ∈ (mapToFractionRing K S B hS).range ↔ ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹

Tactic:
mem_range_mapToFractionRing_iff

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
⊢ (∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩) ↔
    ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ sInf (Ideal.under R ⁻¹' I.minimalPrimes) = Ideal.map (algebraMap R A) q

Tactic:
refine le_antisymm (sInf_le ?_) (le_sInf fun J hJ ↦ ?_)

Goal state after:
case refine_1
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ Ideal.map (algebraMap R A) q ∈ Ideal.under R ⁻¹' I.minimalPrimes

case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
⊢ Ideal.map (algebraMap R A) q ≤ J
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s ∩ closure[inst✝] (coborder s ∩ s) ⊆ s

Tactic:
inter_eq_right.mpr subset_coborder,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s ∩ closure[inst✝] s ⊆ s
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : ↑(f ⁻¹' s)
y : ↑s
h : y ⤳ s.restrictPreimage f x
a : α
ha : a ⤳ ↑x
hy : f a = ↑y
⊢ a ∈ f ⁻¹' s

Tactic:
simp [hy]

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a : α
ha : aᶜ ∈ L
⊢ a ∈ L

Tactic:
by simpa using compl_mem ha

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a \ b ∈ L

Tactic:
_root_.sdiff_eq

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a ⊓ bᶜ ∈ L
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
⊢ ∃ κ a, W = ⨆ k, U (a k)

Tactic:
obtain ⟨Us, hsub, hUs⟩ := Opens.isBasis_iff_cover.mp hU W
  choose a ha using hsub
  use Us, fun i ↦ a i.2
  simp [hUs, ha, sSup_eq_iSup' Us]

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
rcases eq_or_ne s ⊥ with rfl | h₀

Goal state after:
case inl
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
H : ∀ y < ⊥, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ ⊥ = sSup S

case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S