mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

Goal state after:
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)
⊢ _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
e : X × X → X × X → Prop
h_refl : ∀ {x : X × X}, e x x
h_symm : ∀ {x y : X × X}, e x y → e y x
h_trans : ∀ {x y z : X × X}, e x y → e y z → e x z
h_rel : ∀ {x y : X}, IsMaximal x (x ⊔ y) → e (x, x ⊔ y) (x ⊓ y, y)
x y : X × X
h_iso : Iso x y
⊢ e x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (x ⊔ y)
hyz : IsMaximal y (x ⊔ y)
⊢ IsMaximal (x ⊓ y) y

Tactic:
rw [inf_comm]

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (x ⊔ y)
hyz : IsMaximal y (x ⊔ y)
⊢ IsMaximal (y ⊓ x) y
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:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (x ⊔ y)
hyz : IsMaximal y (x ⊔ y)
⊢ IsMaximal (x ⊓ y) y

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : IsMaximal x b
hyb : IsMaximal y b
⊢ IsMaximal a y

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : IsMaximal x b
hyb : IsMaximal y b
⊢ IsMaximal a y

Tactic:
by
  have hb : x ⊔ y = b := sup_eq_of_isMaximal hxb hyb hxy
  subst a b
  exact isMaximal_inf_right_of_isMaximal_sup hxb hyb

Goal state after:
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, Nat.card ↥↑(P ↑p) = ∏ p, ↑p ^ (Nat.card G).factorization ↑p

Tactic:
by

Goal state after:
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
⊢ ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥P) ≃* G

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y a b : X
hm : IsMaximal x a
ha : x ⊔ y = a
hb : x ⊓ y = b
⊢ Iso (x, a) (b, y)

Tactic:
by

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

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ List.IsChain (fun x1 x2 ↦ x1 < x2) (toList s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ s₁ = s₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ (eraseLast s).last ≤ last s

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
hi : ↑i < (s.length - 1).succ
⊢ (eraseLast s).toFun ⟨↑i, hi⟩ = s.toFun i

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hx : x ≠ last s
hxs : x ∈ s
⊢ x ∈ eraseLast s

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ ↑i < s.length

Tactic:
by

Goal state after:
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 ∈ eraseLast s ↔ x ≠ last s ∧ x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
⊢ s.length - 1 < s.length

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
⊢ IsMaximal (eraseLast s).last (last s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
⊢ s = (eraseLast s).snoc (last s) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : IsMaximal (eraseLast s).last (last s)
hs : s.length = 0
⊢ last s = (eraseLast s).last

Tactic:
by

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

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: 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),
    Iso ((smash s₁ s₂ hs).toFun i.castSucc, (smash s₁ s₂ hs).toFun i.succ)
      ((smash t₁ t₂ ht).toFun (e i).castSucc, (smash t₁ t₂ ht).toFun (e i).succ)

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: 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
⊢ e (Fin.last s₁.length) = Fin.last s₂.length

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: 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
j : Fin s₁.length
⊢ e j.castSucc = ((Exists.choose hequiv) j).castSucc

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: 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₂)
⊢ Equivalent (snoc s₁ x₁ hsat₁) (snoc s₂ x₂ hsat₂)

Tactic:
by

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

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
⊢ ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
⊢ ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
⊢ ∃ y, 0 ≠ y

Tactic:
by

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

Goal state before:
pp: 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
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module S N
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] N
hl : Function.Bijective ⇑l
⊢ IsSimpleModule R M ↔ IsSimpleModule S N

Tactic:
by

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

Goal state before:
pp: S : Type u_3
inst✝⁶ : Ring S
M : Type u_4
inst✝⁵ : AddCommGroup M
R : Type u_6
inst✝⁴ : CommRing R
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
h : Function.Surjective ⇑(algebraMap R S)
⊢ IsSimpleModule R M ↔ IsSimpleModule S M

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ IsSimpleModule R ↥m ↔ IsAtom m

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ IsSimpleModule R (M ⧸ m) ↔ IsCoatom m

Tactic:
by

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
A B : Submodule R M
hAB : A ≤ B
⊢ A ⋖ B ↔ IsSimpleModule R (↥B ⧸ Submodule.comap B.subtype A)

Tactic:
by

Goal state after:
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✝ : IsSimpleModule R M
S : Submodule R M
⊢ ∃ a, S = R ∙ a

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ Function.Surjective ⇑(toSpanSingleton R M m)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ Ideal.IsMaximal (toSpanSingleton R M m).ker

Tactic:
by

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
⊢ IsSimpleModule R M ↔ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝² : AddCommGroup M
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R M
simple : IsSimpleModule R M
⊢ (Module.annihilator R M).IsMaximal

Tactic:
by

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
x✝¹ : Nontrivial M ∧ ∀ (x : M), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M x)
left✝ : Nontrivial M
h : ∀ (x : M), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M x)
m : Submodule R M
ne_bot : ¬m = ⊥
x : M
hxm : x ∈ m
hx0 : x ≠ 0
z : M
x✝ : z ∈ ⊤
⊢ z ∈ m

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
⊢ (∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)) ↔ ∀ (x : R), x ≠ 0 → IsUnit x

Tactic:
by

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
h : sSup {m | IsSimpleModule R ↥m} = ⊤
⊢ sSup {a | IsAtom a} = ⊤

Tactic:
by

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 : Submodule R M
inst✝ : IsSemisimpleModule R ↥N
⊢ N = ⊥ ∨ ∃ m ≤ N, IsSimpleModule R ↥m

Tactic:
by

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 : 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:
by

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:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
N : Submodule R M
⊢ sSup {m | IsSimpleModule R ↥m ∧ m ≤ N} = N

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝⁴ : Ring R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Nontrivial M
⊢ ∃ m, IsSimpleModule R ↥m

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ sSup {m | IsSimpleModule R ↥m} = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ ∃ s, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝³ : AddCommGroup M
R : Type u_6
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ (Module.annihilator R M).IsRadical

Tactic:
by

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Ring S
M' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
N' : Type u_7
inst✝² : AddCommGroup N'
inst✝¹ : Module S N'
σ : R →+* S
l : M' →ₛₗ[σ] N'
inst✝ : RingHomSurjective σ
hl : Function.Bijective ⇑l
⊢ IsSemisimpleModule R M' ↔ IsSemisimpleModule S N'

Tactic:
by

Goal state after:
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, IsSemisimpleModule R ↥(p i)
hp' : ⨆ i ∈ s, p i = ⊤
⊢ IsSemisimpleModule R M

Tactic:
by

Goal state after:
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, IsSemisimpleModule R ↥(p i)
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Tactic:
by

Goal state after:
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
p : ι → Submodule R M
hp : ∀ (i : ι), IsSemisimpleModule R ↥(p i)
hp' : ⨆ i, p i = ⊤
⊢ ⨆ i ∈ Set.univ, p i = ⊤

Tactic:
by

Goal state after:
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
ι : Type u_7
M : ι → Type u_6
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), IsSemisimpleModule R (M i)
⊢ IsSemisimpleModule R (Π₀ (i : ι), M i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_2.refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i✝ : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
i : Fin ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)
⊢ Iso
    (((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun
        (Fin.last (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)).castSucc.castSucc,
      ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun
        (Fin.last (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)).castSucc.succ)
    (((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun
        ((Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc)
            (Fin.last (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)).castSucc).castSucc,
      ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun
        ((Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc)
            (Fin.last (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)).castSucc).succ)

Tactic:
erw [Equiv.swap_apply_right, snoc_castSucc, snoc_castSucc, snoc_castSucc,
          Fin.succ_castSucc, snoc_castSucc, Fin.succ_last, last_snoc', last_snoc', last_snoc']
        exact hr₁

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ ((DFinsupp.lsum ℕ) fun i ↦ (↑i).subtype).range = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ ∃ s x, sSupIndep s ∧ ∀ (m : ↑s), IsSimpleModule R ↥↑m

Tactic:
by

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
⊢ IsSemisimpleModule R M ↔ ∃ s x, ∀ (m : ↑s), IsSimpleModule R ↥↑m

Tactic:
by

Goal state after:
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
ι : Type u_7
inst✝³ : Finite ι
M : ι → Type u_6
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), IsSemisimpleModule R (M i)
⊢ ⨆ i, (single R M i).range = ⊤

Tactic:
by

Goal state after:
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
ι : Type u_7
inst✝³ : Finite ι
M : ι → Type u_6
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), IsSemisimpleModule R (M i)
⊢ IsSemisimpleModule R ((i : ι) → M i)

Tactic:
by

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
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t ↦ Bool.rec q p t
⊢ ∀ i ∈ Set.univ, IsSemisimpleModule R ↥(f i)

Tactic:
by

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
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
⊢ IsSemisimpleModule R ↥(p ⊔ q)

Tactic:
by

Goal state after: