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

Goal state before:
pp: case left
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Function.Injective (primeSpectrumProdOfSum R S)

Tactic:
rintro (⟨I, hI⟩ | ⟨J, hJ⟩) (⟨I', hI'⟩ | ⟨J', hJ'⟩) h <;>
          simp only [mk.injEq, Ideal.prod_inj, primeSpectrumProdOfSum] at h

Goal state after:
case left.inl.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
hI : I.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h : I = I' ∧ True
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inl { asIdeal := I', isPrime := hI' }

case left.inl.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
hI : I.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : I = ⊤ ∧ ⊤ = J'
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inr { asIdeal := J', isPrime := hJ' }

case left.inr.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h : ⊤ = I' ∧ J = ⊤
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inl { asIdeal := I', isPrime := hI' }

case left.inr.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : True ∧ J = J'
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inr { asIdeal := J', isPrime := hJ' }
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
N : Type (max u_1 u_3)
x✝³ : AddCommGroup N
x✝² : Module R N
N' : Type (max u_1 u_3)
x✝¹ : AddCommGroup N'
x✝ : Module R N'
f : N →ₗ[R] N'
aux : lTensor M f = 0
⊢ f = 0

Tactic:
zero_iff_lTensor_zero (R := R) (M := S) f,

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
N : Type (max u_1 u_3)
x✝³ : AddCommGroup N
x✝² : Module R N
N' : Type (max u_1 u_3)
x✝¹ : AddCommGroup N'
x✝ : Module R N'
f : N →ₗ[R] N'
aux : lTensor M f = 0
⊢ lTensor S f = 0
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 ι
p : PrimeSpectrum ((i : ι) → R i)
⊢ ∃ i q, comap (Pi.evalRingHom R i) q = p

Tactic:
cases nonempty_fintype ι
  let e (i) : Π i, R i := Function.update 1 i 0
  have H : ∏ i, e i = 0 := by
    ext j
    rw [Finset.prod_apply, Pi.zero_apply, Finset.prod_eq_zero (Finset.mem_univ j)]
    simp [e]
  obtain ⟨i, hi⟩ : ∃ i, e i ∈ p.asIdeal := by
    simpa [← H, Ideal.IsPrime.prod_mem_iff] using p.asIdeal.zero_mem
  let h₁ : Function.Surjective (Pi.evalRingHom R i) := RingHomSurjective.is_surjective
  have h₂ : RingHom.ker (Pi.evalRingHom R i) ≤ p.asIdeal := by
    intro x hx
    convert! p.asIdeal.mul_mem_left x hi
    ext j
    by_cases hj : i = j
    · subst hj; simpa [e]
    · simp [e, Function.update_of_ne (.symm hj)]
  have : (p.asIdeal.map (Pi.evalRingHom R i)).comap (Pi.evalRingHom R i) = p.asIdeal := by
    rwa [Ideal.comap_map_of_surjective _ h₁, sup_eq_left]
  exact ⟨i, ⟨_, Ideal.map_isPrime_of_surjective h₁ h₂⟩, PrimeSpectrum.ext this⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : NoZeroDivisors R
inst✝¹ : Ring.KrullDimLE 1 R
inst✝ : Algebra R S
P : Ideal S
p : R
hP : P ≠ ⊤
hp : Prime p
⊢ P.LiesOver (span {p}) ↔ (algebraMap R S) p ∈ P

Tactic:
have hP : P.under R ≠ ⊤ := Ideal.comap_ne_top _ hP

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : NoZeroDivisors R
inst✝¹ : Ring.KrullDimLE 1 R
inst✝ : Algebra R S
P : Ideal S
p : R
hP✝ : P ≠ ⊤
hp : Prime p
hP : under R P ≠ ⊤
⊢ P.LiesOver (span {p}) ↔ (algebraMap R S) p ∈ P
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:
← 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.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✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
S : Subalgebra A K
z : K
⊢ ∃ x y, z = (algebraMap (↥S) K) x / (algebraMap (↥S) K) y

Tactic:
rcases IsFractionRing.div_surjective A z with ⟨x, y, _, eq⟩

Goal state after:
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S✝ : Submonoid A
hS : S✝ ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
S : Subalgebra A K
z : K
x y : A
left✝ : y ∈ A⁰
eq : (algebraMap A K) x / (algebraMap A K) y = z
⊢ ∃ x y, z = (algebraMap (↥S) K) x / (algebraMap (↥S) K) y
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

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

Tactic:
have H : ∃ m, x ^ m * y ^ n ∈ I := ⟨n, mul_pow x y n ▸ hx⟩

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
⊢ ∃ y ∉ I, x * y ∈ I
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
⊢ I.asIdeal.IsMaximal

Tactic:
by_contra h

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
⊢ False
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
x✝ : x ∈ ⊤
i : ι
hxi : x ∈ U i
V : Opens X
hV : V ∈ S
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(U i)
⊢ ∃ i, x ∈ (↑i).1

Tactic:
exact ⟨⟨(V, i), hV, hVU⟩, hxV⟩

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set ↑(f ⁻¹' s)
⊢ IsClosed[instTopologicalSpaceSubtype] t → IsClosed[instTopologicalSpaceSubtype] (s.restrictPreimage f '' t)

Tactic:
suffices ∀ u, IsClosed u → Subtype.val ⁻¹' u = t →
    ∃ v, IsClosed v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t by
      simpa [isClosed_induced_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set ↑(f ⁻¹' s)
⊢ ∀ (u : Set α),
    IsClosed[inst✝¹] u → Subtype.val ⁻¹' u = t → ∃ v, IsClosed[inst✝] v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ IsOpen[inst✝] s ↔ ∀ (i : ι), IsOpen[inst✝] (s ∩ ↑(U i))

Tactic:
constructor
  · exact fun H i ↦ H.inter (U i).isOpen
  · intro H
    simpa [← inter_iUnion, hU.iSup_set_eq_univ] using isOpen_iUnion H

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ s', (∃ U Z, IsOpen[inst✝] U ∧ IsClosed[inst✝] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s) →
    ∃ U Z, (∃ t, IsOpen[inst✝] t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed[inst✝] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z

Tactic:
· rintro ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩
    exact ⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
⊢ ⨅ i, s i = { carrier := ⋂ i, ↑(s i), isClosed' := ⋯ }

Tactic:
ext1; simp

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_3
U : ι → Opens X
hU : IsOpenCover U
inst✝ : ∀ (i : ι), PrespectralSpace ↥(U i)
⊢ PrespectralSpace X

Tactic:
refine .of_isTopologicalBasis (hU.isTopologicalBasis fun i ↦ isTopologicalBasis) ?_

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_3
U : ι → Opens X
hU : IsOpenCover U
inst✝ : ∀ (i : ι), PrespectralSpace ↥(U i)
⊢ ∀ U_1 ∈ ⋃ i, (fun x ↦ Subtype.val '' x) '' {U_2 | IsOpen[instTopologicalSpaceSubtype] U_2 ∧ IsCompact U_2},
    IsCompact U_1
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
S : Set α
hS : IsIrreducible S
hS' : IsClosed S
⊢ IsGenericPoint hS.genericPoint S

Tactic:
by
  convert! hS.isGenericPoint_genericPoint_closure; exact hS'.closure_eq.symm

Goal state after:
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
Z : IrreducibleCloseds X
⊢ ∀ (a : { x // x ∈ {V | (f ⁻¹' ↑V).Nonempty} }) (b : IrreducibleCloseds Y), ↑a < b → ∃ a', a < a' ∧ ↑a' = b

Tactic:
intro a b hlt

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
Z : IrreducibleCloseds X
a : { x // x ∈ {V | (f ⁻¹' ↑V).Nonempty} }
b : IrreducibleCloseds Y
hlt : ↑a < b
⊢ ∃ a', a < a' ∧ ↑a' = b
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p q : Ideal R
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : Q.LiesOver q
hle : p ≤ q
h : p = q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
subst h
    use Q

Goal state after:
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
⊢ ↑0 + 1 = 1

Tactic:
Submodule.coe_zero,

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
⊢ 0 + 1 = 1
Module: Mathlib.Data.ZMod.Aut

Goal state before:
pp: n : ℕ
h : ∀ (f : AddAut (ZMod n)) (x : ZMod n), f 1 * x = f x
x : Additive (ZMod n)ˣ
⊢ (fun f ↦ Additive.ofMul (Units.mkOfMulEqOne (f 1) ((-f) 1) ⋯)) ((fun x ↦ AddAut.mulLeft (Additive.toMul x)) x) = x

Tactic:
by simp [← Additive.toMul_symm_eq, Equiv.symm_apply_eq,
      Units.ext_iff, Units.smul_def, -toMul_smul]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D₁ D₂ : Derivation R A M
⊢ (let __LinearMap := ↑R f ∘ₗ ↑(D₁ + D₂);
    { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ }) =
    (let __LinearMap := ↑R f ∘ₗ ↑D₁;
      { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ }) +
      let __LinearMap := ↑R f ∘ₗ ↑D₂;
      { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

Tactic:
ext; exact LinearMap.map_add _ _ _

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
⊢ (zeroLocus {f})ᶜ = ↑⊥ ↔ IsNilpotent f

Tactic:
simp only [Set.eq_univ_iff_forall, Set.singleton_subset_iff, TopologicalSpace.Opens.coe_bot,
    nilpotent_iff_mem_prime, Set.compl_empty_iff, mem_zeroLocus, SetLike.mem_coe]

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R
⊢ (∀ (x : PrimeSpectrum R), f ∈ x.asIdeal) ↔ ∀ (J : Ideal R), J.IsPrime → f ∈ J
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
⊢ (∀ (x : PrimeSpectrum R), f ∈ x.asIdeal) ↔ ∀ (J : Ideal R), J.IsPrime → f ∈ J

Tactic:
exact ⟨fun h I hI => h ⟨I, hI⟩, fun h ⟨I, hI⟩ => h I hI⟩

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ IsOpen (Set.range (comap (algebraMap R S)))

Tactic:
localization_away_comap_range S r

Goal state after:
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ IsOpen ↑(basicOpen r)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
h : IsCyclic G
σ : G →* G
⊢ ∃ m, ∀ (g : G), σ g = g ^ m

Tactic:
by
  obtain ⟨h, hG⟩ := IsCyclic.exists_generator (α := G)
  obtain ⟨m, hm⟩ := hG (σ h)
  refine ⟨m, fun g => ?_⟩
  obtain ⟨n, rfl⟩ := hG g
  rw [map_zpow, ← hm, ← zpow_mul, ← zpow_mul']

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case a_eq_b
G : Type u
inst✝ : Monoid G
eq_one : exponent G = 1
a b : G
⊢ a ^ 1 = b ^ 1

Tactic:
← eq_one,

Goal state after:
case a_eq_b
G : Type u
inst✝ : Monoid G
eq_one : exponent G = 1
a b : G
⊢ a ^ exponent G = b ^ exponent G
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
by_contra h

Goal state after:
case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : ¬exponent G ∣ n
⊢ False
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
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
hg : ¬g = 1
⊢ orderOf g ∣ p

Tactic:
h g hg

Goal state after:
case neg
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
hg : ¬g = 1
⊢ p ∣ p
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
⊢ (Set.range orderOf).Finite

Tactic:
by_contra h

Goal state after:
case refine_1
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬(Set.range orderOf).Finite
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
x : α
⊢ ∃! n, x = a ^ n.val

Tactic:
by
  obtain ⟨n, rfl⟩ := ha x
  refine ⟨n, (?_ : a ^ n = _), fun y (hy : a ^ n = _) ↦ ?_⟩
  · rw [← zpow_natCast, zpow_eq_zpow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers ha,
      Int.modEq_comm, Int.modEq_iff_add_fac, Nat.card_eq_fintype_card, ← ZMod.intCast_eq_iff]
  · rw [← zpow_natCast, zpow_eq_zpow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers ha,
      Nat.card_eq_fintype_card, ← ZMod.intCast_eq_intCast_iff] at hy
    simp [hy]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ orderOf t < orderOf (t ^ p ^ k * g)

Tactic:
(Commute.all _ g).orderOf_mul_eq_mul_orderOf_of_coprime hcoprime,

Goal state after:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ orderOf t < orderOf (t ^ p ^ k) * orderOf g
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
⊢ ∃ a, ∃ (_ : a ∈ Finset.univ) (_ : ↑1 ≠ 0), Quotient.mk'' ↑a = Quotient.mk'' b

Tactic:
have : k = 0 := by
      contrapose! hb
      simp [key, hk, hb]

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝¹ : Fintype α
this✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
this : k = 0
⊢ ∃ a, ∃ (_ : a ∈ Finset.univ) (_ : ↑1 ≠ 0), Quotient.mk'' ↑a = Quotient.mk'' b
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
q : Ideal R
hq₁ : q ∈ (Ideal.comap f I).minimalPrimes
hq₂ : q ≤ x.asIdeal
⊢ x ∈ closure (comap f '' zeroLocus ↑I)

Tactic:
obtain ⟨p', hp', hp'', rfl⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f _ hq₁

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
p' : Ideal S
hp' : p'.IsPrime
hp'' : I ≤ p'
hq₁ : Ideal.comap f p' ∈ (Ideal.comap f I).minimalPrimes
hq₂ : Ideal.comap f p' ≤ x.asIdeal
⊢ x ∈ closure (comap f '' zeroLocus ↑I)
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
s : Set G
inst✝ : Finite ↑s
⊢ rank ↥(closure s) ≤ Nat.card ↑s

Tactic:
by
  have := Fintype.ofFinite s
  rw [Nat.card_eq_fintype_card, ← s.toFinset_card, ← rank_congr (congr_arg _ s.coe_toFinset)]
  exact rank_closure_finset_le_card s.toFinset

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:
have h1 : P ≤ centralizer (zpowers x : Set G) := by rwa [le_centralizer_iff, zpowers_le]

Goal state after:
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
h1 : ↑P ≤ centralizer ↑(zpowers x)
⊢ ∃ n ∈ normalizer ↑P, g⁻¹ * x * g = n⁻¹ * x * n
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 ∣ (↑P).index
⊢ False

Tactic:
P.index_eq_card

Goal state after:
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)
⊢ False
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: case succ
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
n : ℕ
hn : orderOf g = p ^ (n + 1)
w✝ : ℕ
hn' : orderOf g = p' ^ w✝
⊢ g = 1

Tactic:
exact absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos (hn ▸ hn')) hne

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Infinite G
inst✝ : Group G
g : G
hg : zpowers g = ⊤
⊢ Function.Bijective ⇑((zpowersHom G) g)

Tactic:
by
  refine ⟨(MonoidHom.ker_eq_bot_iff _).mp ?_, MonoidHom.range_eq_top.mp hg⟩
  simp [zpowersHom_ker_eq, ← infinite_zpowers, hg, Set.infinite_univ]

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

Goal state before:
pp: G : Type u_2
inst✝¹ : CommGroup G
hG : IsCyclic G
inst✝ : Finite G
d : ℕ
g : G
h : Subgroup.zpowers g = ⊤
⊢ Nat.card ↥(powMonoidHom d).range = Nat.card G / (Nat.card G).gcd d

Tactic:
rw [MonoidHom.range_eq_map, ← h, MonoidHom.map_zpowers, Nat.card_zpowers, powMonoidHom_apply,
    orderOf_pow, orderOf_eq_card_of_zpowers_eq_top h]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
this✝ : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hn : p ^ n ≤ p ^ m
hm : Nat.card G = p ^ m
⊢ p ^ n ∣ p ^ m

Tactic:
exact pow_dvd_pow _ <| (Nat.pow_le_pow_iff_right hp.one_lt).1 hn

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (R ∙ x).annihilator = torsionOf R M x

Tactic:
simpa [torsionOf] using Submodule.annihilator_span_singleton x

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ N ≤ comap ((LinearMap.lsmul R M) 1) (I • span R s)

pp: case refine_3
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ s ⊆ ↑N

Tactic:
· rw [hs]
      intro n hn
      rw [mem_comap]
      change (1 : R) • n ∈ I • N
      rw [one_smul]
      exact hin hn

Goal state after:
case refine_3
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ s ⊆ ↑N
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun x ↦
    match x with
    | 0 => P
    | 1 => Q
⊢ (↑⊤).Pairwise fun i j ↦ map i ⊔ map j = ⊤

Tactic:
· aesop (add norm [Fin.univ_succ, Set.pairwise_pair, map, sup_comm])

Goal state after: