mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization ↑f.symm).comp (mapPiLocalization ↑f) = RingHom.id (PiLocalization R)

Tactic:
rw [← mapPiLocalization_comp, RingEquiv.symm_comp, mapPiLocalization_id]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
⊢ Finite (PrimeSpectrum R)

Tactic:
by
  replace surj := (mapPiLocalization_bijective _ ⟨toPiLocalization_injective R, surj⟩).2.comp surj
  rw [← AlgHom.coe_toRingHom,
    ← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj
  exact finite_of_toPiLocalization_pi_surjective surj.of_comp

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U : Opens α
⊢ ↑Uᶜ = interior (↑U)ᶜ

Tactic:
← interior_compl,

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
U : Opens α
⊢ ↑(Opens.interior (↑U)ᶜ) = interior (↑U)ᶜ
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us

Tactic:
by
  constructor
  · intro hB U
    refine ⟨{ V : Opens α | V ∈ B ∧ V ≤ U }, fun U hU => hU.left, ext ?_⟩
    rw [coe_sSup, hB.open_eq_sUnion' U.isOpen]
    simp_rw [sUnion_eq_biUnion, iUnion, mem_ofPred_eq, iSup_and, iSup_image]
    rfl
  · intro h
    rw [isBasis_iff_nbhd]
    intro U x hx
    rcases h U with ⟨Us, hUs, rfl⟩
    rcases mem_sSup.1 hx with ⟨U, Us, xU⟩
    exact ⟨U, hUs Us, xU, le_sSup Us⟩

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: 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)
hU' : iSup U = ⊤
⊢ IsEmbedding f

Tactic:
(IsOpenCover.mk hU').isEmbedding_iff_restrictPreimage h

Goal state after:
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)
hU' : iSup U = ⊤
⊢ ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f)
Module: Mathlib.Topology.Spectral.Prespectral

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

Tactic:
apply le_antisymm
    · simp only [iSup_le_iff]
      exact fun _ ↦ id
    · intro x hxU
      obtain ⟨V, ⟨h₁, h₂⟩, hxV, hVU⟩ := isTopologicalBasis.exists_subset_of_mem_open hxU U.2
      simp only [Opens.mem_iSup]
      exact ⟨⟨⟨_, h₂⟩, h₁⟩, hVU, hxV⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
⊢ ?m.62

Tactic:
refine hc.elim_finite_subcover (fun s : Us ↦ f '' s.1) (fun s ↦ h _ s.1.2) (fun x hx ↦ ?_)
    obtain ⟨x, rfl⟩ := hs hx
    obtain ⟨i, hi, hx⟩ := mem_sSup.mp <| by rwa [← heq]
    exact Set.mem_iUnion.mpr ⟨⟨i, hi⟩, x, hx, rfl⟩

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case isSublattice
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s : Set X
⊢ IsSublattice {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}

Tactic:
exact ⟨fun s hs t ht ↦ ⟨hs.1.union ht.1, hs.2.union ht.2⟩,
      fun s hs t ht ↦ ⟨hs.1.inter ht.1, hs.2.inter_isOpen ht.2 ht.1⟩⟩

Goal state after:
Module: Mathlib.Topology.Constructible

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

Tactic:
let e : V ≃ₜ Subtype.val '' V :=
    (Equiv.Set.image _ V Subtype.val_injective).toHomeomorphOfIsInducing
      ((U i).2.isOpenEmbedding_subtypeVal.restrict (by simp [MapsTo]) hV).isInducing

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (↑(U i) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set ↑↑(U i)
hVx : V ∈ 𝓝 ⟨x, hi⟩
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (V ↓∩ ↑(U i) ↓∩ s)
e : ↑V ≃ₜ ↑(Subtype.val '' V) := (Equiv.Set.image Subtype.val V ⋯).toHomeomorphOfIsInducing ⋯
⊢ IsConstructible ((Subtype.val '' V) ↓∩ s)
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: case convert_1
A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this✝ : PreservesFiniteLimits (extendScalars f)
this : (extendScalars f).ReflectsIsomorphisms
⊢ HasEqualizerOfIsCosplitPair (extendScalars f)

pp: case convert_2
A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this✝ : PreservesFiniteLimits (extendScalars f)
this : (extendScalars f).ReflectsIsomorphisms
⊢ PreservesLimitOfIsCosplitPair (extendScalars f)

Tactic:
· exact ⟨inferInstance⟩

Goal state after:
case convert_2
A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this✝ : PreservesFiniteLimits (extendScalars f)
this : (extendScalars f).ReflectsIsomorphisms
⊢ PreservesLimitOfIsCosplitPair (extendScalars f)
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: case convert_2
A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this✝ : PreservesFiniteLimits (extendScalars f)
this : (extendScalars f).ReflectsIsomorphisms
⊢ PreservesLimitOfIsCosplitPair (extendScalars f)

Tactic:
· exact ⟨inferInstance⟩

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

Goal state before:
pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ CommRingCat.of (S ⊗[R] S) ⟶ CommRingCat.of (T ⊗[R] A)

Tactic:
exact CommRingCat.ofHom
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T)
      (IsScalarTower.toAlgHom R S A)).toRingHom

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

Goal state before:
pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ IsPushout
    (CommRingCat.ofHom
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A)).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.includeLeft.comp (algebraMap S T)))

Tactic:
· refine .of_iso
      (isPushout_map_codiagonal (CommRingCat.ofHom <| algebraMap S T)
        (CommRingCat.ofHom <| algebraMap S A) (CommRingCat.ofHom <| algebraMap R S))
      ?_ ?_ (.refl _) ?_ ?_ ?_ ?_ ?_
    · exact (CommRingCat.isPushout_tensorProduct R S S).isoPushout.symm
    · exact pushout.congrHom (by simp [IsScalarTower.algebraMap_eq R S T])
          (by simp [IsScalarTower.algebraMap_eq R S A]) ≪≫
        (CommRingCat.isPushout_tensorProduct R T A).isoPushout.symm
    · exact (CommRingCat.isPushout_tensorProduct S T A).isoPushout.symm
    all_goals ext <;> simp

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
⊢ IsClosed (zeroLocus ↑(RingHom.ker (RingHom.fst R S)))

Tactic:
isClosed_zeroLocus

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
⊢ IsClosed (zeroLocus ↑(RingHom.ker (RingHom.snd R S)))

Tactic:
isClosed_zeroLocus

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ TopologicalSpace.Opens.IsBasis (Set.range basicOpen)

Tactic:
by
  unfold TopologicalSpace.Opens.IsBasis
  convert! isTopologicalBasis_basic_opens (R := R)
  rw [← Set.range_comp]
  rfl

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inl
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p = 0
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p

pp: case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p ≠ 0
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p

Tactic:
· refine ⟨1, by rw [h, pow_zero, orderOf_one]⟩

Goal state after:
case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p ≠ 0
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ 0 < Finset.univ.lcm orderOf

Tactic:
simpa [pos_iff_ne_zero, Finset.lcm_eq_zero_iff] using fun x => (_root_.orderOf_pos x).ne'

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

Goal state before:
pp: case right
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
⊢ (fun x ↦ x ^ n) '' ↑J ⊆ ↑(I ^ n ⊔ J ^ n)

Tactic:
rintro _ ⟨x, hx, rfl⟩; exact Ideal.mem_sup_right (Ideal.pow_mem_pow hx n)

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
this : ∀ (x : G), ¬orderOf x = 0
⊢ exponent G = ⨆ g, orderOf g

Tactic:
exact exponent_eq_iSup_orderOf fun g => Ne.bot_lt <| this g

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
this : Finite G
k : ℕ
hk : Nat.card ↥P = p ^ k
h_cop : p ∣ Nat.card ↥H ∧ p ∣ H.index
⊢ (Nat.card ↥H).gcd H.index ≠ 1

Tactic:
exact Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp.out, h_cop⟩

Goal state after:
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₁
inst✝³ : FunLike F M M₁
inst✝² : AddMonoidHomClass F M M₁
inst✝¹ : Module (ZMod n) M
inst✝ : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
⊢ f (c • x) = c • f x

Tactic:
by
  rw [← ZMod.intCast_zmod_cast c]
  exact map_intCast_smul f _ _ (cast c) x

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

Goal state before:
pp: case h.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
h1 : ∑ m ∈ d.properDivisors, #{a | orderOf a = m} = ∑ m ∈ d.properDivisors, φ m
h2 : ∑ m ∈ d.divisors, #{a | orderOf a = m} = ∑ m ∈ d.divisors, φ m
⊢ #{a | orderOf a = d} = φ d

Tactic:
simpa [← cons_self_properDivisors hd0, ← h1] using h2

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hα : Nontrivial α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ Nat.card α ≠ 1

Tactic:
contrapose! hα

Goal state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : Nat.card α = 1
⊢ Subsingleton α
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = f.ker
tH : IsMulTorsion H
tN : IsMulTorsion ↥N
g : G
⊢ IsOfFinOrder g

Tactic:
obtain ⟨ngn, ngnpos, hngn⟩ := (tH <| f g).exists_pow_eq_one
  have hmem := MonoidHom.mem_ker.mpr ((f.map_pow g ngn).trans hngn)
  lift g ^ ngn to N using hN.symm ▸ hmem with gn h
  obtain ⟨nn, nnpos, hnn⟩ := (tN gn).exists_pow_eq_one
  exact isOfFinOrder_iff_pow_eq_one.mpr <| ⟨ngn * nn, mul_pos ngnpos nnpos, by
    rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]⟩

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

pp: case «1»
α : 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 : 1 < 3
ha' : p ^ 1 = orderOf g
⊢ orderOf g = p

pp: case «2»
α : 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 : 2 < 3
ha' : p ^ 2 = orderOf g
⊢ orderOf g = p

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

Goal state after:
case «1»
α : 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 : 1 < 3
ha' : p ^ 1 = orderOf g
⊢ orderOf g = p

case «2»
α : 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 : 2 < 3
ha' : p ^ 2 = orderOf g
⊢ orderOf g = p
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p ↥Q
hp : ↑P < comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ False

Tactic:
exact hp.ne' (P.3 hQ hp.le)

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : ↑(MulAut.conjNormal (↑n * g) • P) = ↑P
⊢ ↑n * g ∈ normalizer ↑(map N.subtype ↑P)

Tactic:
pointwise_smul_def,

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : MulAut.conjNormal (↑n * g) • ↑P = ↑P
⊢ ↑n * g ∈ normalizer ↑(map N.subtype ↑P)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ Classical.choose ⋯ ≡ 1 [ZMOD ↑(orderOf g)]

Tactic:
rw [← zpow_eq_zpow_iff_modEq, zpow_one]

Goal state after:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ g ^ Classical.choose ⋯ = g
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ sSup (range f) = ⟨sSup s, hx✝⟩

Tactic:
· rw [Subtype.ext_iff]
    change sSup (((↑) : Iic a → α) '' (range f)) = sSup s
    congr
    ext b
    simpa [f] using hx b

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a | IsAtom a}
⊢ sSup u = ⨆ i ∈ s, f i

Tactic:
u,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a | IsAtom a}
⊢ sSup (⋃ i, ⋃ (hi : i ∈ s), t i hi) = ⨆ i ∈ s, f i
Module: Mathlib.GroupTheory.Sylow

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

Tactic:
← index_mul_card P.1

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ n ∣ (↑P).index * Nat.card ↥↑P
⊢ p ^ n ∣ Nat.card ↥↑P
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Ring S
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hR : IsSemisimpleRing R
hS : IsSemisimpleRing S
⊢ IsSemisimpleRing (R × S)

Tactic:
by
  let : Module (R × S) R := Module.compHom _ (.fst R S)
  let : Module (R × S) S := Module.compHom _ (.snd R S)
  -- e₁, e₂ got falsely flagged by the unused argument linter
  let _e₁ : R →ₛₗ[.fst R S] R := { AddMonoidHom.id R with map_smul' := fun _ _ ↦ rfl }
  let _e₂ : S →ₛₗ[.snd R S] S := { AddMonoidHom.id S with map_smul' := fun _ _ ↦ rfl }
  rw [IsSemisimpleRing, ← _e₁.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hR
  rw [IsSemisimpleRing, ← _e₂.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hS
  rw [IsSemisimpleRing, ← Submodule.topEquiv.isSemisimpleModule_iff_of_bijective
    (LinearEquiv.bijective _), ← LinearMap.sup_range_inl_inr]
  exact .sup (.range _) (.range _)

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

Goal state before:
pp: case single.monomial
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'
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ (map R' f) (single R (n✝ + i) (a✝ • m)) =
    Polynomial.map (algebraMap R R') ((monomial n✝) a✝) • (map R' f) (single R i m)

Tactic:
map_single,

Goal state after:
case single.monomial
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'
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ single R' (n✝ + i) (f (a✝ • m)) = Polynomial.map (algebraMap R R') ((monomial n✝) a✝) • (map R' f) (single R i m)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single.monomial
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'
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ single R' (n✝ + i) (f (a✝ • m)) = (monomial n✝) ((algebraMap R R') a✝) • (map R' f) (single R i m)

Tactic:
map_single,

Goal state after:
case single.monomial
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'
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ single R' (n✝ + i) (f (a✝ • m)) = (monomial n✝) ((algebraMap R R') a✝) • single R' i (f m)
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
P Q : Ideal R
hc : P ⊔ Q = ⊤
⊢ torsionBySet R M ↑P ⊔ torsionBySet R M ↑Q = torsionBySet R M ↑(P ⊓ Q)

Tactic:
let map : Fin 2 → Ideal R | 0 => P | 1 => Q
  have heq := Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf
    (p := map) (M := M) (S := ⊤) ?_
  · have : ⨆ i, ⨆ (_ : i = 0 ∨ i = 1), torsionBySet R M ↑(map i) =
        torsionBySet R M ↑(map 0) ⊔ torsionBySet R M ↑(map 1) := iSup_pair
    simpa [Finset.top_eq_univ, Fin.univ_succ, Fin.isValue, coe_iInf, this] using heq
  · simp_all [Set.pairwise_pair, Fin.univ_succ, map, sup_comm]

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

Goal state before:
pp: case single
R : Type u_2
inst✝² : CommRing R
S : Type u_8
inst✝¹ : CommRing S
inst✝ : Algebra S R
x : R
i : ℕ
m : S
⊢ x ^ i * (algebraMap S R) m = (eval x) ((map R (Algebra.linearMap S R)) (single S i m))

Tactic:
map_single,

Goal state after:
case single
R : Type u_2
inst✝² : CommRing R
S : Type u_8
inst✝¹ : CommRing S
inst✝ : Algebra S R
x : R
i : ℕ
m : S
⊢ x ^ i * (algebraMap S R) m = (eval x) (single R i ((Algebra.linearMap S R) m))
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
i : ℕ
m : M
⊢ (eval p) ((map R[X] (lsingle R 0)) (single R i m)) = p ^ i • single R 0 m

Tactic:
map_single,

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
i : ℕ
m : M
⊢ (eval p) (single R[X] i ((lsingle R 0) m)) = p ^ i • single R 0 m