mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ (A + U * C * V) * (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) =
    A * ⅟A - A * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A -
      U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A

Tactic:
simp_rw [add_sub_assoc, add_mul, mul_sub, Matrix.mul_assoc]

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
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 + U * C * V * ⅟A - U * C * (⅟C + V * ⅟A * U) * ⅟(⅟C + V * ⅟A * U) * V * ⅟A = 1

Tactic:
by
      rw [Matrix.mul_invOf_cancel_right]
      abel

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

Goal state before:
pp: case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
⊢ A.det • B = A.det • C

Tactic:
rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←
      mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]

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 B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate
⊢ (A * B).adjugate = B.adjugate * A.adjugate

Tactic:
have f'_g_mul : ∀ M N : Matrix n n α, f' (g M * g N) = M * N := by
    intro M N
    rw [map_mul, f'_inv, f'_inv]

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), f' (g M * g N) = M * N
⊢ (A * B).adjugate = B.adjugate * A.adjugate
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
this✝ : Invertible (M.toBlock p p)
this : (fun i ↦ k ≤ b i) = q
⊢ (M⁻¹.toBlock (fun i ↦ k ≤ b i) fun i ↦ b i < k) = 0

Tactic:
rw [this, ← Matrix.zero_mul (M.toBlock p p)⁻¹, ← h_mul_eq_zero,
    mul_inv_cancel_right_of_invertible]

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

Goal state before:
pp: 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 (fromBlocks A B C D)
this✝ : Invertible 1 := invertibleOne
this : Invertible 1 := invertibleOne
iDC : Invertible (fromBlocks 1 0 (⅟D * C) 1) := fromBlocksZero₁₂Invertible 1 (⅟D * C) 1
⊢ Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D)

Tactic:
letI iBD : Invertible (fromBlocks 1 (B * ⅟D) 0 1 : Matrix (m ⊕ n) (m ⊕ n) α) :=
    fromBlocksZero₂₁Invertible _ _ _

Goal state after:
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 (fromBlocks A B C D)
this✝ : Invertible 1 := invertibleOne
this : Invertible 1 := invertibleOne
iDC : Invertible (fromBlocks 1 0 (⅟D * C) 1) := fromBlocksZero₁₂Invertible 1 (⅟D * C) 1
iBD : Invertible (fromBlocks 1 (B * ⅟D) 0 1) := fromBlocksZero₂₁Invertible 1 (B * ⅟D) 1
⊢ Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D)
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: 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 A
inst✝ : Invertible (fromBlocks A B C D)
⊢ Invertible (D - C * ⅟A * B)

Tactic:
letI iABCD' :=
    submatrixEquivInvertible (fromBlocks A B C D) (Equiv.sumComm _ _) (Equiv.sumComm _ _)

Goal state after:
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 A
inst✝ : Invertible (fromBlocks A B C D)
iABCD' : Invertible ((fromBlocks A B C D).submatrix ⇑(Equiv.sumComm n m) ⇑(Equiv.sumComm n m)) :=
  (fromBlocks A B C D).submatrixEquivInvertible (Equiv.sumComm n m) (Equiv.sumComm n m)
⊢ Invertible (D - C * ⅟A * B)
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
⊢ IsNilpotent (P.sum fun n a ↦ (monomial n) a)

Tactic:
exact isNilpotent_sum (fun i _ ↦ by simpa only [isNilpotent_monomial_iff] using h i)

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ f ((Fintype.linearCombination R b) (Pi.single i 1)) = f (b i)

Tactic:
Fintype.linearCombination_apply_single,

Goal state after:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ f (1 • b i) = f (b i)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
⊢ Represents b (A * A') (f * f')

Tactic:
by
  delta Matrix.Represents PiToModule.fromMatrix
  rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, map_mul]
  ext
  dsimp [PiToModule.fromEnd]
  rw [← h'.congr_fun, ← h.congr_fun]
  rfl

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ ((LinearMap.llcomp R (ι → R) (ι → R) M) (Fintype.linearCombination R b) ∘ₗ algEquivMatrix'.symm.toLinearMap) 1 =
    (PiToModule.fromEnd R b) 1

Tactic:
rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, map_one]

Goal state after:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ ((LinearMap.llcomp R (ι → R) (ι → R) M) (Fintype.linearCombination R b)) 1 = (PiToModule.fromEnd R b) 1
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ toENat p.spanRank = ⨅ s, ↑(↑s).card

Tactic:
spanRank_toENat_eq_iInf_encard

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard = ⨅ s, ↑(↑s).card
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
⊢ s.encard = ↑p.spanFinrank

Tactic:
have := fg_iff_spanRank_eq_spanFinrank.mpr h

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ s.encard = ↑p.spanFinrank
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this : Algebra R S := f.toAlgebra
⊢ f.IsIntegralElem z

Tactic:
have := (IsIntegral.fg_adjoin_singleton hx).mul (IsIntegral.fg_adjoin_singleton hy)

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this✝ : Algebra R S := f.toAlgebra
this : (Subalgebra.toSubmodule R[x] * Subalgebra.toSubmodule R[y]).FG
⊢ f.IsIntegralElem z
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r✝ : R
f : R[X]
r : R
P : R[X]
⊢ (taylorAlgHom (-r)) ((↑↑(taylorAlgHom r).toRingHom).toFun P) = P

Tactic:
by simp [taylor, comp_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r✝ : R
f : R[X]
r : R
P : R[X]
⊢ (↑↑(taylorAlgHom r).toRingHom).toFun ((taylorAlgHom (-r)) P) = P

Tactic:
by simp [taylor, comp_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (∑ x ∈ Finset.antidiagonal n, p.coeff x.1 * q.coeff x.2) * r ^ (p.natDegree + q.natDegree - n)

Tactic:
rw [← coeff_mul]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
ha : a ≤ p.natDegree
hb : b ≤ q.natDegree
⊢ p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
    p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))

Tactic:
| inr hb =>

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).scaleRoots r = r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r

Tactic:
natDegree_mul' h,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).scaleRoots r = r ^ (p.natDegree + q.natDegree - (p.natDegree + q.natDegree)) • (p * q).scaleRoots r
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
f : R[X]
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : R →+* S
hi : Function.Injective ⇑i
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), i (j a a_1) = a
⊢ f.Splits

Tactic:
splits_iff_exists_multiset

Goal state after:
R : Type u_1
inst✝² : CommRing R
f : R[X]
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : R →+* S
hi : Function.Injective ⇑i
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), i (j a a_1) = a
⊢ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
⊢ IsField (R ⧸ comap (algebraMap R S) I)

Tactic:
have : IsPrime (I.comap (algebraMap R S)) := comap_isPrime _ _

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
this : (comap (algebraMap R S) I).IsPrime
⊢ IsField (R ⧸ comap (algebraMap R S) I)
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
⊢ IsIntegral R t

Tactic:
let φ := aeval (R := R) s

Goal state after:
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
⊢ IsIntegral R t
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
⊢ IsAlgebraic R z

Tactic:
by
  have ⟨t, ht, r, hr, eq⟩ := alg_y.exists_nonzero_eq_adjoin_mul hy
  have := alg_yz.mul (Algebra.isAlgebraic_adjoin_singleton_iff.mpr alg_y _ ht)
  rw [mul_right_comm, eq, ← Algebra.smul_def] at this
  exact this.of_smul (mem_nonZeroDivisors_of_ne_zero hr)

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case mp
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
f : R →ₗ[R] M := (LinearMap.lsmul R M).flip m
a : A
h : a • 1 ⊗ₜ[R] m = 0
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor A f)) a) 1 = ((AlgebraTensorModule.curry 0) a) 1

Tactic:
smul_tmul',

Goal state after:
case mp
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
f : R →ₗ[R] M := (LinearMap.lsmul R M).flip m
a : A
h : (a • 1) ⊗ₜ[R] m = 0
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor A f)) a) 1 = ((AlgebraTensorModule.curry 0) a) 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
S : Type u_1
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FaithfullyFlat R M
⊢ FaithfullyFlat S (S ⊗[R] M)

Tactic:
by
  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.Algebra.Order.Ring.Idempotent

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

Tactic:
by
    simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup,
      (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq, add_comm, a.2.2]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
⊢ ∃ y ∉ I, x * y ∈ I

Tactic:
have : Nat.find H ≠ 0 :=
    fun h ↦ hy ⟨n, by simpa only [h, pow_zero, one_mul] using Nat.find_spec H⟩

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
this : Nat.find H ≠ 0
⊢ ∃ y ∉ I, x * y ∈ I
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

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

Tactic:
· 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: 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 A
⊢ (Ideal.comap (algebraMap R A) J).minimalPrimes = Ideal.comap (algebraMap R A) '' J.minimalPrimes

Tactic:
by
  conv_rhs => rw [← map_under S A J, minimalPrimes_map S]
  refine (Set.image_preimage_eq_iff.mpr ?_).symm
  exact subset_trans (Ideal.minimalPrimes_comap_subset (algebraMap R A) J) (by simp)

Goal state after:
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
⊢ U ⊆ ⋃ i, (b ∘ f') i

Tactic:
by rw [e]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ Function.Surjective ⇑(piLocalizationToMaximal R)

Tactic:
by
  classical
  exact fun r ↦ ⟨fun I ↦ if h : I.1.IsMaximal then r ⟨_, h⟩ else 0, funext fun _ ↦ dif_pos _⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
⊢ I.asIdeal.IsMaximal

Tactic:
classical
  have ⟨J, max, le⟩ := I.1.exists_le_maximal I.2.ne_top
  obtain ⟨r, hr⟩ := surj (Function.update 0 ⟨J, max.isPrime⟩ 1)
  by_contra h
  have hJ : algebraMap _ _ r = _ := (congr_fun hr _).trans (Function.update_self ..)
  have hI : algebraMap _ _ r = _ := congr_fun hr I
  rw [← IsLocalization.lift_eq (M := J.primeCompl) (S := Localization J.primeCompl), hJ, map_one,
    Function.update_of_ne] at hI
  · exact one_ne_zero hI
  · intro eq; have : I.1 = J := congr_arg (·.1) eq; exact h (this ▸ max)
  · exact fun ⟨s, hs⟩ ↦ IsLocalization.map_units (M := I.1.primeCompl) _ ⟨s, fun h ↦ hs (le h)⟩

Goal state after:
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: case neg
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
x : X
hx : x ∈ s
i : ι
hi : x ∈ ↑(U i)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst✝] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
⊢ IsPreirreducible s

Tactic:
choose j haj using mem_iUnion.mp <| hsU ha₁

Goal state after:
case neg
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
x : X
hx : x ∈ s
i : ι
hi : x ∈ ↑(U i)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst✝] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ ↑(U j)
⊢ IsPreirreducible s
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case hb'
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ ∀ (i : ι), IsCompact (b i).carrier

Tactic:
exact hb'

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case insert
α✝ : Type u_1
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
a✝ : Set α
s✝ : Set (Set α)
ha : a✝ ∉ s✝
hs : s✝.Finite
ih :
  (∀ t ∈ s✝, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t) →
    (∀ t ∈ s✝, IsCompact t) → (∀ t ∈ s✝, IsOpen[inst✝¹] t) → s✝.Nonempty → IsCompact (⋂₀ s✝)
ho : ∀ t ∈ insert a✝ s✝, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ insert a✝ s✝, IsCompact t
h : ∀ t ∈ insert a✝ s✝, IsOpen[inst✝¹] t
⊢ (insert a✝ s✝).Nonempty → IsCompact (⋂₀ insert a✝ s✝)

Tactic:
| insert ha hs ih =>

Goal state after:
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : QuasiSober Y
inst✝² : T0Space Y
inst✝¹ : QuasiSober X
inst✝ : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ coheight (irreducibleSetEquivPoints.symm (f x)) = coheight (irreducibleSetEquivPoints.symm x)

Tactic:
← Topology.IsOpenEmbedding.coheight_map hf

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : QuasiSober Y
inst✝² : T0Space Y
inst✝¹ : QuasiSober X
inst✝ : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ coheight (irreducibleSetEquivPoints.symm (f x)) = coheight (map f ⋯ (irreducibleSetEquivPoints.symm x))
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
F : A →ₗ[R] ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
this : (f x - (algebraMap A B) x) * (f y - (algebraMap A B) y) = 0
⊢ f (x * y) - (algebraMap A B) (x * y) = x • (f y - (algebraMap A B) y) + y • (f x - (algebraMap A B) x)

Tactic:
simp only [map_mul, sub_mul, mul_sub, Algebra.smul_def] at this ⊢

Goal state after:
case refine_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
F : A →ₗ[R] ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
this : f x * f y - (algebraMap A B) x * f y - (f x * (algebraMap A B) y - (algebraMap A B) x * (algebraMap A B) y) = 0
⊢ f x * f y - (algebraMap A B) x * (algebraMap A B) y =
    (algebraMap A B) x * f y - (algebraMap A B) x * (algebraMap A B) y +
      ((algebraMap A B) y * f x - (algebraMap A B) y * (algebraMap A B) x)
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: b : ℕ
⊢ factorizationLCMLeft 0 b = 1

Tactic:
simp [factorizationLCMLeft]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a : ℕ
⊢ a.factorizationLCMLeft 0 = 1

Tactic:
simp [factorizationLCMLeft]

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

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf : Function.Injective ⇑(ConcreteCategory.hom f)
hg : (Hom.hom g).Flat
⊢ Function.Injective ⇑(ConcreteCategory.hom (pushout.inr f g))

Tactic:
algebraize [f.hom, g.hom]

Goal state after:
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf : Function.Injective ⇑(ConcreteCategory.hom f)
hg : (Hom.hom g).Flat
algInst✝¹ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑T := (Hom.hom g).toAlgebra
algebraizeInst✝ : Module.Flat ↑R ↑T
⊢ Function.Injective ⇑(ConcreteCategory.hom (pushout.inr f g))