mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det = X ^ Fintype.card m * ((scalar n) X - (B * A).map ⇑C).det

Tactic:
rw [← (isUnit_neg_one.pow _).isRegular.left.eq_iff, ← hdet_NM, ← hdet_MN, det_mul_comm]

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

Goal state before:
pp: m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ (A * 1 + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det

Tactic:
rwa [← Matrix.mul_nonsing_inv_cancel_left A (replicateCol ι u * replicateRow ι v),
    ← Matrix.mul_add, det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
nilp : IsNilpotent e
⊢ e = 0

Tactic:
obtain ⟨rfl | n, hn⟩ := nilp
  · rw [pow_zero] at hn; rw [← one_mul e, hn, zero_mul]
  · rw [← hn, idem.pow_succ_eq]

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

Goal state before:
pp: case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this✝ : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
s : { s // span R s = p }
this : ↑(⨅ s', ⨅ (_ : span R s' = p), s'.encard) ≤ ↑(↑s).encard
⊢ ↑(⨅ s, ⨅ (_ : span R s = p), s.encard) ≤ #↑↑s

Tactic:
apply le_trans this

Goal state after:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this✝ : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
s : { s // span R s = p }
this : ↑(⨅ s', ⨅ (_ : span R s' = p), s'.encard) ≤ ↑(↑s).encard
⊢ ↑(↑s).encard ≤ #↑↑s
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:
by
  rw [spanRank_toENat_eq_iInf_encard]
  rcases eq_or_ne (⨅ (s : Set M) (_ : span R s = p), s.encard) ⊤ with (h1 | h2)
  · rw [h1, eq_comm]; simp_rw [iInf_eq_top] at h1 ⊢
    exact fun s ↦ False.elim (Set.encard_ne_top_iff.mpr s.1.finite_toSet (h1 s.1 s.2))
  · simp_rw [← Set.encard_coe_eq_coe_finsetCard]
    apply le_antisymm
    · exact le_iInf fun s ↦ iInf₂_le (s.1 : Set M) s.2
    · refine le_iInf fun s ↦ le_iInf fun h ↦ ?_
      by_cases hs : s.Finite
      · exact iInf_le_of_le ⟨hs.toFinset, by simpa⟩ (by simp)
      · rw [Set.Infinite.encard_eq hs]
        exact OrderTop.le_top _

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = p) → ⨅ s, #↑↑s < ℵ₀

Tactic:
rintro ⟨s, hs₁, hs₂⟩

Goal state after:
case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
hs₁ : s.Finite
hs₂ : span R s = p
⊢ ⨅ s, #↑↑s < ℵ₀
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
h✝ : Nontrivial R
s : Finset M
hs_card : s.card = ⊤.spanFinrank
hs_span : Submodule.span R ↑s = ⊤
this : Submodule.span R (Set.range Subtype.val) = ⊤
A : ↥(isRepresentation R Subtype.val)
h : ∀ (i j : ↥s), ↑A i j ∈ I
hI : range ((isRepresentation.toEnd R Subtype.val this) A) ≤ I • ⊤
⊢ ∀ (k : ℕ), (↑A).charpoly.coeff k ∈ I ^ ((↑A).charpoly.natDegree - k)

Tactic:
by simpa using coeff_charpoly_mem_ideal_pow h

Goal state after:
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, s.encard = ↑p.spanFinrank ∧ span R s = p

Tactic:
obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p

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
⊢ ∃ s, s.encard = ↑p.spanFinrank ∧ span R s = p
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{max u v}
h : lift.{v, u} p.spanRank ≤ a
⊢ ∃ s, lift.{v, u} #↑s ≤ a ∧ span R s = p

Tactic:
obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p

Goal state after:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{max u v}
h : lift.{v, u} p.spanRank ≤ a
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
⊢ ∃ s, lift.{v, u} #↑s ≤ a ∧ span R s = p
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : Fintype.card n = 0
⊢ Monic 1

Tactic:
apply monic_one

Goal state after:
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
⊢ f.range.spanRank ≤ ⊤.spanRank

Tactic:
simpa using spanRank_map_le f ⊤

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R →+* T
I : Ideal R
hI : I.FG
⊢ Submodule.spanFinrank (map f I) ≤ Submodule.spanFinrank I

Tactic:
rw [← Submodule.FG.spanRank_le_iff (hI.map f), ← Cardinal.lift_le.{u}, Cardinal.lift_natCast,
    ← Cardinal.lift_natCast.{v}, ← Submodule.FG.spanRank_eq_spanFinrank hI]
  exact I.lift_spanRank_map_le f

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
⊢ eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace

Tactic:
by
  let e := Matrix.reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
  rw [← Matrix.det_reindexLinearEquiv_self R[X] (Fintype.equivFin n)]
  convert! derivative_det_one_add_X_smul_aux (e M)
  · ext; simp [map_add, e]
  · delta trace
    rw [← (Fintype.equivFin n).symm.sum_comp]
    simp_rw [e, coe_reindexLinearEquiv, reindex_apply, diag_apply, submatrix_apply]

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
⊢ eval 0 M.charpolyRev = 1

Tactic:
by
  rw [charpolyRev, ← coe_evalRingHom, RingHom.map_det, ← det_one (R := R) (n := n)]
  have : (1 - (X : R[X]) • M.map C).map (eval 0) = 1 := by
    ext i j; rcases eq_or_ne i j with hij | hij <;> simp [hij, one_apply]
  congr

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
i : σ
j : ι
⊢ (tensorEquivSum R σ ι S) (X i ⊗ₜ[R] X j) = X (Sum.inl i) * X (Sum.inr j)

Tactic:
by
  simp [tensorEquivSum, algebraTensorAlgEquiv, sumAlgEquiv, renameEquiv, rename, X, C, monomial,
    Finsupp.mapDomain_add, add_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
f : R[X]
hf : f.Splits
S : Type u_2
inst✝ : Semiring S
i : R →+* S
⊢ (map i f).Splits

Tactic:
induction hf using Submonoid.closure_induction

Goal state after:
case mem
R : Type u_1
inst✝¹ : Semiring R
f : R[X]
S : Type u_2
inst✝ : Semiring S
i : R →+* S
x✝ : R[X]
h✝ : x✝ ∈ {x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x}
⊢ (map i x✝).Splits

case one
R : Type u_1
inst✝¹ : Semiring R
f : R[X]
S : Type u_2
inst✝ : Semiring S
i : R →+* S
⊢ (map i 1).Splits

case mul
R : Type u_1
inst✝¹ : Semiring R
f : R[X]
S : Type u_2
inst✝ : Semiring S
i : R →+* S
x✝ y✝ : R[X]
hx✝ : x✝ ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy✝ : y✝ ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
a✝¹ : (map i x✝).Splits
a✝ : (map i y✝).Splits
⊢ (map i (x✝ * y✝)).Splits
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
n : ℕ
left✝ : ¬(ofSubring T p).coeff n = 0
h'n : (ofSubring T p).coeff n = i
⊢ (ofSubring T p).coeff n ∈ ↑T

Tactic:
coeff_ofSubring

Goal state after:
R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
n : ℕ
left✝ : ¬(ofSubring T p).coeff n = 0
h'n : (ofSubring T p).coeff n = i
⊢ ↑(p.coeff n) ∈ ↑T
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
| f.natDegree

Tactic:
rw [hf.eq_prod_roots, natDegree_C_mul hf0, natDegree_multiset_prod_X_sub_C_eq_card]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
| f.roots.card
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
⊢ IsAlgebraic A x ↔ IsAlgebraic K x

Tactic:
constructor <;> rintro ⟨p, hp, px⟩
  · refine ⟨p.map (algebraMap A K), fun h => hp (Polynomial.ext fun i => ?_), ?_⟩
    · have : algebraMap A K (p.coeff i) = 0 :=
        _root_.trans (Polynomial.coeff_map _ _).symm (by simp [h])
      exact to_map_eq_zero_iff.mp this
    · exact (Polynomial.aeval_map_algebraMap K _ _).trans px
  · exact
      ⟨integerNormalization _ p, mt integerNormalization_eq_zero_iff.mp hp,
        integerNormalization_aeval_eq_zero _ p px⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
⊢ (C a * X + C b).Splits

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
R : Type u_1
inst✝ : DivisionSemiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
ha : a = 0
⊢ (C a * X + C b).Splits

case neg
R : Type u_1
inst✝ : DivisionSemiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
ha : ¬a = 0
⊢ (C a * X + C b).Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case neg
R : Type u_1
inst✝ : DivisionSemiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
ha : ¬a = 0
⊢ (C a * (X + C (a⁻¹ * b))).Splits

Tactic:
exact (X_add_C (a⁻¹ * b)).C_mul a

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegralClosure A R B
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
⊢ mk' A ((algebraMap S B) 0) ⋯ = 0

Tactic:
by simp only [map_zero, mk'_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
this : f = (f.comp (C a * X + C b)).comp (C a⁻¹ * (X - C b))
⊢ (C a⁻¹ * (X - C b)).natDegree ≤ 1

Tactic:
rw [natDegree_C_mul (mt inv_eq_zero.mp ha), natDegree_X_sub_C]

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : CommRing A
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Algebra.IsIntegral A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
⊢ ⊥.primesOver B = {⊥}

Tactic:
ext p
  refine ⟨fun ⟨_, ⟨h⟩⟩ ↦ p.eq_bot_of_comap_eq_bot h.symm, ?_⟩
  rintro rfl
  exact ⟨Ideal.isPrime_bot, Ideal.bot_liesOver_bot A B⟩

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

Goal state before:
pp: case refine_1.refine_2.h₁
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
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q.natDegree ∉ q.support →
    (if q.natDegree ≤ q.natDegree + N then (q.coeff q.natDegree).coeff ((revAt N) (q.natDegree + N - q.natDegree))
      else 0) =
      0

Tactic:
· simp +contextual

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus (s \ {0}) = zeroLocus s

Tactic:
rw [← zeroLocus_insert_zero, ← zeroLocus_insert_zero (s := s)]; simp

Goal state after:
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
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Bijective ⇑(LinearMap.lTensor M f) ↔ Function.Bijective ⇑f

Tactic:
simp [Function.Bijective]

Goal state after:
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
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rs) (↥Rts) A
this✝¹ : Nontrivial ↥Rs
this✝ : Nontrivial S
this : IsDomain ↥Rt
⊢ Rts.IsAlgebraic

Tactic:
isAlgebraic_adjoin_iff

Goal state after:
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
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rs) (↥Rts) A
this✝¹ : Nontrivial ↥Rs
this✝ : Nontrivial S
this : IsDomain ↥Rt
⊢ ∀ x ∈ s, IsAlgebraic (↥Rt) x
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
a₁ a₂ : A
ha : ∀ (a : B), a₁ • a = a₂ • a
⊢ a₁ = a₂

Tactic:
apply Module.FaithfullyFlat.tensorProduct_mk_injective (A := A) (B := B) A

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
a₁ a₂ : A
ha : ∀ (a : B), a₁ • a = a₂ • a
⊢ ((TensorProduct.mk A B A) 1) a₁ = ((TensorProduct.mk A B A) 1) a₂
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
I : Ideal R
inst✝⁸ : I.IsPrime
J : Ideal A
K : Ideal B
inst✝⁷ : J.IsPrime
inst✝⁶ : K.IsPrime
inst✝⁵ : J.LiesOver I
inst✝⁴ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝³ : IsLiesOverAlgebra I J
inst✝² : K.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime K)
inst✝ : IsLiesOverAlgebra I K
⊢ IsLocalHom (localRingHom I J (algebraMap R A) ⋯)

Tactic:
exact isLocalHom_localRingHom _ _ _ (J.over_def I)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
⊢ p ∈ (comap f ⊥).minimalPrimes

Tactic:
rwa [comap_bot_of_injective f hf]

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

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

Tactic:
· rw [← IsLocalization.under_le_under_iff q.primeCompl A,
      AtPrime.map_eq_maximalIdeal q A, AtPrime.under_maximalIdeal A q]
    apply hIq.2 hJ.1
    have := hJ.isPrime.ne_top
    rw [ne_eq, Ideal.comap_eq_top_iff, ← ne_eq, ← disjoint_under_iff q.primeCompl A J] at this
    exact Set.disjoint_compl_left_iff_subset.mp this

Goal state after:
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
hW : IsCompact W.carrier
⊢ ∃ κ, ∃ (_ : Finite κ), ∃ a, W = ⨆ k, U (a k)

Tactic:
obtain ⟨κ, a, heq⟩ := hU.exists_iSup_eq W
  obtain ⟨s, hs⟩ := hW.elim_finite_subcover _ (fun k : κ ↦ (U (a k)).2) (by simp [heq])
  use s, s.finite_toSet, a ∘ Subtype.val
  refine le_antisymm ?_ ?_
  · simpa [← SetLike.coe_subset_coe, Set.iUnion_subtype]
  · rw [heq, iSup_le_iff]
    intro i
    exact le_iSup_of_le _ le_rfl

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ (∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))) →
    ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)), 𝓝 x = Filter.comap Subtype.val (Filter.comap f (𝓝 ((f ∘ Subtype.val) x)))

Tactic:
intro H i x
    rw [Function.comp_apply, ← H, ← IsInducing.subtypeVal.nhds_eq_comap]

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : 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
⊢ f '' (f ⁻¹' U ∩ f ⁻¹' V) = U ∩ V

Tactic:
← Set.preimage_inter,

Goal state after:
α : 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
⊢ f '' f ⁻¹' (U ∩ V) = U ∩ V
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
x : X
hx : f x ∈ U
⊢ f x ∈ ⋃ i, f '' ↑↑i

Tactic:
obtain ⟨i, hi, hx⟩ := mem_sSup.mp <| by rwa [← heq]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
x : X
hx✝ : f x ∈ U
i : Opens X
hi : i ∈ Us
hx : x ∈ i
⊢ f x ∈ ⋃ i, f '' ↑↑i
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case refine_1
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen[inst✝] t
htcomp : IsCompact t
⊢ IsCompact (s ∩ t)

Tactic:
exact hs htcomp htopen

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
f : X → Y
hf : IsOpenEmbedding f
Z : IrreducibleCloseds X
⊢ coheight (map f ⋯ Z) = coheight ((orderIsoOfIsOpenEmbedding f hf) Z)

Tactic:
refine .symm (coheight_eq_of_strictMono Subtype.val (Subtype.strictMono_coe _) ?_ _)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
Z : IrreducibleCloseds X
⊢ ∀ (a : { x // x ∈ {V | (f ⁻¹' ↑V).Nonempty} }) (b : IrreducibleCloseds Y), ↑a < b → ∃ a', a < a' ∧ ↑a' = b
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
this : IsLocalHom (algebraMap (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
⊢ Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))

Tactic:
have : Module.FaithfullyFlat (Localization.AtPrime (P.under R)) (Localization.AtPrime P) :=
    Module.FaithfullyFlat.of_flat_of_isLocalHom

Goal state after:
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
this✝ : IsLocalHom (algebraMap (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
this : Module.FaithfullyFlat (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P)
⊢ Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
induction n with
  | zero => rw [pow_zero, map_one_eq_zero, zero_smul]
  | succ n ihn =>
    rcases eq_zero_or_pos n with (rfl | hpos)
    · simp
    · have : a * a ^ (n - 1) = a ^ n := by rw [← pow_succ', Nat.sub_add_cancel hpos]
      simp only [pow_succ', leibniz, ihn, smul_comm a n (_ : M), smul_smul a, add_smul, this,
        Nat.add_succ_sub_one, add_zero, one_nsmul]

Goal state after: