awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
this : IsPretransitive G α
B : Set α
hB : ∀ ⦃g : G⦄ ⦃a : α⦄, a ∈ B → g • a ∈ B → g • B = B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
h_1 : Membership.mem (γ := Set α) ⊤ c
h' : ¬a = c
g : G
hga : g • a = a
hgb : g • b = c
⊢ a ∈ B

Tactic:
exact ha
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
this : IsPretransitive G α
B : Set α
hB : ∀ ⦃g : G⦄ ⦃a : α⦄, a ∈ B → g • a ∈ B → g • B = B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
h_1 : Membership.mem (γ := Set α) ⊤ c
h' : ¬a = c
g : G
hga : g • a = a
hgb : g • b = c
neg : g • b ∈ g • B
⊢ c ∈ B

Tactic:
rw [← hB (g := g) ha (by rw [hga]; exact ha), ← hgb]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
this : IsPretransitive G α
B : Set α
hB : ∀ ⦃g : G⦄ ⦃a : α⦄, a ∈ B → g • a ∈ B → g • B = B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
h_1 : Membership.mem (γ := Set α) ⊤ c
h' : ¬a = c
g : G
hga : g • a = a
hgb : g • b = c
⊢ g • b ∈ g • B

Tactic:
smul_mem_smul_set hb

Premises used: Set.smul_mem_smul_set
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
this : IsPretransitive G α
B : Set α
hB : ∀ ⦃g : G⦄ ⦃a : α⦄, a ∈ B → g • a ∈ B → g • B = B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
h_1 : Membership.mem (γ := Set α) ⊤ c
h' : ¬a = c
g : G
hga : g • a = a
hgb : g • b = c
⊢ g • b ∈ g • B

Tactic:
exact smul_mem_smul_set hb

Premises used: Set.smul_mem_smul_set
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
inst_2 : IsMultiplyPretransitive G α n
hmn : m ≤ n
hα : (↑n : ℕ∞) ≤ ENat.card α
obtain :
  ∀ (p : ℕ) [IsMultiplyPretransitive G α (m + p)] (hmn : m ≤ m + p) (hα : (↑(m + p) : ℕ∞) ≤ ENat.card α),
    IsMultiplyPretransitive G α m
⊢ IsMultiplyPretransitive G α m

Tactic:
obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hmn

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m p : ℕ
inst_2 : IsMultiplyPretransitive G α (m + p)
hmn : m ≤ m + p
hα : (↑(m + p) : ℕ∞) ≤ ENat.card α
⊢ IsMultiplyPretransitive G α m

Tactic:
IsPretransitive.of_surjective_map
    (f := embMap G α (castAddEmb p))
    (Fin.Embedding.restrictSurjective_of_add_le_ENatCard hα) inferInstance

Premises used: inferInstance, Fin.Embedding.restrictSurjective_of_add_le_ENatCard, MulAction.IsPretransitive.of_surjective_map
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m p : ℕ
inst_2 : IsMultiplyPretransitive G α (m + p)
hmn : m ≤ m + p
hα : (↑(m + p) : ℕ∞) ≤ ENat.card α
⊢ IsMultiplyPretransitive G α m

Tactic:
exact IsPretransitive.of_surjective_map
    (f := embMap G α (castAddEmb p))
    (Fin.Embedding.restrictSurjective_of_add_le_ENatCard hα) inferInstance

Premises used: inferInstance, Fin.Embedding.restrictSurjective_of_add_le_ENatCard, MulAction.IsPretransitive.of_surjective_map
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
inst_2 : IsMultiplyPretransitive G α n
hmn : m ≤ n
hα : n ≤ Nat.card α
inst_3 : Finite α
obtain :
  ∀ (p : ℕ) [IsMultiplyPretransitive G α (m + p)] (hmn : m ≤ m + p) (hα : m + p ≤ Nat.card α),
    IsMultiplyPretransitive G α m
⊢ IsMultiplyPretransitive G α m

Tactic:
obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hmn

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m : ℕ
inst_2 : Finite α
p : ℕ
inst_3 : IsMultiplyPretransitive G α (m + p)
hmn : m ≤ m + p
hα : m + p ≤ Nat.card α
⊢ IsMultiplyPretransitive G α m

Tactic:
IsPretransitive.of_surjective_map (f := embMap G α (castAddEmb p))
    (Fin.Embedding.restrictSurjective_of_add_le_natCard hα) inferInstance

Premises used: inferInstance, Fin.Embedding.restrictSurjective_of_add_le_natCard, MulAction.IsPretransitive.of_surjective_map
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m : ℕ
inst_2 : Finite α
p : ℕ
inst_3 : IsMultiplyPretransitive G α (m + p)
hmn : m ≤ m + p
hα : m + p ≤ Nat.card α
⊢ IsMultiplyPretransitive G α m

Tactic:
exact IsPretransitive.of_surjective_map (f := embMap G α (castAddEmb p))
    (Fin.Embedding.restrictSurjective_of_add_le_natCard hα) inferInstance

Premises used: inferInstance, Fin.Embedding.restrictSurjective_of_add_le_natCard, MulAction.IsPretransitive.of_surjective_map
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a b : α
g : G
hg : b = g • a
⊢ IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a) ↔
    IsPretransitive.{u_1, u_2} ↥(stabilizer G b) ↥(ofStabilizer G b)

Tactic:
isPretransitive_congr (MulEquiv.surjective _) (ofStabilizer.conjMap_bijective hg)

Premises used: Set.Mem, MulEquiv.surjective, MulAction.isPretransitive_congr, SubMulAction.ofStabilizer.conjMap_bijective
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
a b : α
⊢ IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a) ↔
    IsPretransitive.{u_1, u_2} ↥(stabilizer G b) ↥(ofStabilizer G b)

Tactic:
let ⟨_, hg⟩ := exists_smul_eq G a b
  isPretransitive_iff_of_conj hg.symm

Premises used: SubMulAction.ofStabilizer.isPretransitive_iff_of_conj, MulAction.IsPretransitive, Membership.mem, Subtype, SubMulAction.ofStabilizer, _private.0.SubMulAction.ofStabilizer.isPretransitive_iff.match_1, Iff, MulAction.stabilizer, Eq.symm, MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
n : ℕ
a b : α
g : G
hg : b = g • a
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n ↔
    IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G b)) (↥(ofStabilizer G b)) n

Tactic:
IsPretransitive.of_embedding_congr (MulEquiv.surjective _) (ofStabilizer.conjMap_bijective hg)

Premises used: MulEquiv.surjective, SubMulAction.ofStabilizer.conjMap_bijective, MulAction.IsPretransitive.of_embedding_congr
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a b : α
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n ↔
    IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G b)) (↥(ofStabilizer G b)) n

Tactic:
let ⟨_, hg⟩ := exists_smul_eq G a b
  isMultiplyPretransitive_iff_of_conj hg.symm

Premises used: Membership.mem, SubMulAction.ofStabilizer.isMultiplyPretransitive_iff_of_conj, Subtype, SubMulAction.ofStabilizer, _private.0.SubMulAction.ofStabilizer.isPretransitive_iff.match_1, Iff, MulAction.IsMultiplyPretransitive, MulAction.stabilizer, Eq.symm, MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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

Tactic:
⟨fun hn ↦ ⟨fun x y ↦ ?_⟩, fun hn ↦ ⟨fun x y ↦ ?_⟩⟩

Premises used: MulAction.IsPretransitive.mk, Iff.intro
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
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
⊢ IsMultiplyPretransitive G α n.succ ↔ IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) n

Tactic:
refine ⟨fun hn ↦ ⟨fun x y ↦ ?_⟩, fun hn ↦ ⟨fun x y ↦ ?_⟩⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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)
refine_1 : ∀ (g : G) (hgxy : g • snoc x = snoc y), ∃ (g : ↥(stabilizer G a)), g • x = y
⊢ ∃ (g : ↥(stabilizer G a)), g • x = y

Tactic:
obtain ⟨g, hgxy⟩ := exists_smul_eq G (ofStabilizer.snoc x) (ofStabilizer.snoc y)

Premises used: SubMulAction.ofStabilizer.snoc, MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
⊢ ∀ (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

Premises used: DFunLike.ext_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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 : α)
⊢ Eq (α := α) ((g • snoc x : (a : Fin n.succ) → α) (last n) : α) ((snoc y : (a : Fin n.succ) → α) (last n) : α)

Tactic:
hgxy (last n)

Premises used: Fin.last
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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 : α)
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) : α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G a) g

Tactic:
convert! hgxy (last n)

Premises used: Fin.last
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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 ↔
    Eq (α := α) ((g • snoc x : (a : Fin n.succ) → α) (last n) : α) ((snoc y : (a : Fin n.succ) → α) (last n) : α)

Tactic:
simp [ofStabilizer.snoc_last]

Premises used: SubMulAction.ofStabilizer.snoc_last
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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

Tactic:
have hg : g ∈ stabilizer G a := by
      rw [DFunLike.ext_iff] at hgxy
      convert! hgxy (last n)
      simp [ofStabilizer.snoc_last]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
h : Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • x = y
⊢ ∃ (g : ↥(stabilizer G a)), g • x = y

Tactic:
use ⟨g, hg⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
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) : α)
⊢ Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • x = y

Tactic:
ext i
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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 (↑((x : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α) =
    (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
⊢ 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:
simp only [smul_apply, SubMulAction.val_smul_of_tower, subgroup_smul_def]

Premises used: Function.Embedding.smul_apply, MulAction.subgroup_smul_def, SubMulAction.val_smul_of_tower
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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) : α) : α)
h₃ h₄ :
  Eq.{u_2 + 1} (α := α) (↑((y : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α)
    (↑((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) : α)

Tactic:
rw [← ofStabilizer.snoc_castSucc x, ← smul_apply, hgxy, ofStabilizer.snoc_castSucc]

Premises used: Function.Embedding.smul_apply, SubMulAction.ofStabilizer.snoc_castSucc
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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 ↪ α
refine_2 : ∀ (gx : G) (x1 : Fin n ↪ ↥(ofStabilizer G a)) (hgx : gx • x = snoc x1), ∃ (g : G), g • x = y
⊢ ∃ (g : G), g • x = y

Tactic:
obtain ⟨gx, x1, hgx⟩ := exists_smul_of_last_eq G a x

Premises used: SubMulAction.exists_smul_of_last_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
refine_2 : ∀ (gy : G) (y1 : Fin n ↪ ↥(ofStabilizer G a)) (hgy : gy • y = snoc y1), ∃ (g : G), g • x = y
⊢ ∃ (g : G), g • x = y

Tactic:
obtain ⟨gy, y1, hgy⟩ := exists_smul_of_last_eq G a y

Premises used: SubMulAction.exists_smul_of_last_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
refine_2 : ∀ (g : ↥(stabilizer G a)) (hg : g • x1 = y1), ∃ (g : G), g • x = y
⊢ ∃ (g : G), g • x = y

Tactic:
obtain ⟨g, hg⟩ := hn.exists_smul_eq x1 y1

Premises used: MulAction.IsPretransitive.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
h : (gy⁻¹ * (↑g : G) * gx) • x = y
⊢ ∃ (g : G), g • x = y

Tactic:
use gy⁻¹ * g * gx
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
h :
  ∀ (i : Fin n.succ),
    Eq (α := α) (((gy⁻¹ * (↑g : G) * gx) • x : (a : Fin n.succ) → α) i : α) ((y : (a : Fin n.succ) → α) i : α)
⊢ (gy⁻¹ * (↑g : G) * gx) • x = y

Tactic:
ext i
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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 :
  (↑g : G) • HSMul.hSMul (β := α) gx ((x : (a : Fin n.succ) → α) i : α) =
    HSMul.hSMul (β := α) gy ((y : (a : Fin n.succ) → α) i : α)
⊢ Eq (α := α) (((gy⁻¹ * (↑g : G) * gx) • x : (a : Fin n.succ) → α) i : α) ((y : (a : Fin n.succ) → α) i : α)

Tactic:
simp only [mul_smul, smul_apply, inv_smul_eq_iff]

Premises used: Function.Embedding.smul_apply, inv_smul_eq_iff, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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 : Eq (α := α) (((↑g : G) • snoc x1 : (a : Fin n.succ) → α) i : α) ((snoc y1 : (a : Fin n.succ) → α) i : α)
⊢ (↑g : G) • HSMul.hSMul (β := α) gx ((x : (a : Fin n.succ) → α) i : α) =
    HSMul.hSMul (β := α) gy ((y : (a : Fin n.succ) → α) i : α)

Tactic:
simp only [← smul_apply _ _ i, hgy, hgx]

Premises used: Function.Embedding.smul_apply
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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 : HSMul.hSMul (β := α) (↑g : G) ((snoc x1 : (a : Fin n.succ) → α) i : α) = (snoc y1 : (a : Fin n.succ) → α) i
⊢ Eq (α := α) (((↑g : G) • snoc x1 : (a : Fin n.succ) → α) i : α) ((snoc y1 : (a : Fin n.succ) → α) i : α)

Tactic:
simp only [smul_apply]

Premises used: Function.Embedding.smul_apply
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
h₁ :
  HSMul.hSMul (β := α) (↑g : G) ((snoc x1 : (a : Fin n.succ) → α) (last n) : α) =
    (snoc y1 : (a : Fin n.succ) → α) (last n)
⊢ HSMul.hSMul (β := α) (↑g : G) ((snoc x1 : (a : Fin n.succ) → α) i : α) = (snoc y1 : (a : Fin n.succ) → α) i

Tactic:
rcases Fin.eq_castSucc_or_eq_last i with ⟨i, rfl⟩ | ⟨rfl⟩

Premises used: Fin.eq_castSucc_or_eq_last, rfl
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
⊢ HSMul.hSMul (β := α) (↑g : G) ((snoc x1 : (a : Fin n.succ) → α) i.castSucc : α) =
    (snoc y1 : (a : Fin n.succ) → α) i.castSucc

Tactic:
simp [ofStabilizer.snoc_castSucc, ← hg, SetLike.val_smul, subgroup_smul_def]

Premises used: SubMulAction.ofStabilizer.snoc_castSucc, SetLike.val_smul, MulAction.subgroup_smul_def
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
h : (↑g : G) • a = a
⊢ HSMul.hSMul (β := α) (↑g : G) ((snoc x1 : (a : Fin n.succ) → α) (last n) : α) =
    (snoc y1 : (a : Fin n.succ) → α) (last n)

Tactic:
simp only [ofStabilizer.snoc_last, ← hg]

Premises used: SubMulAction.ofStabilizer.snoc_last
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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) • a = a

Tactic:
g.prop

Premises used: Set.Mem, setOf, Subtype.prop
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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) • a = a

Tactic:
exact g.prop

Premises used: Subtype.prop