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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin n) R
⊢ eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace

Tactic:
by
  induction n with
  | zero => simp
  | succ n IH =>
    rw [det_succ_row_zero, map_sum, eval_finsetSum]
    simp only [add_apply, smul_apply, map_apply, smul_eq_mul, X_mul_C, submatrix_add,
      submatrix_smul, Pi.add_apply, Pi.smul_apply, submatrix_map, derivative_mul, map_add,
      derivative_C, zero_mul, derivative_X, mul_one, zero_add, eval_add, eval_mul, eval_C, eval_X,
      mul_zero, add_zero, eval_det_add_X_smul, eval_pow, eval_neg, eval_one]
    rw [Finset.sum_eq_single 0]
    · simp only [Fin.val_zero, pow_zero, derivative_one, eval_zero, one_apply_eq, eval_one,
        mul_one, zero_add, one_mul, Fin.succAbove_zero, submatrix_one _ (Fin.succ_injective _),
        det_one, IH, trace_submatrix_succ]
    · intro i _ hi
      cases n with
      | zero => exact (hi (Subsingleton.elim i 0)).elim
      | succ n =>
        simp only [one_apply_ne' hi, eval_zero, mul_zero, zero_add, zero_mul, add_zero]
        rw [det_eq_zero_of_column_eq_zero 0, eval_zero, mul_zero]
        intro j
        rw [submatrix_apply, Fin.succAbove_of_castSucc_lt, one_apply_ne]
        · exact (bne_iff_ne (a := Fin.succ j) (b := Fin.castSucc 0)).mp rfl
        · rw [Fin.castSucc_zero]; exact lt_of_le_of_ne (Fin.zero_le _) hi.symm
    · exact fun H ↦ (H <| Finset.mem_univ _).elim

Goal state after:
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]
hlifts : p ∈ lifts f
hp : p.Monic
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
rcases subsingleton_or_nontrivial S with hR | hR

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Subsingleton S
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

case inr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Nontrivial S
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
r : R
hp : p ∈ lifts (algebraMap R S)
⊢ r • p ∈ lifts (algebraMap R S)

Tactic:
by
  rw [mem_lifts_iff_mem_alg] at hp ⊢
  exact Subalgebra.smul_mem (mapAlg R S).range hp r

Goal state after:
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 : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
⊢ f.IsIntegralElem (x - y)

Tactic:
simpa only [sub_eq_add_neg] using hx.add f (hy.neg f)

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
if_neg hnik,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ ↑((i + k).choose k) * 0 = if n - k = i then ↑(n.choose k) * r else 0
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
this :
  ∀ (t : R), eval t ((taylor x) p) = ∑ i ∈ Finset.range (((taylor x) p).natDegree + 2), ((taylor x) p).coeff i * t ^ i
⊢ ∃ c, c * y ^ 2 + eval x (derivative p) * y + eval x p = eval y ((taylor x) p)

Tactic:
this,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
this :
  ∀ (t : R), eval t ((taylor x) p) = ∑ i ∈ Finset.range (((taylor x) p).natDegree + 2), ((taylor x) p).coeff i * t ^ i
⊢ ∃ c,
    c * y ^ 2 + eval x (derivative p) * y + eval x p =
      ∑ i ∈ Finset.range (((taylor x) p).natDegree + 2), ((taylor x) p).coeff i * y ^ i
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
this :
  ∀ (t : R), eval t ((taylor x) p) = ∑ i ∈ Finset.range (((taylor x) p).natDegree + 2), ((taylor x) p).coeff i * t ^ i
⊢ ∃ c,
    c * y ^ 2 + eval x (derivative p) * y + eval x p =
      ∑ k ∈ Finset.range (((taylor x) p).natDegree + 1), ((taylor x) p).coeff (k + 1) * y ^ (k + 1) +
        ((taylor x) p).coeff 0 * y ^ 0

Tactic:
Finset.sum_range_succ'

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
this :
  ∀ (t : R), eval t ((taylor x) p) = ∑ i ∈ Finset.range (((taylor x) p).natDegree + 2), ((taylor x) p).coeff i * t ^ i
⊢ ∃ c,
    c * y ^ 2 + eval x (derivative p) * y + eval x p =
      ∑ k ∈ Finset.range ((taylor x) p).natDegree, ((taylor x) p).coeff (k + 1 + 1) * y ^ (k + 1 + 1) +
          ((taylor x) p).coeff (0 + 1) * y ^ (0 + 1) +
        ((taylor x) p).coeff 0 * y ^ 0
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x : R
hx : x ≠ 0
⊢ (C x).integralNormalization = 1

Tactic:
simp [integralNormalization, sum_def, support_C hx, degree_C hx]

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

Goal state before:
pp: case add
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 q : MvPolynomial σ R
hp : (aeval fun x ↦ 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (aeval f) p
hq : (aeval fun x ↦ 1 ⊗ₜ[R] f x) q = 1 ⊗ₜ[R] (aeval f) q
⊢ (aeval fun x ↦ 1 ⊗ₜ[R] f x) (p + q) = 1 ⊗ₜ[R] (aeval f) (p + q)

Tactic:
| add p q hp hq =>

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
a✝ : Nontrivial R
a : R
m : Multiset R
hm : f = C f.leadingCoeff * ((X + C a) * (Multiset.map (fun x ↦ X + C x) m).prod)
ha : a ∈ a ::ₘ m
h : (Irreducible (X + C a) ∧ ∀ m_1 ∈ (Multiset.map (fun x ↦ X + C x) m).toList, IsUnit m_1) ∧ IsUnit (C f.leadingCoeff)
this : m = 0
⊢ (C f.leadingCoeff * ((X + C a) * (Multiset.map (fun x ↦ X + C x) m).prod)).natDegree ≤ 1

Tactic:
this,

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
a✝ : Nontrivial R
a : R
m : Multiset R
hm : f = C f.leadingCoeff * ((X + C a) * (Multiset.map (fun x ↦ X + C x) m).prod)
ha : a ∈ a ::ₘ m
h : (Irreducible (X + C a) ∧ ∀ m_1 ∈ (Multiset.map (fun x ↦ X + C x) m).toList, IsUnit m_1) ∧ IsUnit (C f.leadingCoeff)
this : m = 0
⊢ (C f.leadingCoeff * ((X + C a) * (Multiset.map (fun x ↦ X + C x) 0).prod)).natDegree ≤ 1
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : CommMonoid M
a : A
m : M
b : B
⊢ invFun (single m (a ⊗ₜ[R] b)) = a ⊗ₜ[R] single m b

Tactic:
simp [rTensorEquivAlgEquiv.invFun]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg✝ : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ((C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod).comp g).Splits

Tactic:
mul_comp,

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg✝ : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ((C f.leadingCoeff).comp g * (Multiset.map (fun x ↦ X + C x) m).prod.comp g).Splits
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg.refine_1
R : Type u_5
S : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : (algebraMap R Rₘ) ↑⟨p.leadingCoeff, hM⟩ * b = 1
⊢ (algebraMap R Rₘ) p.leadingCoeff ≠ 0

Tactic:
refine fun hfp => zero_ne_one
      (_root_.trans (zero_mul b).symm (hfp ▸ hb) : (0 : Rₘ) = 1)

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

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ ((Ideal.Quotient.mkₐ S I).comp (Algebra.ofId S S[X])).IsIntegral

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

Goal state after:
S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
eq_top : S[(Ideal.Quotient.mkₐ S I) X] = ⊤
⊢ ((Ideal.Quotient.mkₐ S I).comp (Algebra.ofId S S[X])).IsIntegral
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
y : N1 ⊗[R] M
hy : (LinearMap.rTensor M l12) y = x ⊗ₜ[R] m
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = ⟨x, hx⟩ ⊗ₜ[R] m

Tactic:
refine ⟨LinearMap.rTensor M (LinearMap.rangeRestrict _ ∘ₗ LinearMap.rangeRestrict l12) y,
      Module.Flat.rTensor_preserves_injective_linearMap (LinearMap.ker l23).subtype
      Subtype.val_injective ?_⟩

Goal state after:
case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
y : N1 ⊗[R] M
hy : (LinearMap.rTensor M l12) y = x ⊗ₜ[R] m
⊢ (LinearMap.rTensor M l23.ker.subtype)
      ((TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id)
        ((LinearMap.rTensor M ((Submodule.inclusion complex).rangeRestrict ∘ₗ l12.rangeRestrict)) y)) =
    (LinearMap.rTensor M l23.ker.subtype) (⟨x, hx⟩ ⊗ₜ[R] m)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

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

Tactic:
rw [nilradical, zeroLocus_radical, Ideal.zero_eq_bot, zeroLocus_bot]

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (R ∙ x) * M + (R ∙ x) * (R ∙ y) ≤ M

Tactic:
apply sup_le (show span R {x} * M ≤ M from Ideal.mul_le_right)

Goal state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (R ∙ x) * (R ∙ y) ≤ M
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
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
⊢ finrank R S * finrank S T = finrank R T

Tactic:
by_cases h : FaithfulSMul R S
  · have : FaithfulSMul R T := .trans R S T
    have : IsDomain R := (FaithfulSMul.algebraMap_injective R T).isDomain
    have : IsDomain S := (FaithfulSMul.algebraMap_injective S T).isDomain
    rw [← IsFractionRing.finrank_eq R (FractionRing R) S (FractionRing S),
      ← IsFractionRing.finrank_eq S (FractionRing S) T (FractionRing T),
      ← IsFractionRing.finrank_eq R (FractionRing R) T (FractionRing T),
      Module.finrank_mul_finrank (FractionRing R) (FractionRing S) (FractionRing T)]
  · rw [Module.finrank_eq_zero_of_not_faithfulSMul h, zero_mul,
      Module.finrank_eq_zero_of_not_faithfulSMul]
    exact fun _ ↦ h (FaithfulSMul.tower_bot R S T)

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)

Tactic:
this,

Goal state after:
case add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ 1 ⊗ₜ[R] (r₁ • t₁ * r₂ • t₂) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
this : lTensor B ((TensorProduct.mk A B M) 1) = ↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1
⊢ Function.Injective ⇑(lTensor B ((TensorProduct.mk A B M) 1))

Tactic:
this,

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
this : lTensor B ((TensorProduct.mk A B M) 1) = ↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1
⊢ Function.Injective ⇑(↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : x ∈ comap (algebraMap A B) (map (algebraMap A B) I)
⊢ x ∈ I

Tactic:
rw [Ideal.mem_comap] at hx

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : (algebraMap A B) x ∈ map (algebraMap A B) I
⊢ x ∈ I
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
⊢ ∀ (a b : α), le a b → le b a → a = b

Tactic:
intro _ _ hab hba; simp_rw [eq_le] at hab hba; exact le_antisymm hab hba

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

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
this : r = 0
hr :
  (toPiLocalization ((i : ι) → R i)) r { asIdeal := J, isMaximal := max } =
    Function.update 0 { asIdeal := J, isMaximal := max } 1 { asIdeal := J, isMaximal := max }
⊢ False

Tactic:
this,

Goal state after:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
this : r = 0
hr :
  (toPiLocalization ((i : ι) → R i)) 0 { asIdeal := J, isMaximal := max } =
    Function.update 0 { asIdeal := J, isMaximal := max } 1 { asIdeal := J, isMaximal := max }
⊢ False
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
x : α
⊢ x ∈ ↑(U ⇨ V) ↔ x ∈ ↑(Opens.interior (↑U ⇨ ↑V))

Tactic:
simp_rw [BooleanAlgebra.himp_eq, sup_eq_union, coe_interior, _root_.mem_interior,
    SetLike.mem_coe, mem_himp, ← SetLike.coe_subset_coe, coe_inf, inter_subset]

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
x : α
⊢ (∃ W, ↑W ⊆ (↑U)ᶜ ∪ ↑V ∧ x ∈ W) ↔ ∃ t ⊆ ↑V ∪ (↑U)ᶜ, IsOpen[inst✝] t ∧ x ∈ t
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst✝] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : ↑V = sV
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }

Tactic:
refine ⟨V, H₁, ?_⟩

Goal state after:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst✝] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : ↑V = sV
⊢ x ∈ V ∧ V ≤ { carrier := sU, is_open' := hU }
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst✝] U
hZ : IsClosed[inst✝] Z
this : Z ∪ (frontier (U ∩ Z))ᶜ = univ
⊢ IsOpen[inst✝] ((U ∪ (frontier (U ∩ Z))ᶜ) ∩ (Z ∪ (frontier (U ∩ Z))ᶜ))

Tactic:
this,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst✝] U
hZ : IsClosed[inst✝] Z
this : Z ∪ (frontier (U ∩ Z))ᶜ = univ
⊢ IsOpen[inst✝] ((U ∪ (frontier (U ∩ Z))ᶜ) ∩ univ)
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ t ∈ ↑S, IsClosed[inst✝¹] t
hSi : ∀ t ∈ ↑S, IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
⊢ s ∈ ↑S

Tactic:
rcases isIrreducible_iff_sUnion_isClosed.1 hs.1 S hSc (hSU ▸ Set.subset_univ _) with ⟨t, htS, ht⟩

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ t ∈ ↑S, IsClosed[inst✝¹] t
hSi : ∀ t ∈ ↑S, IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
t : Set α
htS : t ∈ S
ht : s ⊆ t
⊢ s ∈ ↑S
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ closure {x} ⊆ S ∧ S ⊆ closure {x} ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z

Tactic:
this,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ True ∧ S ⊆ closure {x} ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z : Set X
hZ : ¬IsPreirreducible Z
⊢ ∃ A B,
    IsClosed[inst✝¹] A ∧
      IsClosed[inst✝¹] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
simp only [IsPreirreducible, not_forall] at hZ
  rcases hZ with ⟨U₁, U₂, hU₁, hU₂, hU₁Z, hU₂Z, hU₁₂⟩
  rw [Set.not_nonempty_iff_eq_empty, ← Set.subset_empty_iff] at hU₁₂
  obtain ⟨x₁, hx₁⟩ : ∃ x₁ ∈ U₁, x₁ ∈ Z ∧ x₁ ∉ U₂ := by
    obtain ⟨x, hx⟩ := hU₁Z
    use x, hx.2, hx.1, fun h₂ ↦ hU₁₂ ⟨hx.1, hx.2, h₂⟩
  obtain ⟨x₂, hx₂⟩ : ∃ x₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁ := by
    obtain ⟨x, hx⟩ := hU₂Z
    use x, hx.2, hx.1, fun h₁ ↦ hU₁₂ ⟨hx.1, h₁, hx.2⟩
  rw [PrespectralSpace.isTopologicalBasis.isOpen_iff] at hU₁ hU₂
  obtain ⟨W₁, hW₁⟩ := hU₁ x₁ hx₁.1
  obtain ⟨W₂, hW₂⟩ := hU₂ x₂ hx₂.1
  refine ⟨W₁ᶜ, W₂ᶜ, by simpa using hW₁.1.1, by simpa using hW₂.1.1, by simp [hW₁.1.2],
    by simp [hW₂.1.2], fun z hz ↦ ?_, ⟨x₁, by grind⟩, ⟨x₂, by grind⟩⟩
  · by_contra! hc
    simp only [Set.mem_union, Set.mem_compl_iff, not_or, not_not] at hc
    exact hU₁₂ ⟨hz, hW₁.2.2 hc.1, hW₂.2.2 hc.2⟩

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst✝¹] (T ∩ range f))
⊢ x ∈ T

Tactic:
← hT.closure_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst✝¹] (T ∩ range f))
⊢ x ∈ closure[inst✝¹] T
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
p : PrimeSpectrum R
this : (↑(RingEquiv.ofBijective f hf).symm).comp f = id R
⊢ PrimeSpectrum.comap ((↑(RingEquiv.ofBijective f hf).symm).comp f) p = p

Tactic:
this,

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
p : PrimeSpectrum R
this : (↑(RingEquiv.ofBijective f hf).symm).comp f = id R
⊢ PrimeSpectrum.comap (id R) p = p
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
⊢ 0 (a * b) = a • 0 b + b • 0 a

Tactic:
by simp only [add_zero, LinearMap.zero_apply, smul_zero]

Goal state after: