awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
suffices : B = {a}
⊢ b ∉ B

Tactic:
suffices B = {a} by rw [this]; rw [Set.mem_singleton_iff]; exact Ne.symm h
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
inl : ∀ (hyp : Set.Subsingleton.{u_2} (α := X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A)), B = {a}
inr : ∀ (hyp : Eq.{u_2 + 1} (α := Set X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A) Set.univ), B = {a}
⊢ B = {a}

Tactic:
rcases isTrivialBlock_of_isBlock (G := G) (IsBlock.of_subset a hfA) with hyp | hyp

Premises used: MulAction.IsBlock.of_subset, MulAction.IsPreprimitive.isTrivialBlock_of_isBlock
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton.{u_2} (α := X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A)
inl : Membership.mem (γ := Set X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A) a
⊢ B = {a}

Tactic:
apply Set.Subsingleton.eq_singleton_of_mem hyp

Premises used: Set.Subsingleton.eq_singleton_of_mem
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton.{u_2} (α := X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A)
inl : ∀ (i : G), Membership.mem (γ := Set X) (⋂ (_ : a ∈ i • A), i • A) a
⊢ Membership.mem (γ := Set X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A) a

Tactic:
rw [Set.mem_iInter]

Premises used: Set.mem_iInter
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton.{u_2} (α := X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A)
g : G
⊢ Membership.mem (γ := Set X) (⋂ (_ : a ∈ g • A), g • A) a

Tactic:
simp only [Set.mem_iInter, imp_self]

Premises used: Set.mem_iInter, imp_self
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : Eq.{u_2 + 1} (α := Set X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A) Set.univ
⊢ B = Set.univ

Tactic:
change B = Set.univ at hyp

Premises used: Set.univ
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
inr : False
⊢ B = {a}

Tactic:
exfalso
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
inr : A = Set.univ
⊢ False

Tactic:
apply hA'
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
this : ∃ (g : G), a ∈ g • A
obtain : ∀ (g : G) (hg : a ∈ g • A), A = Set.univ
⊢ A = Set.univ

Tactic:
obtain ⟨g, hg⟩ := this
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
g : G
hg : a ∈ g • A
⊢ B ⊆ g • A

Tactic:
have : B ⊆ g • A := Set.biInter_subset_of_mem hg
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
g : G
hg : a ∈ g • A
this : B ⊆ g • A
⊢ A = HSMul.hSMul (β := Set X) g⁻¹ Set.univ

Tactic:
rw [hyp, Set.univ_subset_iff, ← eq_inv_smul_iff] at this

Premises used: Set.univ_subset_iff, eq_inv_smul_iff
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
g : G
hg : a ∈ g • A
this : A = HSMul.hSMul (β := Set X) g⁻¹ Set.univ
rw : HSMul.hSMul (β := Set X) g⁻¹ Set.univ = Set.univ
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set X) Set.univ Set.univ
⊢ A = Set.univ

Tactic:
rw [this, Set.smul_set_univ]

Premises used: Set.smul_set_univ
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
inr : ∃ (g : G), a ∈ g • A
⊢ A = Set.univ

Tactic:
suffices ∃ g : G, a ∈ g • A by
      obtain ⟨g, hg⟩ := this
      have : B ⊆ g • A := Set.biInter_subset_of_mem hg
      rw [hyp, Set.univ_subset_iff, ← eq_inv_smul_iff] at this
      rw [this, Set.smul_set_univ]
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
inr : ∀ (x : X) (hx : x ∈ A), ∃ (g : G), a ∈ g • A
⊢ ∃ (g : G), a ∈ g • A

Tactic:
obtain ⟨x, hx⟩ := hA
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
x : X
hx : x ∈ A
inr : ∀ (g : G) (hg : g • x = a), ∃ (g : G), a ∈ g • A
⊢ ∃ (g : G), a ∈ g • A

Tactic:
obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G x a

Premises used: MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
x : X
hx : x ∈ A
g : G
hg : g • x = a
w : G
w₁ : X
h₁ : x ∈ A ∧ (fun (x : X) ↦ g • x) x = a
⊢ ∃ (g : G), a ∈ g • A

Tactic:
use g, x
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
x x_1 x_2 : α
h : x_1⁻¹ * x_2 ∈ H
rwa : (x * x_1)⁻¹ * x • x_2 ∈ H
rwa₁ : (x * x_1)⁻¹ * (x * x_2) ∈ H
rwa₂ : x_1⁻¹ * x⁻¹ * (x * x_2) ∈ H
rwa₃ : x_1⁻¹ * (x⁻¹ * (x * x_2)) ∈ H
rwa₄ rwa₅ rwa₆ rwa₇ : x_1⁻¹ * x_2 ∈ H
⊢ (x • x_1)⁻¹ * x • x_2 ∈ H

Tactic:
rwa [smul_eq_mul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, mul_assoc, mul_inv_rev, smul_eq_mul
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
b : ↥(Subgroup.op (normalizer (↑H : Set α)))
c x : α
h : c⁻¹ * x ∈ H
rwa : ((↑b : αᵐᵒᵖ) • c)⁻¹ * b • x ∈ H
rwa₁ : ((↑b : αᵐᵒᵖ) • c)⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
rwa₂ : (c * unop (↑b : αᵐᵒᵖ))⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
rwa₃ : (c * unop (↑b : αᵐᵒᵖ))⁻¹ * (x * unop (↑b : αᵐᵒᵖ)) ∈ H
rwa₄ : (unop (↑b : αᵐᵒᵖ))⁻¹ * c⁻¹ * (x * unop (↑b : αᵐᵒᵖ)) ∈ H
rwa₅ : (unop (↑b : αᵐᵒᵖ))⁻¹ * c⁻¹ * x * unop (↑b : αᵐᵒᵖ) ∈ H
rwa₆ : unop (↑b : αᵐᵒᵖ) * ((unop (↑b : αᵐᵒᵖ))⁻¹ * c⁻¹ * x) ∈ H
rwa₇ : unop (↑b : αᵐᵒᵖ) * ((unop (↑b : αᵐᵒᵖ))⁻¹ * (c⁻¹ * x)) ∈ H
rwa₈ rwa₉ rwa₁₀ rwa₁₁ : c⁻¹ * x ∈ H
⊢ (b • c)⁻¹ * b • x ∈ H

Tactic:
rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
      mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]

Premises used: mul_assoc, Subgroup.smul_def, Subtype.prop, Iff.mp, Subgroup.mem_normalizer_iff', mul_inv_rev, MulOpposite.smul_eq_mul_unop, mul_inv_cancel_left
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
hH : H.Normal
x : αᵐᵒᵖ
x_1 x_2 : α
h : x_1⁻¹ * x_2 ∈ H
rwa : (x_1 * unop x)⁻¹ * x • x_2 ∈ H
rwa₁ : (x_1 * unop x)⁻¹ * (x_2 * unop x) ∈ H
rwa₂ : (unop x)⁻¹ * x_1⁻¹ * (x_2 * unop x) ∈ H
rwa₃ : (unop x)⁻¹ * (x_1⁻¹ * (x_2 * unop x)) ∈ H
rwa₄ : x_1⁻¹ * (x_2 * unop x) * (unop x)⁻¹ ∈ H
rwa₅ : x_1⁻¹ * (x_2 * unop x * (unop x)⁻¹) ∈ H
rwa₆ rwa₇ rwa₈ rwa₉ : x_1⁻¹ * x_2 ∈ H
⊢ (x • x_1)⁻¹ * x • x_2 ∈ H

Tactic:
rwa [smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, mul_assoc, hH.mem_comm_iff, mul_assoc,
      mul_inv_cancel_right]

Premises used: mul_inv_cancel_right, Subgroup.Normal.mem_comm_iff, mul_assoc, mul_inv_rev, MulOpposite.smul_eq_mul_unop
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
inst_3 : QuotientAction β H
b : β
a : α
⊢ HSMul.hSMul (β := α ⧸ H) b (↑a : α ⧸ H) = (↑(b • a) : α ⧸ H)

Tactic:
rfl

Premises used: Quot.map, Quotient.map', rfl
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
inst_3 : QuotientAction β H
b : β
q : α ⧸ H
rw : HSMul.hSMul (β := α ⧸ H) b (↑(Quotient.out q) : α ⧸ H) = b • q
rw₁ rw₂ : b • q = b • q
⊢ (↑(b • Quotient.out q) : α ⧸ H) = b • q

Tactic:
rw [← Quotient.smul_mk, QuotientGroup.out_eq']

Premises used: QuotientGroup.out_eq', MulAction.Quotient.smul_mk
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
inst_3 : QuotientAction β H
b : β
q : α ⧸ H
⊢ (↑(b • Quotient.out q) : α ⧸ H) = b • q

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
inst : Group α
H : Subgroup α
a : α
q : α ⧸ H
rw : (Quotient.out q)⁻¹ * (a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q * Quotient.out q) ∈ H
rw₁ :
  Eq (α := α ⧸ H) (↑(Quotient.out q) : α ⧸ H)
    (↑(a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q * Quotient.out q) : α ⧸ H)
rw₂ : q = (↑(a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q * Quotient.out q) : α ⧸ H)
rw₃ : q = (↑(a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q • Quotient.out q) : α ⧸ H)
rw₄ : q = a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q • q
rw₅ : a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q • q = q
rw₆ rw₇ : minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q ∣ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q
⊢ (Quotient.out q)⁻¹ * a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q * Quotient.out q ∈ H

Tactic:
rw [mul_assoc, ← QuotientGroup.eq, QuotientGroup.out_eq', ← smul_eq_mul, Quotient.mk_smul_out,
    eq_comm, pow_smul_eq_iff_minimalPeriod_dvd]

Premises used: QuotientGroup.out_eq', mul_assoc, QuotientGroup.eq, MulAction.pow_smul_eq_iff_minimalPeriod_dvd, eq_comm, MulAction.Quotient.mk_smul_out, smul_eq_mul
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
inst : Group α
H : Subgroup α
g : α
⊢ Eq (α := α ⧸ H) ((MulActionHom.toQuotient H : (a : α) → α ⧸ H) g : α ⧸ H) ((↑g : α ⧸ H) : α ⧸ H)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
g : HasQuotient.Quotient α (B := Subgroup α) (stabilizer α x)
g1 g2 : α
H : (leftRel (stabilizer α x) : α → α → Prop) g1 g2
rw : (g1 * (g1⁻¹ * g2)) • x = g2 • x
rw₁ rw₂ : g2 • x = g2 • x
⊢ g1 • (g1⁻¹ * g2) • x = g2 • x

Tactic:
rw [smul_smul, mul_inv_cancel_left]

Premises used: smul_smul, mul_inv_cancel_left
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
inst : Group α
inst_1 : MulAction α β
x : β
g : α
⊢ ofQuotientStabilizer α x (↑g : α ⧸ stabilizer α x) = g • x

Tactic:
rfl

Premises used: Quotient.liftOn', MulAction.ofQuotientStabilizer, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
inst : Group α
inst_1 : MulAction α β
x : β
g : HasQuotient.Quotient α (B := Subgroup α) (stabilizer α x)
⊢ ofQuotientStabilizer α x g ∈ orbit α x

Tactic:
Quotient.inductionOn' g fun g => ⟨g, rfl⟩

Premises used: Quotient.inductionOn'
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
inst : Group α
inst_1 : MulAction α β
x : β
g : α
g' : HasQuotient.Quotient α (B := Subgroup α) (stabilizer α x)
⊢ ofQuotientStabilizer α x (g • g') = g • ofQuotientStabilizer α x g'

Tactic:
Quotient.inductionOn' g' fun _ => mul_smul _ _ _

Premises used: Quotient.inductionOn'
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
inst : Group α
inst_1 : MulAction α β
x : β
y₁ y₂ : HasQuotient.Quotient α (B := Subgroup α) (stabilizer α x)
g₁ g₂ : α
H : g₁ • x = g₂ • x
rw : Membership.mem (γ := Subgroup α) (stabilizer α x) (g₁⁻¹ * g₂)
⊢ (leftRel (stabilizer α x) : α → α → Prop) g₁ g₂

Tactic:
rw [leftRel_apply]

Premises used: QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
inst : Group α
inst_1 : MulAction α β
x : β
y₁ y₂ : HasQuotient.Quotient α (B := Subgroup α) (stabilizer α x)
g₁ g₂ : α
H : g₁ • x = g₂ • x
rw : g₁⁻¹ • g₂ • x = x
rw₁ : g₁⁻¹ • g₁ • x = x
rw₂ rw₃ : x = x
⊢ (g₁⁻¹ * g₂) • x = x

Tactic:
rw [mul_smul, ← H, inv_smul_smul]

Premises used: inv_smul_smul, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 b : β
x y : HasQuotient.Quotient α (B := Subgroup α) (stabilizer α b)
hxy :
  Eq.{v + 1} (α := (↑(orbit α b) : Type v))
    ((fun (g : HasQuotient.Quotient α (B := Subgroup α) (stabilizer α b)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ orbit α b) (ofQuotientStabilizer α b g) ⋯)
      x)
    ((fun (g : HasQuotient.Quotient α (B := Subgroup α) (stabilizer α b)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ orbit α b) (ofQuotientStabilizer α b g) ⋯)
      y)
⊢ Eq.{v + 1} (α := β)
    (↑((fun (g : HasQuotient.Quotient α (B := Subgroup α) (stabilizer α b)) ↦
            Subtype.mk (p := fun (x : β) ↦ x ∈ orbit α b) (ofQuotientStabilizer α b g) ⋯)
          x) :
      β)
    (↑((fun (g : HasQuotient.Quotient α (B := Subgroup α) (stabilizer α b)) ↦
            Subtype.mk (p := fun (x : β) ↦ x ∈ orbit α b) (ofQuotientStabilizer α b g) ⋯)
          y) :
      β)

Tactic:
congr_arg Subtype.val hxy

Premises used: congr_arg, Subtype.val
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 b : β
x y : HasQuotient.Quotient α (B := Subgroup α) (stabilizer α b)
hxy :
  Eq.{v + 1} (α := (↑(orbit α b) : Type v))
    ((fun (g : HasQuotient.Quotient α (B := Subgroup α) (stabilizer α b)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ orbit α b) (ofQuotientStabilizer α b g) ⋯)
      x)
    ((fun (g : HasQuotient.Quotient α (B := Subgroup α) (stabilizer α b)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ orbit α b) (ofQuotientStabilizer α b g) ⋯)
      y)
⊢ ofQuotientStabilizer α b x = ofQuotientStabilizer α b y

Tactic:
convert! congr_arg Subtype.val hxy

Premises used: congr_arg, Subtype.val
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
inst : Group α
inst_1 : MulAction α β
b : β
inst_2 : Fintype α
inst_3 : Fintype (↑(orbit α b) : Type v)
inst_4 : Fintype ↥(stabilizer α b)
rw : Fintype.card (Prod.{v, u} (↑(orbit α b) : Type v) ↥(stabilizer α b)) = Fintype.card α
rw₁ rw₂ : Fintype.card α = Fintype.card α
⊢ Fintype.card.{v} (↑(orbit α b) : Type v) * Fintype.card.{u} ↥(stabilizer α b) = Fintype.card α

Tactic:
rw [← Fintype.card_prod, Fintype.card_congr (orbitProdStabilizerEquivGroup α b)]

Premises used: Fintype.card_congr, Fintype.card_prod, MulAction.orbitProdStabilizerEquivGroup
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
inst : Group α
inst_1 : MulAction α β
b : β
a : α
⊢ (↑(((Equiv.symm (orbitEquivQuotientStabilizer α b) :
              Equiv.{u + 1, v + 1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α b))
                (↑(orbit α b) : Type v)) :
            (a : α ⧸ stabilizer α b) → (↑(orbit α b) : Type v))
          (↑a : α ⧸ stabilizer α b)) :
      β) =
    a • b

Tactic:
rfl

Premises used: Quotient.liftOn', MulAction.ofQuotientStabilizer, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : ∀ (x : G), Membership.mem (γ := Subgroup G) (stabilizer G (α := G ⧸ H) (↑1 : G ⧸ H)) x ↔ x ∈ H
⊢ stabilizer G (α := G ⧸ H) (↑1 : G ⧸ H) = H

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : G
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (α := G ⧸ H) (↑1 : G ⧸ H)) x ↔ x ∈ H

Tactic:
simp [QuotientGroup.eq]

Premises used: QuotientGroup.eq
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : (a : α) → Fintype (↑(fixedBy β a) : Type v)
inst_4 : Fintype (Quotient (orbitRel α β))
rw : ∑ a : α, Fintype.card.{v} (↑(fixedBy β a) : Type v) = Fintype.card (Prod.{v, u} (Quotient (orbitRel α β)) α)
rw₁ : Fintype.card ((a : α) × (↑(fixedBy β a) : Type v)) = Fintype.card (Prod.{v, u} (Quotient (orbitRel α β)) α)
rw₂ rw₃ :
  Fintype.card (Prod.{v, u} (Quotient (orbitRel α β)) α) = Fintype.card (Prod.{v, u} (Quotient (orbitRel α β)) α)
⊢ ∑ a : α, Fintype.card.{v} (↑(fixedBy β a) : Type v) = Fintype.card.{v} (Quotient (orbitRel α β)) * Fintype.card α

Tactic:
rw [← Fintype.card_prod, ← Fintype.card_sigma,
    Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup α β)]

Premises used: Fintype.card_congr, Fintype.card_sigma, MulAction.sigmaFixedByEquivOrbitsProdGroup, Fintype.card_prod
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 : β
G : Type u_1
inst_2 : Group G
H : Subgroup G
x_2 : G ⧸ H
x : G
y_1 : G ⧸ H
y : G
⊢ ∃ (g : G),
    HSMul.hSMul (β := G ⧸ H) g (Quot.mk (⇑(leftRel H) : G → G → Prop) x) = Quot.mk (⇑(leftRel H) : G → G → Prop) y

Tactic:
⟨y * x⁻¹, QuotientGroup.eq.mpr ?_⟩

Premises used: Iff.mpr, HMul.hMul, QuotientGroup.eq, Inv.inv, Exists.intro
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 : β
G : Type u_1
inst_2 : Group G
H : Subgroup G
x_2 : G ⧸ H
x : G
y_1 : G ⧸ H
y : G
mk : ((fun (x_3 : G) ↦ (y * x⁻¹) • x_3) x)⁻¹ * y ∈ H
⊢ ∃ (g : G),
    HSMul.hSMul (β := G ⧸ H) g (Quot.mk (⇑(leftRel H) : G → G → Prop) x) = Quot.mk (⇑(leftRel H) : G → G → Prop) y

Tactic:
refine ⟨y * x⁻¹, QuotientGroup.eq.mpr ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 : β
G : Type u_1
inst_2 : Group G
H : Subgroup G
x_2 : G ⧸ H
x : G
y_1 : G ⧸ H
y : G
⊢ ((fun (x_3 : G) ↦ (y * x⁻¹) • x_3) x)⁻¹ * y ∈ H

Tactic:
simp only [smul_eq_mul, H.one_mem, inv_mul_cancel, inv_mul_cancel_right]

Premises used: inv_mul_cancel, Subgroup.one_mem, smul_eq_mul, inv_mul_cancel_right
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
G : Type u_1
inst_2 : Group G
H : Subgroup G
mk :
  ∀ (x : G ⧸ H) (x : G) (y : G ⧸ H) (y : G),
    ∃ (g : G),
      HSMul.hSMul (β := G ⧸ H) g (Quot.mk (⇑(leftRel H) : G → G → Prop) x) = Quot.mk (⇑(leftRel H) : G → G → Prop) y
mk₁ : ∀ (x : G ⧸ H) (x : G) (y : G ⧸ H) (y : G), ((fun (x_1 : G) ↦ (y * x⁻¹) • x_1) x)⁻¹ * y ∈ H
⊢ ∀ (x y : G ⧸ H), ∃ (g : G), g • x = y

Tactic:
{ rintro ⟨x⟩ ⟨y⟩
      refine ⟨y * x⁻¹, QuotientGroup.eq.mpr ?_⟩
      simp only [smul_eq_mul, H.one_mem, inv_mul_cancel, inv_mul_cancel_right]}

Premises used: inv_mul_cancel, Subgroup.one_mem, smul_eq_mul, inv_mul_cancel_right
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
H : Subgroup α
inst_3 : Finite.{u + 1} (α ⧸ H)
inl : ∀ (he : IsEmpty β), Finite.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)
inr : ∀ (b : β), Finite.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)
⊢ Finite.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)

Tactic:
rcases isEmpty_or_nonempty β with he | ⟨⟨b⟩⟩

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
H : Subgroup α
inst_3 : Finite.{u + 1} (α ⧸ H)
he : IsEmpty β
⊢ Finite.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)

Tactic:
Quotient.finite _

Premises used: Quotient.finite
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
H : Subgroup α
inst_3 : Finite.{u + 1} (α ⧸ H)
he : IsEmpty β
⊢ Finite.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)

Tactic:
exact Quotient.finite _

Premises used: Quotient.finite
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
H : Subgroup α
inst_3 : Finite.{u + 1} (α ⧸ H)
b : β
⊢ Finite.{u + 1} (Quotient (rightRel H))

Tactic:
have h' : Finite (Quotient (rightRel H)) :=
      Finite.of_equiv _ (quotientRightRelEquivQuotientLeftRel _).symm
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
H : Subgroup α
inst_3 : Finite.{u + 1} (α ⧸ H)
b : β
h' : Finite.{u + 1} (Quotient (rightRel H))
a : Quotient (rightRel H)
g₁ g₂ : α
r : (rightRel H : α → α → Prop) g₁ g₂
⊢ (rightRel H : α → α → Prop) g₂ g₁

Tactic:
replace r := Setoid.symm' _ r
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
H : Subgroup α
inst_3 : Finite.{u + 1} (α ⧸ H)
b : β
h' : Finite.{u + 1} (Quotient (rightRel H))
a : Quotient (rightRel H)
g₁ g₂ : α
r : (rightRel H : α → α → Prop) g₂ g₁
⊢ g₁ * g₂⁻¹ ∈ H

Tactic:
rw [rightRel_eq] at r

Premises used: QuotientGroup.rightRel_eq
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
H : Subgroup α
inst_3 : Finite.{u + 1} (α ⧸ H)
b : β
h' : Finite.{u + 1} (Quotient (rightRel H))
a : Quotient (rightRel H)
g₁ g₂ : α
r : g₁ * g₂⁻¹ ∈ H
simp : ∃ (x : ↥H), x • g₂ • b = g₁ • b
⊢ Eq.{v + 1} (α := orbitRel.Quotient.{u, v} (↥H) β) ((fun (g : α) ↦ ⟦g • b⟧) g₁) ((fun (g : α) ↦ ⟦g • b⟧) g₂)

Tactic:
simp only [Quotient.eq, orbitRel_apply, mem_orbit_iff]

Premises used: MulAction.mem_orbit_iff, MulAction.orbitRel_apply, Quotient.eq