mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case add
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
x y : ↥(Submodule.inclusion complex).range ⊗[R] M
⊢ ∃ a,
    (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a =
      (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) x +
        (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) y

Tactic:
exact ⟨x + y, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
h : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
hf : LinearMap.lTensor M f = 0
⊢ (LinearMap.lTensor M LinearMap.id).ker = (LinearMap.lTensor M f).range

Tactic:
hf,

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
h : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
hf : LinearMap.lTensor M f = 0
⊢ (LinearMap.lTensor M LinearMap.id).ker = LinearMap.range 0
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.rTensor M f = 0
⊢ LinearMap.lTensor M f = 0

Tactic:
ext m n

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.rTensor M f = 0
m : M
n : N
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor M f)) m) n = ((AlgebraTensorModule.curry 0) m) n
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
⊢ Function.Injective ⇑((algebraMap S L).comp (algebraMap R S))

Tactic:
← IsScalarTower.algebraMap_eq

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
⊢ Function.Injective ⇑(algebraMap R L)
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
⊢ lTensor M (AlgebraTensorModule.map LinearMap.id f) = 0

Tactic:
ext m n

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
m : M
n : N
⊢ ((AlgebraTensorModule.curry ((AlgebraTensorModule.curry (lTensor M (AlgebraTensorModule.map LinearMap.id f))) m)) 1)
      n =
    ((AlgebraTensorModule.curry ((AlgebraTensorModule.curry 0) m)) 1) n
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
x : R
⊢ (algebraMap (Localization.AtPrime I) I.ResidueField) ((algebraMap R (Localization.AtPrime I)) x) = 0 ↔ x ∈ I

Tactic:
IsLocalRing.ResidueField.algebraMap_eq,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
x : R
⊢ (IsLocalRing.residue (Localization.AtPrime I)) ((algebraMap R (Localization.AtPrime I)) x) = 0 ↔ x ∈ I
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
this : r = 0
hr :
  (toPiLocalization ((i : ι) → R i)) 0 { asIdeal := J, isMaximal := max } =
    Function.update 0 { asIdeal := J, isMaximal := max } 1 { asIdeal := J, isMaximal := max }
⊢ False

Tactic:
map_zero,

Goal state after:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
this : r = 0
hr :
  0 { asIdeal := J, isMaximal := max } =
    Function.update 0 { asIdeal := J, isMaximal := max } 1 { asIdeal := J, isMaximal := max }
⊢ False
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
this : r = 0
hr :
  (toPiLocalization ((i : ι) → R i)) r { asIdeal := J, isMaximal := max } =
    Function.update 0 { asIdeal := J, isMaximal := max } 1 { asIdeal := J, isMaximal := max }
⊢ False

Tactic:
rw [this, map_zero, Function.update_self] at hr

Goal state after:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
this : r = 0
hr : 0 { asIdeal := J, isMaximal := max } = 1
⊢ False
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
⊢ GeneralizingMap f ↔ ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)

Tactic:
refine ⟨fun hf ↦ fun i ↦ hf.restrictPreimage _, fun hf ↦ fun x y h ↦ ?_⟩
  obtain ⟨i, hx⟩ := hU.exists_mem (f x)
  have h : (⟨y, (U i).2.stableUnderGeneralization h hx⟩ : U i) ⤳
    (U i).1.restrictPreimage f ⟨x, hx⟩ := by rwa [subtype_specializes_iff]
  obtain ⟨a, ha, heq⟩ := hf i h
  refine ⟨a, ?_, congr(($heq).val)⟩
  rwa [subtype_specializes_iff] at ha

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

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U : Opens X
x : X
hxU : x ∈ U
⊢ x ∈
    (fun I ↦ ⨆ U ∈ I, U.toOpens) ((fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }) U)

Tactic:
obtain ⟨V, ⟨h₁, h₂⟩, hxV, hVU⟩ := isTopologicalBasis.exists_subset_of_mem_open hxU U.2

Goal state after:
case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U : Opens X
x : X
hxU : x ∈ U
V : Set X
h₁ : IsOpen[inst✝²] V
h₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ ↑U
⊢ x ∈
    (fun I ↦ ⨆ U ∈ I, U.toOpens) ((fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }) U)
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : LE P
inst✝ : IsCodirectedOrder P
I J : Ideal P
a : P
ha : a ∈ ↑I
b : P
hb : b ∈ ↑J
⊢ (↑I ∩ ↑J).Nonempty

Tactic:
obtain ⟨c, hac, hbc⟩ := exists_le_le a b

Goal state after:
P : Type u_1
inst✝¹ : LE P
inst✝ : IsCodirectedOrder P
I J : Ideal P
a : P
ha : a ∈ ↑I
b : P
hb : b ∈ ↑J
c : P
hac : c ≤ a
hbc : c ≤ b
⊢ (↑I ∩ ↑J).Nonempty
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
⊢ ⊥ ∈ ↑(⨅ s ∈ S, s.toLowerSet)

Tactic:
LowerSet.coe_iInf₂,

Goal state after:
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
⊢ ⊥ ∈ ⋂ i ∈ S, ↑i.toLowerSet
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
a : P
ha : a ∈ ↑(⨅ s ∈ S, s.toLowerSet)
b : P
hb : b ∈ ↑(⨅ s ∈ S, s.toLowerSet)
⊢ a ⊔ b ∈ ↑(⨅ s ∈ S, s.toLowerSet)

Tactic:
LowerSet.coe_iInf₂,

Goal state after:
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
a : P
ha : a ∈ ⋂ i ∈ S, ↑i.toLowerSet
b : P
hb : b ∈ ⋂ i ∈ S, ↑i.toLowerSet
⊢ a ⊔ b ∈ ⋂ i ∈ S, ↑i.toLowerSet
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
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
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
by
  by_cases h : p = q
  · subst h
    use Q
  · have := Q.over_def q
    subst this
    exact Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt Q (lt_of_le_of_ne hle h)

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
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
hpq : p < q
⊢ ∃ P < Q, P.IsPrime ∧ P.LiesOver p

Tactic:
by
  obtain ⟨P, hPQ, _, _⟩ := Q.exists_ideal_le_liesOver_of_le (p := p) (q := q) hpq.le
  refine ⟨P, ?_, inferInstance, inferInstance⟩
  by_contra hc
  have : P = Q := eq_of_le_of_not_lt hPQ hc
  subst this
  simp [P.over_def p, P.over_def q] at hpq

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

Tactic:
by
  refine ⟨fun hf ↦ ?_, fun hf ↦ .comp hf (.of_bijective hg)⟩
  let e := RingEquiv.ofBijective g hg
  have : f = e.symm.toRingHom.comp (e.toRingHom.comp f) := by ext; simp
  rw [this]
  exact .comp hf (.of_bijective e.symm.bijective)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ s ⊆ t

Tactic:
← ht.closure_subset_iff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ closure s ⊆ t
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Function.Injective (comap (algebraMap R S))

Tactic:
by
  intro p q h
  replace h := _root_.congr_arg (fun x : PrimeSpectrum R => Ideal.map (algebraMap R S) x.asIdeal) h
  dsimp only [comap] at h
  rw [IsLocalization.map_under M S, IsLocalization.map_under M S] at h
  ext1
  exact h

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p ≠ 0
ht : exponent G = ⊥
⊢ False

Tactic:
rw [ht] at h
      apply h
      rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]

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

Goal state before:
pp: case a
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ {a | a ^ n = 1}
m : ℕ
hm : g ^ m = x
⊢ g ^ (Fintype.card α / n.gcd (Fintype.card α) * (m / (Fintype.card α / n.gcd (Fintype.card α)))) = x

Tactic:
Nat.mul_div_cancel_left',

Goal state after:
case a
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ {a | a ^ n = 1}
m : ℕ
hm : g ^ m = x
⊢ g ^ m = x

case a
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ {a | a ^ n = 1}
m : ℕ
hm : g ^ m = x
⊢ Fintype.card α / n.gcd (Fintype.card α) ∣ m
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
hJ',

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
⊢ sᶜ ∪ s = Set.univ
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
a : α
inst✝² : Group α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ha : ∀ (x : α), x ∈ zpowers a
⊢ image (fun i ↦ a ^ i) (range (orderOf a)) = univ

Tactic:
IsCyclic.image_range_orderOf ha

Goal state after:
α : Type u_1
a : α
inst✝² : Group α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ha : ∀ (x : α), x ∈ zpowers a
⊢ univ = univ
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
n : ℕ
h : IsPGroup (p ^ n) G
g : G
⊢ ∀ (a : ℕ), g ^ (p ^ n) ^ a = 1 → g ^ p ^ (n * a) = 1

Tactic:
by simp [pow_mul]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Infinite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
rw [Nat.card_eq_zero_of_infinite]
    exact Or.inr ⟨0, rfl⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ sᶜ ∩ zeroLocus ↑J = ∅

Tactic:
hJ',

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ sᶜ ∩ s = ∅
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(H ⊔ K)

Tactic:
rw [← QuotientGroup.ker_mk' K, ← Subgroup.comap_map_eq]

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H))
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
⊢ exponent G = if ∃ g, orderOf g = 0 then 0 else ⨆ g, orderOf g

Tactic:
by
  split_ifs with h
  · obtain ⟨g, hg⟩ := h
    exact exponent_eq_zero_of_order_zero hg
  · have := not_exists.mp h
    exact exponent_eq_iSup_orderOf fun g => Ne.bot_lt <| this g

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
I : Ideal R
⊢ ↑I.minimalPrimes ≃o (↑(irreducibleComponents ↑(zeroLocus ↑I)))ᵒᵈ

Tactic:
let e : {p : Ideal R | p.IsPrime ∧ I ≤ p} ≃o zeroLocus (I : Set R) :=
    ⟨⟨fun x ↦ ⟨⟨x.1, x.2.1⟩, x.2.2⟩, fun x ↦ ⟨x.1.1, x.1.2, x.2⟩, fun _ ↦ rfl, fun _ ↦ rfl⟩, .rfl⟩

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
e : ↑{p | p.IsPrime ∧ I ≤ p} ≃o ↑(zeroLocus ↑I) :=
  { toFun := fun x ↦ ⟨{ asIdeal := ↑x, isPrime := ⋯ }, ⋯⟩, invFun := fun x ↦ ⟨(↑x).asIdeal, ⋯⟩, left_inv := ⋯,
    right_inv := ⋯, map_rel_iff' := ⋯ }
⊢ ↑I.minimalPrimes ≃o (↑(irreducibleComponents ↑(zeroLocus ↑I)))ᵒᵈ
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case «0»
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝² : Finite α
this✝¹ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this✝ : orderOf g ∈ (p ^ 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
a : ℕ
ha : 0 < 3
ha' : p ^ 0 = orderOf g
⊢ orderOf g = p

Tactic:
exact False.elim <| hg <| orderOf_eq_one_iff.mp <| by simp_all

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : (↑P).relIndex (normalizer ↑P) ≠ 0
this✝ : (↑(P.subtype ⋯)).Normal
this : (↑(P.subtype ⋯)).FiniteIndex
⊢ ¬p ∣ (↑P).relIndex (normalizer ↑P) * Nat.card (Sylow p G)

Tactic:
replace hP := not_dvd_index_aux (P.subtype le_normalizer)

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this✝ : (↑(P.subtype ⋯)).Normal
this : (↑(P.subtype ⋯)).FiniteIndex
hP : ¬p ∣ (↑(P.subtype ⋯)).index
⊢ ¬p ∣ (↑P).relIndex (normalizer ↑P) * Nat.card (Sylow p G)
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).symm (i • g) = ↑i

Tactic:
by
  rw [AddEquiv.symm_apply_eq, zmodAddEquivOfGenerator_apply_intCast]

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
e : G ≃* H
⊢ Subgroup.map (↑e) (torsion G) = torsion H

Tactic:
Subgroup.map_equiv_eq_comap_symm,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
e : G ≃* H
⊢ Subgroup.comap (↑e.symm) (torsion G) = torsion H
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ∃ y ∈ I a, ∃ z ∈ I b, y + z = 1

Tactic:
refine ⟨_, ?_, _, ?_, hμ⟩

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ∑ x ∈ t, ↑(μ x) ∈ I a

case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ↑(μ a) ∈ I b
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
⊢ IsSemisimpleRing S

Tactic:
let : Module R S := Module.compHom _ f

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this : Module R S := Module.compHom S f
⊢ IsSemisimpleRing S
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ IsTorsionBySet R M {a} ↔ torsionBySet R M {a} = ⊤

Tactic:
isTorsionBySet_iff_torsionBySet_eq_top

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ torsionBySet R M {a} = ⊤ ↔ torsionBySet R M {a} = ⊤
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case zero
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
⊢ (map R' f) 0 = Polynomial.map (algebraMap R R') p • (map R' f) 0

Tactic:
map_zero,

Goal state after:
case zero
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
⊢ 0 = Polynomial.map (algebraMap R R') p • 0
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case zero
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
⊢ (eval r) 0 = Polynomial.eval r p • (eval r) 0

Tactic:
map_zero,

Goal state after:
case zero
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
⊢ 0 = Polynomial.eval r p • 0
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = torsionBySet R M ↑(Ideal.span {∏ i ∈ S, q i})

Tactic:
←
    Ideal.finset_inf_span_singleton _ _ hq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = torsionBySet R M ↑(S.inf fun i ↦ Ideal.span {q i})