mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
⊢ ∀ (s : Set (CofiniteTopology α)) (f : Ultrafilter (CofiniteTopology α)),
    s ∈ ↑f → ∃ x ∈ s, ↑f ≤ pure x ∨ ↑f ≤ Filter.cofinite

Tactic:
intro s f hs

Goal state after:
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
hs : s ∈ ↑f
⊢ ∃ x ∈ s, ↑f ≤ pure x ∨ ↑f ≤ Filter.cofinite
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst✝¹] (f '' ↑A) = closure[inst✝¹] (f '' ↑B)
⊢ closure[inst✝] ↑A = ↑B

Tactic:
hf.closure_eq_preimage_closure_image,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst✝¹] (f '' ↑A) = closure[inst✝¹] (f '' ↑B)
⊢ f ⁻¹' closure[inst✝¹] (f '' ↑A) = ↑B
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
V : IrreducibleCloseds β
⊢ (fun V ↦ { carrier := f ⁻¹' ↑↑V, isIrreducible' := ⋯, isClosed' := ⋯ }) ((fun T ↦ ⟨map f ⋯ T, ⋯⟩) V) = V

Tactic:
ext
    simp [h.isOpenMap.preimage_closure_image h.injective h.continuous _ V.isClosed]

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
⊢ ∀ (c : Set (Ideal P)), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c

Tactic:
intro S

Goal state after:
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) S → S.Nonempty → ⊤ ∉ S → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds S
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
⊢ ∃ x, IsGenericPoint x t

Tactic:
obtain ⟨i, hi⟩ := hU.exists_mem x

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
⊢ ∃ x, IsGenericPoint x t
Module: Mathlib.Topology.Sober

Goal state before:
pp: case a
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (Subtype.val ⁻¹' t)
⊢ t ⊆ closure (Subtype.val '' closure {H.genericPoint})

Tactic:
H.isGenericPoint_genericPoint_closure.def

Goal state after:
case a
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (Subtype.val ⁻¹' t)
⊢ t ⊆ closure (Subtype.val '' closure (Subtype.val ⁻¹' t))
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
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
⊢ (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp (IsScalarTower.toAlgHom R A B)

Tactic:
by rw [e]; ext; rfl

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case pos
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
h : b.factorization p ≤ a.factorization p
⊢ False

pp: case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
h : ¬b.factorization p ≤ a.factorization p
⊢ False

Tactic:
· simp only [h, reduceIte, pow_eq_zero_iff', ne_eq] at H
    simpa [H.1] using H.2

Goal state after:
case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
h : ¬b.factorization p ≤ a.factorization p
⊢ False
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf : Function.Injective ⇑(ConcreteCategory.hom f)
hg : (Hom.hom g).Flat
⊢ Function.Injective ⇑(ConcreteCategory.hom (pushout.inr f g))

Tactic:
by
  algebraize [f.hom, g.hom]
  have : _ = pushout.inr f g := (CommRingCat.isPushout_tensorProduct R S T).inr_isoPushout_hom
  rw [← this]
  exact (CommRingCat.isPushout_tensorProduct R S T).isoPushout.commRingCatIsoToRingEquiv
    |>.injective.comp (Algebra.TensorProduct.includeRight_injective (B := T) hf)

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

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : zeroLocus ↑x.asIdeal ⊆ {x}
⊢ x.asIdeal.IsMaximal

pp: case mpr
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : x.asIdeal.IsMaximal
⊢ zeroLocus ↑x.asIdeal ⊆ {x}

Tactic:
· rcases x.asIdeal.exists_le_maximal x.2.1 with ⟨m, hm, hxm⟩
    exact (congr_arg asIdeal (@H ⟨m, hm.isPrime⟩ hxm)) ▸ hm

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : x.asIdeal.IsMaximal
⊢ zeroLocus ↑x.asIdeal ⊆ {x}
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1

Tactic:
intros

Goal state after:
case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
i✝ : ℕ
a✝ : i✝ ∈ (a.lcm b).factorization.support
⊢ i✝ ^ 0 = 1
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
⊢ (b⁻¹⁻¹ * b⁻¹ * b⁻¹) • D a + -((a * (b ^ 2)⁻¹) • D b) = ((b ^ 2)⁻¹ * b) • D a + -(((b ^ 2)⁻¹ * a) • D b)

Tactic:
inv_inv

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
⊢ (b * b⁻¹ * b⁻¹) • D a + -((a * (b ^ 2)⁻¹) • D b) = ((b ^ 2)⁻¹ * b) • D a + -(((b ^ 2)⁻¹ * a) • D b)
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
h : D b = 0
⊢ ((b ^ 2)⁻¹ * b) • D a = (b⁻¹ * b⁻¹ * b⁻¹⁻¹) • D a

Tactic:
inv_inv

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
h : D b = 0
⊢ ((b ^ 2)⁻¹ * b) • D a = (b⁻¹ * b⁻¹ * b) • D a
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ exponent G ≠ 0 ↔ ExponentExists G

Tactic:
by
  rw [exponent]
  split_ifs with h
  · simp [h]
  --if this isn't done this way, `to_additive` freaks
  · tauto

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
this : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
⊢ (range (comap (algebraMap R[X] (Away c)[X])))ᶜ = range (comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Tactic:
have := Polynomial.isLocalization (.powers c) (Away c)

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.map C (Submonoid.powers c)) (Away c)[X]
⊢ (range (comap (algebraMap R[X] (Away c)[X])))ᶜ = range (comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
⊢ (range (comap (algebraMap R[X] (Away c)[X])))ᶜ = range (comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Tactic:
let := (mapRingHom (algebraMap R (Away c))).toAlgebra
  have := Polynomial.isLocalization (.powers c) (Away c)
  rw [Submonoid.map_powers] at this
  have surj : Function.Surjective (mapRingHom (Ideal.Quotient.mk (.span {c}))) :=
    Polynomial.map_surjective _ Ideal.Quotient.mk_surjective
  rw [range_comap_of_surjective _ _ surj, localization_away_comap_range _ (C c)]
  simp [Polynomial.ker_mapRingHom, Ideal.map_span]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
Z : Set (PrimeSpectrum S)
hZ : IsClosed Z
hf : StableUnderSpecialization (comap f '' Z)
⊢ IsClosed (comap f '' Z)

Tactic:
by
  obtain ⟨I, rfl⟩ := (PrimeSpectrum.isClosed_iff_zeroLocus_ideal Z).mp hZ
  refine (isClosed_iff_zeroLocus _).mpr ⟨I.comap f, le_antisymm ?_ fun p hp ↦ ?_⟩
  · rintro _ ⟨q, hq, rfl⟩
    exact Ideal.comap_mono hq
  · obtain ⟨q, hqI, hq, hqle⟩ := p.asIdeal.exists_ideal_comap_le_prime I hp
    exact hf ((le_iff_specializes ⟨q.comap f, inferInstance⟩ p).mp hqle) ⟨⟨q, hq⟩, hqI, rfl⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
p : PrimeSpectrum R
⊢ p ∈ ↑(basicOpen e) ↔ p ∈ zeroLocus {f}

Tactic:
suffices e ∉ p.asIdeal ↔ f ∈ p.asIdeal by simpa

Goal state after:
R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
p : PrimeSpectrum R
⊢ e ∉ p.asIdeal ↔ f ∈ p.asIdeal
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 α)
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]

Tactic:
calc
      card α = card (Σ y : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) :=
        card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm
      _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma
      _ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_
      _ = _ := by simp

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 α)
⊢ ∑ a, card { x // Quotient.mk'' x = a } ≡ ∑ _a, 1 [MOD p]
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p✝ : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : Subgroup G
card_eq : Nat.card ↥H = p ^ (Nat.card G).factorization p
⊢ ¬p ^ ((Nat.card G).factorization p + 1) ∣ Nat.card G

Tactic:
exact Nat.pow_succ_factorization_not_dvd Nat.card_pos.ne' Fact.out

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
⊢ (∀ (x : G), x ∈ P ↔ x ∈ g • P) ↔ ∀ (h : G), h ∈ ↑P ↔ g⁻¹ * h * g⁻¹⁻¹ ∈ ↑P

Tactic:
inv_inv

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
⊢ (∀ (x : G), x ∈ P ↔ x ∈ g • P) ↔ ∀ (h : G), h ∈ ↑P ↔ g⁻¹ * h * g ∈ ↑P
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
this : Finite (Sylow p G)
⊢ ¬p ∣ (↑P).index

Tactic:
exact P.not_dvd_index' Nat.card_pos.ne'

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

Goal state before:
pp: G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
g : G
hg : zpowers g = ⊤
⊢ ∃ p, Nat.Prime p ∧ Nonempty (Additive G ≃+ ZMod p)

Tactic:
use orderOf g

Goal state after:
case h
G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
g : G
hg : zpowers g = ⊤
⊢ Nat.Prime (orderOf g) ∧ Nonempty (Additive G ≃+ ZMod (orderOf g))
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : x⁻¹ * n⁻¹⁻¹ * x ∈ H
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H

Tactic:
inv_inv

Goal state after:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x⁻¹⁻¹ = x

Tactic:
inv_inv

Goal state after:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x = x
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
⊢ ∀ (x y : ↥(normalizer ↑H)), (leftRel (comap (normalizer ↑H).subtype H)) x y ↔ (leftRel H) ↑x ↑y

Tactic:
intros

Goal state after:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x✝ y✝ : ↥(normalizer ↑H)
⊢ (leftRel (comap (normalizer ↑H).subtype H)) x✝ y✝ ↔ (leftRel H) ↑x✝ ↑y✝
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : f.ker = ⊤
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic M

Tactic:
← Subgroup.topEquiv.isCyclic,

Goal state after:
case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : f.ker = ⊤
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic ↥⊤
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : 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
⊢ ∃ s_1, (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = ⟨sSup s, hx✝⟩

Tactic:
let f : s → Iic a := fun y ↦ ⟨y, hx _ y.property⟩

Goal state after:
ι : 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, ⋯⟩
⊢ ∃ s_1, (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = ⟨sSup s, hx✝⟩
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

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

Tactic:
← Subgroup.topEquiv.isCyclic,

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

Goal state before:
pp: case refine_2.left
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Injective ⇑(noncommPiCoprod hcomm)

Tactic:
apply Subgroup.injective_noncommPiCoprod_of_iSupIndep
    apply independent_of_coprime_order hcomm
    rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne
    have hp₁' := Fact.mk (Nat.prime_of_mem_primeFactors hp₁)
    have hp₂' := Fact.mk (Nat.prime_of_mem_primeFactors hp₂)
    have hne' : p₁ ≠ p₂ := by simpa using hne
    simp only [← Nat.card_eq_fintype_card]
    apply IsPGroup.coprime_card_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup'

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
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : IsSemisimpleModule R M
P : Type u_6
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
g : P →ₗ[R] N
⊢ ∃ h, f ∘ₗ h = g

Tactic:
have ⟨m, compl⟩ := exists_isCompl (LinearMap.ker f)

Goal state after:
R : Type u_2
inst✝⁷ : Ring R
M : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : IsSemisimpleModule R M
P : Type u_6
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
g : P →ₗ[R] N
m : Submodule R M
compl : IsCompl f.ker m
⊢ ∃ h, f ∘ₗ h = g
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : R ∙ v i ⊓ Submodule.span R (Set.range fun i_1 ↦ v ↑i_1) = ⊥
⊢ r = 0

Tactic:
have : r • v i ∈ (⊥ : Submodule R M) := by
    rw [← hv, Submodule.mem_inf]
    refine ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, ?_⟩
    convert! hi
    ext
    simp

Goal state after:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : R ∙ v i ⊓ Submodule.span R (Set.range fun i_1 ↦ v ↑i_1) = ⊥
this : r • v i ∈ ⊥
⊢ r = 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
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
⊢ Disjoint ((fun i ↦ torsionBySet R M ↑(p i)) i) (T.sup fun i ↦ torsionBySet R M ↑(p i))

Tactic:
disjoint_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
⊢ ((fun i ↦ torsionBySet R M ↑(p i)) i ⊓ T.sup fun i ↦ torsionBySet R M ↑(p i)) = ⊥
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: 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
hn : N.FG
hin : N ≤ I • N
r : R
hr : r - 1 ∈ I
hr' : ∀ n ∈ N, r • n = 0
⊢ ∃ r ∈ I, ∀ n ∈ N, r • n = n

Tactic:
exact ⟨-(r - 1), I.neg_mem hr, fun n hn => by simpa [sub_smul] using hr' n hn⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a b c : M₁ ⟶ M₂), a + b + c = a + (b + c)

Tactic:
intros

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ b✝ c✝ : M₁ ⟶ M₂
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a : M₁ ⟶ M₂), 0 + a = a

Tactic:
intros

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ : M₁ ⟶ M₂
⊢ 0 + a✝ = a✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a : M₁ ⟶ M₂), a + 0 = a

Tactic:
intros

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ : M₁ ⟶ M₂
⊢ a✝ + 0 = a✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a b : M₁ ⟶ M₂), a - b = a + -b

Tactic:
intros

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ b✝ : M₁ ⟶ M₂
⊢ a✝ - b✝ = a✝ + -b✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a : M₁ ⟶ M₂), -a + a = 0

Tactic:
intros

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ : M₁ ⟶ M₂
⊢ -a✝ + a✝ = 0
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a b : M₁ ⟶ M₂), a + b = b + a

Tactic:
intros

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ b✝ : M₁ ⟶ M₂
⊢ a✝ + b✝ = b✝ + a✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
f : unit R ⟶ M
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y),
    (ConcreteCategory.hom (M.map f_1)) ((ConcreteCategory.hom (f.app X)) 1) = (ConcreteCategory.hom (f.app Y)) 1

Tactic:
intros

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
f : unit R ⟶ M
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (M.map f✝)) ((ConcreteCategory.hom (f.app X✝)) 1) = (ConcreteCategory.hom (f.app Y✝)) 1
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (m + n) • s = x✝ + n • s + m • s

Tactic:
add_comm m n,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (n + m) • s = x✝ + n • s + m • s
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
hf : C.d 1 0 ≫ f = 0
⊢ ((C.toSingle₀Equiv X).symm ⟨f, hf⟩).f 0 = f

Tactic:
by
  simp [toSingle₀Equiv]

Goal state after:
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f : C.X 0 ⟶ X
⊢ ((C.toSingle₀Equiv X).symm f).f 0 = f

Tactic:
by
  simp [toSingle₀Equiv]

Goal state after:
Module: Mathlib.Algebra.Homology.Additive

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f✝ : C ⟶ D
i : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X✝ Y✝ : W₁
f : X✝ ⟶ Y✝
⊢ (single W₁ c j ⋙ F.mapHomologicalComplex c).map f ≫
      { hom := { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ },
          inv := { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom =
    { hom := { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ },
          inv := { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      (F ⋙ single W₂ c j).map f

Tactic:
ext i
      dsimp
      split_ifs with h
      · subst h
        simp [single_map_f_self, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]
      · apply (isZero_single_obj_X c j _ _ h).eq_of_tgt

Goal state after: