awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ (x • x_1)⁻¹ * x • x_2 ∈ H
have rwa₄ : x_1⁻¹ * (x_2 * unop x) * (unop x)⁻¹ ∈ 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ (x • x_1)⁻¹ * x • x_2 ∈ H
have rwa₅ : x_1⁻¹ * (x_2 * unop x * (unop x)⁻¹) ∈ 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
have rw : HSMul.hSMul (β := α ⧸ H) b (↑(Quotient.out q) : α ⧸ H) = b • q
Tactic: rw [← Quotient.smul_mk, QuotientGroup.out_eq']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ (↑(b • Quotient.out q) : α ⧸ H) = b • q
have rw₁ : b • q = b • q
Tactic: rw [← Quotient.smul_mk, QuotientGroup.out_eq']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
inst : Group α
H : Subgroup α
a : α
q : α ⧸ H
⊢ (Quotient.out q)⁻¹ * a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q * Quotient.out q ∈ H
have rw : (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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ (Quotient.out q)⁻¹ * a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q * Quotient.out q ∈ H
have rw₁ : Eq (α := α ⧸ H) (↑(Quotient.out q) : α ⧸ H) (↑(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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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)
⊢ (Quotient.out q)⁻¹ * a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q * Quotient.out q ∈ H
have rw₂ : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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)
⊢ (Quotient.out q)⁻¹ * a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q * Quotient.out q ∈ H
have rw₃ : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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)
⊢ (Quotient.out q)⁻¹ * a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q * Quotient.out q ∈ H
have rw₄ : q = a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q • q
Tactic: rw [mul_assoc, ← QuotientGroup.eq, QuotientGroup.out_eq', ← smul_eq_mul, Quotient.mk_smul_out,
    eq_comm, pow_smul_eq_iff_minimalPeriod_dvd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ (Quotient.out q)⁻¹ * a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q * Quotient.out q ∈ H
have rw₅ : a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q • q = q
Tactic: rw [mul_assoc, ← QuotientGroup.eq, QuotientGroup.out_eq', ← smul_eq_mul, Quotient.mk_smul_out,
    eq_comm, pow_smul_eq_iff_minimalPeriod_dvd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ (Quotient.out q)⁻¹ * a ^ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q * Quotient.out q ∈ H
have rw₆ : minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q ∣ minimalPeriod (fun (x : α ⧸ H) ↦ a • x) q
Tactic: rw [mul_assoc, ← QuotientGroup.eq, QuotientGroup.out_eq', ← smul_eq_mul, Quotient.mk_smul_out,
    eq_comm, pow_smul_eq_iff_minimalPeriod_dvd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ g1 • (g1⁻¹ * g2) • x = g2 • x
have rw : (g1 * (g1⁻¹ * g2)) • x = g2 • x
Tactic: rw [smul_smul, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ g1 • (g1⁻¹ * g2) • x = g2 • x
have rw₁ : g2 • x = g2 • x
Tactic: rw [smul_smul, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ (leftRel (stabilizer α x) : α → α → Prop) g₁ g₂
have rw : Membership.mem (γ := Subgroup α) (stabilizer α x) (g₁⁻¹ * g₂)
Tactic: rw [leftRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ (g₁⁻¹ * g₂) • x = x
have rw : g₁⁻¹ • g₂ • x = x
Tactic: rw [mul_smul, ← H, inv_smul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ (g₁⁻¹ * g₂) • x = x
have rw₁ : g₁⁻¹ • g₁ • x = x
Tactic: rw [mul_smul, ← H, inv_smul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ (g₁⁻¹ * g₂) • x = x
have rw₂ : x = x
Tactic: rw [mul_smul, ← H, inv_smul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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)
⊢ Fintype.card.{v} (↑(orbit α b) : Type v) * Fintype.card.{u} ↥(stabilizer α b) = Fintype.card α
have rw : Fintype.card (Prod.{v, u} (↑(orbit α b) : Type v) ↥(stabilizer α b)) = Fintype.card α
Tactic: rw [← Fintype.card_prod, Fintype.card_congr (orbitProdStabilizerEquivGroup α b)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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 α
⊢ Fintype.card.{v} (↑(orbit α b) : Type v) * Fintype.card.{u} ↥(stabilizer α b) = Fintype.card α
have rw₁ : Fintype.card α = Fintype.card α
Tactic: rw [← Fintype.card_prod, Fintype.card_congr (orbitProdStabilizerEquivGroup α b)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ stabilizer G (α := G ⧸ H) (↑1 : G ⧸ H) = H
have h : ∀ (x : G), Membership.mem (γ := Subgroup G) (stabilizer G (α := G ⧸ H) (↑1 : G ⧸ H)) x ↔ x ∈ H
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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 α β))
⊢ ∑ a : α, Fintype.card.{v} (↑(fixedBy β a) : Type v) = Fintype.card.{v} (Quotient (orbitRel α β)) * Fintype.card α
have rw : ∑ a : α, Fintype.card.{v} (↑(fixedBy β a) : Type v) = Fintype.card (Prod.{v, u} (Quotient (orbitRel α β)) α)
Tactic: rw [← Fintype.card_prod, ← Fintype.card_sigma,
    Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup α β)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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 α β)) α)
⊢ ∑ a : α, Fintype.card.{v} (↑(fixedBy β a) : Type v) = Fintype.card.{v} (Quotient (orbitRel α β)) * Fintype.card α
have rw₁ : Fintype.card ((a : α) × (↑(fixedBy β a) : Type v)) = Fintype.card (Prod.{v, u} (Quotient (orbitRel α β)) α)
Tactic: rw [← Fintype.card_prod, ← Fintype.card_sigma,
    Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup α β)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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 α β)) α)
⊢ ∑ a : α, Fintype.card.{v} (↑(fixedBy β a) : Type v) = Fintype.card.{v} (Quotient (orbitRel α β)) * Fintype.card α
have rw₂ : Fintype.card (Prod.{v, u} (Quotient (orbitRel α β)) α) = Fintype.card (Prod.{v, u} (Quotient (orbitRel α β)) α)
Tactic: rw [← Fintype.card_prod, ← Fintype.card_sigma,
    Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup α β)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
have mk : ((fun (x_3 : G) ↦ (y * x⁻¹) • x_3) x)⁻¹ * y ∈ H
Tactic: refine ⟨y * x⁻¹, QuotientGroup.eq.mpr ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
G : Type u_1
inst_2 : Group G
H : Subgroup G
⊢ ∀ (x y : G ⧸ H), ∃ (g : G), g • x = y
have 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
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]}
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ ∀ (x y : G ⧸ H), ∃ (g : G), g • x = y
have mk₁ : ∀ (x : G ⧸ H) (x : G) (y : G ⧸ H) (y : G), ((fun (x_1 : G) ↦ (y * x⁻¹) • x_1) x)⁻¹ * y ∈ H
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]}
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
H : Subgroup α
inst_3 : Finite.{u + 1} (α ⧸ H)
⊢ Finite.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)
have inl : ∀ (he : IsEmpty β), Finite.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)
Tactic: rcases isEmpty_or_nonempty β with he | ⟨⟨b⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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) β)
⊢ Finite.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)
have inr : ∀ (b : β), Finite.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)
Tactic: rcases isEmpty_or_nonempty β with he | ⟨⟨b⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (hypothesis)
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.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)
have h' : Finite.{u + 1} (Quotient (rightRel H))
Tactic: have h' : Finite (Quotient (rightRel H)) :=
      Finite.of_equiv _ (quotientRightRelEquivQuotientLeftRel _).symm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (hypothesis)
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₂
⊢ Eq.{v + 1} (α := orbitRel.Quotient.{u, v} (↥H) β) ((fun (g : α) ↦ ⟦g • b⟧) g₁) ((fun (g : α) ↦ ⟦g • b⟧) g₂)
have r₁ : (rightRel H : α → α → Prop) g₂ g₁
Tactic: replace r := Setoid.symm' _ r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (hypothesis)
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₁
⊢ Eq.{v + 1} (α := orbitRel.Quotient.{u, v} (↥H) β) ((fun (g : α) ↦ ⟦g • b⟧) g₁) ((fun (g : α) ↦ ⟦g • b⟧) g₂)
have r₁ : g₁ * g₂⁻¹ ∈ H
Tactic: rw [rightRel_eq] at r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
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
⊢ Eq.{v + 1} (α := orbitRel.Quotient.{u, v} (↥H) β) ((fun (g : α) ↦ ⟦g • b⟧) g₁) ((fun (g : α) ↦ ⟦g • b⟧) g₂)
have simp : ∃ (x : ↥H), x • g₂ • b = g₁ • b
Tactic: simp only [Quotient.eq, orbitRel_apply, mem_orbit_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 : β
H : Subgroup α
ω : Quotient (orbitRel α β)
q : orbitRel.Quotient.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v)
x : (↑(orbitRel.Quotient.orbit ω) : Type v)
⊢ ⟦(↑x : β)⟧ = ω
have hx : (↑x : β) ∈ orbitRel.Quotient.orbit ω
Tactic: have hx := x.property
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 : β
H : Subgroup α
ω : Quotient (orbitRel α β)
q : orbitRel.Quotient.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v)
x : (↑(orbitRel.Quotient.orbit ω) : Type v)
hx : (↑x : β) ∈ orbitRel.Quotient.orbit ω
⊢ ⟦(↑x : β)⟧ = ω
have rwa : ∀ (hx : Quotient.mk'' (↑x : β) = ω), ⟦(↑x : β)⟧ = ω
Tactic: rwa [orbitRel.Quotient.mem_orbit] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
H : Subgroup α
ω : Quotient (orbitRel α β)
q : orbitRel.Quotient.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v)
a b : (↑(orbitRel.Quotient.orbit ω) : Type v)
h :
  (orbitRel ↥H (↑(orbitRel.Quotient.orbit ω) : Type v) :
      (↑(orbitRel.Quotient.orbit ω) : Type v) → (↑(orbitRel.Quotient.orbit ω) : Type v) → Prop)
    a b
⊢ Eq.{v + 1} (α :=
    Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
      (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω})) (orbitRel.{u, v} (↥H) β)))
    ((fun (x : (↑(orbitRel.Quotient.orbit ω) : Type v)) ↦
        (⟦Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑x : β) ⋯⟧ :
          Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
            (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}))
              (orbitRel.{u, v} (↥H) β))))
      a)
    ((fun (x : (↑(orbitRel.Quotient.orbit ω) : Type v)) ↦
        (⟦Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑x : β) ⋯⟧ :
          Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
            (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}))
              (orbitRel.{u, v} (↥H) β))))
      b)
have h₁ : ⟦(↑a : β)⟧ = ⟦(↑b : β)⟧
Tactic: simp only [← Quotient.eq, orbitRel.Quotient.subgroup_quotient_eq_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
H : Subgroup α
ω : Quotient (orbitRel α β)
q : orbitRel.Quotient.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v)
a b : (↑(orbitRel.Quotient.orbit ω) : Type v)
h : ⟦(↑a : β)⟧ = ⟦(↑b : β)⟧
⊢ Eq.{v + 1} (α :=
    Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
      (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω})) (orbitRel.{u, v} (↥H) β)))
    ((fun (x : (↑(orbitRel.Quotient.orbit ω) : Type v)) ↦
        (⟦Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑x : β) ⋯⟧ :
          Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
            (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}))
              (orbitRel.{u, v} (↥H) β))))
      a)
    ((fun (x : (↑(orbitRel.Quotient.orbit ω) : Type v)) ↦
        (⟦Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑x : β) ⋯⟧ :
          Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
            (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}))
              (orbitRel.{u, v} (↥H) β))))
      b)
have simp : ∀ (h : (orbitRel (↥H) β : β → β → Prop) (↑a : β) (↑b : β)),
  (Setoid.comap Subtype.val (orbitRel (↥H) β) :
      { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} } → { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} } → Prop)
    (Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑a : β) sorry)
    (Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑b : β) sorry)
Tactic: simp only [Quotient.eq] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 : β
H : Subgroup α
ω : Quotient (orbitRel α β)
q :
  Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
    (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω})) (orbitRel.{u, v} (↥H) β))
x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }
⊢ (↑x : β) ∈ orbitRel.Quotient.orbit ω
have hx : (↑x : β) ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}
Tactic: have hx := x.property
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 : β
H : Subgroup α
ω : Quotient (orbitRel α β)
q :
  Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
    (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω})) (orbitRel.{u, v} (↥H) β))
x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }
hx : (↑x : β) ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}
⊢ (↑x : β) ∈ orbitRel.Quotient.orbit ω
have hx₁ : ⟦(↑x : β)⟧ = ω
Tactic: simp only [Set.mem_preimage, Set.mem_singleton_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 : β
H : Subgroup α
ω : Quotient (orbitRel α β)
q :
  Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
    (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω})) (orbitRel.{u, v} (↥H) β))
x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }
hx : ⟦(↑x : β)⟧ = ω
⊢ (↑x : β) ∈ orbitRel.Quotient.orbit ω
have rwa : Quotient.mk'' (↑x : β) = ω
Tactic: rwa [orbitRel.Quotient.mem_orbit, @Quotient.mk''_eq_mk]