awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Group R
inst_1 : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ Eq (α := Submonoid R) (Subgroup.toSubmonoid (MulAction.stabilizer R m))
    (Subgroup.toSubmonoid (MulAction.stabilizer R (↑m : M)))

Tactic:
exact stabilizer_of_subMul.submonoid m

Premises used: SubMulAction.stabilizer_of_subMul.submonoid
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
T : Type u''
R : Type u
M : Type v
inst : Group R
inst_1 : MulAction R M
s : SubMulAction R M
⊢ ∀ (c : R) {x : M}, x ∈ (↑s : Set M)ᶜ → c • x ∈ (↑s : Set M)ᶜ

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Group R
inst_1 : MulAction R M
s : SubMulAction R M
⊢ sᶜ.carrier = (↑s : Set M)ᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : SubMulAction R M
h : (↑p : Set M).Nonempty
⊢ 0 ∈ p

Tactic:
let ⟨x, hx⟩ := h
  zero_smul R (x : M) ▸ p.smul_mem 0 hx

Premises used: Membership.mem, Eq.rec, zero_smul, SubMulAction.smul_mem, _private.0.SubMulAction.zero_mem.match_1, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : SubMulAction R M
x : M
hx : x ∈ p
rw : HSMul.hSMul.{u, v, v} (α := R) (-1) x ∈ p
⊢ -x ∈ p

Tactic:
rw [← neg_one_smul R]

Premises used: neg_one_smul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : SubMulAction R M
x : M
hx : x ∈ p
⊢ HSMul.hSMul.{u, v, v} (α := R) (-1) x ∈ p

Tactic:
p.smul_mem _ hx

Premises used: SubMulAction.smul_mem
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : SubMulAction R M
x : M
hx : x ∈ p
⊢ HSMul.hSMul.{u, v, v} (α := R) (-1) x ∈ p

Tactic:
exact p.smul_mem _ hx

Premises used: SubMulAction.smul_mem
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : SubMulAction R M
x : M
h : -x ∈ p
rw : - -x ∈ p
⊢ x ∈ p

Tactic:
rw [← neg_neg x]

Premises used: neg_neg
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : SubMulAction R M
x : M
h : -x ∈ p
⊢ - -x ∈ p

Tactic:
neg_mem _ h

Premises used: SubMulAction.neg_mem, Set.Mem
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : SubMulAction R M
x : M
h : -x ∈ p
⊢ - -x ∈ p

Tactic:
exact neg_mem _ h

Premises used: SubMulAction.neg_mem
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : SubMulAction R M
x : ↥p
⊢ (↑(-x) : M) = -(↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
R : Type u
M : Type v
inst : GroupWithZero S
inst_1 : Monoid R
inst_2 : MulAction R M
inst_3 : SMul S R
inst_4 : MulAction S M
inst_5 : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
s0 : s ≠ 0
⊢ s • x ∈ p ↔ x ∈ p

Tactic:
p.smul_mem_iff' (Units.mk0 s s0)

Premises used: Set.Mem, Units.mk0, SubMulAction.smul_mem_iff'
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
s : SubMulAction M α
⊢ s.inclusion.toFun = Subtype.val (p := fun (x : α) ↦ x ∈ s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
s : SubMulAction M α
⊢ Eq (α := (a : ↥s) → α) (⇑s.inclusion : (a : ↥s) → α) (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
s : SubMulAction M α
rw : Set.range (ι := ↥s) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) = s.carrier
⊢ Set.range (ι := ↥s) (⇑s.inclusion : (a : ↥s) → α) = s.carrier

Tactic:
rw [inclusion.coe_eq]

Premises used: SubMulAction.inclusion.coe_eq
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
s : SubMulAction M α
⊢ Set.range (ι := ↥s) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) = s.carrier

Tactic:
Subtype.range_coe

Premises used: Subtype.range_coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
s : SubMulAction M α
⊢ Set.range (ι := ↥s) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) = s.carrier

Tactic:
exact Subtype.range_coe

Premises used: Subtype.range_coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
s : SubMulAction M α
⊢ Injective (α := ↥s) (β := α) (⇑s.inclusion : (a : ↥s) → α)

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
T : Type u''
R_1 : Type u
M_1 : Type v
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
⊢ ∀ (c : Rˣ) {x : M},
    Membership.mem (γ := Set M) {x : M | x ≠ 0} x → Membership.mem (γ := Set M) {x : M | x ≠ 0} (c • x)

Tactic:
simp [Units.smul_def]

Premises used: Units.smul_def
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
a : Rˣ
x : { x : M // x ≠ 0 }
⊢ (↑(a • x) : M) = a • (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
y : { v : M // v ≠ 0 }
a : Rˣ
⊢ Eq.{u_2 + 1} (α := M) ((fun (m : Rˣ) ↦ m • (↑y : M)) a) (↑((fun (m : Rˣ) ↦ m • y) a) : M)

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
y : { v : M // v ≠ 0 }
a : Rˣ
⊢ (MulAction.orbitRel Rˣ M : M → M → Prop) (↑((fun (m : Rˣ) ↦ m • y) a) : M) (↑y : M)

Tactic:
exact ⟨a, by simp⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
x y : { v : M // v ≠ 0 }
a : Rˣ
ha : (fun (m : Rˣ) ↦ m • (↑y : M)) a = (↑x : M)
a₁ : (↑((fun (m : Rˣ) ↦ m • y) a) : M) = (↑x : M)
⊢ (fun (m : Rˣ) ↦ m • y) a = x

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
x y : { v : M // v ≠ 0 }
a : Rˣ
ha : (fun (m : Rˣ) ↦ m • (↑y : M)) a = (↑x : M)
⊢ (↑((fun (m : Rˣ) ↦ m • y) a) : M) = (↑x : M)

Tactic:
simpa
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
x y : { v : M // v ≠ 0 }
a : Rˣ
ha : (fun (m : Rˣ) ↦ m • (↑y : M)) a = (↑x : M)
⊢ (MulAction.orbitRel Rˣ { v : M // v ≠ 0 } : { v : M // v ≠ 0 } → { v : M // v ≠ 0 } → Prop) x y

Tactic:
exact ⟨a, by ext; simpa⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
H : Subgroup G
hH : H.Normal
g : G
a : α
ha : a ∈ MulAction.fixedPoints.{u_1, u_2} (↥H) α
h : ↥H
rw : (g⁻¹ * (↑h : G) * g) • a = a
⊢ h • g • a = g • a

Tactic:
rw [Subgroup.smul_def, ← inv_smul_eq_iff, smul_smul, smul_smul]

Premises used: inv_smul_eq_iff, smul_smul, Subgroup.smul_def
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
H : Subgroup G
hH : H.Normal
g : G
a : α
ha : a ∈ MulAction.fixedPoints.{u_1, u_2} (↥H) α
h : ↥H
⊢ (g⁻¹ * (↑h : G) * g) • a = a

Tactic:
ha ⟨_, hH.conj_mem' _ h.2 _⟩

Premises used: Subtype.mk, Subtype.property, Subgroup.Normal.conj_mem'
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
H : Subgroup G
hH : H.Normal
g : G
a : α
ha : a ∈ MulAction.fixedPoints.{u_1, u_2} (↥H) α
h : ↥H
⊢ (g⁻¹ * (↑h : G) * g) • a = a

Tactic:
exact ha ⟨_, hH.conj_mem' _ h.2 _⟩

Premises used: Subtype.mk, Subtype.property, Subgroup.Normal.conj_mem'
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
H : Subgroup G
hH : H.Normal
g : G
a : (↑(MulAction.fixedPoints.{u_1, u_2} (↥H) α) : Type u_2)
⊢ (↑(g • a) : α) = g • (↑a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Support
Goal:
G : Type u_1
α : Type u_3
inst : SMul G α
s : Set α
a : α
ha : a ∈ s
⊢ Supports G s a

Tactic:
fun _ h => h ha

Premises used: MulAction.Supports
-- Module: Mathlib.GroupTheory.GroupAction.Support
Goal:
G : Type u_1
α : Type u_3
β : Type u_4
inst : SMul G α
inst_1 : SMul G β
s t : Set α
b : β
h : s ⊆ t
hs : Supports G s b
⊢ Supports G t b

Tactic:
fun _ hg =>
  (hs _) fun _ ha => hg <| h ha

Premises used: MulAction.Supports
-- Module: Mathlib.GroupTheory.GroupAction.Support
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group H
inst_1 : SMul G α
inst_2 : SMul G β
inst_3 : MulAction H α
inst_4 : SMul H β
inst_5 : SMulCommClass G H β
inst_6 : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
a : ∀ ⦃a : α⦄, a ∈ s → g' • a = a
⊢ g' • g • b = g • b

Tactic:
rw [smul_comm, h]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.GroupTheory.GroupAction.Support
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group H
inst_1 : SMul G α
inst_2 : SMul G β
inst_3 : MulAction H α
inst_4 : SMul H β
inst_5 : SMulCommClass G H β
inst_6 : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
a : α
ha : a ∈ s
⊢ g' • g • a = g • a

Tactic:
have := Set.forall_mem_image.1 hg' ha
-- Module: Mathlib.GroupTheory.GroupAction.Support
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group H
inst_1 : SMul G α
inst_2 : SMul G β
inst_3 : MulAction H α
inst_4 : SMul H β
inst_5 : SMulCommClass G H β
inst_6 : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
a : α
ha : a ∈ s
this : g' • g • a = g • a
a₁ : ∀ (this : g • g' • a = g • a), g' • a = a
a₂ a₃ a₄ a₅ : ∀ (this : g' • a = a), g' • a = a
⊢ g' • a = a

Tactic:
rwa [smul_comm, smul_left_cancel_iff] at this

Premises used: SMulCommClass.smul_comm, smul_left_cancel_iff
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
hG : ∀ (x : X), ∃ (g : G), g • a = x
x y : X
obtain : ∀ (g : G) (hx : g • a = x), ∃ (g : G), g • x = y
⊢ ∃ (g : G), g • x = y

Tactic:
obtain ⟨g, hx⟩ := hG x
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
hG : ∀ (x : X), ∃ (g : G), g • a = x
x y : X
g : G
hx : g • a = x
obtain : ∀ (h : G) (hy : h • a = y), ∃ (g : G), g • x = y
⊢ ∃ (g : G), g • x = y

Tactic:
obtain ⟨h, hy⟩ := hG y
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
hG : ∀ (x : X), ∃ (g : G), g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
rw : (h * g⁻¹) • g • a = y
rw₁ : (h * g⁻¹ * g) • a = y
rw₂ : h • a = y
rw₃ rw₄ : y = y
⊢ (h * g⁻¹) • x = y

Tactic:
rw [← hx, smul_smul, inv_mul_cancel_right, hy]

Premises used: smul_smul, inv_mul_cancel_right
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
hG : ∀ (x : X), ∃ (g : G), g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ ∃ (g : G), g • x = y

Tactic:
exact ⟨h * g⁻¹, by rw [← hx, smul_smul, inv_mul_cancel_right, hy]⟩
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
rw : (∀ (x : X), ∃ (g : G), g • a = x) ↔ ∀ (x : X), x ∈ orbit G a ↔ Membership.mem (γ := Set X) Set.univ x
⊢ IsPretransitive G X ↔ orbit G a = Set.univ

Tactic:
rw [isPretransitive_iff_base a, Set.ext_iff]

Premises used: MulAction.isPretransitive_iff_base, Set.ext_iff
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
h : ∀ (a_1 : X), (∃ (g : G), g • a = a_1) ↔ (a_1 ∈ orbit G a ↔ Membership.mem (γ := Set X) Set.univ a_1)
⊢ (∀ (x : X), ∃ (g : G), g • a = x) ↔ ∀ (x : X), x ∈ orbit G a ↔ Membership.mem (γ := Set X) Set.univ x

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a x : X
h : (∃ (g : G), g • a = x) ↔ (x ∈ orbit G a ↔ True)
h₁ : (∃ (g : G), g • a = x) ↔ x ∈ orbit G a
⊢ (∃ (g : G), g • a = x) ↔ (x ∈ orbit G a ↔ Membership.mem (γ := Set X) Set.univ x)

Tactic:
simp_rw [Set.mem_univ, iff_true, mem_orbit_iff]

Premises used: iff_true, MulAction.mem_orbit_iff, Set.mem_univ
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPretransitive M α
exists_smul_eq : ∀ (x y : β), ∃ (g : N), g • x = y
⊢ IsPretransitive N β

Tactic:
apply MulAction.IsPretransitive.mk

Premises used: MulAction.IsPretransitive.mk
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPretransitive M α
x y : β
exists_smul_eq : ∀ (x' : α), ∃ (g : N), HSMul.hSMul (β := β) g ((f : (a : α) → β) x' : β) = y
⊢ ∃ (g : N), g • x = y

Tactic:
obtain ⟨x', rfl⟩ := hf x

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPretransitive M α
y : β
x' : α
exists_smul_eq : ∀ (y' : α), ∃ (g : N), HSMul.hSMul (β := β) g ((f : (a : α) → β) x' : β) = (f : (a : α) → β) y'
⊢ ∃ (g : N), HSMul.hSMul (β := β) g ((f : (a : α) → β) x' : β) = y

Tactic:
obtain ⟨y', rfl⟩ := hf y

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPretransitive M α
x' y' : α
exists_smul_eq :
  ∀ (g : M), ∃ (g_1 : N), HSMul.hSMul (β := β) g_1 ((f : (a : α) → β) x' : β) = (f : (a : α) → β) (g • x')
⊢ ∃ (g : N), HSMul.hSMul (β := β) g ((f : (a : α) → β) x' : β) = (f : (a : α) → β) y'

Tactic:
obtain ⟨g, rfl⟩ := h.exists_smul_eq x' y'

Premises used: MulAction.IsPretransitive.exists_smul_eq, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPretransitive M α
x' : α
g : M
⊢ HSMul.hSMul (β := β) (φ g) ((f : (a : α) → β) x' : β) = (f : (a : α) → β) (g • x')

Tactic:
simp only [map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPretransitive M α
x' : α
g : M
⊢ ∃ (g_1 : N), HSMul.hSMul (β := β) g_1 ((f : (a : α) → β) x' : β) = (f : (a : α) → β) (g • x')

Tactic:
exact ⟨φ g, by simp only [map_smulₛₗ]⟩
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
mp : IsPretransitive M α → IsPretransitive N β
mpr : IsPretransitive N β → IsPretransitive M α
⊢ IsPretransitive M α ↔ IsPretransitive N β

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ IsPretransitive M α → IsPretransitive N β

Tactic:
apply IsPretransitive.of_surjective_map hf.surjective

Premises used: Function.Bijective.surjective, MulAction.IsPretransitive.of_surjective_map
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hN : IsPretransitive N β
mpr : ∀ (x y : α), ∃ (g : M), g • x = y
⊢ IsPretransitive M α

Tactic:
apply IsPretransitive.mk

Premises used: MulAction.IsPretransitive.mk
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hN : IsPretransitive N β
x y : α
mpr : ∀ (k : N) (hk : HSMul.hSMul (β := β) k ((f : (a : α) → β) x : β) = (f : (a : α) → β) y), ∃ (g : M), g • x = y
⊢ ∃ (g : M), g • x = y

Tactic:
obtain ⟨k, hk⟩ := hN.exists_smul_eq (f x) (f y)

Premises used: MulAction.IsPretransitive.exists_smul_eq, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hN : IsPretransitive N β
x y : α
k : N
hk : HSMul.hSMul (β := β) k ((f : (a : α) → β) x : β) = (f : (a : α) → β) y
mpr : ∀ (g : M) (hk : HSMul.hSMul (β := β) (φ g) ((f : (a : α) → β) x : β) = (f : (a : α) → β) y), ∃ (g : M), g • x = y
⊢ ∃ (g : M), g • x = y

Tactic:
obtain ⟨g, rfl⟩ := hφ k

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hN : IsPretransitive N β
x y : α
g : M
hk : HSMul.hSMul (β := β) (φ g) ((f : (a : α) → β) x : β) = (f : (a : α) → β) y
h : g • x = y
⊢ ∃ (g : M), g • x = y

Tactic:
use g
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hN : IsPretransitive N β
x y : α
g : M
hk : HSMul.hSMul (β := β) (φ g) ((f : (a : α) → β) x : β) = (f : (a : α) → β) y
h : Eq.{u_6 + 1} (α := β) ((f : (a : α) → β) (g • x) : β) ((f : (a : α) → β) y : β)
⊢ g • x = y

Tactic:
apply hf.injective

Premises used: Function.Bijective.injective
-- Module: Mathlib.GroupTheory.GroupAction.Transitive
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hN : IsPretransitive N β
x y : α
g : M
hk : HSMul.hSMul (β := β) (φ g) ((f : (a : α) → β) x : β) = (f : (a : α) → β) y
⊢ Eq.{u_6 + 1} (α := β) ((f : (a : α) → β) (g • x) : β) ((f : (a : α) → β) y : β)

Tactic:
simp only [hk, map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
⊢ HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g : E) (((σ' : (a : G) → E) g)⁻¹ : E) ∈ S.inl.range

Tactic:
simp only [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, rightHom_section,
    mul_inv_cancel]

Premises used: map_inv, GroupExtension.Section.rightHom_section, MonoidHom.mem_ker, map_mul, mul_inv_cancel, GroupExtension.range_inl_eq_ker_rightHom
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
⊢ HMul.hMul (α := E) (β := E) (((σ : (a : G) → E) g)⁻¹ : E) ((σ' : (a : G) → E) g : E) ∈ S.inl.range

Tactic:
simp only [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, rightHom_section,
    inv_mul_cancel]

Premises used: inv_mul_cancel, map_inv, GroupExtension.Section.rightHom_section, MonoidHom.mem_ker, map_mul, GroupExtension.range_inl_eq_ker_rightHom
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
obtain :
  ∀ (n : N)
    (hn :
      (S.inl : (a : N) → E) n = HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g : E) (((σ' : (a : G) → E) g)⁻¹ : E)),
    ∃ (n : N),
      (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ' : (a : G) → E) g : E)
⊢ ∃ (n : N), (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ' : (a : G) → E) g : E)

Tactic:
obtain ⟨n, hn⟩ := mul_inv_mem_range_inl σ σ' g

Premises used: GroupExtension.Section.mul_inv_mem_range_inl
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : (S.inl : (a : N) → E) n = HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g : E) (((σ' : (a : G) → E) g)⁻¹ : E)
rw :
  (σ : (a : G) → E) g =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g : E) (((σ' : (a : G) → E) g)⁻¹ : E))
      ((σ' : (a : G) → E) g : E)
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) ((σ : (a : G) → E) g : E) ((σ : (a : G) → E) g : E)
⊢ (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ' : (a : G) → E) g : E)

Tactic:
rw [hn, inv_mul_cancel_right]

Premises used: inv_mul_cancel_right
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : (S.inl : (a : N) → E) n = HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g : E) (((σ' : (a : G) → E) g)⁻¹ : E)
⊢ ∃ (n : N), (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ' : (a : G) → E) g : E)

Tactic:
exact ⟨n, by rw [hn, inv_mul_cancel_right]⟩