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

Goal state before:
pp: case refine_2
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
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ 1 ⊗ₜ[R] (r • t) * (algebraMap S (S ⊗[R] T)) ((algebraMap R S) r) * x = 1 ⊗ₜ[R] (r • t) * (algebraMap S (S ⊗[R] T)) a

Tactic:
simp only [tmul_smul, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self,
      RingHomCompTriple.comp_apply, Algebra.smul_mul_assoc, Algebra.TensorProduct.tmul_mul_tmul,
      one_mul, mul_one, id_apply, ← e]
    rw [Algebra.algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc]

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

Goal state before:
pp: 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 = b

Tactic:
refine Subtype.ext <| Prod.ext_iff.mpr ⟨eq_of_mul_eq_add_eq_one a.1.2 ?_ ?_ ?_, eq⟩
  · rw [mul_comm, a.2.1, eq, b.2.1]
  · rw [add_comm, a.2.2]
  · rw [add_comm, eq, b.2.2]

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

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

Tactic:
rw [← hab, mul_comm, hba]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (∀ (b : { I // I.IsPrime }), IsMax ((PrimeSpectrum.equivSubtype R).symm b)) ↔ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

Tactic:
Subtype.forall,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
⊢ (∀ (a : Ideal R) (b : a.IsPrime), IsMax ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩)) ↔
    ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (∀ (b : { I // I.IsPrime }),
      IsMin ((PrimeSpectrum.equivSubtype R).symm b) ∨ IsMax ((PrimeSpectrum.equivSubtype R).symm b)) ↔
    ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal

Tactic:
Subtype.forall,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      IsMin ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩) ∨ IsMax ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩)) ↔
    ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal
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 := ⋯ }
⊢ (∀ (b : { I // I.IsPrime }),
      (PrimeSpectrum.equivSubtype R).symm b ≠ ⊥ → IsMax ((PrimeSpectrum.equivSubtype R).symm b)) ↔
    ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
Subtype.forall,

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⟩ ≠ ⊥ → IsMax ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩)) ↔
    ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
⊢ Function.Bijective (sigmaToPi R)

Tactic:
refine ⟨sigmaToPi_injective R, ?_⟩
  intro q
  obtain ⟨i, q, rfl⟩ := exists_comap_evalRingHom_eq q
  exact ⟨⟨i, q⟩, rfl⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hba : ↑b * ↑a = ↑b
⊢ ↑a = ↑b

Tactic:
rw [← hab, mul_comm, hba]

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 = 0

Tactic:
sub_self

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ 0 = 0
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
sub_self

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

Goal state before:
pp: case mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : x ∉ range ⇑(algebraMap R K)
hlocal : ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
⊢ False

Tactic:
let denom : Ideal R := (1 : Submodule R K).comap (LinearMap.toSpanSingleton R K x)

Goal state after:
case mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : x ∉ range ⇑(algebraMap R K)
hlocal : ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K x) 1
⊢ False
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : max.IsMaximal
n d : R
hd : d ∈ { asIdeal := max, isMaximal := hmax }.asIdeal.primeCompl
hrange : (algebraMap R K) n * ((algebraMap R K) d)⁻¹ ∉ range ⇑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    (algebraMap R K) n * ((algebraMap R K) d)⁻¹ ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K ((algebraMap R K) n * ((algebraMap R K) d)⁻¹)) 1
hdenom : 1 ∉ denom
hle : denom ≤ max
⊢ (LinearMap.toSpanSingleton R K 1) n = (LinearMap.toSpanSingleton R K ((algebraMap R K) n * ((algebraMap R K) d)⁻¹)) d

Tactic:
simp [Algebra.smul_def, mul_left_comm, mul_inv_cancel₀ <|
      (map_ne_zero_iff _ <| IsFractionRing.injective R K).mpr fun h ↦ hd (h ▸ max.zero_mem :)]

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (a : α), a ≤ top

Tactic:
by intros; simp +instances [eq_le, eq_top]

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

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
hU : IsOpenCover U
h : ∀ (i : ι), PreirreducibleSpace ↥(U i)
h' : ∀ (i : ι), IsPreirreducible (U i).carrier
⊢ univ ⊆ ⋃ i, ↑(U i)

Tactic:
by simpa using hU.iSup_set_eq_univ

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a ⇨ b ∈ L

Tactic:
rw [himp_eq]; exact L.supClosed hb (compl_mem ha)

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:
by
    convert!
      H.isLocallyClosed.image IsInducing.subtypeVal
        (by simpa using isClosed_closure.isLocallyClosed)
    simpa using subset_closure

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

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Closeds α
t : Set α
ht : IsAtom t
⊢ ↑(Closeds.closure t) = t

Tactic:
obtain ⟨x, rfl⟩ := Set.isAtom_iff.1 ht

Goal state after:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Closeds α
x : α
ht : IsAtom {x}
⊢ ↑(Closeds.closure {x}) = {x}
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a = ∅
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)

Tactic:
simp only [ha, Set.sInter_empty, Set.univ_inter]

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a = ∅
⊢ IsCompact (⋂₀ b)
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : LE P
I : Ideal P
p : P
notMem : p ∉ I
hp : ↑I = univ
⊢ False

Tactic:
by
    have := mem_univ p
    rw [← hp] at this
    exact notMem this

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst✝¹] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)
h : IsRetrocompact (f '' U ∪ (range f)ᶜ)
⊢ IsConstructible (f '' U)

Tactic:
simpa [union_inter_distrib_right, inter_eq_left.2 (image_subset_range ..)]
        using (h.isConstructible hfU).sdiff (hfcomp.isConstructible hf.isClosed_range.isOpen_compl)

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

Goal state before:
pp: R S T : Type u_3
x✝⁵ : CommRing R
x✝⁴ : CommRing S
x✝³ : CommRing T
x✝² : Algebra R S
x✝¹ : Algebra R T
x✝ : (algebraMap R T).FaithfullyFlat
⊢ (algebraMap S (TensorProduct R S T)).FaithfullyFlat

Tactic:
rw [faithfullyFlat_algebraMap_iff] at *

Goal state after:
R S T : Type u_3
x✝⁵ : CommRing R
x✝⁴ : CommRing S
x✝³ : CommRing T
x✝² : Algebra R S
x✝¹ : Algebra R T
x✝ : Module.FaithfullyFlat R T
⊢ Module.FaithfullyFlat S (TensorProduct R S T)
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime✝ } =
    { asIdeal := pl, isPrime := ⋯ }
⊢ Ideal.under S Pl ≤ Q

Tactic:
exact (IsLocalization.AtPrime.orderIsoOfPrime _ Q ⟨Pl, inferInstance⟩).2.2

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Module.Flat R S ↔ Module.Flat R S

Tactic:
toAlgebra_algebraMap

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Module.Flat R S ↔ Module.Flat R S
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Flat
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Module.Flat R S
⊢ GeneralizingMap (comap f)

Tactic:
change GeneralizingMap (comap (algebraMap R S))

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Flat
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Module.Flat R S
⊢ GeneralizingMap (comap (algebraMap R S))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s} = {P | P.IsPrime}

Tactic:
by
  refine (subset_antisymm ?_ ?_).trans vanishingIdeal_isIrreducible
  · exact Set.image_mono fun _ ↦ And.right
  rintro _ ⟨s, hs, rfl⟩
  exact ⟨closure s, ⟨isClosed_closure, hs.closure⟩, vanishingIdeal_closure s⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ IrreducibleSpace (PrimeSpectrum R) ↔ (nilradical R).IsPrime

Tactic:
simp [irreducibleSpace_def, isIrreducible_iff_vanishingIdeal_isPrime]

Goal state after:
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ ⟨a, ⋯⟩ ^ (↑k).cast • ⟨b, ⋯⟩ = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩

Tactic:
ZMod.coe_intCast

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ ⟨a, ⋯⟩ ^ (k % ↑(minimalPeriod (fun x ↦ a • x) b)) • ⟨b, ⋯⟩ = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x ↦ h ^ x) m = σ h
n : ℤ
⊢ σ h ^ n = (fun x ↦ h ^ x) n ^ m

Tactic:
← hm,

Goal state after:
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x ↦ h ^ x) m = σ h
n : ℤ
⊢ (fun x ↦ h ^ x) m ^ n = (fun x ↦ h ^ x) n ^ m
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ (↑k).cast • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩ = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩

Tactic:
ZMod.coe_intCast

Goal state after:
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ (k % ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩ = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

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

pp: case inr
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h✝ : Nat.card α ∣ p
h : Nat.card α = p
⊢ IsCyclic α

Tactic:
· exact @isCyclic_of_subsingleton α _ (Nat.card_eq_one_iff_unique.mp h).1

Goal state after:
case inr
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h✝ : Nat.card α ∣ p
h : Nat.card α = p
⊢ IsCyclic α
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}
r : R
eq : ∀ (a : ↑(Set.range f)), (algebraMap R (Localization.Away ↑a)) r = (algE a) (x (e.symm a))
I : PrimeSpectrum R
this : (algebraMap R (Localization.AtPrime (e.symm (e I)).asIdeal)) r = x (e.symm (e I))
⊢ (toPiLocalization R) r I = x I

Tactic:
e.symm_apply_apply

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))
I : PrimeSpectrum R
this : (algebraMap R (Localization.AtPrime I.asIdeal)) r = x I
⊢ (toPiLocalization R) r I = x I
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
⊢ exponent G ∣ p

Tactic:
exponent_dvd

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
⊢ exponent G ∣ t.prod id

Tactic:
exponent_dvd

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
⊢ x = y

Tactic:
by_contra! ne
  wlog ne' : x * y ≠ x generalizing x y
  · apply this y hy x hx eq.symm ne.symm
    rwa [mul_comm, of_not_not ne']
  have : x ∉ Ideal.span {y} := fun mem ↦ ne' <| by
    obtain ⟨r, rfl⟩ := Ideal.mem_span_singleton'.mp mem
    rw [mul_assoc, hy]
  have ⟨p, prime, le, notMem⟩ := Ideal.exists_le_prime_notMem_of_isIdempotentElem _ x hx this
  exact ne_of_mem_of_not_mem' (a := ⟨p, prime⟩) notMem
    (not_not.mpr <| p.span_singleton_le_iff_mem.mp le) eq

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

Goal state before:
pp: case inr
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
this✝ : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
this : I ^ n ⊔ J ^ n = ⊤
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

Tactic:
rw [Ideal.eq_top_iff_one, Submodule.mem_sup] at this

Goal state after:
case inr
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
this✝ : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
this : ∃ y ∈ I ^ n, ∃ z ∈ J ^ n, y + z = 1
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
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
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
h : b.coeff 0 = 1
this : b.natTrailingDegree = 0
⊢ b.trailingCoeff = 1

Tactic:
trailingCoeff,

Goal state after:
case refine_1
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
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
h : b.coeff 0 = 1
this : b.natTrailingDegree = 0
⊢ b.coeff b.natTrailingDegree = 1
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
⊢ IsMulTorsionFree G ↔ torsion G = ⊥

Tactic:
rw [isMulTorsionFree_iff_not_isOfFinOrder, eq_bot_iff, SetLike.le_def]
  simp [not_imp_not, CommGroup.mem_torsion]

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝² : CommGroup M
inst✝¹ : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card N)
inst✝ : IsCyclic ↥f.ker
hN : IsCyclic ↥f.range
hf : Function.Surjective ⇑f
⊢ IsCyclic M

Tactic:
← Subgroup.card_top (G := N),

Goal state after:
M : Type u_4
N : Type u_5
inst✝² : CommGroup M
inst✝¹ : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥⊤)
inst✝ : IsCyclic ↥f.ker
hN : IsCyclic ↥f.range
hf : Function.Surjective ⇑f
⊢ IsCyclic M
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_2
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
i : Fin (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc.castSucc, (snoc s₁ x₁ hsat₁).toFun i.castSucc.succ)
    ((snoc s₂ x₂ hsat₂).toFun (e i.castSucc).castSucc, (snoc s₂ x₂ hsat₂).toFun (e i.castSucc).succ)

Tactic:
change Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc.castSucc,
        (snoc s₁ x₁ hsat₁).toFun i.castSucc.succ)
      ((snoc s₂ x₂ hsat₂).toFun (e i.castSucc).castSucc,
        (snoc s₂ x₂ hsat₂).toFun (e i.castSucc).succ)

Goal state after:
case refine_2
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
i : Fin (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc.castSucc, (snoc s₁ x₁ hsat₁).toFun i.castSucc.succ)
    ((snoc s₂ x₂ hsat₂).toFun (e i.castSucc).castSucc, (snoc s₂ x₂ hsat₂).toFun (e i.castSucc).succ)