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

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rs) (↥Rts) A
this✝¹ : Nontrivial ↥Rs
this✝ : Nontrivial S
this : IsDomain ↥Rt
x : S
hs : x ∈ s
ht : x ∈ t
⊢ IsAlgebraic (↥Rt) x

pp: case neg
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rs) (↥Rts) A
this✝¹ : Nontrivial ↥Rs
this✝ : Nontrivial S
this : IsDomain ↥Rt
x : S
hs : x ∈ s
ht : x ∉ t
⊢ IsAlgebraic (↥Rt) x

Tactic:
· exact isAlgebraic_algebraMap (⟨x, subset_adjoin ht⟩ : Rt)

Goal state after:
case neg
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rs) (↥Rts) A
this✝¹ : Nontrivial ↥Rs
this✝ : Nontrivial S
this : IsDomain ↥Rt
x : S
hs : x ∈ s
ht : x ∉ t
⊢ IsAlgebraic (↥Rt) x
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case mpr
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
⊢ 1 ⊗ₜ[R] 0 = 0

Tactic:
tmul_zero

Goal state after:
case mpr
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
⊢ 0 = 0
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
σ : Type u
⊢ Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u, u_2} (Module.rank R S)

Tactic:
have := Algebra.isPushout_iff R (MvPolynomial σ R) S (MvPolynomial σ S)
    |>.mp inferInstance |>.lift_rank_eq
  rwa [Cardinal.lift_id', Cardinal.lift_umax] at this

Goal state after:
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
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
⊢ (algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)

Tactic:
refine Submodule.span_subset_span R K _ ?_

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
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
⊢ (algebraMap S L) (a * y) ∈ ↑(Submodule.span R (⇑(algebraMap S L) '' b))
Module: Mathlib.RingTheory.Localization.Integral

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

Tactic:
· change IsIntegral _ _
    rw [← isAlgebraic_iff_isIntegral, ← IsAlgebraic.invOf_iff, isAlgebraic_iff_isIntegral]
    apply IsIntegral.tower_top (R := R)
    apply IsIntegral.map (IsScalarTower.toAlgHom R S L)
    exact Algebra.IsIntegral.isIntegral (s : S)

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ RingHom.ker (algebraMap (R ⧸ I) I.ResidueField) = ⊥

Tactic:
refine (Ideal.ker_quotient_lift _ _).trans ?_

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ map (Quotient.mk I) (RingHom.ker ↑(Algebra.ofId R I.ResidueField)) = ⊥
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_5
x : α
s : ι → Opens α
⊢ x ∈ iSup s ↔ ∃ i, x ∈ s i

Tactic:
← SetLike.mem_coe

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_5
x : α
s : ι → Opens α
⊢ x ∈ ↑(iSup s) ↔ ∃ i, x ∈ s i
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a : α
S : Set (BooleanSubalgebra α)
⊢ a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L

Tactic:
← SetLike.mem_coe

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a : α
S : Set (BooleanSubalgebra α)
⊢ a ∈ ↑(sInf S) ↔ ∀ L ∈ S, a ∈ L
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : BooleanAlgebra α
a : α
f : ι → BooleanSubalgebra α
⊢ a ∈ ⨅ i, f i ↔ ∀ (i : ι), a ∈ f i

Tactic:
← SetLike.mem_coe

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝ : BooleanAlgebra α
a : α
f : ι → BooleanSubalgebra α
⊢ a ∈ ↑(⨅ i, f i) ↔ ∀ (i : ι), a ∈ f i
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case inr.refine_3
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
hU'' : ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i) = ⊤
⊢ ∀ (i : ι), f₀ ⁻¹' ↑((Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i)) ⊆ range (iV i)

Tactic:
exact hV

Goal state after:
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).carrier

Tactic:
rw [LowerSet.carrier_eq_coe, LowerSet.coe_iInf₂, Set.mem_iInter₂]
          exact fun s _ ↦ s.bot_mem

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ a * a ^ (n - 1) = a ^ n

Tactic:
rw [← pow_succ', Nat.sub_add_cancel hpos]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
g : α
⊢ orderOf g = Nat.card α ↔ Nat.card α ≤ orderOf g

Tactic:
exact ⟨Eq.ge, le_antisymm orderOf_le_card⟩

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

Goal state before:
pp: case h
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
a : G
ha : Function.Surjective fun x ↦ a ^ x
⊢ a ^ k ≠ 1

Tactic:
contrapose! k_lt_card_G

Goal state after:
case h
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x ↦ a ^ x
k_lt_card_G : a ^ k = 1
⊢ Nat.card G ≤ k
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.Away ↑(e I))) r = (algE (e I)) (x (e.symm (e I)))
⊢ (toPiLocalization R) r I = x I

Tactic:
rwa [← AlgEquiv.symm_apply_eq, AlgEquiv.commutes, e.symm_apply_apply] at this

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : PrimeSpectrum R
⊢ x ≤ y ↔ y ∈ closure {x}

Tactic:
rw [← asIdeal_le_asIdeal, ← zeroLocus_vanishingIdeal_eq_closure, mem_zeroLocus,
    vanishingIdeal_singleton, SetLike.coe_subset_coe]

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

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(k % ↑(Nat.find hex)).natAbs
hk₅ : g ^ (k % ↑(Nat.find hex)).natAbs ∈ H
h : ¬(k % ↑(Nat.find hex)).natAbs = 0
⊢ ↑(k % ↑(Nat.find hex)).natAbs < ↑(Nat.find hex)

Tactic:
rw [← hk₄]

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(k % ↑(Nat.find hex)).natAbs
hk₅ : g ^ (k % ↑(Nat.find hex)).natAbs ∈ H
h : ¬(k % ↑(Nat.find hex)).natAbs = 0
⊢ k % ↑(Nat.find hex) < ↑(Nat.find hex)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
⊢ (∃ n, ∃ k ≤ n, Nat.card G = p ^ k) ↔ ∃ n, Nat.card G = p ^ n

Tactic:
exact ⟨fun ⟨n, k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨n, hn⟩ ↦ ⟨n, n, le_rfl, hn⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fact (Nat.Prime p)
⊢ (∃ n, ∃ k ≤ n, Monoid.exponent G = p ^ k) ↔ ∃ n, Monoid.exponent G = p ^ n

Tactic:
exact ⟨fun ⟨n, k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨n, hn⟩ ↦ ⟨n, n, le_rfl, hn⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case refine_1
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
x✝ : ∃ n, Nat.card G ∣ p ^ n
n : ℕ
hn : Nat.card G ∣ p ^ n
⊢ (Nat.card G).primeFactors ⊆ p.primeFactors

Tactic:
rcases eq_or_ne n 0 with (rfl | hn0)

Goal state after:
case refine_1.inl
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
x✝ : ∃ n, Nat.card G ∣ p ^ n
hn : Nat.card G ∣ p ^ 0
⊢ (Nat.card G).primeFactors ⊆ p.primeFactors

case refine_1.inr
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
x✝ : ∃ n, Nat.card G ∣ p ^ n
n : ℕ
hn : Nat.card G ∣ p ^ n
hn0 : n ≠ 0
⊢ (Nat.card G).primeFactors ⊆ p.primeFactors
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 : ∃ y ∈ I ^ n, ∃ z ∈ J ^ n, y + z = 1
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

Tactic:
obtain ⟨x, hx, y, hy, add⟩ := 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
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ Subgroup.map f (Subgroup.closure ↑S) = ⊤

Tactic:
hS2,

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ Subgroup.map f ⊤ = ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
rw [← zeroLocus_minimalPrimes, ← zeroLocus_vanishingIdeal_eq_closure]
    exact Set.mem_image_of_mem _

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ closure (zeroLocus ↑I) ∈ irreducibleComponents (PrimeSpectrum R) ↔ vanishingIdeal (zeroLocus ↑I) ∈ minimalPrimes R

Tactic:
exact vanishingIdeal_mem_minimalPrimes.symm

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
this✝ : fixedPoints (↥↑P) (Sylow p G) = {P}
this : Nat.card ↑(fixedPoints (↥↑P) (Sylow p G)) = 1
⊢ Nat.card (Sylow p G) ≡ 1 [MOD p]

Tactic:
exact (P.2.card_modEq_card_fixedPoints (Sylow p G)).trans (by rw [this])

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
⊢ zpowers x ≤ centralizer ↑↑P

Tactic:
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
⊢ x ∈ centralizer ↑↑P
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
h1 : ↑P ≤ centralizer ↑(zpowers x)
⊢ zpowers x ≤ centralizer ↑↑(g • P)

Tactic:
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)
⊢ x ∈ centralizer ↑↑(g • P)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Nat.Prime (Nat.card (ZMod p))

Tactic:
simpa using hp.out

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
⊢ (∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a) ↔ torsion G ≤ ⊥

Tactic:
SetLike.le_def

Goal state after:
G : Type u_1
inst✝ : CommGroup G
⊢ (∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a) ↔ ∀ ⦃x : G⦄, x ∈ torsion G → x ∈ ⊥
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:
rw [Subgroup.map_equiv_eq_comap_symm, e.symm.comap_torsion]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu' : ∀ a ∈ u, IsAtom a
hu : f i = ↑(sSup u)
⊢ ↑(sSup u) = sSup (Subtype.val '' u)

Tactic:
Iic.coe_sSup

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ 1 ∣ Nat.card G
key : p ^ 1 ∣ Nat.card ↥↑P
⊢ p ∣ Nat.card ↥↑P

Tactic:
rwa [pow_one] at key

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
Q : Sylow p G
x✝ : G
h1 : P = Q
x : G
h2 : P = default
⊢ Q = default

Tactic:
rw [← h1, ← h2]

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : (s.toFun ⟨s.length - 1, ⋯⟩.castSucc, s.toFun ⟨s.length - 1, ⋯⟩.succ) ∈ {(x, y) | IsMaximal x y}
⊢ IsMaximal (s.toFun ⟨s.length.pred, ⋯⟩) (s.toFun (Fin.last s.length))

Tactic:
simp only [Fin.castSucc_mk, Fin.succ_mk, mem_ofPred_eq] at this

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : IsMaximal (s.toFun ⟨s.length - 1, ⋯⟩) (s.toFun ⟨s.length - 1 + 1, ⋯⟩)
⊢ IsMaximal (s.toFun ⟨s.length.pred, ⋯⟩) (s.toFun (Fin.last s.length))
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: 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
hx : a ∈ t
this : ∀ i ∈ Finset.cons a t hat, i ≠ a → ↑(μ a) ∈ I i
⊢ False

Tactic:
exact hat hx

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
m : Submodule R M
⊢ IsSimpleModule R (M ⧸ m) ↔ IsCoatom m

Tactic:
by
  rw [← Set.isSimpleOrder_Ici_iff_isCoatom, isSimpleModule_iff]
  exact (Submodule.comapMkQRelIso m).isSimpleOrder_iff

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
inst✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ IsSimpleModule R (R ⧸ (toSpanSingleton R M m).ker)

Tactic:
exact congr (quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm)

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
⊢ (sSup {m | IsSimpleModule R ↥m}).annihilator.IsRadical

Tactic:
sSup_eq_iSup',

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
⊢ (⨆ a, ↑a).annihilator.IsRadical
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
J : Ideal R
f : Module.End R R
idem : IsIdempotentElem f
h : IsCompl (LinearMap.range f) J
⊢ R ∙ f 1 = Ideal.span {f 1}

Tactic:
Ideal.submodule_span_eq

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
J : Ideal R
f : Module.End R R
idem : IsIdempotentElem f
h : IsCompl (LinearMap.range f) J
⊢ Ideal.span {f 1} = Ideal.span {f 1}
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
p : ι → Ideal R
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
hM : IsTorsionBySet R M ↑(⨅ i ∈ S, p i)
⊢ ⨆ i, torsionBySet R M ↑(p ↑i) = ⊤

Tactic:
apply (iSup_subtype'' ↑S fun i => torsionBySet R M <| p i).trans

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
p : ι → Ideal R
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
hM : IsTorsionBySet R M ↑(⨅ i ∈ S, p i)
⊢ ⨆ t ∈ ↑S, torsionBySet R M ↑(p t) = ⊤
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ I • sSup (N '' S) i ≤ sSup (N '' S) (i + 1)

Tactic:
sSup_eq_iSup',

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ I • (⨆ a, ↑a) i ≤ (⨆ a, ↑a) (i + 1)