internlm/Lean-Github huggingface dataset:
Theorem: commutator_le_iwasawa
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
⊢ commutator M ≤ N
Tactic:
obtain a : α := Nontrivial.to_nonempty.some
Proof state after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ commutator M ≤ N
Theorem: commutator_le_iwasawa
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ commutator M ≤ N
Tactic:
refine' contains_commutators_of N nN (IwaS.T a) _ (IwaS.is_comm a)
Proof state after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ N ⊔ IwaS.T a = ⊤
Theorem: commutator_le_iwasawa
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ N ⊔ IwaS.T a = ⊤
Tactic:
rw [eq_top_iff, ← IwaS.is_generator, iSup_le_iff]
Proof state after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ ∀ (i : α), IwaS.T i ≤ N ⊔ IwaS.T a
Theorem: commutator_le_iwasawa
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ ∀ (i : α), IwaS.T i ≤ N ⊔ IwaS.T a
Tactic:
intro x
Proof state after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a x : α
⊢ IwaS.T x ≤ N ⊔ IwaS.T a
Theorem: commutator_le_iwasawa
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a x : α
⊢ IwaS.T x ≤ N ⊔ IwaS.T a
Tactic:
obtain ⟨g, rfl⟩ := MulAction.exists_smul_eq N a x
Proof state after:
case intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ IwaS.T (g • a) ≤ N ⊔ IwaS.T a
Theorem: commutator_le_iwasawa
Proof state before:
case intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ IwaS.T (g • a) ≤ N ⊔ IwaS.T a
Tactic:
rw [Subgroup.smul_def, IwaS.is_conj g a]
Proof state after:
case intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ MulAut.conj ↑g • IwaS.T a ≤ N ⊔ IwaS.T a
Theorem: commutator_le_iwasawa
Proof state before:
case intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ MulAut.conj ↑g • IwaS.T a ≤ N ⊔ IwaS.T a
Tactic:
rintro _ ⟨k, hk, rfl⟩
Proof state after:
case intro.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a
Theorem: commutator_le_iwasawa
Proof state before:
case intro.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a
Tactic:
have hg' : ↑g ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_left (Subtype.mem g)
Proof state after:
case intro.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
hg' : ↑g ∈ N ⊔ IwaS.T a
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a
Theorem: commutator_le_iwasawa
Proof state before:
case intro.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
hg' : ↑g ∈ N ⊔ IwaS.T a
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a
Tactic:
have hk' : k ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_right hk
Proof state after:
case intro.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
hg' : ↑g ∈ N ⊔ IwaS.T a
hk' : k ∈ N ⊔ IwaS.T a
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a
Theorem: commutator_le_iwasawa
Proof state before:
case intro.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
hg' : ↑g ∈ N ⊔ IwaS.T a
hk' : k ∈ N ⊔ IwaS.T a
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a
Tactic:
exact (N ⊔ IwaS.T a).mul_mem ((N ⊔ IwaS.T a).mul_mem hg' hk') ((N ⊔ IwaS.T a).inv_mem hg')
Proof state after:
no goals
Theorem: is_simple_iwasawa
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
⊢ IsSimpleGroup M
Tactic:
apply IsSimpleGroup.mk
Proof state after:
case eq_bot_or_eq_top_of_normal
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
⊢ ∀ (H : Subgroup M), Subgroup.Normal H → H = ⊥ ∨ H = ⊤
Theorem: is_simple_iwasawa
Proof state before:
case eq_bot_or_eq_top_of_normal
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
⊢ ∀ (H : Subgroup M), Subgroup.Normal H → H = ⊥ ∨ H = ⊤
Tactic:
intro N nN
Proof state after:
case eq_bot_or_eq_top_of_normal
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
⊢ N = ⊥ ∨ N = ⊤
Theorem: is_simple_iwasawa
Proof state before:
case eq_bot_or_eq_top_of_normal
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
⊢ N = ⊥ ∨ N = ⊤
Tactic:
cases or_iff_not_imp_left.mpr (commutator_le_iwasawa is_qprim IwaS nN) 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))
Proof state after:
no goals
Theorem: is_simple_iwasawa
Proof state before:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
⊢ N = ⊥ ∨ N = ⊤
Tactic:
refine' Or.inl (N.eq_bot_iff_forall.mpr fun n hn => _)
Proof state after:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
⊢ n = 1
Theorem: is_simple_iwasawa
Proof state before:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
⊢ n = 1
Tactic:
apply is_faithful.eq_of_smul_eq_smul
Proof state after:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
⊢ ∀ (a : α), n • a = 1 • a
Theorem: is_simple_iwasawa
Proof state before:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
⊢ ∀ (a : α), n • a = 1 • a
Tactic:
intro x
Proof state after:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
x : α
⊢ n • x = 1 • x
Theorem: is_simple_iwasawa
Proof state before:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
x : α
⊢ n • x = 1 • x
Tactic:
rw [one_smul]
Proof state after:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
x : α
⊢ n • x = x
Theorem: is_simple_iwasawa
Proof state before:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
x : α
⊢ n • x = x
Tactic:
exact Set.eq_univ_iff_forall.mp h x ⟨n, hn⟩
Proof state after:
no goals
Theorem: is_simple_iwasawa
Proof state before:
case eq_bot_or_eq_top_of_normal.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : commutator M ≤ N
⊢ N = ⊥ ∨ N = ⊤
Tactic:
exact Or.inr (top_le_iff.mp (le_trans (ge_of_eq is_perfect) h))
Proof state after:
no goals
Theorem: ULift.surjective_iff_surjective
Proof state before:
α : Type u
β : Type v
f : α → β
⊢ Iff (Function.Surjective.{max (u_1 + 1) (u + 1), max (u_2 + 1) (v + 1)} (ULift.map.{u, v, u_1, u_2} f))
    (Function.Surjective.{u + 1, v + 1} f)
Tactic:
rw [← Equiv.comp_surjective, comp_uLift_eq_uLift_comp, Equiv.surjective_comp]
Proof state after:
no goals
Theorem: ULift.injective_iff_injective
Proof state before:
α : Type u
β : Type v
f : α → β
⊢ Iff (Function.Injective.{max (u_1 + 1) (u + 1), max (u_2 + 1) (v + 1)} (ULift.map.{u, v, u_1, u_2} f))
    (Function.Injective.{u + 1, v + 1} f)
Tactic:
rw [← Equiv.comp_injective, comp_uLift_eq_uLift_comp, Equiv.injective_comp]
Proof state after:
no goals
Theorem: ULift.bijective_iff_bijective
Proof state before:
α : Type u
β : Type v
f : α → β
⊢ Iff (Function.Bijective.{max (u_1 + 1) (u + 1), max (u_2 + 1) (v + 1)} (ULift.map.{u, v, u_1, u_2} f))
    (Function.Bijective.{u + 1, v + 1} f)
Tactic:
rw [← Equiv.comp_bijective, comp_uLift_eq_uLift_comp, Equiv.bijective_comp]
Proof state after:
no goals
Theorem: MulAction.IsPretransitive.mk_base_iff
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ IsPretransitive G X ↔ ∀ (x : X), ∃ g, g • a = x
Tactic:
constructor
Proof state after:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ IsPretransitive G X → ∀ (x : X), ∃ g, g • a = x

case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (∀ (x : X), ∃ g, g • a = x) → IsPretransitive G X
Theorem: MulAction.IsPretransitive.mk_base_iff
Proof state before:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ IsPretransitive G X → ∀ (x : X), ∃ g, g • a = x
Tactic:
intro hG x
Proof state after:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : IsPretransitive G X
x : X
⊢ ∃ g, g • a = x
Theorem: MulAction.IsPretransitive.mk_base_iff
Proof state before:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : IsPretransitive G X
x : X
⊢ ∃ g, g • a = x
Tactic:
let hG_eq := hG.exists_smul_eq
Proof state after:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : IsPretransitive G X
x : X
hG_eq : ∀ (x y : X), ∃ g, g • x = y := exists_smul_eq
⊢ ∃ g, g • a = x
Theorem: MulAction.IsPretransitive.mk_base_iff
Proof state before:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : IsPretransitive G X
x : X
hG_eq : ∀ (x y : X), ∃ g, g • x = y := exists_smul_eq
⊢ ∃ g, g • a = x
Tactic:
exact hG_eq a x
Proof state after:
no goals
Theorem: MulAction.IsPretransitive.mk_base_iff
Proof state before:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (∀ (x : X), ∃ g, g • a = x) → IsPretransitive G X
Tactic:
intro hG
Proof state after:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
⊢ IsPretransitive G X
Theorem: MulAction.IsPretransitive.mk_base_iff
Proof state before:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
⊢ IsPretransitive G X
Tactic:
apply IsPretransitive.mk
Proof state after:
case mpr.exists_smul_eq
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
⊢ ∀ (x y : X), ∃ g, g • x = y
Theorem: MulAction.IsPretransitive.mk_base_iff
Proof state before:
case mpr.exists_smul_eq
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
⊢ ∀ (x y : X), ∃ g, g • x = y
Tactic:
intro x y
Proof state after:
case mpr.exists_smul_eq
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
⊢ ∃ g, g • x = y
Theorem: MulAction.IsPretransitive.mk_base_iff
Proof state before:
case mpr.exists_smul_eq
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g, hx⟩ := hG x
Proof state after:
case mpr.exists_smul_eq.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
⊢ ∃ g, g • x = y
Theorem: MulAction.IsPretransitive.mk_base_iff
Proof state before:
case mpr.exists_smul_eq.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨h, hy⟩ := hG y
Proof state after:
case mpr.exists_smul_eq.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ ∃ g, g • x = y
Theorem: MulAction.IsPretransitive.mk_base_iff
Proof state before:
case mpr.exists_smul_eq.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ ∃ g, g • x = y
Tactic:
use h * g⁻¹
Proof state after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • x = y
Theorem: MulAction.IsPretransitive.mk_base_iff
Proof state before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • x = y
Tactic:
rw [← hx]
Proof state after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • g • a = y
Theorem: MulAction.IsPretransitive.mk_base_iff
Proof state before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • g • a = y
Tactic:
rw [smul_smul, inv_mul_cancel_right]
Proof state after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ h • a = y
Theorem: MulAction.IsPretransitive.mk_base_iff
Proof state before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ h • a = y
Tactic:
exact hy
Proof state after:
no goals
Theorem: MulAction.IsPretransitive.mk_base
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
⊢ IsPretransitive G X
Tactic:
apply IsPretransitive.mk
Proof state after:
case exists_smul_eq
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
⊢ ∀ (x y : X), ∃ g, g • x = y
Theorem: MulAction.IsPretransitive.mk_base
Proof state before:
case exists_smul_eq
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
⊢ ∀ (x y : X), ∃ g, g • x = y
Tactic:
intro x y
Proof state after:
case exists_smul_eq
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
⊢ ∃ g, g • x = y
Theorem: MulAction.IsPretransitive.mk_base
Proof state before:
case exists_smul_eq
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g, hx⟩ := hG x
Proof state after:
case exists_smul_eq.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
⊢ ∃ g, g • x = y
Theorem: MulAction.IsPretransitive.mk_base
Proof state before:
case exists_smul_eq.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨h, hy⟩ := hG y
Proof state after:
case exists_smul_eq.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ ∃ g, g • x = y
Theorem: MulAction.IsPretransitive.mk_base
Proof state before:
case exists_smul_eq.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ ∃ g, g • x = y
Tactic:
use h * g⁻¹
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • x = y
Theorem: MulAction.IsPretransitive.mk_base
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • x = y
Tactic:
rw [← hx]
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • g • a = y
Theorem: MulAction.IsPretransitive.mk_base
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • g • a = y
Tactic:
rw [smul_smul, inv_mul_cancel_right]
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ h • a = y
Theorem: MulAction.IsPretransitive.mk_base
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ h • a = y
Tactic:
exact hy
Proof state after:
no goals