awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
⊢ IsMultiplyPretransitive G α n.succ ↔ IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
have refine_1 : ∀ (hn : IsMultiplyPretransitive G α n.succ) (x y : Fin n ↪ ↥(ofStabilizer G a)), ∃ (g : ↥(stabilizer G a)), g • x = y
Tactic: refine ⟨fun hn ↦ ⟨fun x y ↦ ?_⟩, fun hn ↦ ⟨fun x y ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
refine_1 :
  ∀ (hn : IsMultiplyPretransitive G α n.succ) (x y : Fin n ↪ ↥(ofStabilizer G a)), ∃ (g : ↥(stabilizer G a)), g • x = y
⊢ IsMultiplyPretransitive G α n.succ ↔ IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
have refine_2 : ∀ (hn : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n) (x y : Fin n.succ ↪ α),
  ∃ (g : G), g • x = y
Tactic: refine ⟨fun hn ↦ ⟨fun x y ↦ ?_⟩, fun hn ↦ ⟨fun x y ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
⊢ ∃ (g : ↥(stabilizer G a)), g • x = y
have refine_1 : ∀ (g : G) (hgxy : g • snoc x = snoc y), ∃ (g : ↥(stabilizer G a)), g • x = y
Tactic: obtain ⟨g, hgxy⟩ := exists_smul_eq G (ofStabilizer.snoc x) (ofStabilizer.snoc y)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : g • snoc x = snoc y
⊢ Membership.mem (γ := Subgroup G) (stabilizer G a) g
have hgxy₁ : ∀ (x_1 : Fin n.succ),
  Eq (α := α) ((g • snoc x : (a : Fin n.succ) → α) x_1 : α) ((snoc y : (a : Fin n.succ) → α) x_1 : α)
Tactic: rw [DFunLike.ext_iff] at hgxy
Cleared hypotheses: hgxy
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy :
  ∀ (x_1 : Fin n.succ),
    Eq (α := α) ((g • snoc x : (a : Fin n.succ) → α) x_1 : α) ((snoc y : (a : Fin n.succ) → α) x_1 : α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G a) g
have a₁ : Membership.mem (γ := Subgroup G) (stabilizer G a) g ↔
  Eq (α := α) ((g • snoc x : (a : Fin n.succ) → α) (last n) : α) ((snoc y : (a : Fin n.succ) → α) (last n) : α)
Tactic: convert! hgxy (last n)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : g • snoc x = snoc y
⊢ ∃ (g : ↥(stabilizer G a)), g • x = y
have hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
Tactic: have hg : g ∈ stabilizer G a := by
      rw [DFunLike.ext_iff] at hgxy
      convert! hgxy (last n)
      simp [ofStabilizer.snoc_last]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : g • snoc x = snoc y
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
⊢ ∃ (g : ↥(stabilizer G a)), g • x = y
have h : Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • x = y
Tactic: use ⟨g, hg⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : g • snoc x = snoc y
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
⊢ Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • x = y
have h : ∀ (i : Fin n),
  Eq.{u_2 + 1} (α := α)
    (↑((Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • x :
            (a_1 : Fin n) → ↥(ofStabilizer G a))
          i) :
      α)
    (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
Tactic: ext i
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : g • snoc x = snoc y
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
i : Fin n
⊢ Eq.{u_2 + 1} (α := α)
    (↑((Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • x :
            (a_1 : Fin n) → ↥(ofStabilizer G a))
          i) :
      α)
    (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
have h : HSMul.hSMul (β := α) g (↑((x : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α) =
  (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
Tactic: simp only [smul_apply, SubMulAction.val_smul_of_tower, subgroup_smul_def]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : g • snoc x = snoc y
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
i : Fin n
⊢ HSMul.hSMul (β := α) g (↑((x : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α) =
    (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
have h : HSMul.hSMul (β := α) g ((snoc x : (a : Fin n.succ) → α) i.castSucc : α) =
  (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
Tactic: rw [← ofStabilizer.snoc_castSucc x, ← smul_apply, hgxy, ofStabilizer.snoc_castSucc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : g • snoc x = snoc y
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
i : Fin n
h :
  HSMul.hSMul (β := α) g ((snoc x : (a : Fin n.succ) → α) i.castSucc : α) =
    (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
⊢ HSMul.hSMul (β := α) g (↑((x : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α) =
    (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
have h₁ : Eq (α := α) ((g • snoc x : (a : Fin n.succ) → α) i.castSucc : α)
  ((↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α) : α)
Tactic: rw [← ofStabilizer.snoc_castSucc x, ← smul_apply, hgxy, ofStabilizer.snoc_castSucc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : g • snoc x = snoc y
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
i : Fin n
h :
  HSMul.hSMul (β := α) g ((snoc x : (a : Fin n.succ) → α) i.castSucc : α) =
    (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
h₁ :
  Eq (α := α) ((g • snoc x : (a : Fin n.succ) → α) i.castSucc : α)
    ((↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α) : α)
⊢ HSMul.hSMul (β := α) g (↑((x : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α) =
    (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
have h₂ : Eq (α := α) ((snoc y : (a : Fin n.succ) → α) i.castSucc : α) ((↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α) : α)
Tactic: rw [← ofStabilizer.snoc_castSucc x, ← smul_apply, hgxy, ofStabilizer.snoc_castSucc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : g • snoc x = snoc y
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
i : Fin n
h :
  HSMul.hSMul (β := α) g ((snoc x : (a : Fin n.succ) → α) i.castSucc : α) =
    (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
h₁ :
  Eq (α := α) ((g • snoc x : (a : Fin n.succ) → α) i.castSucc : α)
    ((↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α) : α)
h₂ :
  Eq (α := α) ((snoc y : (a : Fin n.succ) → α) i.castSucc : α)
    ((↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α) : α)
⊢ HSMul.hSMul (β := α) g (↑((x : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α) =
    (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
have h₃ : Eq.{u_2 + 1} (α := α) (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
  (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
Tactic: rw [← ofStabilizer.snoc_castSucc x, ← smul_apply, hgxy, ofStabilizer.snoc_castSucc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
x y : Fin n.succ ↪ α
⊢ ∃ (g : G), g • x = y
have refine_2 : ∀ (gx : G) (x1 : Fin n ↪ ↥(ofStabilizer G a)) (hgx : gx • x = snoc x1), ∃ (g : G), g • x = y
Tactic: obtain ⟨gx, x1, hgx⟩ := exists_smul_of_last_eq G a x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
x y : Fin n.succ ↪ α
gx : G
x1 : Fin n ↪ ↥(ofStabilizer G a)
hgx : gx • x = snoc x1
⊢ ∃ (g : G), g • x = y
have refine_2 : ∀ (gy : G) (y1 : Fin n ↪ ↥(ofStabilizer G a)) (hgy : gy • y = snoc y1), ∃ (g : G), g • x = y
Tactic: obtain ⟨gy, y1, hgy⟩ := exists_smul_of_last_eq G a y
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
x y : Fin n.succ ↪ α
gx : G
x1 : Fin n ↪ ↥(ofStabilizer G a)
hgx : gx • x = snoc x1
gy : G
y1 : Fin n ↪ ↥(ofStabilizer G a)
hgy : gy • y = snoc y1
⊢ ∃ (g : G), g • x = y
have refine_2 : ∀ (g : ↥(stabilizer G a)) (hg : g • x1 = y1), ∃ (g : G), g • x = y
Tactic: obtain ⟨g, hg⟩ := hn.exists_smul_eq x1 y1
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
x y : Fin n.succ ↪ α
gx : G
x1 : Fin n ↪ ↥(ofStabilizer G a)
hgx : gx • x = snoc x1
gy : G
y1 : Fin n ↪ ↥(ofStabilizer G a)
hgy : gy • y = snoc y1
g : ↥(stabilizer G a)
hg : g • x1 = y1
⊢ ∃ (g : G), g • x = y
have h : (gy⁻¹ * (↑g : G) * gx) • x = y
Tactic: use gy⁻¹ * g * gx
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
x y : Fin n.succ ↪ α
gx : G
x1 : Fin n ↪ ↥(ofStabilizer G a)
hgx : gx • x = snoc x1
gy : G
y1 : Fin n ↪ ↥(ofStabilizer G a)
hgy : gy • y = snoc y1
g : ↥(stabilizer G a)
hg : g • x1 = y1
⊢ (gy⁻¹ * (↑g : G) * gx) • x = y
have h : ∀ (i : Fin n.succ),
  Eq (α := α) (((gy⁻¹ * (↑g : G) * gx) • x : (a : Fin n.succ) → α) i : α) ((y : (a : Fin n.succ) → α) i : α)
Tactic: ext i
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
x y : Fin n.succ ↪ α
gx : G
x1 : Fin n ↪ ↥(ofStabilizer G a)
hgx : gx • x = snoc x1
gy : G
y1 : Fin n ↪ ↥(ofStabilizer G a)
hgy : gy • y = snoc y1
g : ↥(stabilizer G a)
hg : g • x1 = y1
i : Fin n.succ
⊢ Eq (α := α) (((gy⁻¹ * (↑g : G) * gx) • x : (a : Fin n.succ) → α) i : α) ((y : (a : Fin n.succ) → α) i : α)
have h : (↑g : G) • HSMul.hSMul (β := α) gx ((x : (a : Fin n.succ) → α) i : α) =
  HSMul.hSMul (β := α) gy ((y : (a : Fin n.succ) → α) i : α)
Tactic: simp only [mul_smul, smul_apply, inv_smul_eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
x y : Fin n.succ ↪ α
gx : G
x1 : Fin n ↪ ↥(ofStabilizer G a)
hgx : gx • x = snoc x1
gy : G
y1 : Fin n ↪ ↥(ofStabilizer G a)
hgy : gy • y = snoc y1
g : ↥(stabilizer G a)
hg : g • x1 = y1
i : Fin n.succ
⊢ (↑g : G) • HSMul.hSMul (β := α) gx ((x : (a : Fin n.succ) → α) i : α) =
    HSMul.hSMul (β := α) gy ((y : (a : Fin n.succ) → α) i : α)
have h : Eq (α := α) (((↑g : G) • snoc x1 : (a : Fin n.succ) → α) i : α) ((snoc y1 : (a : Fin n.succ) → α) i : α)
Tactic: simp only [← smul_apply _ _ i, hgy, hgx]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
x y : Fin n.succ ↪ α
gx : G
x1 : Fin n ↪ ↥(ofStabilizer G a)
hgx : gx • x = snoc x1
gy : G
y1 : Fin n ↪ ↥(ofStabilizer G a)
hgy : gy • y = snoc y1
g : ↥(stabilizer G a)
hg : g • x1 = y1
i : Fin n.succ
⊢ Eq (α := α) (((↑g : G) • snoc x1 : (a : Fin n.succ) → α) i : α) ((snoc y1 : (a : Fin n.succ) → α) i : α)
have h : HSMul.hSMul (β := α) (↑g : G) ((snoc x1 : (a : Fin n.succ) → α) i : α) = (snoc y1 : (a : Fin n.succ) → α) i
Tactic: simp only [smul_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
x y : Fin n.succ ↪ α
gx : G
x1 : Fin n ↪ ↥(ofStabilizer G a)
hgx : gx • x = snoc x1
gy : G
y1 : Fin n ↪ ↥(ofStabilizer G a)
hgy : gy • y = snoc y1
g : ↥(stabilizer G a)
hg : g • x1 = y1
i : Fin n.succ
⊢ HSMul.hSMul (β := α) (↑g : G) ((snoc x1 : (a : Fin n.succ) → α) i : α) = (snoc y1 : (a : Fin n.succ) → α) i
have h : ∀ (i : Fin n),
  HSMul.hSMul (β := α) (↑g : G) ((snoc x1 : (a : Fin n.succ) → α) i.castSucc : α) =
    (snoc y1 : (a : Fin n.succ) → α) i.castSucc
Tactic: rcases Fin.eq_castSucc_or_eq_last i with ⟨i, rfl⟩ | ⟨rfl⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
x y : Fin n.succ ↪ α
gx : G
x1 : Fin n ↪ ↥(ofStabilizer G a)
hgx : gx • x = snoc x1
gy : G
y1 : Fin n ↪ ↥(ofStabilizer G a)
hgy : gy • y = snoc y1
g : ↥(stabilizer G a)
hg : g • x1 = y1
i : Fin n.succ
h :
  ∀ (i : Fin n),
    HSMul.hSMul (β := α) (↑g : G) ((snoc x1 : (a : Fin n.succ) → α) i.castSucc : α) =
      (snoc y1 : (a : Fin n.succ) → α) i.castSucc
⊢ HSMul.hSMul (β := α) (↑g : G) ((snoc x1 : (a : Fin n.succ) → α) i : α) = (snoc y1 : (a : Fin n.succ) → α) i
have h₁ : HSMul.hSMul (β := α) (↑g : G) ((snoc x1 : (a : Fin n.succ) → α) (last n) : α) =
  (snoc y1 : (a : Fin n.succ) → α) (last n)
Tactic: rcases Fin.eq_castSucc_or_eq_last i with ⟨i, rfl⟩ | ⟨rfl⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
x y : Fin n.succ ↪ α
gx : G
x1 : Fin n ↪ ↥(ofStabilizer G a)
hgx : gx • x = snoc x1
gy : G
y1 : Fin n ↪ ↥(ofStabilizer G a)
hgy : gy • y = snoc y1
g : ↥(stabilizer G a)
hg : g • x1 = y1
⊢ HSMul.hSMul (β := α) (↑g : G) ((snoc x1 : (a : Fin n.succ) → α) (last n) : α) =
    (snoc y1 : (a : Fin n.succ) → α) (last n)
have h : (↑g : G) • a = a
Tactic: simp only [ofStabilizer.snoc_last, ← hg]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
⊢ ∃ (g : ↥(fixingSubgroup G s)), g • x = y
have this : IsMultiplyPretransitive G α (s.ncard + m)
Tactic: have : IsMultiplyPretransitive G α (s.ncard + m) := by rw [hmn]; infer_instance
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
⊢ ∃ (g : ↥(fixingSubgroup G s)), g • x = y
have Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
Tactic: have Hs : Nonempty (Fin (s.ncard) ≃ s) :=
      Finite.card_eq.mp (by simp [Nat.card_coe_set_eq])
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
⊢ ∃ (g : ↥(fixingSubgroup G s)), g • x = y
have hx : let x' := append (s := s) x;
x' = append (s := s) x
Tactic: set x' := ofFixingSubgroup.append x with hx
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
⊢ ∃ (g : ↥(fixingSubgroup G s)), g • x = y
have hy : let y' := append (s := s) y;
y' = append (s := s) y
Tactic: set y' := ofFixingSubgroup.append y with hy
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
⊢ ∃ (g : ↥(fixingSubgroup G s)), g • x = y
have obtain : ∀ (g : G) (hg : g • x' = y'), ∃ (g : ↥(fixingSubgroup G s)), g • x = y
Tactic: obtain ⟨g, hg⟩ := exists_smul_eq G x' y'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this_1 : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
this : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) g
⊢ ∃ (g : ↥(fixingSubgroup G s)), g • x = y
have h : Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (fixingSubgroup G s) x) g this • x = y
Tactic: use ⟨g, this⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this_1 : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
this : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) g
⊢ Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (fixingSubgroup G s) x) g this • x = y
have h : ∀ (i : Fin m),
  Eq.{u_2 + 1} (α := α)
    (↑((Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (fixingSubgroup G s) x) g this • x :
            (a : Fin m) → ↥(ofFixingSubgroup G s))
          i) :
      α)
    (↑((y : (a : Fin m) → ↥(ofFixingSubgroup G s)) i) : α)
Tactic: ext i
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this_1 : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
this : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) g
i : Fin m
⊢ Eq.{u_2 + 1} (α := α)
    (↑((Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (fixingSubgroup G s) x) g this • x :
            (a : Fin m) → ↥(ofFixingSubgroup G s))
          i) :
      α)
    (↑((y : (a : Fin m) → ↥(ofFixingSubgroup G s)) i) : α)
have h : HSMul.hSMul (β := α) g (↑((x : (a : Fin m) → ↥(ofFixingSubgroup G s)) i) : α) =
  (↑((y : (a : Fin m) → ↥(ofFixingSubgroup G s)) i) : α)
Tactic: rw [smul_apply, SetLike.val_smul, Subgroup.mk_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
⊢ ∃ (g : ↥(fixingSubgroup G s)), g • x = y
have suffices : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) g
Tactic: suffices g ∈ fixingSubgroup G s by
      use ⟨g, this⟩
      ext i
      rw [smul_apply, SetLike.val_smul, Subgroup.mk_smul]
      simp [← ofFixingSubgroup.append_right, ← smul_apply, ← hx, ← hy, hg]