mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ 1 * ↑I ≤ span R (↑T * ↑T') * ↑I

Tactic:
one_le.2 one_mem

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ span R (↑T * ↑T') * ↑I ≤ span R (↑T * ↑T') * ↑I
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
⊢ ↑(toENat p.spanRank).toNat = p.spanRank

Tactic:
toNat_toENat,

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
⊢ ↑(toNat p.spanRank) = p.spanRank
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
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
⊢ eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace

Tactic:
← Matrix.det_reindexLinearEquiv_self R[X] (Fintype.equivFin n)

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
⊢ eval 0
      (derivative ((reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n)) (1 + X • M.map ⇑C)).det) =
    M.trace
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (hasseDeriv k) f = f.sum fun i r ↦ (monomial (i - k)) (↑(i.choose k) * r)

Tactic:
dsimp [hasseDeriv]

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (lsum fun i ↦ monomial (i - k) ∘ₗ DistribSMul.toLinearMap R R (i.choose k)) f =
    f.sum fun i r ↦ (monomial (i - k)) (↑(i.choose k) * r)
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
⊢ ((hasseDeriv k) ((monomial n) r)).coeff i = ((monomial (n - k)) (↑(n.choose k) * r)).coeff i

Tactic:
simp only [hasseDeriv_coeff, coeff_monomial]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.integralNormalization.degree = p.degree

Tactic:
by
  nontriviality R
  by_cases hp : p = 0; · simp [hp]
  rw [degree_eq_natDegree hp]
  refine degree_eq_of_le_of_coeff_ne_zero ?_ (by simp [integralNormalization_coeff_natDegree, *])
  exact (Finset.sup_le fun i h =>
      WithBot.coe_le_coe.2 <| le_natDegree_of_mem_supp i <| support_integralNormalization_subset h)

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
⊢ ((Multiset.map (fun x ↦ X + C x) m).prod.scaleRoots r).Splits

Tactic:
induction m using Multiset.induction_on with
    | empty => simp
    | cons a s IH =>
      rw [Multiset.map_cons, Multiset.prod_cons, mul_scaleRoots', X_add_C_scaleRoots]
      · exact .mul (.X_add_C _) IH
      · simp only [leadingCoeff_X_add_C, one_mul, ne_eq, leadingCoeff_eq_zero]
        exact (monic_multiset_prod_of_monic _ _ fun a _ ↦ monic_X_add_C _).ne_zero

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

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

Tactic:
obtain ⟨b, hb₁, hb₂⟩ := integerNormalization_spec M p

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
b : R
hb₁ : b ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = b • p
⊢ ∃ b, Polynomial.map (algebraMap R S) (integerNormalization M p) = ↑b • p
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case mp.refine_1
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
p : A[X]
hp : p ≠ 0
px : (aeval x) p = 0
h : Polynomial.map (algebraMap A K) p = 0
i : ℕ
⊢ p.coeff i = coeff 0 i

Tactic:
have : algebraMap A K (p.coeff i) = 0 :=
        _root_.trans (Polynomial.coeff_map _ _).symm (by simp [h])

Goal state after:
case mp.refine_1
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
p : A[X]
hp : p ≠ 0
px : (aeval x) p = 0
h : Polynomial.map (algebraMap A K) p = 0
i : ℕ
this : (algebraMap A K) (p.coeff i) = 0
⊢ p.coeff i = coeff 0 i
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hg₀ : g ≠ 0
hg : g.Splits
⊢ (f * g).Splits ↔ f.Splits

Tactic:
simp [splits_mul', *]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hf₀ : f ≠ 0
hg : f.Splits
⊢ (f * g).Splits ↔ g.Splits

Tactic:
simp [splits_mul', *]

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
⊢ S[(Ideal.Quotient.mkₐ S I) X] = ⊤

Tactic:
ext g

Goal state after:
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ S[(Ideal.Quotient.mkₐ S I) X] ↔ g ∈ ⊤
Module: Mathlib.Algebra.Polynomial.Splits

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

Tactic:
rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← g.coe_toRingHom,
    ← hf.roots_map, map_map, g.comp_algebraMap, ← rootSet]

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
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)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
⊢ False

Tactic:
have eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0 := fun m ↦
    ex.apply_apply_eq_zero (n1 ⊗ₜ[R] m)

Goal state after:
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)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
⊢ False
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: 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 = ⊤
⊢ ∀ z ∉ M, M < M + R ∙ z

Tactic:
intro z

Goal state after:
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 = ⊤
z : R
⊢ z ∉ M → M < M + R ∙ z
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

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

Tactic:
intro z

Goal state after:
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
z : A
⊢ z ∉ M → M < M + A ∙ z
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
⊢ ∀ {m₂ : A}, (∀ (a : B), a₁ • a = m₂ • a) → a₁ = m₂

Tactic:
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
⊢ (∀ (a : B), a₁ • a = a₂ • a) → a₁ = 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
inst✝⁵ : Algebra.EssFiniteType R A
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal A
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ Algebra.EssFiniteType p.ResidueField q.ResidueField

Tactic:
have : Algebra.EssFiniteType R q.ResidueField := .comp _ A _

Goal state after:
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
inst✝⁵ : Algebra.EssFiniteType R A
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal A
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : Algebra.EssFiniteType R q.ResidueField
⊢ Algebra.EssFiniteType p.ResidueField q.ResidueField
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ x ∈ p.asIdeal

Tactic:
rw [← sub_sub_cancel x' x]

Goal state after:
case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ x' - (x' - x) ∈ p.asIdeal
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
by simp_rw [mul_sub, mul_one, a.2.eq, sub_self]

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
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
⊢ ∃ p' ∈ I.minimalPrimes, comap f p' = p

Tactic:
obtain ⟨p', h₁, h₂, h₃⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f p H
  obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le h₂
  refine ⟨q, hq, Eq.symm ?_⟩
  have := hq.isPrime
  have := (Ideal.comap_mono hq').trans_eq h₃
  exact (H.2 ⟨inferInstance, Ideal.comap_mono hq.le⟩ this).antisymm this

Goal state after:
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 : α), le a a

Tactic:
intros; simp [eq_le]

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
⊢ ⊤ ≤ ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i)

Tactic:
simpa [Set.range_subset_iff, SetLike.le_def] using hU

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
hs : IsClosed[inst✝¹] s
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsClosed[inst✝¹] t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ s = ⋃₀ S

Tactic:
by
  lift s to Closeds α using hs
  rcases NoetherianSpace.exists_finite_set_closeds_irreducible s with ⟨S, hSf, hS, rfl⟩
  refine ⟨(↑) '' S, hSf.image _, Set.forall_mem_image.2 fun S _ ↦ S.2, Set.forall_mem_image.2 hS,
    ?_⟩
  lift S to Finset (Closeds α) using hSf
  simp [← Finset.sup_id_eq_sSup, Closeds.coe_finset_sup]

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsOpen[inst✝] s
⊢ IsQuasiSeparated s ↔ QuasiSeparatedSpace ↑s

Tactic:
rw [← isQuasiSeparated_univ_iff]
  convert! (hs.isOpenEmbedding_subtypeVal.isQuasiSeparated_iff (s := Set.univ)).symm
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s : Finset ι
f : ι → Compacts α
⊢ ↑(s.sup f) = s.sup fun i ↦ ↑(f i)

Tactic:
refine Finset.cons_induction_on s rfl fun a s _ h => ?_

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : a ∉ s
h : ↑(s.sup f) = s.sup fun i ↦ ↑(f i)
⊢ ↑((Finset.cons a s x✝).sup f) = (Finset.cons a s x✝).sup fun i ↦ ↑(f i)
Module: Mathlib.Topology.Sober

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

Tactic:
show _ = _ from hx

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst✝¹] (T ∩ range f))
hxT : f y ∈ T
⊢ f ⁻¹' closure[inst✝¹] (T ∩ range f) = f ⁻¹' T
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑W
hV : IsClosed V
⊢ IsClosed (Subtype.val ⁻¹' (W ∩ V))

Tactic:
Subtype.preimage_coe_self_inter W V

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑W
hV : IsClosed V
⊢ IsClosed (Subtype.val ⁻¹' V)
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: 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) ⋯
⊢ (f x - (algebraMap A B) x) * (f y - (algebraMap A B) y) = 0

Tactic:
rw [← Ideal.mem_bot, ← hI, pow_two]

Goal state after:
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) ⋯
⊢ (f x - (algebraMap A B) x) * (f y - (algebraMap A B) y) ∈ I * I
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: 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
hI✝ : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
x y : A
⊢ ↑(f x) * ↑(f y) = 0

Tactic:
rw [← Ideal.mem_bot, ← hI, pow_two]

Goal state after:
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
hI✝ : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
x y : A
⊢ ↑(f x) * ↑(f y) ∈ I * I
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Flat
⊢ (ulift.{u₁, u₂, u_1, u_2} f).Flat

Tactic:
· exact .comp (.comp (.of_bijective <| Equiv.bijective _) hf)
      (.of_bijective <| Equiv.bijective _)

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

Goal state before:
pp: case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1

Tactic:
· intros; rw [pow_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R),
      x ⊓ y ≤ vanishingIdeal (zeroLocus ↑I) → x ≤ vanishingIdeal (zeroLocus ↑I) ∨ y ≤ vanishingIdeal (zeroLocus ↑I)) ↔
    ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
vanishingIdeal_zeroLocus_eq_radical,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I.radical → x ≤ I.radical ∨ y ≤ I.radical) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
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
r : R
⊢ D ((algebraMap R A) r) = 0

Tactic:
by
  rw [← mul_one r, map_mul, map_one, ← smul_def, map_smul, map_one_eq_zero, smul_zero]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.mp
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
⊢ exponent G ∣ n → ∀ (g : G), g ^ n = 1

Tactic:
intro h g

Goal state after:
case inr.mp
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
h : exponent G ∣ n
g : G
⊢ g ^ n = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ¬∃ x ∈ H, x ≠ 1
x : α
h : x ∈ H
⊢ x ∈ ⊥

Tactic:
by simp at *; tauto

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃x_1 y : PrimeSpectrum R⦄, x_1 ⤳ y → x_1 ∈ {x} → y ∈ {x}) ↔ IsMax x

Tactic:
← le_iff_specializes,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃x_1 y : PrimeSpectrum R⦄, x_1 ≤ y → x_1 ∈ {x} → y ∈ {x}) ↔ IsMax x
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃x_1 y : PrimeSpectrum R⦄, y ⤳ x_1 → x_1 ∈ {x} → y ∈ {x}) ↔ IsMin x

Tactic:
← le_iff_specializes,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃x_1 y : PrimeSpectrum R⦄, y ≤ x_1 → x_1 ∈ {x} → y ∈ {x}) ↔ IsMin x
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite : (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
this : exponent G ∣ t.prod id
⊢ exponent G ≠ 0

Tactic:
by
      intro h
      rw [h, zero_dvd_iff] at this
      exact htpos.ne' this

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
⊢ I * J ≤ nilradical R

Tactic:
refine Ideal.radical_le_radical_iff.mp (le_of_eq ?_)

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
⊢ (I * J).radical = Ideal.radical 0
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsClopen s ↔ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}

Tactic:
rw [isClopen_iff_mul_add, exists_comm]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ b a, a * b = 0 ∧ a + b = 1 ∧ s = ↑(basicOpen a)) ↔ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsAddTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ n • f = 0

Tactic:
simp only [← Nat.cast_smul_eq_nsmul R _ f, ← nsmul_one, hn, zero_smul]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ IsPGroup p ↥↑P

Tactic:
exact P.2

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
⊢ Group.rank (G ⧸ torsion G) = 0 ↔ IsMulTorsion G

Tactic:
Group.rank_eq_zero_iff,

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
⊢ Subsingleton (G ⧸ torsion G) ↔ IsMulTorsion G
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : f.ker = ⊤
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic ↥⊤

Tactic:
← h

Goal state after:
case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : f.ker = ⊤
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic ↥f.ker