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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : M →ₗ[A] N
⊢ (r • D).compDer = (RingHom.id A) r • D.compDer

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : M →ₗ[A] N
x✝ : Derivation R A M
a✝ : A
⊢ ((r • D).compDer x✝) a✝ = (((RingHom.id A) r • D.compDer) x✝) a✝
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum R
⊢ (primeSpectrumProd R S).symm (Sum.inl x) = comap (RingHom.fst R S) x

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum R
x✝ : R × S
⊢ x✝ ∈ ((primeSpectrumProd R S).symm (Sum.inl x)).asIdeal ↔ x✝ ∈ (comap (RingHom.fst R S) x).asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum S
⊢ (primeSpectrumProd R S).symm (Sum.inr x) = comap (RingHom.snd R S) x

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum S
x✝ : R × S
⊢ x✝ ∈ ((primeSpectrumProd R S).symm (Sum.inr x)).asIdeal ↔ x✝ ∈ (comap (RingHom.snd R S) x).asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
⊢ ↑(Submonoid.powers r) ⊓ ↑x.asIdeal ⊆ ⊥ ↔ r ∉ x.asIdeal

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
⊢ ↑(Submonoid.powers r) ⊓ ↑x.asIdeal ⊆ ⊥ → r ∉ x.asIdeal

case mpr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
⊢ r ∉ x.asIdeal → ↑(Submonoid.powers r) ⊓ ↑x.asIdeal ⊆ ⊥
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
⊢ IsCyclic α ↔ ∃ g, zpowers g = ⊤

Tactic:
by
  simp only [eq_top_iff', mem_zpowers_iff]
  exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ IsCyclic ↥H ↔ ∃ g, zpowers g = H

Tactic:
rw [isCyclic_iff_exists_zpowers_eq_top]

Goal state after:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ g, zpowers g = ⊤) ↔ ∃ g, zpowers g = H
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
constructor

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

case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
⊢ (∀ (g : G), g ^ n = 1) → exponent G ∣ n
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
q : PrimeSpectrum (R i)
hp : comap (Pi.evalRingHom R i) q ∈ ↑(basicOpen (Pi.single i f))
⊢ comap (Pi.evalRingHom R i) q = comap (Pi.evalRingHom R i) q

Tactic:
ext

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
q : PrimeSpectrum (R i)
hp : comap (Pi.evalRingHom R i) q ∈ ↑(basicOpen (Pi.single i f))
x✝ : (i : ι) → R i
⊢ x✝ ∈ (comap (Pi.evalRingHom R i) q).asIdeal ↔ x✝ ∈ (comap (Pi.evalRingHom R i) q).asIdeal
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
⊢ DenseRange (comap f) ↔ ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ DenseRange (comap f) → ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)

case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ (∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)) →
    DenseRange (comap f)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_3
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ p ∣ exponent G

Tactic:
· obtain ⟨g, hg⟩ := exists_ne (1 : G)
    simpa [h g hg] using Monoid.order_dvd_exponent g

Goal state after:
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)
H : Subgroup G
inst✝ : H.FiniteIndex
⊢ ∃ n, H.index = p ^ n

Tactic:
obtain ⟨n, hn⟩ := iff_card.mp (hG.to_quotient H.normalCore)
  obtain ⟨k, _, hk2⟩ :=
    (Nat.dvd_prime_pow hp.out).mp
      ((congr_arg _ (H.normalCore.index_eq_card.trans hn)).mp
        (Subgroup.index_dvd_of_le H.normalCore_le))
  exact ⟨k, hk2⟩

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
⊢ (fun x ↦ x ^ n) '' ↑I ⊆ ↑(I ^ n ⊔ J ^ n) ∧ (fun x ↦ x ^ n) '' ↑J ⊆ ↑(I ^ n ⊔ J ^ n)

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
⊢ Ideal.span (↑I ∪ ↑J) = ⊤

Tactic:
constructor

Goal state after:
case left
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) '' ↑I ⊆ ↑(I ^ n ⊔ J ^ n)

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)

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
⊢ Ideal.span (↑I ∪ ↑J) = ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
⊢ Algebra.IsIntegral R S

Tactic:
constructor

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := ⋯
a✝¹ : Nontrivial R
a✝ : Nontrivial S
⊢ ∀ (x : S), IsIntegral R x
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
⊢ (b.reverse * X ^ (1 + c.natDegree)).Monic

Tactic:
refine Monic.mul ?_ (by simp)
    have h : b.coeff 0 = 1 := by simpa using! congr(($e).coeff 0)
    have : b.natTrailingDegree = 0 := by simp [h]
    rw [Monic.def, reverse_leadingCoeff, trailingCoeff, this, h]

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

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
⊢ Module (ZMod n) M

Tactic:
have h_mod (c : ℕ) (x : M) : (c % n) • x = c • x := by
    suffices (c % n + c / n * n) • x = c • x by rwa [add_nsmul, mul_nsmul, h, add_zero] at this
    rw [Nat.mod_add_div']
  have := NeZero.ne n
  match n with
  | n + 1 => exact {
    smul := fun (c : Fin _) x ↦ c.val • x
    smul_zero := fun _ ↦ nsmul_zero _
    zero_smul := fun _ ↦ zero_nsmul _
    smul_add := fun _ _ _ ↦ nsmul_add _ _ _
    one_smul := fun _ ↦ (h_mod _ _).trans <| one_nsmul _
    add_smul := fun _ _ _ ↦ (h_mod _ _).trans <| add_nsmul _ _ _
    mul_smul := fun _ _ _ ↦ (h_mod _ _).trans <| mul_nsmul' _ _ _
  }

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
S : Type u_4
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₁
inst✝¹ : SetLike S M
inst✝ : AddSubgroupClass S M
x : M
K : S
f₁ f₂ : M →+ M₁
⊢ toZModLinearMap n (f₁ + f₂) = toZModLinearMap n f₁ + toZModLinearMap n f₂

Tactic:
ext

Goal state after:
n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
S : Type u_4
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₁
inst✝¹ : SetLike S M
inst✝ : AddSubgroupClass S M
x : M
K : S
f₁ f₂ : M →+ M₁
x✝ : M
⊢ (toZModLinearMap n (f₁ + f₂)) x✝ = (toZModLinearMap n f₁ + toZModLinearMap n f₂) x✝
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
constructor

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

case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) → vanishingIdeal s ∈ minimalPrimes R
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U ↔ U = ⊤

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → U = ⊤

case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ U = ⊤ → closedPoint R ∈ U
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
P : Sylow p G
⊢ stabilizer G P = normalizer ↑P

Tactic:
ext

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
P : Sylow p G
x✝ : G
⊢ x✝ ∈ stabilizer G P ↔ x✝ ∈ normalizer ↑P
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
⊢ y ^ (-m) * a ∈ f.ker

Tactic:
by rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x m, hm, inv_mul_cancel]

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

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
⊢ ((zmultiplesHom G) g).ker = zmultiples ↑(addOrderOf g)

Tactic:
ext

Goal state after:
G : Type u_2
inst✝ : AddGroup G
g : G
x✝ : ℤ
⊢ x✝ ∈ ((zmultiplesHom G) g).ker ↔ x✝ ∈ zmultiples ↑(addOrderOf g)
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
tG : IsMulTorsion G
⊢ torsion G = ⊤

Tactic:
ext

Goal state after:
G : Type u_1
inst✝ : CommMonoid G
tG : IsMulTorsion G
x✝ : G
⊢ x✝ ∈ torsion G ↔ x✝ ∈ ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

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

Tactic:
constructor

Goal state after:
case h.left
G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
g : G
hg : zpowers g = ⊤
⊢ Nat.Prime (Nat.card G)

case h.right
G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
g : G
hg : zpowers g = ⊤
⊢ Nonempty (Additive G ≃+ ZMod (Nat.card G))
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
inst✝³ : LE α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.univ = {⊤, ⊥}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝³ : LE α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
a✝ : α
⊢ a✝ ∈ Finset.univ ↔ a✝ ∈ {⊤, ⊥}
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : {x | a ⋖ x}.Finite
h : ∀ (b : α), a ⋖ b → (Set.Ici b).Finite
b : α
hb : b ∈ Set.Ici a \ {a}
⊢ b ∈ ⋃ i ∈ {x | a ⋖ x}, Set.Ici i

Tactic:
obtain ⟨x, hax, hxb⟩ := ((show a ≤ b from hb.1).lt_of_ne (Ne.symm hb.2)).exists_covby_le

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : {x | a ⋖ x}.Finite
h : ∀ (b : α), a ⋖ b → (Set.Ici b).Finite
b : α
hb : b ∈ Set.Ici a \ {a}
x : α
hax : a ⋖ x
hxb : x ≤ b
⊢ b ∈ ⋃ i ∈ {x | a ⋖ x}, Set.Ici i
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_2
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝ : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
⊢ IsCyclic (M × N)

Tactic:
· let f := MonoidHom.snd M N
    let e : f.ker ≃* M := by
      rw [MonoidHom.ker_snd]
      exact ((Subgroup.prodEquiv ..).trans .prodUnique).trans Subgroup.topEquiv
    let _ := hM.commGroup; let _ := hN.commGroup
    rw [← e.isCyclic] at hM
    rw [← Nat.card_congr e.toEquiv] at h
    exact isCyclic_of_coprime_card_ker f h Prod.snd_surjective

Goal state after:
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: 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 ∈ Finset.cons a t hat, ↑(μ i) = 1) ↔
    ((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤

Tactic:
constructor

Goal state after:
case refine_2.mp
ι : 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 ∈ Finset.cons a t hat, ↑(μ i) = 1) →
    ((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤

case refine_2.mpr
ι : 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 = ⊤
⊢ (((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤) →
    ∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_2
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) ∧ Fintype.card ((i : ↥ps) → ↥↑(P ↑i)) = Fintype.card G

Tactic:
constructor

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

case refine_2.right
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
⊢ Fintype.card ((i : ↥ps) → ↥↑(P ↑i)) = Fintype.card G
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i ↦ s.toFun ⟨↑i, ⋯⟩) ↔ x ≠ last s ∧ x ∈ range s.toFun

Tactic:
constructor

Goal state after:
case mp
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i ↦ s.toFun ⟨↑i, ⋯⟩) → x ≠ last s ∧ x ∈ range s.toFun

case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ≠ last s ∧ x ∈ range s.toFun → x ∈ range fun i ↦ s.toFun ⟨↑i, ⋯⟩
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 : N →ₗ[R] M
hf : Function.Injective ⇑f
g : N →ₗ[R] P
m : Submodule R M
compl : IsCompl f.range m
⊢ (g ∘ₗ LinearMap.linearProjOfIsCompl m f hf compl) ∘ₗ f = g

Tactic:
ext

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 : N →ₗ[R] M
hf : Function.Injective ⇑f
g : N →ₗ[R] P
m : Submodule R M
compl : IsCompl f.range m
x✝ : N
⊢ ((g ∘ₗ LinearMap.linearProjOfIsCompl m f hf compl) ∘ₗ f) x✝ = g x✝
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp' : ⨆ i ∈ s, p i = ⊤
hp : ∀ i ∈ s, ComplementedLattice (Submodule R ↥(p i))
i : ι
hi : i ∈ s
⊢ ComplementedLattice ↑(Set.Iic (p i))

Tactic:
simpa only [← (p i).mapIic.complementedLattice_iff] using hp i hi

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁0 : s₁.length = 0
this✝ : ∀ (x : X), x ∈ s₁ ↔ x = last s₁
this : ∀ (x : X), x ∈ s₂ ↔ x = last s₂
⊢ s₁ = s₂

Tactic:
ext

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁0 : s₁.length = 0
this✝ : ∀ (x : X), x ∈ s₁ ↔ x = last s₁
this : ∀ (x : X), x ∈ s₂ ↔ x = last s₂
x✝ : X
⊢ x✝ ∈ s₁ ↔ x✝ ∈ s₂
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
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
a : Module.End R M
a0 : a ≠ 0
⊢ a * ↑(LinearEquiv.ofBijective a ⋯).symm = 1

Tactic:
ext

Goal state after:
ι : 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
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
a : Module.End R M
a0 : a ≠ 0
x✝ : M
⊢ (a * ↑(LinearEquiv.ofBijective a ⋯).symm) x✝ = 1 x✝
Module: Mathlib.Algebra.Module.Torsion.Basic

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

Tactic:
by
  simpa [torsionOf] using Submodule.annihilator_span_singleton x

Goal state after:
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
hv : iSupIndep fun i ↦ R ∙ v i
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
⊢ r = 0

Tactic:
replace hv := iSupIndep_def.mp hv i

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 : Disjoint (R ∙ v i) (⨆ j, ⨆ (_ : j ≠ i), R ∙ v j)
⊢ r = 0
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) = ⊥
⊢ (Set.range fun i_1 ↦ v ↑i_1) = v '' (Set.univ \ {i})

Tactic:
ext

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) = ⊥
x✝ : M
⊢ (x✝ ∈ Set.range fun i_1 ↦ v ↑i_1) ↔ x✝ ∈ v '' (Set.univ \ {i})
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
n : ℕ
m₁ m₂ : M
⊢ single R n (m₁ + m₂) = single R n m₁ + single R n m₂

Tactic:
ext

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m₁ m₂ : M
a✝ : ℕ
⊢ (single R n (m₁ + m₂)).coeff a✝ = (single R n m₁ + single R n m₂).coeff a✝