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

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
⊢ IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k

Tactic:
[

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
⊢ IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
⊢ IsPGroup p G ↔ ∃ n, Nat.card G = p ^ n

Tactic:
[

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
⊢ IsPGroup p G ↔ ∃ n, Nat.card G = p ^ n
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ IsPGroup p G ↔ ∃ k, ∀ (g : G), g ^ p ^ k = 1

Tactic:
[

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ IsPGroup p G ↔ ∃ k, ∀ (g : G), g ^ p ^ k = 1
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ IsPGroup p G ↔ ∃ n, Monoid.exponent G ∣ p ^ n

Tactic:
[

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ IsPGroup p G ↔ ∃ n, Monoid.exponent G ∣ p ^ n
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fact (Nat.Prime p)
⊢ IsPGroup p G ↔ ∃ n, Monoid.exponent G = p ^ n

Tactic:
[

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fact (Nat.Prime p)
⊢ IsPGroup p G ↔ ∃ n, Monoid.exponent G = p ^ n
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ⇑ϕ
⊢ IsPGroup p H

Tactic:
[

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ⇑ϕ
⊢ IsPGroup p H
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
this : 1 = (orderOf (t ^ p ^ k)).factorization p + 1
⊢ ¬p ^ 1 ∣ orderOf (t ^ p ^ k)

Tactic:
this

Goal state after:
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
this : 1 = (orderOf (t ^ p ^ k)).factorization p + 1
⊢ ¬p ^ ((orderOf (t ^ p ^ k)).factorization p + 1) ∣ orderOf (t ^ p ^ k)
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 α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : Nontrivial ↑(fixedPoints G α)
b : α
hb : b ∈ fixedPoints G α
hba : ⟨b, hb⟩ ≠ ⟨a, ha⟩
hab : a = b
⊢ ⟨b, hb⟩ = ⟨a, ha⟩

Tactic:
[

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 α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : Nontrivial ↑(fixedPoints G α)
b : α
hb : b ∈ fixedPoints G α
hba : ⟨b, hb⟩ ≠ ⟨a, ha⟩
hab : a = b
⊢ ⟨b, hb⟩ = ⟨a, ha⟩
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case H
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ a ∈ Set.range fun g ↦ orderOf g, a ≤ exponent G

Tactic:
[

Goal state after:
case H
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ a ∈ Set.range fun g ↦ orderOf g, a ≤ exponent G
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
g : G
hx : x < orderOf g
hg : orderOf g = exponent G
⊢ ∃ a ∈ Set.range fun g ↦ orderOf g, x < a

Tactic:
[

Goal state after:
case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
g : G
hx : x < orderOf g
hg : orderOf g = exponent G
⊢ ∃ a ∈ Set.range fun g ↦ orderOf g, x < a
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Group G
n : ℤ
⊢ ↑(Monoid.exponent G) ∣ n ↔ ∀ (g : G), g ^ n = 1

Tactic:
[

Goal state after:
G : Type u
inst✝ : Group G
n : ℤ
⊢ ↑(Monoid.exponent G) ∣ n ↔ ∀ (g : G), g ^ n = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Group G
n m : ℤ
⊢ ↑(Monoid.exponent G) ∣ n - m ↔ ∀ (g : G), g ^ n = g ^ m

Tactic:
[

Goal state after:
G : Type u
inst✝ : Group G
n m : ℤ
⊢ ↑(Monoid.exponent G) ∣ n - m ↔ ∀ (g : G), g ^ n = g ^ m
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
h : IsClopen s
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)

Tactic:
have ⟨e, f, h⟩ := exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen h
    exact ⟨e, f, by simp only [h, and_self]⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
h : ∀ (g : G), orderOf g ∣ 2
a b : G
⊢ Commute a b

Tactic:
[

Goal state after:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
h : ∀ (g : G), orderOf g ∣ 2
a b : G
⊢ Commute a b
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ Nat.card (G ⧸ center G) ∣ p

Tactic:
← mul_dvd_mul_iff_left (NeZero.ne p),

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ p * Nat.card (G ⧸ center G) ∣ p * p
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
hϕ : IsPGroup p ↥ϕ.ker
h : ↑P ≤ ϕ.range
Q : Subgroup K
hQ : IsPGroup p ↥Q
hle : comap ϕ ↑P ≤ Q
⊢ Q = comap ϕ ↑P

Tactic:
by
      show Q = P.1.comap ϕ
      rw [← P.3 (hQ.map ϕ) (le_trans (ge_of_eq (map_comap_eq_self h)) (map_mono hle))]
      exact (comap_map_eq_self ((P.1.ker_le_comap ϕ).trans hle)).symm

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints (↥H) (Sylow p G) ↔ H ≤ normalizer ↑P

Tactic:
[

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints (↥H) (Sylow p G) ↔ H ≤ normalizer ↑P
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : ¬0 < #{a | orderOf a = d}
⊢ False

Tactic:
[

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : ¬0 < #{a | orderOf a = d}
⊢ False
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this✝ : fixedPoints (↥↑P) (Sylow p G) = {P}
this : Nat.card ↑(fixedPoints (↥↑P) (Sylow p G)) = 1
⊢ Nat.card ↑(fixedPoints (↥↑P) (Sylow p G)) ≡ 1 [MOD p]

Tactic:
this

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this✝ : fixedPoints (↥↑P) (Sylow p G) = {P}
this : Nat.card ↑(fixedPoints (↥↑P) (Sylow p G)) = 1
⊢ 1 ≡ 1 [MOD p]
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)
h : ↥(centralizer ↑(zpowers x))
hh : h • (g • P).subtype h2 = P.subtype h1
⊢ ∃ n ∈ normalizer ↑P, g⁻¹ * x * g = n⁻¹ * x * n

Tactic:
[

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)
h : ↥(centralizer ↑(zpowers x))
hh : h • (g • P).subtype h2 = P.subtype h1
⊢ ∃ n ∈ normalizer ↑P, g⁻¹ * x * g = n⁻¹ * x * n
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 ↦ x * x_1) n 1
⊢ ↑((fun x_1 ↦ ⟨x, ⋯⟩ * x_1)^[n] 1) = ↑1

Tactic:
by
      dsimp
      rw [mul_left_iterate]
      change _ * 1 = 1
      rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk,
        (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]

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

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

Tactic:
[

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyCoatomic α
ha : (Set.Iic a).Infinite
hfin : {x | x ⋖ a}.Finite
⊢ ∃ b, b ⋖ a ∧ (Set.Iic b).Infinite

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyCoatomic α
ha : (Set.Iic a).Infinite
hfin : {x | x ⋖ a}.Finite
⊢ ∃ b, b ⋖ a ∧ (Set.Iic b).Infinite
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu' : ∀ a ∈ u, IsAtom a
hu : f i = ↑(sSup u)
⊢ f i = sSup (Subtype.val '' u)

Tactic:
[

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu' : ∀ a ∈ u, IsAtom a
hu : f i = ↑(sSup u)
⊢ f i = sSup (Subtype.val '' u)
Module: Mathlib.Order.CompactlyGenerated.Intervals

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

Tactic:
[

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

Goal state before:
pp: case a
ι : 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 : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
x✝ : ι
a✝ : x✝ ∈ t
⊢ ↑((Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ + fun i ↦ ⟨↑(μ i), ⋯⟩) x✝) =
    Pi.single (Exists.choose h) (↑(μ a)) x✝ + ↑(μ x✝)

Tactic:
rename_i i _

Goal state after:
case a
ι : 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 : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
⊢ ↑((Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ + fun i ↦ ⟨↑(μ i), ⋯⟩) i) = Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)
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:
[

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ List.IsChain (fun x1 x2 ↦ x1 < x2) (toList s)
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:
[

Goal state after:
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
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:
set f : Submodule R B ≃o Set.Iic B := B.mapIic with hf
  rw [covBy_iff_coatom_Iic hAB, isSimpleModule_iff_isCoatom, ← OrderIso.isCoatom_iff f, hf]
  simp [-OrderIso.isCoatom_iff, Submodule.map_comap_subtype, inf_eq_right.2 hAB]

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

Goal state after:
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} = ⊤
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
this : sSup {m | IsSimpleModule R ↥m} = ⊤
⊢ ∃ s, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m

Tactic:
[

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
this : sSup {m | IsSimpleModule R ↥m} = ⊤
⊢ ∃ s, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
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:
[

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

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, IsSemisimpleModule R ↥(p i)
hp' : ⨆ i ∈ s, p i = ⊤
⊢ IsSemisimpleModule R 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, IsSemisimpleModule R ↥(p i)
x1✝ : ι
x2✝ : x1✝ ∈ s
⊢ p x1✝ ≤ (⨆ i ∈ s, p i).subtype.range

Tactic:
[

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, IsSemisimpleModule R ↥(p i)
x1✝ : ι
x2✝ : x1✝ ∈ s
⊢ p x1✝ ≤ (⨆ i ∈ s, p i).subtype.range
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:
[

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
ι : 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 = ⊤
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 * if h : a = 0 then 0 else ↑(LinearEquiv.ofBijective a ⋯).symm) = 1

Tactic:
[

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
⊢ (a * if h : a = 0 then 0 else ↑(LinearEquiv.ofBijective a ⋯).symm) = 1
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ IsTorsionBySet R M s ↔ s ⊆ ↑(annihilator R M)

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ IsTorsionBySet R M s ↔ s ⊆ ↑(annihilator R M)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
h : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ p ∈ torsionBy R M '' s, x ∈ p

Tactic:
rintro _ ⟨a, ha, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
h : ∀ (a : ↑s), ↑a • x = 0
a : R
ha : a ∈ s
⊢ x ∈ torsionBy R M a
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: case smul
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 : M
g : End R M
x✝ : M
hx✝ : x✝ ∈ span (End R M) ↑s
h : ((toModuleEnd (End R M) M) r) x✝ = f x✝
⊢ ((toModuleEnd (End R M) M) r) (g • x✝) = f (g • x✝)

Tactic:
[

Goal state after:
case smul
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 : M
g : End R M
x✝ : M
hx✝ : x✝ ∈ span (End R M) ↑s
h : ((toModuleEnd (End R M) M) r) x✝ = f x✝
⊢ ((toModuleEnd (End R M) M) r) (g • x✝) = f (g • x✝)
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
a : A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
p : R[X]
n : ℕ
k : R
h :
  ∀ (x : AEval R M a),
    (f ∘ₗ ↑(of R M a).symm).toFun ((C k * X ^ n) • x) =
      (RingHom.id R[X]) (C k * X ^ n) • (f ∘ₗ ↑(of R M a).symm).toFun x
m : AEval R M a
⊢ (f ∘ₗ ↑(of R M a).symm).toFun ((C k * X ^ (n + 1)) • m) =
    (RingHom.id R[X]) (C k * X ^ (n + 1)) • (f ∘ₗ ↑(of R M a).symm).toFun m

Tactic:
[

Goal state after:
R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
a : A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
p : R[X]
n : ℕ
k : R
h :
  ∀ (x : AEval R M a),
    (f ∘ₗ ↑(of R M a).symm).toFun ((C k * X ^ n) • x) =
      (RingHom.id R[X]) (C k * X ^ n) • (f ∘ₗ ↑(of R M a).symm).toFun x
m : AEval R M a
⊢ (f ∘ₗ ↑(of R M a).symm).toFun ((C k * X ^ (n + 1)) • m) =
    (RingHom.id R[X]) (C k * X ^ (n + 1)) • (f ∘ₗ ↑(of R M a).symm).toFun m
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
a : A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
p : R[X]
n : ℕ
k : R
h : ∀ (x : AEval R M a), f ((of R M a).symm ((C k * X ^ n) • x)) = (C k * X ^ n) • f ((of R M a).symm x)
m : AEval R M a
⊢ f ((of R M a).symm ((C k * X ^ (n + 1)) • m)) = (C k * X ^ (n + 1)) • f ((of R M a).symm m)

Tactic:
[

Goal state after:
R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
a : A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
p : R[X]
n : ℕ
k : R
h : ∀ (x : AEval R M a), f ((of R M a).symm ((C k * X ^ n) • x)) = (C k * X ^ n) • f ((of R M a).symm x)
m : AEval R M a
⊢ f ((of R M a).symm ((C k * X ^ (n + 1)) • m)) = (C k * X ^ (n + 1)) • f ((of R M a).symm m)