mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H
y✝ : G ⧸ H
y : G
hy : Quotient.mk'' y ∈ orbit ↥H ↑x
b : G
hb₁ : b ∈ H
hb₂✝ : (fun m ↦ m • ↑x) ⟨b, hb₁⟩ = Quotient.mk'' y
hb₂ : x * ((b * x)⁻¹ * y) * x⁻¹ ∈ H
⊢ b⁻¹ * (x * (y⁻¹ * x)⁻¹ * x⁻¹) ∈ H

Tactic:
simpa using

Goal state after:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H
y✝ : G ⧸ H
y : G
hy : Quotient.mk'' y ∈ orbit ↥H ↑x
b : G
hb₁ : b ∈ H
hb₂✝ : (fun m ↦ m • ↑x) ⟨b, hb₁⟩ = Quotient.mk'' y
hb₂ : x * ((b * x)⁻¹ * y) * x⁻¹ ∈ H
⊢ b⁻¹ * (y * x⁻¹) ∈ H
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : ↑b ≤ iSup (Subtype.val ∘ s)
t : Finset ι
ht : ↑b ≤ ⨆ a_1 ∈ t, (Subtype.val ∘ s) a_1
⊢ ↑b ≤ ↑(⨆ a_1 ∈ t, s a_1)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : ↑b ≤ iSup (Subtype.val ∘ s)
t : Finset ι
ht : ↑b ≤ ⨆ a_1 ∈ t, (Subtype.val ∘ s) a_1
⊢ ↑b ≤ ⨆ i ∈ t, ↑(s i)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
cyc✝ : IsCyclic (M × N)
inst✝¹ : Finite M
inst✝ : Finite N
hM✝ : IsCyclic M
hN✝ : IsCyclic N
x✝² : CommGroup (M × N) := IsCyclic.commGroup
cyc : (Monoid.exponent M).lcm (Monoid.exponent N) = Nat.card M * Nat.card N
x✝¹ : CommGroup M := IsCyclic.commGroup
hM : Monoid.exponent M = Nat.card M
x✝ : CommGroup N := IsCyclic.commGroup
hN : Monoid.exponent N = Nat.card N
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
simpa using

Goal state after:
M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
cyc✝ : IsCyclic (M × N)
inst✝¹ : Finite M
inst✝ : Finite N
hM✝ : IsCyclic M
hN✝ : IsCyclic N
x✝² : CommGroup (M × N) := IsCyclic.commGroup
cyc : (Monoid.exponent M).lcm (Monoid.exponent N) = Nat.card M * Nat.card N
x✝¹ : CommGroup M := IsCyclic.commGroup
hM : Monoid.exponent M = Nat.card M
x✝ : CommGroup N := IsCyclic.commGroup
hN : Monoid.exponent N = Nat.card N
⊢ (Nat.card M).Coprime (Nat.card N)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inl
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod 0)
h✝ : Infinite N
f : ZMod 0 →+ ZMod 2 := (ZMod.castHom ⋯ (ZMod 2)).toAddMonoidHom
hf : Function.Surjective ⇑(ZMod.castHom ⋯ (ZMod 2))
this : IsAddCyclic (ZMod 2 × ZMod 2)
⊢ False

Tactic:
simpa using

Goal state after:
case inl
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod 0)
h✝ : Infinite N
f : ZMod 0 →+ ZMod 2 := (ZMod.castHom ⋯ (ZMod 2)).toAddMonoidHom
hf : Function.Surjective ⇑(ZMod.castHom ⋯ (ZMod 2))
this : IsAddCyclic (ZMod 2 × ZMod 2)
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h✝ : Finite N
ZN : Type := ZMod (Nat.card N)
this : IsAddCyclic (ZMod (Nat.card N) × ZN)
⊢ Nat.card N = 1

Tactic:
simpa using

Goal state after:
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h✝ : Finite N
ZN : Type := ZMod (Nat.card N)
this : IsAddCyclic (ZMod (Nat.card N) × ZN)
⊢ Nat.card N = 1
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, ⋯⟩
b : α
⊢ b ∈ Subtype.val '' range f ↔ b ∈ s

Tactic:
simpa using

Goal state after:
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, ⋯⟩
b : α
⊢ b ∈ s → b ≤ a
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
H' : Subgroup G
H'H : H' ≤ H
H'card : Nat.card ↥H' = p ^ m
⊢ Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'

Tactic:
simpa using

Goal state after:
G : Type u
inst✝ : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
H' : Subgroup G
H'H : H' ≤ H
H'card : Nat.card ↥H' = p ^ m
⊢ p ^ m ≤ k ∧ k < p * p ^ m
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
g : G
hg : g ∈ (↑H \ {1}).toFinset
⊢ g ∈ H ∧ g ≠ 1

Tactic:
simpa using

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
g : G
hg : g ∈ (↑H \ {1}).toFinset
⊢ g ∈ H ∧ ¬g = 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
g : G
hg✝ : g ∈ (↑H \ {1}).toFinset
hg : g ∈ H
hg1 : g ≠ 1
⊢ p ∣ orderOf g

Tactic:
simpa using

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
g : G
hg✝ : g ∈ (↑H \ {1}).toFinset
hg : g ∈ H
hg1 : g ≠ 1
⊢ p ∣ orderOf g
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: 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 ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : ⟨p₁, hp₁⟩ ≠ ⟨p₂, hp₂⟩
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ p₁ ≠ p₂

Tactic:
simpa using

Goal state after:
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 ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : ⟨p₁, hp₁⟩ ≠ ⟨p₂, hp₂⟩
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ ¬p₁ = p₂
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: 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 ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : ⟨p₁, hp₁⟩ ≠ ⟨p₂, hp₂⟩
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ p₁ ≠ p₂

Tactic:
simpa using

Goal state after:
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 ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : ⟨p₁, hp₁⟩ ≠ ⟨p₂, hp₂⟩
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ ¬p₁ = p₂
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ x ≤ y ∨ y ≤ x

Tactic:
rcases Set.mem_range.1 hx with ⟨i, rfl⟩

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
y : X
hy : y ∈ s
i : Fin (s.length + 1)
hx : s.toFun i ∈ s
⊢ s.toFun i ≤ y ∨ y ≤ s.toFun i
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
⊢ ↑i ≠ s.length

Tactic:
simpa using

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
⊢ ¬↑i = s.length
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : s₁.Equivalent s₂
i : Fin s₂.length
⊢ Iso (s₁.toFun ((Exists.choose h).symm i).castSucc, s₁.toFun ((Exists.choose h).symm i).succ)
    (s₂.toFun i.castSucc, s₂.toFun i.succ)

Tactic:
simpa using

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : s₁.Equivalent s₂
i : Fin s₂.length
⊢ Iso (s₁.toFun ((Exists.choose h).symm i).castSucc, s₁.toFun ((Exists.choose h).symm i).succ)
    (s₂.toFun i.castSucc, s₂.toFun i.succ)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i✝ : Fin (smash s₁ s₂ hs).length
i : Fin s₁.length
⊢ Iso ((smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).succ)
    ((smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).castSucc,
      (smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).succ)

Tactic:
simpa using

Goal state after:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i✝ : Fin (smash s₁ s₂ hs).length
i : Fin s₁.length
⊢ Iso (s₁.toFun i.castSucc, s₁.toFun i.succ)
    (t₁.toFun ((Exists.choose h₁) i).castSucc, t₁.toFun ((Exists.choose h₁) i).succ)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i✝ : Fin (smash s₁ s₂ hs).length
i : Fin s₂.length
⊢ Iso ((smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).succ)
    ((smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).castSucc,
      (smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).succ)

Tactic:
simpa using

Goal state after:
case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i✝ : Fin (smash s₁ s₂ hs).length
i : Fin s₂.length
⊢ Iso (s₂.toFun i.castSucc, s₂.toFun i.succ)
    (t₂.toFun ((Exists.choose h₂) i).castSucc, t₂.toFun ((Exists.choose h₂) i).succ)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).castSucc, (snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).succ)
    ((snoc s₂ x₂ hsat₂).toFun (Fin.last s₂.length).castSucc, (snoc s₂ x₂ hsat₂).toFun (Fin.last s₂.length).succ)

Tactic:
simpa using

Goal state after:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso (last s₁, x₁) (last s₂, x₂)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i✝ : Fin (snoc s₁ x₁ hsat₁).length
i : Fin (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc.castSucc, (snoc s₁ x₁ hsat₁).toFun i.castSucc.succ)
    ((snoc s₂ x₂ hsat₂).toFun ((Exists.choose hequiv) i).castSucc.castSucc,
      (snoc s₂ x₂ hsat₂).toFun ((Exists.choose hequiv) i).castSucc.succ)

Tactic:
simpa using

Goal state after:
case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i✝ : Fin (snoc s₁ x₁ hsat₁).length
i : Fin (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)
⊢ Iso (s₁.toFun i.castSucc, s₁.toFun i.succ)
    (s₂.toFun ((Exists.choose hequiv) i).castSucc, s₂.toFun ((Exists.choose hequiv) i).succ)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : s₁.Equivalent s₂
⊢ s₁.length = s₂.length

Tactic:
simpa using

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : s₁.Equivalent s₂
⊢ s₁.length = s₂.length
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✝ : IsSemisimpleModule R M
N : Submodule R M
⊢ sSup {m | IsSimpleModule R ↥m ∧ m ≤ N} = N

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
N : Submodule R M
⊢ sSup {m | IsAtom m ∧ m ≤ N} = N
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✝¹ : IsSemisimpleModule R M
inst✝ : Nontrivial M
⊢ ∃ m, IsSimpleModule R ↥m

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝⁴ : Ring R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Nontrivial M
⊢ ∃ m, IsAtom m
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✝ : IsSemisimpleModule R M
⊢ sSup {m | IsSimpleModule R ↥m} = ⊤

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ sSup {m | IsAtom m} = ⊤
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 using

Goal state after:
ι : 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 (Submodule R ↥(p i))
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₂
⊢ ¬0 < s₂.length → ¬0 < s₁.length

Tactic:
simpa using

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₂
⊢ s₂.length = 0 → s₁.length = 0
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
R : Type u_6
inst✝² : DivisionRing R
inst✝¹ : Module R M
inst✝ : Nontrivial M
v : M
hv : v ≠ 0
w : M
f : M →ₗ[R] M
eq : f ∘ₗ toSpanSingleton R M v = toSpanSingleton R M w
⊢ (toSpanSingleton (Module.End R M) M v) f = w

Tactic:
simpa using

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
R : Type u_6
inst✝² : DivisionRing R
inst✝¹ : Module R M
inst✝ : Nontrivial M
v : M
hv : v ≠ 0
w : M
f : M →ₗ[R] M
eq : f ∘ₗ toSpanSingleton R M v = toSpanSingleton R M w
⊢ f v = w
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:
simpa using

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (R ∙ x).annihilator = (LinearMap.toSpanSingleton R M x).ker
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
t : CompositionSeries X
htb : head t = (eraseLast s).head
htl : t.length + 1 = n
htt : last t = x ⊓ (eraseLast s).last
hteqv : Equivalent (eraseLast s) (snoc t (eraseLast s).last ⋯)
hmtx : IsMaximal (last t) x
⊢ ((snoc t (eraseLast s).last ⋯).last, last s) ∈ {(x, y) | IsMaximal x y}

Tactic:
simpa using

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
t : CompositionSeries X
htb : head t = (eraseLast s).head
htl : t.length + 1 = n
htt : last t = x ⊓ (eraseLast s).last
hteqv : Equivalent (eraseLast s) (snoc t (eraseLast s).last ⋯)
hmtx : IsMaximal (last t) x
⊢ IsMaximal (s.toFun ⟨s.length - 1, ⋯⟩) (last s)
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) = ⊥
this : r • v i ∈ ⊥
⊢ r ∈ torsionOf R M (v i)

Tactic:
simpa using

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 • v i = 0
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: case add
R : Type u_2
inst✝⁴ : Ring R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite (End R M) M
s : Finset M
hs : span (End R M) ↑s = ⊤
f : End (End R M) M
r : R
hr : ∀ m ∈ s, f m = r • m
m x✝ y✝ : M
hx✝ : x✝ ∈ span (End R M) ↑s
hy✝ : y✝ ∈ span (End R M) ↑s
h₁ : ((toModuleEnd (End R M) M) r) x✝ = f x✝
h₂ : ((toModuleEnd (End R M) M) r) y✝ = f y✝
⊢ ((toModuleEnd (End R M) M) r) (x✝ + y✝) = f (x✝ + y✝)

Tactic:
simpa using

Goal state after:
case add
R : Type u_2
inst✝⁴ : Ring R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite (End R M) M
s : Finset M
hs : span (End R M) ↑s = ⊤
f : End (End R M) M
r : R
hr : ∀ m ∈ s, f m = r • m
m x✝ y✝ : M
hx✝ : x✝ ∈ span (End R M) ↑s
hy✝ : y✝ ∈ span (End R M) ↑s
h₁ : ((toModuleEnd (End R M) M) r) x✝ = f x✝
h₂ : ((toModuleEnd (End R M) M) r) y✝ = f y✝
⊢ r • x✝ + r • y✝ = f x✝ + f y✝