mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
hg : (∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s * ↑s ^ x + g 0 * r * ↑s ^ x = 0
⊢ g i = 0

Tactic:
rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg

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

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝² : Fintype n
ι : Type u_8
inst✝¹ : Unique ι
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ (replicateCol ι a * replicateRow ι b).trace = a ⬝ᵥ b

Tactic:
apply Finset.sum_congr rfl
  simp [mul_apply]

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

Goal state before:
pp: R : Type u_1
m : Type u_10
n : Type u_11
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B).det = A.det ^ Fintype.card n * B.det ^ Fintype.card m

Tactic:
by
  refine (det_kroneckerMapBilinear (Algebra.lmul ℕ R).toLinearMap mul_mul_mul_comm _ _).trans ?_
  simp

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

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
⊢ ((MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)).adjugate.adjugate =
    ((MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)).det ^ (Fintype.card n - 2) •
      (MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)

Tactic:
← AlgHom.map_adjugate,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
⊢ ((MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ).adjugate).adjugate =
    ((MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)).det ^ (Fintype.card n - 2) •
      (MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
⊢ ((MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ).adjugate).adjugate =
    ((MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)).det ^ (Fintype.card n - 2) •
      (MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)

Tactic:
← AlgHom.map_adjugate,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
⊢ (MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ).adjugate.adjugate =
    ((MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)).det ^ (Fintype.card n - 2) •
      (MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b j ≤ b i
c : R
⊢ (⇑toDual ∘ b) i ≤ (⇑toDual ∘ b) j

Tactic:
by exact toDual_le_toDual.mpr hij

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

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)
this : A = (A.submatrix ⇑e₁ ⇑e₂).submatrix ⇑e₁.symm ⇑e₂.symm
⊢ A * (⅟(A.submatrix ⇑e₁ ⇑e₂)).submatrix ⇑e₂.symm ⇑e₁.symm = 1

Tactic:
conv in _ * _ =>
      congr
      rw [this]

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)
this : A = (A.submatrix ⇑e₁ ⇑e₂).submatrix ⇑e₁.symm ⇑e₂.symm
⊢ (A.submatrix ⇑e₁ ⇑e₂).submatrix ⇑e₁.symm ⇑e₂.symm * (⅟(A.submatrix ⇑e₁ ⇑e₂)).submatrix ⇑e₂.symm ⇑e₁.symm = 1
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i ↦ b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i ↦ b i < k) fun j ↦ b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
hA : A.BlockTriangular b'
⊢ M⁻¹ i j = 0

Tactic:
have hb' : image b' univ ⊂ image b univ := by
    convert! image_subtype_univ_ssubset_image_univ k b _ (fun a => a < k) (lt_irrefl _)
    convert! max'_mem (α := α) _ _

Goal state after:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i ↦ b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i ↦ b i < k) fun j ↦ b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
hA : A.BlockTriangular b'
hb' : image b' univ ⊂ image b univ
⊢ M⁻¹ i j = 0
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
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 A
⊢ det 1 * det 1 * (A.det * (D - C * ⅟A * B).det) * (det 1 * det 1) = A.det * (D - C * ⅟A * B).det

Tactic:
det_one,

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
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 A
⊢ 1 * det 1 * (A.det * (D - C * ⅟A * B).det) * (1 * det 1) = A.det * (D - C * ⅟A * B).det
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
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 A
⊢ 1 * det 1 * (A.det * (D - C * ⅟A * B).det) * (1 * det 1) = A.det * (D - C * ⅟A * B).det

Tactic:
det_one,

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
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 A
⊢ 1 * 1 * (A.det * (D - C * ⅟A * B).det) * (1 * 1) = A.det * (D - C * ⅟A * B).det
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
this : Invertible 1
⊢ det 1 * (D - C * B).det = (D - C * B).det

Tactic:
det_one,

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
this : Invertible 1
⊢ 1 * (D - C * B).det = (D - C * B).det
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
this : Invertible 1
⊢ det 1 * (A - B * C).det = (A - B * C).det

Tactic:
det_one,

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
this : Invertible 1
⊢ 1 * (A - B * C).det = (A - B * C).det
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_2.inr
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent ((reflect N P).coeff i)

Tactic:
· simpa [revAt_eq_self_of_lt hi] using h i

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : R[X]
| P

Tactic:
← modByMonic_add_div P X

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : R[X]
| P %ₘ X + X * (P /ₘ X)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: 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
⊢ span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree)) = Subalgebra.toSubmodule R[x]

Tactic:
nontriviality A

Goal state after:
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
⊢ span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree)) = Subalgebra.toSubmodule R[x]
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case e'_3
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 = eval 0 (det 1)

Tactic:
det_one,

Goal state after:
case e'_3
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 = eval 0 1
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
⊢ g • 1 = 1

Tactic:
by ext; exact smul_one g

Goal state after:
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
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
h_blocks :
  A.submatrix ⇑e ⇑e = fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1
⊢ (A.submatrix ⇑e ⇑e).det = (M.submatrix Subtype.val Subtype.val).det

Tactic:
rw [h_blocks, Matrix.det_fromBlocks_zero₂₁, Matrix.det_one, mul_one]

Goal state after:
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
⊢ map T.subtype (p.toSubring T hp) = p

Tactic:
ext n
  simp [coeff_map]

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

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.Splits
hf0 : (C f.leadingCoeff * 1).degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) 0).prod
⊢ ∃ a, eval a f = 0

Tactic:
mul_one,

Goal state after:
case neg.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.Splits
hf0 : (C f.leadingCoeff).degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) 0).prod
⊢ ∃ a, eval a f = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
b : R
hb : b ∈ ↑M
h : IsInteger R[X] ((algebraMap R R[X]) b • p)
⊢ ∃ b ∈ M, ∃ q, Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support

Tactic:
algebraMap_smul

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
b : R
hb : b ∈ ↑M
h : IsInteger R[X] (b • p)
⊢ ∃ b ∈ M, ∃ q, Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
⊢ (f.Splits ∨ g = 0) ∧ (g.Splits ∨ f = 0) → (f * g).Splits

Tactic:
by rintro ⟨hp | rfl, hq | rfl⟩ <;> simp [*]

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

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
f : R[X]
hf : f.natDegree ≤ 1
⊢ f.Splits

Tactic:
obtain ⟨a, b, rfl⟩ := exists_eq_X_add_C_of_natDegree_le_one hf
  by_cases ha : a = 0
  · simp_all
  · rw [← mul_inv_cancel_left₀ ha b, C_mul, ← mul_add]
    exact (X_add_C (a⁻¹ * b)).C_mul a

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra R B
f : R[X]
hf : (map (algebraMap R A) f).Splits
g : A →ₐ[R] B
⊢ Algebra.adjoin R (f.rootSet B) = g.range ↔ Algebra.adjoin R (f.rootSet A) = ⊤

Tactic:
← hf.image_rootSet g,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra R B
f : R[X]
hf : (map (algebraMap R A) f).Splits
g : A →ₐ[R] B
⊢ Algebra.adjoin R (⇑g '' f.rootSet A) = g.range ↔ Algebra.adjoin R (f.rootSet 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
⊢ a * -eval a p.reverse.divX = 1

Tactic:
mul_neg,

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
⊢ -(a * eval a p.reverse.divX) = 1
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
x✝ : Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
flat : Flat R M
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
I : Ideal R
hI : I ≠ ⊤
r : I • ⊤ = ⊤
m : Ideal R
hm : m.IsMaximal
le : I ≤ m
⊢ ⊤ ≤ I • ⊤

Tactic:
by simp [r]

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

Goal state before:
pp: case right.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : Ideal R
hp : p.IsPrime
hI : (p.prod ⊤).IsPrime
⊢ ∃ a, primeSpectrumProdOfSum R S a = { asIdeal := p.prod ⊤, isPrime := hI }

pp: case right.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : Ideal S
hp : p.IsPrime
hI : (⊤.prod p).IsPrime
⊢ ∃ a, primeSpectrumProdOfSum R S a = { asIdeal := ⊤.prod p, isPrime := hI }

Tactic:
· exact ⟨Sum.inl ⟨p, hp⟩, rfl⟩

Goal state after:
case right.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : Ideal S
hp : p.IsPrime
hI : (⊤.prod p).IsPrime
⊢ ∃ a, primeSpectrumProdOfSum R S a = { asIdeal := ⊤.prod p, isPrime := hI }
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ GaloisConnection (fun s ↦ zeroLocus s) fun t ↦ ↑(vanishingIdeal t)

Tactic:
have ideal_gc : GaloisConnection Ideal.span _ := (Submodule.gi R R).gc

Goal state after:
R : Type u
inst✝ : CommSemiring R
ideal_gc : GaloisConnection Ideal.span SetLike.coe
⊢ GaloisConnection (fun s ↦ zeroLocus s) fun t ↦ ↑(vanishingIdeal t)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : x.asIdeal.IsPrime
⊢ x.asIdeal = ⊤

Tactic:
rw [Ideal.eq_top_iff_one]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : x.asIdeal.IsPrime
⊢ 1 ∈ x.asIdeal
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 S A
inst✝ : NoZeroDivisors S
s t : Set S
alg : ∀ x ∈ s \ t, IsAlgebraic (↥(adjoin R t)) x
a : A
ha : IsAlgebraic (↥(adjoin R s)) a
⊢ IsAlgebraic (↥(adjoin R t)) a

Tactic:
set Rs := adjoin R s
  set Rt := adjoin R t
  let Rts := adjoin Rt s
  let _ : Algebra Rs Rts := (Subalgebra.inclusion
    (T := Rts.restrictScalars R) <| adjoin_le <| by apply subset_adjoin).toAlgebra
  have : IsScalarTower Rs Rts A := .of_algebraMap_eq fun ⟨a, _⟩ ↦ rfl
  have : Algebra.IsAlgebraic Rt Rts := by
    have := ha.nontrivial
    have := Subtype.val_injective (p := (· ∈ Rs)).nontrivial
    have := (isDomain_iff_noZeroDivisors_and_nontrivial Rt).mpr ⟨inferInstance, inferInstance⟩
    rw [← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]
    intro x hs
    by_cases ht : x ∈ t
    · exact isAlgebraic_algebraMap (⟨x, subset_adjoin ht⟩ : Rt)
    exact alg _ ⟨hs, ht⟩
  have : IsAlgebraic Rts a := ha.extendScalars (by apply Subalgebra.inclusion_injective)
  exact this.restrictScalars Rt

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

Goal state before:
pp: case h.refine_1
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ (M + A ∙ x) * (M + A ∙ y) ≤ M

Tactic:
rw [add_mul]
    apply sup_le (show M * (M + span A {y}) ≤ M from Ideal.mul_le_left)
    rw [mul_add]
    apply sup_le (show span A {x} * M ≤ M from Ideal.mul_le_right)
    rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
⊢ g.SurjectiveOnStalks

Tactic:
by
  intro I hI
  have := hg I hI
  rw [Localization.localRingHom_comp (I.comap (g.comp f)) (I.comap g) _ _ rfl _ rfl,
    RingHom.coe_comp] at this
  exact this.of_comp

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

Goal state before:
pp: A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
h_nzI : I ≠ ⊥
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
by
  induction I using IsNoetherian.induction with | hgt M hgt =>
  change Ideal A at M
  have hA_nont : Nontrivial A := IsDomain.toNontrivial
  by_cases h_topM : M = ⊤
  · rcases h_topM with rfl
    obtain ⟨p_id, h_nzp, h_pp⟩ : ∃ p : Ideal A, p ≠ ⊥ ∧ p.IsPrime := by
      apply Ring.not_isField_iff_exists_prime.mp h_fA
    use ({⟨p_id, h_pp⟩} : Multiset (PrimeSpectrum A)), le_top
    rwa [Multiset.map_singleton, Multiset.prod_singleton]
  by_cases h_prM : M.IsPrime
  · use ({⟨M, h_prM⟩} : Multiset (PrimeSpectrum A))
    rw [Multiset.map_singleton, Multiset.prod_singleton]
    exact ⟨le_rfl, h_nzI⟩
  obtain ⟨x, hx, y, hy, h_xy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left h_topM
  have lt_add : ∀ z ∉ M, M < M + span A {z} := by
    intro z hz
    refine lt_of_le_of_ne le_sup_left fun m_eq => hz ?_
    rw [m_eq]
    exact mem_sup_right (mem_span_singleton_self z)
  obtain ⟨Wx, h_Wx_le, h_Wx_ne⟩ := hgt (M + span A {x}) (lt_add _ hx) (ne_bot_of_gt (lt_add _ hx))
  obtain ⟨Wy, h_Wy_le, h_Wx_ne⟩ := hgt (M + span A {y}) (lt_add _ hy) (ne_bot_of_gt (lt_add _ hy))
  use Wx + Wy
  rw [Multiset.map_add, Multiset.prod_add]
  refine ⟨le_trans (mul_le_mul' h_Wx_le h_Wy_le) ?_, mt Ideal.mul_eq_bot.mp ?_⟩
  · rw [add_mul]
    apply sup_le (show M * (M + span A {y}) ≤ M from Ideal.mul_le_left)
    rw [mul_add]
    apply sup_le (show span A {x} * M ≤ M from Ideal.mul_le_right)
    rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]
  · rintro (hx | hy) <;> contradiction

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).1 + (↑a).2 * 1 = 1

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).1 + (↑a).2 = 1
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ 1 - (↑a * 1 - ↑a * ↑b) = 1 - ↑a + (↑b - (↑b * 1 - ↑b * ↑a))

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ 1 - (↑a - ↑a * ↑b) = 1 - ↑a + (↑b - (↑b - ↑b * ↑a))
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ ↑a * 1 - ↑a * ↑a = 0

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ ↑a - ↑a * ↑a = 0
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:
by
  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.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us

Tactic:
obtain ⟨Us', hsub, hsup⟩ := isBasis_iff_cover.mp hB U

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
t : Set α
ht : t ⊆ ⋃ i, f i
⊢ IsCompact (⋃ i, t ∩ f i)

Tactic:
exact isCompact_iUnion fun i => hf i _ Set.inter_subset_right

Goal state after: