awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
inst_2 : N.Normal
a : X
g : G
rw :
  orbit.{u_1, u_2} (↥N) (g • a) = orbit.{u_1, u_2} (↥N) a ∨
    Disjoint (orbit.{u_1, u_2} (↥N) (g • a)) (orbit.{u_1, u_2} (↥N) a)
⊢ g • orbit.{u_1, u_2} (↥N) a = orbit.{u_1, u_2} (↥N) a ∨
    Disjoint (g • orbit.{u_1, u_2} (↥N) a) (orbit.{u_1, u_2} (↥N) a)

Tactic:
rw [smul_orbit_eq_orbit_smul]

Premises used: MulAction.smul_orbit_eq_orbit_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
inst_2 : N.Normal
a : X
g : G
⊢ orbit.{u_1, u_2} (↥N) (g • a) = orbit.{u_1, u_2} (↥N) a ∨
    Disjoint (orbit.{u_1, u_2} (↥N) (g • a)) (orbit.{u_1, u_2} (↥N) a)

Tactic:
apply orbit.eq_or_disjoint

Premises used: MulAction.orbit.eq_or_disjoint
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
inst_2 : N.Normal
left : Setoid.IsPartition.{u_2} (α := X) (range fun (a : X) ↦ orbit.{u_1, u_2} (↥N) a)
right : ∀ ⦃B : Set X⦄, Membership.mem (γ := Set (Set X)) (range fun (a : X) ↦ orbit.{u_1, u_2} (↥N) a) B → IsBlock G B
⊢ IsBlockSystem.{u_1, u_2} G (X := X) (range fun (a : X) ↦ orbit.{u_1, u_2} (↥N) a)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
inst_2 : N.Normal
⊢ Setoid.IsPartition.{u_2} (α := X) (range fun (a : X) ↦ orbit.{u_1, u_2} (↥N) a)

Tactic:
apply IsPartition.of_orbits

Premises used: MulAction.IsPartition.of_orbits
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
inst_2 : N.Normal
a : X
⊢ IsBlock.{u_1, u_2} G (X := X) ((fun (a : X) ↦ orbit.{u_1, u_2} (↥N) a) a)

Tactic:
.orbit_of_normal a

Premises used: MulAction.IsBlock.orbit_of_normal
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
inst_2 : N.Normal
a : X
⊢ IsBlock.{u_1, u_2} G (X := X) ((fun (a : X) ↦ orbit.{u_1, u_2} (↥N) a) a)

Tactic:
exact .orbit_of_normal a
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G H H
simp : ∀ ⦃g₁ g₂ : G⦄, g₁ • (↑s : Set H) ≠ g₂ • (↑s : Set H) → ∀ ⦃a : H⦄, a ∈ g₁ • (↑s : Set H) → a ∉ g₂ • (↑s : Set H)
⊢ IsBlock G (↑s : Set H)

Tactic:
simp only [IsBlock, disjoint_left]

Premises used: MulAction.IsBlock, Set.disjoint_left
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G H H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
⊢ False

Tactic:
hab ?_
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G H H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
refine : a • (↑s : Set H) = b • (↑s : Set H)
⊢ False

Tactic:
refine hab ?_
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G H H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • c • (↑s : Set H) = b • c • (↑s : Set H)
rw₁ : (a • c) • (↑s : Set H) = b • c • (↑s : Set H)
rw₂ : (b • d) • (↑s : Set H) = b • c • (↑s : Set H)
rw₃ : b • d • (↑s : Set H) = b • c • (↑s : Set H)
rw₄ : b • d • (↑s : Set H) = b • (↑s : Set H)
rw₅ rw₆ : b • (↑s : Set H) = b • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)

Tactic:
rw [← smul_coe_set hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe_set hc, smul_coe_set hd]

Premises used: smul_assoc, smul_coe_set
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
simp : ∀ ⦃g₁ g₂ : G⦄, g₁ • (↑s : Set H) ≠ g₂ • (↑s : Set H) → ∀ ⦃a : H⦄, a ∈ g₁ • (↑s : Set H) → a ∉ g₂ • (↑s : Set H)
⊢ IsBlock G (↑s : Set H)

Tactic:
simp only [IsBlock, disjoint_left]

Premises used: MulAction.IsBlock, Set.disjoint_left
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
⊢ False

Tactic:
hab ?_
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
refine : a • (↑s : Set H) = b • (↑s : Set H)
⊢ False

Tactic:
refine hab ?_
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • op c • (↑s : Set H) = b • op c • (↑s : Set H)
rw₁ : (a • op c) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₂ : op (a • c) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₃ : op (b • d) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₄ : (b • op d) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₅ : b • op d • (↑s : Set H) = b • op c • (↑s : Set H)
rw₆ : b • op d • (↑s : Set H) = b • (↑s : Set H)
rw₇ rw₈ : b • (↑s : Set H) = b • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)

Tactic:
rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc,
    op_smul_coe_set hd]

Premises used: smul_assoc, op_smul_coe_set, MulOpposite.op_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
rw :
  ∀ ⦃g : G⦄,
    (g • orbit.{u_1, u_2} (↥H) a ∩ orbit.{u_1, u_2} (↥H) a).Nonempty →
      g • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
⊢ IsBlock G (orbit.{u_1, u_2} (↥H) a)

Tactic:
rw [isBlock_iff_smul_eq_of_nonempty]

Premises used: MulAction.isBlock_iff_smul_eq_of_nonempty
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : Eq.{u_2 + 1} (α := X) ((fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) h₁)) ((fun (m : ↥H) ↦ m • a) h₂)
this : g ∈ H
rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) g this) : G) • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
rw₁ : Subtype.mk (p := fun (x : G) ↦ x ∈ H) g this • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
rw₂ rw₃ : orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
⊢ g • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a

Tactic:
rw [← Subgroup.coe_mk H g this, ← H.toSubmonoid.smul_def, smul_orbit (⟨g, this⟩ : H) a]

Premises used: Subgroup.coe_mk, MulAction.smul_orbit, Submonoid.smul_def, Subtype.mk
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : Eq.{u_2 + 1} (α := X) ((fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) h₁)) ((fun (m : ↥H) ↦ m • a) h₂)
suffices : g ∈ H
⊢ g • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a

Tactic:
suffices g ∈ H by
    rw [← Subgroup.coe_mk H g this, ← H.toSubmonoid.smul_def, smul_orbit (⟨g, this⟩ : H) a]
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : Eq.{u_2 + 1} (α := X) ((fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) h₁)) ((fun (m : ↥H) ↦ m • a) h₂)
rw : (↑h₂⁻¹ : G) * g * (↑h₁ : G) ∈ H
⊢ g ∈ H

Tactic:
rw [← mul_mem_cancel_left h₂⁻¹.2, ← mul_mem_cancel_right h₁.2]

Premises used: Inv.inv, mul_mem_cancel_right, mul_mem_cancel_left, Subtype.property
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : Eq.{u_2 + 1} (α := X) ((fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) h₁)) ((fun (m : ↥H) ↦ m • a) h₂)
a₁ : Membership.mem (γ := Subgroup G) (stabilizer G a) ((↑h₂⁻¹ : G) * g * (↑h₁ : G))
⊢ (↑h₂⁻¹ : G) * g * (↑h₁ : G) ∈ H

Tactic:
apply hH
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : Eq.{u_2 + 1} (α := X) ((fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) h₁)) ((fun (m : ↥H) ↦ m • a) h₂)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G a) ((↑h₂⁻¹ : G) * g * (↑h₁ : G))

Tactic:
simpa only [mem_stabilizer_iff, InvMemClass.coe_inv, mul_smul, inv_smul_eq_iff]

Premises used: inv_smul_eq_iff, InvMemClass.coe_inv, MulAction.mem_stabilizer_iff, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
rwa : g • a ∈ g • B
rwa₁ rwa₂ rwa₃ rwa₄ : a ∈ B
⊢ a ∈ g • B

Tactic:
rwa [← hg, smul_mem_smul_set_iff]

Premises used: Set.smul_mem_smul_set_iff
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
h : ∀ (x : X), x ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a ↔ x ∈ B
⊢ orbit.{u_1, u_2} (↥(stabilizer G B)) a = B

Tactic:
ext x
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
h : x ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a → x ∈ B
h₁ : x ∈ B → x ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a
⊢ x ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a ↔ x ∈ B

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : Membership.mem (γ := Subgroup G) (stabilizer G B) k
h : k • a ∈ B
⊢ (fun (m : ↥(stabilizer G B)) ↦ m • a)
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G B) x) k k_mem) ∈
    B

Tactic:
simp only [Subgroup.mk_smul]

Premises used: Subgroup.mk_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : Membership.mem (γ := Subgroup G) (stabilizer G B) k
h : a ∈ B
⊢ k • a ∈ B

Tactic:
rw [← k_mem, Set.smul_mem_smul_set_iff]

Premises used: Set.smul_mem_smul_set_iff
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : Membership.mem (γ := Subgroup G) (stabilizer G B) k
⊢ a ∈ B

Tactic:
ha
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : Membership.mem (γ := Subgroup G) (stabilizer G B) k
⊢ a ∈ B

Tactic:
exact ha
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
hx : x ∈ B
h : ∀ (k : G) (hx : k • a ∈ B), k • a ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a
⊢ x ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a

Tactic:
obtain ⟨k, rfl⟩ := exists_smul_eq G a x

Premises used: MulAction.exists_smul_eq, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
hx : k • a ∈ B
⊢ k • a ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a

Tactic:
⟨⟨k, hB.smul_eq_of_mem ha hx⟩, rfl⟩

Premises used: Set.Mem, setOf, Subtype.mk, MulAction.orbit, Exists.intro, Set.range, rfl, MulAction.IsBlock.smul_eq_of_mem
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
hx : k • a ∈ B
⊢ k • a ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a

Tactic:
exact ⟨⟨k, hB.smul_eq_of_mem ha hx⟩, rfl⟩
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
h : ∀ (g : G), Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g ↔ g ∈ H
⊢ stabilizer G (orbit.{u_1, u_2} (↥H) a) = H

Tactic:
ext g
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
h : Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g → g ∈ H
h₁ : g ∈ H → Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g ↔ g ∈ H

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g
h : ∀ (b : ↥H) (h : (fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) b) = a), g ∈ H
⊢ g ∈ H

Tactic:
obtain ⟨-, ⟨b, rfl⟩, h⟩ := hg.symm ▸ mem_orbit_self a

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g
b : ↥H
h : (fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) b) = a
⊢ Membership.mem (γ := Subgroup G) (stabilizer G a) (g * (↑b : G))

Tactic:
simp_rw [H.toSubmonoid.smul_def, ← mul_smul, ← mem_stabilizer_iff] at h

Premises used: Submonoid.smul_def, MulAction.mem_stabilizer_iff, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g
b : ↥H
h : Membership.mem (γ := Subgroup G) (stabilizer G a) (g * (↑b : G))
⊢ g ∈ H

Tactic:
(mul_mem_cancel_right b.2).mp (hH h)

Premises used: Iff.mp, mul_mem_cancel_right, Subtype.property
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g
b : ↥H
h : Membership.mem (γ := Subgroup G) (stabilizer G a) (g * (↑b : G))
⊢ g ∈ H

Tactic:
exact (mul_mem_cancel_right b.2).mp (hH h)

Premises used: Iff.mp, mul_mem_cancel_right, Subtype.property
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ H
h : Subtype.mk (p := fun (x : G) ↦ x ∈ H) g hg • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g

Tactic:
rw [mem_stabilizer_iff, ← Subgroup.coe_mk H g hg, ← Submonoid.smul_def (S := H.toSubmonoid)]

Premises used: Subgroup.coe_mk, Submonoid.smul_def, MulAction.mem_stabilizer_iff
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ H
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ H) g hg • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a

Tactic:
apply smul_orbit (G := H)

Premises used: MulAction.smul_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
simp : LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B') ↔ B ⊆ B'
⊢ LE.le.{u_1} (α := (↑(Ici (stabilizer G a)) : Type u_1))
      (({
              toFun := fun (x : { B : Set X // a ∈ B ∧ IsBlock G B }) ↦
                match (motive := { B : Set X // a ∈ B ∧ IsBlock G B } → (↑(Ici (stabilizer G a)) : Type u_1)) x with
                | ⟨B, ⋯⟩ =>
                  Subtype.mk (p := fun (x : Subgroup G) ↦
                    Membership.mem (γ := Set (Subgroup G)) (Ici (stabilizer G a)) x) (stabilizer G B) ⋯,
              invFun := fun (x : (↑(Ici (stabilizer G a)) : Type u_1)) ↦
                match (motive := (↑(Ici (stabilizer G a)) : Type u_1) → { B : Set X // a ∈ B ∧ IsBlock G B }) x with
                | ⟨H, hH⟩ => Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) (orbit.{u_1, u_2} (↥H) a) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a_1 : { B : Set X // a ∈ B ∧ IsBlock G B }) → (↑(Ici (stabilizer G a)) : Type u_1))
          (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯) :
        (↑(Ici (stabilizer G a)) : Type u_1))
      (({
              toFun := fun (x : { B : Set X // a ∈ B ∧ IsBlock G B }) ↦
                match (motive := { B : Set X // a ∈ B ∧ IsBlock G B } → (↑(Ici (stabilizer G a)) : Type u_1)) x with
                | ⟨B, ⋯⟩ =>
                  Subtype.mk (p := fun (x : Subgroup G) ↦
                    Membership.mem (γ := Set (Subgroup G)) (Ici (stabilizer G a)) x) (stabilizer G B) ⋯,
              invFun := fun (x : (↑(Ici (stabilizer G a)) : Type u_1)) ↦
                match (motive := (↑(Ici (stabilizer G a)) : Type u_1) → { B : Set X // a ∈ B ∧ IsBlock G B }) x with
                | ⟨H, hH⟩ => Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) (orbit.{u_1, u_2} (↥H) a) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a_1 : { B : Set X // a ∈ B ∧ IsBlock G B }) → (↑(Ici (stabilizer G a)) : Type u_1))
          (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B' ⋯) :
        (↑(Ici (stabilizer G a)) : Type u_1)) ↔
    LE.le (α := { B : Set X // a ∈ B ∧ IsBlock G B }) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯)
      (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B' ⋯)

Tactic:
simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, Set.le_eq_subset]

Premises used: Set.le_eq_subset, Equiv.coe_fn_mk, Subtype.mk_le_mk
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
mp : LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B') → B ⊆ B'
mpr : B ⊆ B' → LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B')
⊢ LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B') ↔ B ⊆ B'

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B')
b : X
hb : b ∈ B
mp : ∀ (k : G) (hb : k • a ∈ B), k • a ∈ B'
⊢ b ∈ B'

Tactic:
obtain ⟨k, rfl⟩ := htGX.exists_smul_eq a b

Premises used: MulAction.IsPretransitive.exists_smul_eq, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B')
k : G
hb : k • a ∈ B
this : Membership.mem (γ := Subgroup G) (stabilizer G B') k
⊢ k • a ∈ B'

Tactic:
this.symm ▸ (Set.smul_mem_smul_set ha')

Premises used: Eq.rec, Eq.symm, Set.smul_mem_smul_set
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B')
k : G
hb : k • a ∈ B
this : Membership.mem (γ := Subgroup G) (stabilizer G B') k
⊢ k • a ∈ B'

Tactic:
exact this.symm ▸ (Set.smul_mem_smul_set ha')
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B')
k : G
hb : k • a ∈ B
mp : Membership.mem (γ := Subgroup G) (stabilizer G B') k
⊢ k • a ∈ B'

Tactic:
suffices k ∈ stabilizer G B' by
        exact this.symm ▸ (Set.smul_mem_smul_set ha')
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B')
k : G
hb : k • a ∈ B
⊢ Membership.mem (γ := Subgroup G) (stabilizer G B') k

Tactic:
hBB' (hB.smul_eq_of_mem ha hb)

Premises used: MulAction.IsBlock.smul_eq_of_mem
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B')
k : G
hb : k • a ∈ B
⊢ Membership.mem (γ := Subgroup G) (stabilizer G B') k

Tactic:
exact hBB' (hB.smul_eq_of_mem ha hb)

Premises used: MulAction.IsBlock.smul_eq_of_mem
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : B ⊆ B'
g : G
hgB : Membership.mem (γ := Subgroup G) (stabilizer G B) g
mpr : g • a ∈ B'
⊢ Membership.mem (γ := Subgroup G) (stabilizer G B') g

Tactic:
apply hB'.smul_eq_of_mem ha'

Premises used: MulAction.IsBlock.smul_eq_of_mem
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : B ⊆ B'
g : G
hgB : Membership.mem (γ := Subgroup G) (stabilizer G B) g
⊢ g • a ∈ B'

Tactic:
hBB' <| hgB.symm ▸ (Set.smul_mem_smul_set ha)

Premises used: Eq.rec, Eq.symm, Set.smul_mem_smul_set