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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : i = j
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j

Tactic:
subst h

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ (M.charmatrix i i).coeff k = (X.coeff k - (C M).coeff k) i i
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
⊢ (fromBlocks M₁₁ 0 M₂₁ M₂₂).charpoly = M₁₁.charpoly * M₂₂.charpoly

Tactic:
simp only [charpoly, charmatrix_fromBlocks, Matrix.map_zero _ (Polynomial.C_0), neg_zero,
    det_fromBlocks_zero₁₂]

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

Goal state before:
pp: case pos.intro.intro
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 α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val✝¹ : Invertible A
val✝ : Invertible D
this : Invertible (fromBlocks A B 0 D) := A.fromBlocksZero₂₁Invertible B D
⊢ ⅟(fromBlocks A B 0 D) = fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D

Tactic:
invOf_fromBlocks_zero₂₁_eq

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
hdet_MN :
  (M * N).det = (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det)
hdet_NM :
  (N * M).det = (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card m * ((scalar n) X - (B * A).map ⇑C).det)
⊢ (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det) = (N * M).det

Tactic:
← hdet_MN,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
hdet_MN :
  (M * N).det = (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det)
hdet_NM :
  (N * M).det = (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card m * ((scalar n) X - (B * A).map ⇑C).det)
⊢ (M * N).det = (N * M).det
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: case h
R : Type u_1
x : R
inst✝ : Ring R
n : ℕ
hn : x ^ n = 0
⊢ (-x) ^ n = 0

Tactic:
neg_pow,

Goal state after:
case h
R : Type u_1
x : R
inst✝ : Ring R
n : ℕ
hn : x ^ n = 0
⊢ (-1) ^ n * x ^ n = 0
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
S : Type u_2
M N : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module S N
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] N
hf : Function.Injective ⇑f
p : Submodule R M
⊢ (map f p).spanRank = p.spanRank

Tactic:
simpa using lift_spanRank_map_eq_of_injective f hf p

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

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

Tactic:
rcases Finset.mem_image.1 (SetLike.mem_coe.mp hs) with ⟨k, -, rfl⟩

Goal state after:
case refine_1
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
k : ℕ
hs : x ^ k ∈ ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))
⊢ x ^ k ∈ ↑(Subalgebra.toSubmodule R[x])
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
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C A.det * ((scalar n) X - C.mapMatrix A⁻¹).det) =
    C A⁻¹.det * (C.mapMatrix A * ((scalar n) X - C.mapMatrix A⁻¹)).det

Tactic:
by simp [RingHom.map_det]

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
i j : n
⊢ (1 - X • M.map ⇑C).map (eval 0) i j = 1 i j

Tactic:
rcases eq_or_ne i j with hij | hij <;> simp [hij, one_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
hk : 1 < k
⊢ (hasseDeriv k) X = 0

Tactic:
by
  rw [← monomial_one_one_eq_X, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : n < i + 1
⊢ r ^ (i - n) * ↑(i.choose n) = r ^ (i - n) * ↑(i.choose n)

pp: case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : ¬n < i + 1
⊢ 0 = r ^ (i - n) * ↑(i.choose n)

Tactic:
· rfl

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : ¬n < i + 1
⊢ 0 = r ^ (i - n) * ↑(i.choose n)
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
hn : x.2 ≤ n
⊢ (monomial (m + n - (x.2 + x.1))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
add_comm x.2 x.1,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
hn : x.2 ≤ n
⊢ (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : ¬p.natDegree ≤ n
h₂ : ¬n = p.natDegree
⊢ 0 = 0

Tactic:
· rfl

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
h : ¬p.coeff n = 0
⊢ ↑⟨p.coeff n, ⋯⟩ = p.coeff n

Tactic:
· rfl

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

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
← tsub_add_cancel_of_le (le_tsub_of_add_le_left this),

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n - 1 + 1) ∈
    Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
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
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
this✝ : NoZeroDivisors R
this : Nontrivial R
⊢ IsAlgebraic R a

Tactic:
have : IsDomain R := NoZeroDivisors.to_isDomain _

Goal state after:
case pos
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
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
⊢ IsAlgebraic R a
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
e : ¬I = ⊤
m : Ideal R
hm : m.IsMaximal
hm' : I ≤ m
⊢ False

Tactic:
exact hx.not_lt (show x < ⟨m, hm.isPrime⟩ from hI.trans_le hm')

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

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : ¬FaithfulSMul R S
⊢ finrank R S * finrank S T = finrank R T

Tactic:
Module.finrank_eq_zero_of_not_faithfulSMul h,

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : ¬FaithfulSMul R S
⊢ 0 * finrank S T = finrank 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
alg : Algebra.IsAlgebraic R S
inst✝¹ : IsDomain S
inst✝ : FaithfulSMul R S
this : IsDomain R
⊢ Module.rank (FractionRing R[X]) (FractionRing S[X]) = Module.rank R S

Tactic:
rank_fractionRing,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝¹ : IsDomain S
inst✝ : FaithfulSMul R S
this : IsDomain R
⊢ Module.rank R[X] S[X] = Module.rank R S
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
alg : Algebra.IsAlgebraic R S
inst✝¹ : IsDomain S
inst✝ : FaithfulSMul R S
σ : Type u
this : IsDomain R
⊢ Module.rank (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) = lift.{u, u_2} (Module.rank R S)

Tactic:
rank_fractionRing,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝¹ : IsDomain S
inst✝ : FaithfulSMul R S
σ : Type u
this : IsDomain R
⊢ Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = lift.{u, u_2} (Module.rank R 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
x✝³ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (M ⊗[R] N)
this : LinearMap.id = 0
⊢ Subsingleton N

Tactic:
subsingleton_iff_forall_eq 0

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝³ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (M ⊗[R] N)
this : LinearMap.id = 0
⊢ ∀ (y : N), y = 0
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 ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (N ⊗[R] M)
this : LinearMap.id = 0
⊢ Subsingleton N

Tactic:
subsingleton_iff_forall_eq 0

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝³ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (N ⊗[R] M)
this : LinearMap.id = 0
⊢ ∀ (y : N), y = 0
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
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
⊢ (algebraMap S (S ⊗[R] T)).SurjectiveOnStalks

Tactic:
by
  let g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
  intro J hJ
  rw [surjective_localRingHom_iff]
  intro x
  obtain ⟨t, r, a, ht, e⟩ := hf.exists_mul_eq_tmul x (J.comap g) inferInstance
  refine ⟨a, algebraMap _ _ r, 1 ⊗ₜ (r • t), ht, ?_, ?_⟩
  · intro H
    simp only [Algebra.algebraMap_eq_smul_one (A := S), Algebra.TensorProduct.algebraMap_apply,
      Algebra.algebraMap_self, id_apply, smul_tmul, ← Algebra.algebraMap_eq_smul_one (A := T)] at H
    rw [Ideal.mem_comap, Algebra.smul_def, g.map_mul] at ht
    exact ht (J.mul_mem_right _ H)
  · simp only [tmul_smul, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self,
      RingHomCompTriple.comp_apply, Algebra.smul_mul_assoc, Algebra.TensorProduct.tmul_mul_tmul,
      one_mul, mul_one, id_apply, ← e]
    rw [Algebra.algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc]

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
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
⊢ f.SurjectiveOnStalks ↔ Function.Surjective ⇑f

Tactic:
by
  refine ⟨fun H x ↦ ?_, fun h ↦ surjectiveOnStalks_of_surjective h⟩
  obtain ⟨y, r, c, hc, hr, e⟩ :=
    (surjective_localRingHom_iff _).mp (H (IsLocalRing.maximalIdeal _) inferInstance) x
  simp only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, not_not] at hc hr
  refine ⟨(isUnit_of_map_unit f r hr).unit⁻¹ * y, ?_⟩
  apply hr.mul_right_injective
  apply hc.mul_right_injective
  simp only [← map_mul, ← mul_assoc, IsUnit.mul_val_inv, one_mul, e]

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

Goal state before:
pp: case of_equiv
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_5
inst✝ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
ih : ∀ (U : α✝ → Opens α), ↑(⨅ i, U i) = ⋂ i, ↑(U i)
U : β✝ → Opens α
⊢ ↑(⨅ i, U i) = ⋂ i, ↑(U i)

Tactic:
rw [← e.iInf_comp, ← e.surjective.iInter_comp, ih]

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Tactic:
tfae_have 1 ↔ 2 := by
    simp_rw [isWellFounded_iff]
    exact Opens.compl_bijective.2.wellFounded_iff (@OrderIso.compl (Set α)).lt_iff_lt.symm
  tfae_have 1 ↔ 4 := noetherianSpace_iff_opens α
  tfae_have 1 → 3 := @NoetherianSpace.isCompact α _
  tfae_have 3 → 4 := fun h s => h s
  tfae_finish

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ NoetherianSpace ↑s ↔ ∀ t ⊆ s, IsCompact t

Tactic:
by
  simp only [noetherianSpace_iff_isCompact, IsEmbedding.subtypeVal.isCompact_iff,
    Subtype.forall_set_subtype]

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset (↑s × ↑s)
⊢ ∀ (hx : (t.sup fun x ↦ ↑x.1 \ ↑x.2) ∈ closure s), p (t.sup fun x ↦ ↑x.1 \ ↑x.2) hx

Tactic:
refine t.induction (by simpa using sdiff _ bot_mem _ bot_mem) fun x t _ ih hxt ↦ ?_
  simp only [Finset.sup_insert] at hxt ⊢
  exact sup _ _ _ ((mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mpr ⟨_, rfl⟩)
    (sdiff _ x.1.2 _ x.2.2) (ih _)

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ f x ∈ f '' s

Tactic:
exact hV hx

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
⊢ x ∉ I

Tactic:
intro hx
  apply hI.top_notMem
  have ht : x ⊔ xᶜ ∈ I := sup_mem ‹_› ‹_›
  rwa [sup_compl_eq_top] at ht

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: case none
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤
    match none with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)

pp: case some
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
val✝ : ι
⊢ sequenceOfCofinals p 𝒟 n ≤
    match some val✝ with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)

Tactic:
· rfl

Goal state after:
case some
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
val✝ : ι
⊢ sequenceOfCofinals p 𝒟 n ≤
    match some val✝ with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case cons
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact ((Finset.cons i s ih).inf t)

Tactic:
rw [Finset.inf_cons]
    exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
hs : IsConstructible s
⊢ IsConstructible (f '' s)

Tactic:
induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    exact (hUcomp.image_of_isEmbedding hfopen.isEmbedding hfcomp).isConstructible <|
      hfopen.isOpenMap _ hUopen
  | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
  | compl s hs hs' =>
    rw [← range_sdiff_image hfopen.injective]
    exact (hfcomp.isConstructible hfopen.isOpen_range).sdiff hs'

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsLocallyConstructible (t i)) → IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ IsLocallyConstructible ((Finset.cons i s ih).inf t)

Tactic:
rw [Finset.inf_cons]
    exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p q : Ideal R
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : Q.LiesOver q
hle : p ≤ q
h : p = q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
subst h

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p : Ideal R
inst✝³ : p.IsPrime
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : p.IsPrime
inst✝ : Q.LiesOver p
hle : p ≤ p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ IsLocalHom (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯)

Tactic:
exact Localization.isLocalHom_localRingHom (P.under R) P (algebraMap R S) Ideal.LiesOver.over

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

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

Tactic:
algebraize [f, g, (g.comp f)]
  exact Module.Flat.trans R S T

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
hs : IsClosed s
ht : IsClosed t
⊢ s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s

Tactic:
by
  rw [Set.ssubset_def, vanishingIdeal_anti_mono_iff hs, vanishingIdeal_anti_mono_iff ht,
    lt_iff_le_not_ge]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R
⊢ basicOpen f ⊓ basicOpen g ≤ basicOpen g

Tactic:
exact inf_le_right

Goal state after: