mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (LinearMap.rTensor M (l12.range.subtype ∘ₗ l12.rangeRestrict)) y = (LinearMap.rTensor M l12) y

Tactic:
LinearMap.subtype_comp_codRestrict

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 l12) y = (LinearMap.rTensor M l12) y
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

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

Tactic:
zeroLocus_radical,

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ zeroLocus ↑0 = Set.univ
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) * (R ∙ y) ≤ M

Tactic:
span_mul_span,

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
⊢ span R ({x} * {y}) ≤ M
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case hy
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral R ↑s

Tactic:
exact Algebra.IsIntegral.isIntegral (s : S)

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

Goal state before:
pp: case h.refine_1
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
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ (A ∙ x) * (A ∙ y) ≤ M

Tactic:
span_mul_span,

Goal state after:
case h.refine_1
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
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ span A ({x} * {y}) ≤ M
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 * (↑a).1 = (↑b).1 * (↑a).2

pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 + (↑a).1 = 1

pp: case refine_3
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 + (↑b).1 = 1

Tactic:
· rw [mul_comm, a.2.1, eq, b.2.1]

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 + (↑a).1 = 1

case refine_3
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 + (↑b).1 = 1
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsMaximal
⊢ Function.Surjective ⇑((algebraMap (R ⧸ I) I.ResidueField).comp (algebraMap R (R ⧸ I)))

Tactic:
exact I.bijective_algebraMap_quotient_residueField.surjective.comp Ideal.Quotient.mk_surjective

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a✝ b✝ : B
h : (mapToFractionRing K S B hS).rangeRestrict a✝ = (mapToFractionRing K S B hS).rangeRestrict b✝
a b : A
⊢ (algebraMap A B) a = (algebraMap A B) b ↔ (algebraMap A K) a = (algebraMap A K) b

Tactic:
exact ⟨fun h => congr_arg _ (IsLocalization.injective _ hS h),
        fun h => congr_arg _ (IsFractionRing.injective A K h)⟩

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ ↑a - ↑a * ↑a = 0

Tactic:
by rw [a.2, sub_self]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
⊢ ∃ p ∈ I.minimalPrimes, y ∉ p

Tactic:
by
      simpa [← Ideal.sInf_minimalPrimes] using hy

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
⊢ Finite (MaximalSpectrum R)

Tactic:
by
  replace surj := mapPiLocalization_bijective _ ⟨toPiLocalization_injective R, surj⟩
    |>.2.comp surj
  rw [← AlgHom.coe_toRingHom,
    ← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj
  exact finite_of_toPiLocalization_pi_surjective surj.of_comp

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ ∀ x ∈ closure s,
    ∀ y ∈ closure s,
      (∃ t, x = t.sup fun x ↦ ↑x.1 \ ↑x.2) →
        (∃ t, y = t.sup fun x ↦ ↑x.1 \ ↑x.2) → ∃ t, x ⊔ y = t.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
rintro _ - _ - ⟨t₁, rfl⟩ ⟨t₂, rfl⟩
    exact ⟨t₁ ∪ t₂, by rw [Finset.sup_union]⟩

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible ↑t
h₂ : s ⊓ z₂ = sSup S₂
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
refine ⟨S₁ ∪ S₂, hSf₁.union hSf₂, Set.union_subset_iff.2 ⟨hS₁, hS₂⟩, ?_⟩

Goal state after:
case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible ↑t
h₂ : s ⊓ z₂ = sSup S₂
⊢ s = sSup (S₁ ∪ S₂)
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
⊢ IsQuasiSeparated univ ↔ QuasiSeparatedSpace α

Tactic:
rw [quasiSeparatedSpace_iff]

Goal state after:
α : Type u_3
inst✝ : TopologicalSpace α
⊢ IsQuasiSeparated univ ↔
    ∀ (U V : Set α), IsOpen[inst✝] U → IsCompact U → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
⊢ SetLike.coe '' {U | IsCompact ↑U} = {U | IsOpen[inst✝¹] U ∧ IsCompact U}

Tactic:
ext s

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
s : Set X
⊢ s ∈ SetLike.coe '' {U | IsCompact ↑U} ↔ s ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
⊢ ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ K ⊆ W ∧ W ⊆ U

Tactic:
by
  refine hK.induction_on ⟨∅, by simp⟩ (fun s t hst ⟨W, Wc, Wo, hKW, hWU⟩ ↦ ?_) ?_ ?_
  · use W, Wc, Wo, subset_trans hst hKW, hWU
  · intro s t ⟨W₁, Wc₁, Wo₁, hKW₁, hWU₁⟩ ⟨W₂, Wc₂, Wo₂, hKW₂, hWU₂⟩
    exact ⟨W₁ ∪ W₂, Wc₁.union Wc₂, Wo₁.union Wo₂, Set.union_subset_union hKW₁ hKW₂,
      Set.union_subset hWU₁ hWU₂⟩
  · intro x hx
    obtain ⟨V, h, hxV, hVU⟩ :=
      PrespectralSpace.isTopologicalBasis.exists_subset_of_mem_open (hKU hx) hU
    exact ⟨V, mem_nhdsWithin.mpr ⟨V, h.1, hxV, Set.inter_subset_left⟩, V, h.2, h.1, subset_rfl, hVU⟩

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
⊢ IsLocallyConstructible (s ∪ t)

Tactic:
rintro x
  obtain ⟨U, hxU, hU, hsU⟩ := hs x
  obtain ⟨V, hxV, hV, htV⟩ := ht x
  refine ⟨U ∩ V, Filter.inter_mem hxU hxV, hU.inter hV, ?_⟩
  have : (U ∩ V) ↓∩ (s ∪ t) =
      inclusion inter_subset_left ⁻¹' (U ↓∩ s) ∪ inclusion inter_subset_right ⁻¹' (V ↓∩ t) := by
    ext; simp
  rw [this]
  exact .union (hsU.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)
    (htV.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)

Goal state after:
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
⊢ HasGoingDown R S

Tactic:
by
  apply of_comap_localRingHom_surjective
  intro P hP
  let := Localization.AtPrime.algebraOfLiesOver (P.under R) P
  have : IsLocalHom (algebraMap (Localization.AtPrime <| P.under R) (Localization.AtPrime P)) := by
    rw [RingHom.algebraMap_toAlgebra]
    exact Localization.isLocalHom_localRingHom (P.under R) P (algebraMap R S) Ideal.LiesOver.over
  have : Module.FaithfullyFlat (Localization.AtPrime (P.under R)) (Localization.AtPrime P) :=
    Module.FaithfullyFlat.of_flat_of_isLocalHom
  apply PrimeSpectrum.comap_surjective_of_faithfullyFlat

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 : T →+* R
hg : Function.Bijective ⇑g
⊢ (f.comp g).Flat ↔ f.Flat

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ .comp (.of_bijective hg) hf⟩

Goal state after:
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 : T →+* R
hg : Function.Bijective ⇑g
hf : (f.comp g).Flat
⊢ f.Flat
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ CommRingCat.of S ⟶ CommRingCat.of (T ⊗[S] A)

pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ IsPushout
    (CommRingCat.ofHom
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A)).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom) ?m.69

Tactic:
· exact CommRingCat.ofHom
      (RingHom.comp (Algebra.TensorProduct.includeLeft (S := R)).toRingHom (algebraMap S T))

Goal state after:
R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ IsPushout
    (CommRingCat.ofHom
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A)).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.includeLeft.comp (algebraMap S T)))
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : a.factorization p ≠ 0
⊢ (a.factorization ⊔ b.factorization) p ≠ 0

Tactic:
exact (lt_sup_iff.mpr <| .inl <| Nat.pos_of_ne_zero hp).ne'

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

Goal state before:
pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ p ^ (a.lcm b).factorization p ∣ p ^ b.factorization p

Tactic:
· rw [factorization_lcm ha hb]; apply pow_dvd_pow; exact sup_le (not_le.1 le).le le_rfl

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Surjective ⇑f
s : Set (PrimeSpectrum S)
x✝ : ∃ s_1, sᶜ = zeroLocus s_1
F : Set S
hF : sᶜ = zeroLocus F
⊢ zeroLocus F = sᶜ

Tactic:
hF

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Surjective ⇑f
s : Set (PrimeSpectrum S)
x✝ : ∃ s_1, sᶜ = zeroLocus s_1
F : Set S
hF : sᶜ = zeroLocus F
⊢ zeroLocus F = zeroLocus F
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
⊢ ∀ (a : α), orderOf a = Nat.card α ↔ Nat.card α ≤ orderOf a

Tactic:
intro g

Goal state after:
α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
g : α
⊢ orderOf g = Nat.card α ↔ Nat.card α ≤ orderOf g
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
⊢ (∀ (g : G), g ^ n = 1) ↔ ∀ (g : G), orderOf g ∣ n

Tactic:
orderOf_dvd_iff_pow_eq_one

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ ∀ b ∈ Finset.univ, orderOf b ∣ exponent G

Tactic:
intro g

Goal state after:
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
⊢ g ∈ Finset.univ → orderOf g ∣ exponent G
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
a : ↑(Set.range f)
⊢ IsLocalization.Away (f (e.symm a)) (Localization.Away ↑a)

Tactic:
by
      simp_rw [e, Equiv.apply_ofInjective_symm]; infer_instance

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

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ (∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)) →
    DenseRange (comap f)

Tactic:
intro H p
    obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le (J := p.asIdeal) bot_le
    exact ((le_iff_specializes ⟨q, hq.1.1⟩ p).mp hq').mem_closed isClosed_closure
      (subset_closure (H q hq))

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ ∀ (g : G), orderOf g ∣ p

Tactic:
intro g

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
g : G
⊢ orderOf g ∣ p
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_2
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
⊢ ∀ (g : G), orderOf g ∣ t.prod id

Tactic:
intro g

Goal state after:
case refine_2
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
g : G
⊢ orderOf g ∣ t.prod id
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝² : LeftCancelMonoid G
inst✝¹ : Finite G
inst✝ : Nontrivial G
⊢ 1 < exponent G

Tactic:
rw [Nat.one_lt_iff_ne_zero_and_ne_one]
  exact ⟨exponent_ne_zero_of_finite, mt exp_eq_one_iff.mp (not_subsingleton G)⟩

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
⊢ (∀ (g : G), ∃ k, g ^ p ^ k = 1) ↔ ∀ (g : G), ∃ k, orderOf g ∣ p ^ k

Tactic:
orderOf_dvd_iff_pow_eq_one

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ (∃ k, ∀ (g : G), orderOf g ∣ p ^ k) ↔ ∃ k, ∀ (g : G), g ^ p ^ k = 1

Tactic:
orderOf_dvd_iff_pow_eq_one

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
⊢ IsPGroup p ↥(Subgroup.comap ϕ H)

Tactic:
intro g

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
⊢ ∃ k, g ^ p ^ k = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = ⨆ g, orderOf g

Tactic:
rw [iSup]
  by_cases ExponentExists G
  case neg he =>
    rw [← exponent_eq_zero_iff] at he
    rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]
  case pos he =>
    rw [csSup_eq_of_forall_le_of_forall_lt_exists_gt (Set.range_nonempty _)]
    · simp_rw [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
      exact orderOf_le_exponent he
    intro x hx
    obtain ⟨g, hg⟩ := exists_orderOf_eq_exponent he
    rw [← hg] at hx
    simp_rw [Set.mem_range, exists_exists_eq_and]
    exact ⟨g, hx⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
h : ∀ (g : G), orderOf g ∣ 2
a b : G
⊢ Commute a b

Tactic:
orderOf_dvd_iff_pow_eq_one

Goal state after:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ Commute a b
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
h : (↑P).Normal
⊢ g • P = P

Tactic:
by
  simp only [smul_eq_iff_mem_normalizer, ← P.coe_coe, P.normalizer_eq_top, mem_top]

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) → vanishingIdeal s ∈ minimalPrimes R

Tactic:
rw [← vanishingIdeal_irreducibleComponents, ← vanishingIdeal_closure]
    exact Set.mem_image_of_mem _

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
⊢ IsSimpleGroup α

Tactic:
subst h
  have : Finite α := Nat.finite_of_card_ne_zero hp.1.ne_zero
  have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp hp.1.one_lt
  exact ⟨fun H _ => H.eq_bot_or_eq_top_of_prime_card⟩

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
⊢ ∃ n ∈ normalizer ↑P, g⁻¹ * x * g = n⁻¹ * x * n

Tactic:
by
  have h1 : P ≤ centralizer (zpowers x : Set G) := by rwa [le_centralizer_iff, zpowers_le]
  have h2 : ↑(g • P) ≤ centralizer (zpowers x : Set G) := by
    rw [le_centralizer_iff, zpowers_le]
    rintro - ⟨z, hz, rfl⟩
    specialize hy z hz
    rwa [← mul_assoc, ← eq_mul_inv_iff_mul_eq, mul_assoc, mul_assoc, mul_assoc, ← mul_assoc,
      eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc] at hy
  obtain ⟨h, hh⟩ :=
    exists_smul_eq (centralizer (zpowers x : Set G)) ((g • P).subtype h2) (P.subtype h1)
  simp_rw [smul_subtype, Subgroup.smul_def, smul_smul] at hh
  refine ⟨h * g, smul_eq_iff_mem_normalizer.mp (subtype_injective hh), ?_⟩
  rw [← mul_assoc, Commute.right_comm (h.prop x (mem_zpowers x)), mul_inv_rev, inv_mul_cancel_right]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
⊢ Nat.card (G ⧸ H) * Nat.card ↥H = s * p * Nat.card ↥H

Tactic:
← card_eq_card_quotient_mul_card_subgroup H,

Goal state after:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
⊢ Nat.card G = s * p * Nat.card ↥H