awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
P : Type u_3
inst_2 : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst_3 : Monoid A
inst_4 : MulDistribMulAction M A
B : Type u_5
inst_5 : Monoid B
inst_6 : MulDistribMulAction N B
B₁ : Type u_6
inst_7 : Monoid B₁
inst_8 : MulDistribMulAction M B₁
C : Type u_7
inst_9 : Monoid C
inst_10 : MulDistribMulAction P C
A' : Type u_8
inst_11 : Group A'
inst_12 : MulDistribMulAction M A'
B' : Type u_9
inst_13 : Group B'
inst_14 : MulDistribMulAction N B'
R : Type u_10
inst_15 : Semiring R
inst_16 : MulSemiringAction M R
R' : Type u_11
inst_17 : Ring R'
inst_18 : MulSemiringAction M R'
S : Type u_12
inst_19 : Semiring S
inst_20 : MulSemiringAction N S
S' : Type u_13
inst_21 : Ring S'
inst_22 : MulSemiringAction N S'
T : Type u_14
inst_23 : Semiring T
inst_24 : MulSemiringAction P T
f g : R →ₑ+*[φ] S
h : Eq (α := (a : R) → S) ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun) f) ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun) g)
rcases :
  ∀ (tF : MulActionHom.{u_1, u_2, u_10, u_12} (M := M) (N := N) (⇑φ : (a : M) → N) R S) (map_zero' : tF.toFun 0 = 0)
    (map_add' : ∀ (x y : R), tF.toFun (x + y) = tF.toFun x + tF.toFun y)
    (map_one' : { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun 1 = 1)
    (map_mul' :
      ∀ (x y : R),
        { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun (x * y) =
          { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun x *
            { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun y)
    (h :
      Eq (α := (a : R) → S)
        ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun)
          { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add', map_one' := map_one',
            map_mul' := map_mul' })
        ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun) g)),
    { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add', map_one' := map_one', map_mul' := map_mul' :
        R →ₑ+*[φ] S } =
      g
⊢ f = g

Tactic:
rcases f with ⟨⟨tF, _, _⟩, _, _⟩
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f : R →ₑ+*[φ] S
⊢ Eq (α := (a : R) → S) (⇑(↑f : R →+* S) : (a : R) → S) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f : R →ₑ+*[φ] S
⊢ Eq (α := (a : R) → S) (⇑(↑f : R →ₑ+[φ] S) : (a : R) → S) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f g : R →ₑ+*[φ] S
⊢ (∀ (x : R), Eq.{u_12 + 1} (α := S) ((f : (a : R) → S) x : S) ((g : (a : R) → S) x : S)) → f = g

Tactic:
DFunLike.ext f g

Premises used: DFunLike.ext
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f : R →ₑ+*[φ] S
⊢ Eq.{u_12 + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)

Tactic:
map_zero f

Premises used: map_zero
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f : R →ₑ+*[φ] S
x y : R
⊢ (f : (a : R) → S) (x + y) = HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)

Tactic:
map_add f x y

Premises used: map_add
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R' : Type u_11
inst_2 : Ring R'
inst_3 : MulSemiringAction M R'
S' : Type u_13
inst_4 : Ring S'
inst_5 : MulSemiringAction N S'
f : R' →ₑ+*[φ] S'
x : R'
⊢ Eq.{u_13 + 1} (α := S') ((f : (a : R') → S') (-x) : S') (-(f : (a : R') → S') x : S')

Tactic:
map_neg f x

Premises used: map_neg
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R' : Type u_11
inst_2 : Ring R'
inst_3 : MulSemiringAction M R'
S' : Type u_13
inst_4 : Ring S'
inst_5 : MulSemiringAction N S'
f : R' →ₑ+*[φ] S'
x y : R'
⊢ (f : (a : R') → S') (x - y) = HSub.hSub (α := S') (β := S') ((f : (a : R') → S') x : S') ((f : (a : R') → S') y : S')

Tactic:
map_sub f x y

Premises used: map_sub
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f : R →ₑ+*[φ] S
⊢ Eq.{u_12 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)

Tactic:
map_one f

Premises used: map_one
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f : R →ₑ+*[φ] S
x y : R
⊢ (f : (a : R) → S) (x * y) = HMul.hMul (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)

Tactic:
map_mul f x y

Premises used: map_mul
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f : R →ₑ+*[φ] S
m : M
x : R
⊢ (f : (a : R) → S) (m • x) =
    HSMul.hSMul.{u_2, u_12, u_12} (α := N) (β := S) ((φ : (a : M) → N) m : N) ((f : (a : R) → S) x : S)

Tactic:
map_smulₛₗ f m x

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
R : Type u_10
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
S : Type u_12
inst_3 : Semiring S
inst_4 : MulSemiringAction M S
f : R →+*[M] S
m : M
x : R
⊢ (f : (a : R) → S) (m • x) = HSMul.hSMul (β := S) m ((f : (a : R) → S) x : S)

Tactic:
map_smulₛₗ f m x

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
R : Type u_10
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
x : R
⊢ (MulSemiringActionHom.id M : (a : R) → R) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
P : Type u_3
inst_2 : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
R : Type u_10
inst_3 : Semiring R
inst_4 : MulSemiringAction M R
S : Type u_12
inst_5 : Semiring S
inst_6 : MulSemiringAction N S
T : Type u_14
inst_7 : Semiring T
inst_8 : MulSemiringAction P T
g : S →ₑ+*[ψ] T
f : R →ₑ+*[φ] S
inst_9 : φ.CompTriple ψ χ
x : R
⊢ Eq.{u_14 + 1} (α := T) ((g.comp f : (a : R) → T) x : T) ((g : (a : S) → T) ((f : (a : R) → S) x : S) : T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
rw :
  Eq.{u_12 + 1} (α := S) ((MulSemiringActionHom.id N : (a : S) → S) ((f : (a : R) → S) x : S) : S)
    ((f : (a : R) → S) x : S)
rw₁ rw₂ : Eq.{u_12 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x : S)
⊢ Eq.{u_12 + 1} (α := S) ((comp (MulSemiringActionHom.id N) f : (a : R) → S) x : S) ((f : (a : R) → S) x : S)

Tactic:
rw [comp_apply, id_apply]

Premises used: MulSemiringActionHom.id_apply, MulSemiringActionHom.comp_apply
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
rw :
  Eq.{u_12 + 1} (α := S) ((f : (a : R) → S) ((MulSemiringActionHom.id M : (a : R) → R) x : R) : S)
    ((f : (a : R) → S) x : S)
rw₁ rw₂ : Eq.{u_12 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x : S)
⊢ Eq.{u_12 + 1} (α := S) ((f.comp (MulSemiringActionHom.id M) : (a : R) → S) x : S) ((f : (a : R) → S) x : S)

Tactic:
rw [comp_apply, id_apply]

Premises used: MulSemiringActionHom.id_apply, MulSemiringActionHom.comp_apply
-- Module: Mathlib.GroupTheory.GroupAction.Hom
Goal:
R : Type u_1
M : Type u_2
inst : SMul R M
N : Type u_3
F : Type u_4
inst_1 : SMul R N
inst_2 : FunLike F M N
inst_3 : MulActionHomClass F R M N
f : F
r : R
h1 : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
h2 : IsSMulRegular N r
⊢ IsSMulRegular M r

Tactic:
fun x y h3 => h1 <| h2 <|
  (map_smulₛₗ f r x).symm.trans ((congrArg f h3).trans (map_smulₛₗ f r y))

Premises used: congrArg, MulActionSemiHomClass.map_smulₛₗ, IsSMulRegular, Function.Injective, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.GroupTheory.GroupAction.IterateAct
Goal:
α : Type u_1
f : α → α
⊢ Countable (IterateMulAct f)

Tactic:
Function.Injective.countable fun _ _ ↦ IterateMulAct.ext

Premises used: Function.Injective.countable, IterateMulAct.ext
-- Module: Mathlib.GroupTheory.GroupAction.IterateAct
Goal:
α : Type u_1
f : α → α
a b c : IterateMulAct f
val : (a * b * c).val = (a * (b * c)).val
⊢ a * b * c = a * (b * c)

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.IterateAct
Goal:
α : Type u_1
f : α → α
a b c : IterateMulAct f
⊢ (a * b * c).val = (a * (b * c)).val

Tactic:
apply Nat.add_assoc

Premises used: Nat.add_assoc
-- Module: Mathlib.GroupTheory.GroupAction.IterateAct
Goal:
α : Type u_1
f : α → α
x : IterateMulAct f
val : (1 * x).val = x.val
⊢ 1 * x = x

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.IterateAct
Goal:
α : Type u_1
f : α → α
x : IterateMulAct f
⊢ (1 * x).val = x.val

Tactic:
apply Nat.zero_add

Premises used: Nat.zero_add
-- Module: Mathlib.GroupTheory.GroupAction.IterateAct
Goal:
α : Type u_1
f : α → α
x : IterateMulAct f
val :
  IterateMulAct.val.{u_1} (α := α) (f := f) { val := 0 * x.val : IterateMulAct f } =
    IterateMulAct.val.{u_1} (α := α) (f := f) 1
⊢ Eq (α := IterateMulAct f) { val := 0 * x.val } 1

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.IterateAct
Goal:
α : Type u_1
f : α → α
x : IterateMulAct f
⊢ val.{u_1} (α := α) (f := f) { val := 0 * x.val : IterateMulAct f } = val.{u_1} (α := α) (f := f) 1

Tactic:
apply Nat.zero_mul

Premises used: Nat.zero_mul
-- Module: Mathlib.GroupTheory.GroupAction.IterateAct
Goal:
α : Type u_1
f : α → α
n : ℕ
a : IterateMulAct f
val :
  IterateMulAct.val.{u_1} (α := α) (f := f) { val := (n + 1) * a.val : IterateMulAct f } =
    ({ val := n * a.val : IterateMulAct f } * a).val
⊢ { val := (n + 1) * a.val } = { val := n * a.val : IterateMulAct f } * a

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.IterateAct
Goal:
α : Type u_1
f : α → α
n : ℕ
a : IterateMulAct f
⊢ val.{u_1} (α := α) (f := f) { val := (n + 1) * a.val : IterateMulAct f } =
    ({ val := n * a.val : IterateMulAct f } * a).val

Tactic:
apply Nat.succ_mul

Premises used: Nat.succ_mul
-- Module: Mathlib.GroupTheory.GroupAction.IterateAct
Goal:
α : Type u_1
f : α → α
x x_1 : IterateMulAct f
val : (x * x_1).val = (x_1 * x).val
⊢ x * x_1 = x_1 * x

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.IterateAct
Goal:
α : Type u_1
f : α → α
x x_1 : IterateMulAct f
⊢ (x * x_1).val = (x_1 * x).val

Tactic:
apply Nat.add_comm

Premises used: Nat.add_comm
-- Module: Mathlib.GroupTheory.GroupAction.IterateAct
Goal:
α : Type u_1
f : α → α
n : ℕ
x : α
⊢ HSMul.hSMul (α := IterateMulAct f) { val := n : IterateMulAct f } x = f^[n] x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
⊢ IsPretransitive.{u_1, u_2} (↥N) α

Tactic:
have is_transN := IsQuasiPreprimitive.isPretransitive_of_normal hNX
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
⊢ Nontrivial α

Tactic:
have ntα : Nontrivial α := nontrivial_of_fixedPoints_ne_univ hNX
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
obtain : ∀ (a : α), commutator M ≤ N
⊢ commutator M ≤ N

Tactic:
obtain a : α := Nontrivial.to_nonempty.some

Premises used: Nonempty.some, Nontrivial.to_nonempty
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a : α
apply : N ⊔ IwaS.T a = ⊤
⊢ commutator M ≤ N

Tactic:
apply nN.commutator_le_of_self_sup_commutative_eq_top ?_ (IwaS.is_comm a)

Premises used: Subgroup.Normal.commutator_le_of_self_sup_commutative_eq_top, MulAction.IwasawaStructure.is_comm
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a : α
rw : ∀ (i : α), IwaS.T i ≤ N ⊔ IwaS.T a
⊢ N ⊔ IwaS.T a = ⊤

Tactic:
rw [eq_top_iff, ← IwaS.is_generator, iSup_le_iff]

Premises used: MulAction.IwasawaStructure.is_generator, eq_top_iff, iSup_le_iff
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a x : α
obtain : ∀ (g : ↥N), IwaS.T (g • a) ≤ N ⊔ IwaS.T a
⊢ IwaS.T x ≤ N ⊔ IwaS.T a

Tactic:
obtain ⟨g, rfl⟩ := MulAction.exists_smul_eq N a x

Premises used: Membership.mem, Subtype, MulAction.exists_smul_eq, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
rw : HSMul.hSMul (α := MulAut M) ((MulAut.conj : (a : M) → MulAut M) (↑g : M) : MulAut M) (IwaS.T a) ≤ N ⊔ IwaS.T a
⊢ IwaS.T (g • a) ≤ N ⊔ IwaS.T a

Tactic:
rw [Subgroup.smul_def, IwaS.is_conj g a]

Premises used: Subgroup.smul_def, MulAction.IwasawaStructure.is_conj, Subtype.val
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ (↑(IwaS.T a) : Set M)
⊢ (↑g : M) ∈ N ⊔ IwaS.T a

Tactic:
have hg' : ↑g ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_left (Subtype.mem g)
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ (↑(IwaS.T a) : Set M)
hg' : (↑g : M) ∈ N ⊔ IwaS.T a
⊢ k ∈ N ⊔ IwaS.T a

Tactic:
have hk' : k ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_right hk
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ (↑(IwaS.T a) : Set M)
hg' : (↑g : M) ∈ N ⊔ IwaS.T a
hk' : k ∈ N ⊔ IwaS.T a
⊢ Membership.mem (α := M) (N ⊔ IwaS.T a)
    ((((MulDistribMulAction.toMonoidEnd (MulAut M) M : (a : MulAut M) → Monoid.End M)
              ((MulAut.conj : (a : M) → MulAut M) (↑g : M)) :
            Monoid.End M) :
          (a : M) → M)
        k :
      M)

Tactic:
(N ⊔ IwaS.T a).mul_mem ((N ⊔ IwaS.T a).mul_mem hg' hk') ((N ⊔ IwaS.T a).inv_mem hg')

Premises used: Set.Mem, MulAction.IwasawaStructure.T, Subgroup.inv_mem, Max.max, Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ (↑(IwaS.T a) : Set M)
hg' : (↑g : M) ∈ N ⊔ IwaS.T a
hk' : k ∈ N ⊔ IwaS.T a
⊢ Membership.mem (α := M) (N ⊔ IwaS.T a)
    ((((MulDistribMulAction.toMonoidEnd (MulAut M) M : (a : MulAut M) → Monoid.End M)
              ((MulAut.conj : (a : M) → MulAut M) (↑g : M)) :
            Monoid.End M) :
          (a : M) → M)
        k :
      M)

Tactic:
exact (N ⊔ IwaS.T a).mul_mem ((N ⊔ IwaS.T a).mul_mem hg' hk') ((N ⊔ IwaS.T a).inv_mem hg')

Premises used: MulAction.IwasawaStructure.T, Subgroup.inv_mem, Max.max, Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
eq_bot_or_eq_top_of_normal : ∀ (H : Subgroup M), H.Normal → H = ⊥ ∨ H = ⊤
⊢ IsSimpleGroup M

Tactic:
apply IsSimpleGroup.mk

Premises used: IsSimpleGroup.mk
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints.{u_1, u_2} (↥N) α = Set.univ
⊢ N = ⊥ ∨ N = ⊤

Tactic:
Or.inl (N.eq_bot_iff_forall.mpr fun n hn => ?_)

Premises used: Iff.mpr, Subgroup.eq_bot_iff_forall, Or.inl
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints.{u_1, u_2} (↥N) α = Set.univ
eq_bot_or_eq_top_of_normal : ∀ (n : M) (hn : n ∈ N), n = 1
⊢ N = ⊥ ∨ N = ⊤

Tactic:
refine Or.inl (N.eq_bot_iff_forall.mpr fun n hn => ?_)

Premises used: Iff.mpr, Subgroup.eq_bot_iff_forall, Or.inl
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints.{u_1, u_2} (↥N) α = Set.univ
n : M
hn : n ∈ N
eq_bot_or_eq_top_of_normal : ∀ (a : α), n • a = HSMul.hSMul.{u_1, u_2, u_2} (α := M) 1 a
⊢ n = 1

Tactic:
apply is_faithful.eq_of_smul_eq_smul

Premises used: FaithfulSMul.eq_of_smul_eq_smul
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints.{u_1, u_2} (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
eq_bot_or_eq_top_of_normal : n • x = x
⊢ n • x = HSMul.hSMul.{u_1, u_2, u_2} (α := M) 1 x

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints.{u_1, u_2} (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
⊢ n • x = x

Tactic:
Set.eq_univ_iff_forall.mp h x ⟨n, hn⟩

Premises used: Set.eq_univ_iff_forall, Subtype.mk, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints.{u_1, u_2} (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
⊢ n • x = x

Tactic:
exact Set.eq_univ_iff_forall.mp h x ⟨n, hn⟩

Premises used: Set.eq_univ_iff_forall, Subtype.mk, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : commutator M ≤ N
⊢ N = ⊥ ∨ N = ⊤

Tactic:
Or.inr (top_le_iff.mp (le_trans (ge_of_eq is_perfect) h))

Premises used: ge_of_eq, top_le_iff, Iff.mp, Or.inr, le_trans
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : commutator M ≤ N
⊢ N = ⊥ ∨ N = ⊤

Tactic:
exact Or.inr (top_le_iff.mp (le_trans (ge_of_eq is_perfect) h))

Premises used: ge_of_eq, top_le_iff, Iff.mp, Or.inr, le_trans
-- Module: Mathlib.GroupTheory.GroupAction.Iwasawa
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
⊢ fixedPoints.{u_1, u_2} (↥N) α = Set.univ ∨ commutator M ≤ N

Tactic:
cases or_iff_not_imp_left.mpr (IwaS.commutator_le N) with
  | inl h =>
    refine Or.inl (N.eq_bot_iff_forall.mpr fun n hn => ?_)
    apply is_faithful.eq_of_smul_eq_smul
    intro x
    rw [one_smul]
    exact Set.eq_univ_iff_forall.mp h x ⟨n, hn⟩
  | inr h => exact Or.inr (top_le_iff.mp (le_trans (ge_of_eq is_perfect) h))

Premises used: MulAction.IwasawaStructure.commutator_le, Iff.mpr, FaithfulSMul.eq_of_smul_eq_smul, one_smul, Subgroup.eq_bot_iff_forall, Classical.or_iff_not_imp_left, Or.inl
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
rw : IsMultiplyPretransitive G α 1
⊢ IsPretransitive G α

Tactic:
rw [← is_one_pretransitive_iff]

Premises used: MulAction.is_one_pretransitive_iff