mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
r : R
hr : IsUnit r
s : Set R
⊢ zeroLocus (r • s) = zeroLocus s

Tactic:
by
  ext; simp [Set.subset_def, ← Set.image_smul, Ideal.unit_mul_mem_iff_mem _ hr]

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
⊢ (∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x) →
    Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)

Tactic:
refine fun H y ↦ Localization.ind (fun ⟨y, t, h⟩ ↦ ?_) y

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
⊢ ∃ a, (Localization.localRingHom (Ideal.comap f P) P f ⋯) a = Localization.mk (y, ⟨t, h⟩).1 (y, ⟨t, h⟩).2
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case tmul
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₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : (algebraMap R T) s ∉ J
e : c * (algebraMap R T) s * x₂ = c * (algebraMap R T) y
⊢ x₁ ⊗ₜ[R] ((algebraMap R T) s * c * x₂) = (y • x₁) ⊗ₜ[R] c

Tactic:
mul_comm _ c,

Goal state after:
case tmul
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₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : (algebraMap R T) s ∉ J
e : c * (algebraMap R T) s * x₂ = c * (algebraMap R T) y
⊢ x₁ ⊗ₜ[R] (c * (algebraMap R T) s * x₂) = (y • x₁) ⊗ₜ[R] c
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
⊢ ∃ I, ∃ (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)

Tactic:
let J : Ideal (Π i, R i) := -- `J := Π₀ i, R i` is an ideal in `Π i, R i`
  { __ := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom
    smul_mem' := by
      rintro r _ ⟨x, rfl⟩
      refine ⟨.mk x.support fun i ↦ r i * x i, funext fun i ↦ show dite _ _ _ = _ from ?_⟩
      simp_rw +instances [DFinsupp.coeFnAddMonoidHom]
      refine dite_eq_left_iff.mpr fun h ↦ ?_
      rw [DFinsupp.notMem_support_iff.mp h, mul_zero] }

Goal state after:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
⊢ ∃ I, ∃ (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case pos
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
j : ι
hj : i = j
⊢ x j = (x * e i) j

Tactic:
subst hj; simpa [e]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := { bot := { asIdeal := ⊥, isPrime := inst✝ }, bot_le := ⋯ }
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      (PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩ ≠ ⊥ → ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal.IsMaximal) ↔
    ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
forall_comm (α := _ ≠ ⊥),

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := { bot := { asIdeal := ⊥, isPrime := inst✝ }, bot_le := ⋯ }
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      (PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩ ≠ ⊥ → ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal.IsMaximal) ↔
    ∀ (I : Ideal R), I.IsPrime → I ≠ ⊥ → I.IsMaximal
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)

Tactic:
by
  refine ⟨fun hf ↦ fun i ↦ hf.comp (U i).isOpenEmbedding'.isOpenMap, fun hf ↦ ?_⟩
  intro V hV
  convert! isOpen_iUnion (fun i ↦ hf i _ <| isOpen_induced hV)
  simp_rw [Set.image_comp, Set.image_preimage_eq_inter_range, ← Set.image_iUnion,
    Subtype.range_coe_subtype, SetLike.setOfPred_mem_eq, hU.iUnion_inter]

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
tfae_2_to_3 : IsOpen[inst✝] (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)) →
    ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
tfae_4_to_5 :
  (∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s) →
    IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)
x✝ : IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)
H : IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s) := x✝
⊢ IsLocallyClosed s

Tactic:
convert!
      H.isLocallyClosed.image IsInducing.subtypeVal
        (by simpa using isClosed_closure.isLocallyClosed)
    simpa using subset_closure

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (↑(U i) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set ↑↑(U i)
hVx : V ∈ 𝓝 ⟨x, hi⟩
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (V ↓∩ ↑(U i) ↓∩ s)
⊢ MapsTo Subtype.val V ↑V

Tactic:
simp [MapsTo]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingDown R S
inst✝ : HasGoingDown S T
⊢ GeneralizingMap (PrimeSpectrum.comap ((algebraMap S T).comp (algebraMap R S)))

Tactic:
simp only [PrimeSpectrum.comap_comp]

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingDown R S
inst✝ : HasGoingDown S T
⊢ GeneralizingMap (PrimeSpectrum.comap (algebraMap R S) ∘ PrimeSpectrum.comap (algebraMap S T))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ closure {x} = zeroLocus ↑x.asIdeal

Tactic:
rw [← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_singleton]

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

Goal state before:
pp: case refine_4
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)
⊢ pushout.map (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S))
        (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
        (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) (CommRingCat.ofHom (algebraMap S T))
        (CommRingCat.ofHom (algebraMap S A)) (𝟙 (CommRingCat.of R)) ⋯ ⋯ ≫
      (pushout.congrHom ⋯ ⋯ ≪≫ ⋯.isoPushout.symm).hom =
    ⋯.isoPushout.symm.hom ≫
      CommRingCat.ofHom
        (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A)).toRingHom

pp: case refine_5
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)
⊢ pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ (Iso.refl (CommRingCat.of S)).hom =
    ⋯.isoPushout.symm.hom ≫ CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom

pp: case refine_6
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)
⊢ pushout.map (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
        (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) (CommRingCat.ofHom (algebraMap S T))
        (CommRingCat.ofHom (algebraMap S A)) (𝟙 (CommRingCat.of T)) (𝟙 (CommRingCat.of A))
        (CommRingCat.ofHom (algebraMap R S)) ⋯ ⋯ ≫
      ⋯.isoPushout.symm.hom =
    (pushout.congrHom ⋯ ⋯ ≪≫ ⋯.isoPushout.symm).hom ≫
      CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom

pp: case refine_7
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.ofHom (algebraMap S T) ≫
        pushout.inl (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A))) ≫
      ⋯.isoPushout.symm.hom =
    (Iso.refl (CommRingCat.of S)).hom ≫ CommRingCat.ofHom (Algebra.TensorProduct.includeLeft.comp (algebraMap S T))

Tactic:
all_goals ext <;> simp

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

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : Set S
⊢ zeroLocus (⇑(algebraMap R S) '' ↑(Ideal.comap (algebraMap R S) (Ideal.span s))) = zeroLocus s

Tactic:
← zeroLocus_span,

Goal state after:
case mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : Set S
⊢ zeroLocus ↑(Ideal.span (⇑(algebraMap R S) '' ↑(Ideal.comap (algebraMap R S) (Ideal.span s)))) = zeroLocus s
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : Monoid G
g : G
h : ¬ExponentExists G
⊢ g ^ exponent G = 1

Tactic:
· simp_rw [exponent, dif_neg h, pow_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ a ∈ H, zpowers a = H) ↔ ∃ g, zpowers g = H

Tactic:
exact exists_congr fun g ↦ and_iff_right_of_imp fun h ↦ h ▸ mem_zpowers g

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
⊢ (fun x ↦ comap (Pi.evalRingHom R i) x) '' ↑(basicOpen f) = ↑(basicOpen (Pi.single i f))

Tactic:
exact PrimeSpectrum.comap_evalRingHom_basicOpen _ _

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ orderOf (g ^ k) = p ^ t.succ

Tactic:
apply orderOf_eq_prime_pow

Goal state after:
case inr.hnot
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ ¬(g ^ k) ^ p ^ t = 1

case hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ (g ^ k) ^ p ^ (t + 1) = 1
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 ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
⊢ ∃ a, (toPiLocalization R) a = x

Tactic:
obtain ⟨r, eq, -⟩ := Localization.existsUnique_algebraMap_eq_of_span_eq_top _ span_eq
    (fun a ↦ algE a (x _)) fun a b ↦ by
      obtain rfl | ne := eq_or_ne a b; · rfl
      have nil : IsNilpotent (a * b : R) := (basicOpen_eq_bot_iff _).mp <| by
        simp_rw [basicOpen_mul, SetLike.ext'_iff, TopologicalSpace.Opens.coe_inf, hf]
        exact bot_unique (fun _ ⟨ha, hb⟩ ↦ ne <| e.symm.injective (ha.symm.trans hb))
      apply (IsLocalization.subsingleton (M := .powers (a * b : R)) nil).elim

Goal state after:
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 ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
r : R
eq : ∀ (a : ↑(Set.range f)), (algebraMap R (Localization.Away ↑a)) r = (algE a) (x (e.symm a))
⊢ ∃ a, (toPiLocalization R) a = x
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case inr
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup p G
hp : p ≠ 0
q : ℕ
hq : q ∈ (Nat.card G).primeFactors
hqp : Nat.Prime q
hqdvd : q ∣ Nat.card G
right✝ : Nat.card G ≠ 0
g : G
hg : orderOf g = q
k : ℕ
hk : orderOf g ∣ p ^ k
⊢ q ∈ p.primeFactors

Tactic:
exact Nat.mem_primeFactors.mpr ⟨hqp, hqp.dvd_of_dvd_pow <| hg ▸ hk, hp⟩

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
n₁ n₂ : ℕ
heq₂ : Nat.card ↥H₂ = p₂ ^ n₂
⊢ (p₁ ^ n₁).Coprime (Nat.card ↥H₂)

Tactic:
heq₂

Goal state after:
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
n₁ n₂ : ℕ
heq₂ : Nat.card ↥H₂ = p₂ ^ n₂
⊢ (p₁ ^ n₁).Coprime (p₂ ^ n₂)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
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.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : IsClosed (comap (mapRingHom f) '' zeroLocus {p})
⊢ 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})

Tactic:
← zeroLocus_span,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : IsClosed (comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p}))
⊢ 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
h : G
x✝ : h ∈ g • P
a : G
b : a ∈ ↑↑P
c : ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) a = h
⊢ g⁻¹ * ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) a * g ∈ ↑P

Tactic:
simpa [mul_assoc] using b

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal '' irreducibleComponents (PrimeSpectrum R) =
    irreducibleComponents (PrimeSpectrum R)

Tactic:
Set.EqOn.image_eq_self

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ irreducibleComponents (PrimeSpectrum R) = irreducibleComponents (PrimeSpectrum R)

R : Type u
inst✝ : CommSemiring R
⊢ Set.EqOn ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) id (irreducibleComponents (PrimeSpectrum R))
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_4
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
⊢ Nonempty (Additive G ≃+o ℤ) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr

Goal state after:
G : Type u_4
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
⊢ Nonempty (G ≃*o Multiplicative ℤ) ↔ Nonempty (G ≃*o Multiplicative ℤ)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (zmodAddEquivOfGenerator hg hn) ↑i = i • g

Tactic:
by
  change (ZMod.cast (i : ZMod n) : ℤ) • g = i • g
  rw [ZMod.coe_intCast, Int.emod_def, eq_comm, ← sub_eq_zero, sub_eq_add_neg, ← sub_zsmul,
    Int.sub_sub_self, mul_zsmul', natCast_zsmul, ← hn, card_nsmul_eq_zero', zsmul_zero]

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso
    ((snoc s₁ x₁ hsat₁).toFun
        (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)).castSucc,
      (snoc s₁ x₁ hsat₁).toFun (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)).succ)
    ((snoc s₂ x₂ hsat₂).toFun
        (e (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length))).castSucc,
      (snoc s₂ x₂ hsat₂).toFun
        (e (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length))).succ)

Tactic:
change Iso ((snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).castSucc,
        (snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).succ)
      ((snoc s₂ x₂ hsat₂).toFun (e (Fin.last s₁.length)).castSucc,
        (snoc s₂ x₂ hsat₂).toFun (e (Fin.last s₁.length)).succ)
    rw [he_last]
    simpa [apply_last] using hlast

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

Goal state before:
pp: R : Type u_2
inst✝⁷ : Ring R
M : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : IsSemisimpleModule R M
P : Type u_6
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
g : P →ₗ[R] N
⊢ ∃ h, f ∘ₗ h = g

Tactic:
have ⟨m, compl⟩ := exists_isCompl (LinearMap.ker f)
  let e := (Submodule.quotientEquivOfIsCompl _ m compl).symm ≪≫ₗ f.quotKerEquivOfSurjective hf
  refine ⟨Submodule.subtype _ ∘ₗ e.symm.toLinearMap ∘ₗ g, LinearMap.ext fun x ↦ ?_⟩
  obtain ⟨z, eq⟩ := e.surjective (g x)
  simp only [LinearMap.comp_apply, ← eq, LinearEquiv.coe_coe, e.symm_apply_apply]
  simp [e]

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

Goal state before:
pp: M : Type u_4
inst✝³ : AddCommGroup M
R : Type u_6
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ ⊤.annihilator.IsRadical

Tactic:
← sSup_simples_eq_top,

Goal state after:
M : Type u_4
inst✝³ : AddCommGroup M
R : Type u_6
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ (sSup {m | IsSimpleModule R ↥m}).annihilator.IsRadical
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
q : Submodule R[X] (AEval R M a)
⊢ (fun p ↦
        let __AddSubmonoid := AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid;
        { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
      ((fun q ↦ ⟨(Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q), ⋯⟩) q) =
    q

Tactic:
by ext; aesop

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
i : ℕ
⊢ (a✝ * b✝).coeff i ∈ I ^ i

Tactic:
by
    rw [coeff_mul]
    apply Ideal.sum_mem
    rintro ⟨j, k⟩ e
    rw [← Finset.mem_antidiagonal.mp e, pow_add]
    exact Ideal.mul_mem_mul (hf j) (hg k)

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : ↑B
⊢ (ConcreteCategory.hom (map fac)) (d b) = d ((ConcreteCategory.hom g') b)

Tactic:
algebraize [f.hom, f'.hom, g.hom, g'.hom, f'.hom.comp g.hom]
  have := IsScalarTower.of_algebraMap_eq' (congrArg Hom.hom fac)
  exact _root_.KaehlerDifferential.map_D A A' B B' b

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.cotangentToQuotientSquare.range = Submodule.restrictScalars R I.cotangentIdeal

Tactic:
trans LinearMap.range (I.cotangentToQuotientSquare.comp I.toCotangent)

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.cotangentToQuotientSquare.range = (I.cotangentToQuotientSquare ∘ₗ I.toCotangent).range

R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ (I.cotangentToQuotientSquare ∘ₗ I.toCotangent).range = Submodule.restrictScalars R I.cotangentIdeal