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 α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
inst_4 : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (x : n ↪ β) → n ↪ α := fun (x : n ↪ β) ↦ x.trans (Function.Embedding.ofSurjective (⇑f : (a : α) → β) hf)
⊢ ∀ (x : n ↪ β) (i : n), f.toFun ((aux x : (a : n) → α) i) = (x : (a : n) → β) i

Tactic:
have aux_apply (x : n ↪ β) (i : n) : f.toFun (aux x i) = x i := by
      simp only [trans_apply, aux]
      apply Function.surjInv_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
inst_4 : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (x : n ↪ β) → n ↪ α := fun (x : n ↪ β) ↦ x.trans (Function.Embedding.ofSurjective (⇑f : (a : α) → β) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x : (a : n) → α) i) = (x : (a : n) → β) i
obtain : ∀ (g : G) (hg : g • aux x = aux y), ∃ (g : H), g • x = y
⊢ ∃ (g : H), g • x = y

Tactic:
obtain ⟨g, hg⟩ := exists_smul_eq (M := G) (aux x) (aux y)

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 α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
inst_4 : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (x : n ↪ β) → n ↪ α := fun (x : n ↪ β) ↦ x.trans (Function.Embedding.ofSurjective (⇑f : (a : α) → β) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x : (a : n) → α) i) = (x : (a : n) → β) i
g : G
hg : g • aux x = aux y
h : σ g • x = y
⊢ ∃ (g : H), g • x = y

Tactic:
use σ g
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
inst_4 : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (x : n ↪ β) → n ↪ α := fun (x : n ↪ β) ↦ x.trans (Function.Embedding.ofSurjective (⇑f : (a : α) → β) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x : (a : n) → α) i) = (x : (a : n) → β) i
g : G
hg : g • aux x = aux y
h : ∀ (i : n), Eq.{u_4 + 1} (α := β) ((σ g • x : (a : n) → β) i : β) ((y : (a : n) → β) i : β)
⊢ σ g • 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 α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
inst_4 : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (x : n ↪ β) → n ↪ α := fun (x : n ↪ β) ↦ x.trans (Function.Embedding.ofSurjective (⇑f : (a : α) → β) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x : (a : n) → α) i) = (x : (a : n) → β) i
g : G
hg : g • aux x = aux y
i : n
h :
  ∀ (hg : ∀ (x_1 : n), Eq.{u_2 + 1} (α := α) ((g • aux x : (a : n) → α) x_1 : α) ((aux y : (a : n) → α) x_1 : α))
    (i : n), Eq.{u_4 + 1} (α := β) ((σ g • x : (a : n) → β) i : β) ((y : (a : n) → β) i : β)
⊢ Eq.{u_4 + 1} (α := β) ((σ g • x : (a : n) → β) i : β) ((y : (a : n) → β) i : β)

Tactic:
rw [DFunLike.ext_iff] at hg

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 α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
inst_4 : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (x : n ↪ β) → n ↪ α := fun (x : n ↪ β) ↦ x.trans (Function.Embedding.ofSurjective (⇑f : (a : α) → β) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x : (a : n) → α) i) = (x : (a : n) → β) i
g : G
hg : ∀ (x_1 : n), Eq.{u_2 + 1} (α := α) ((g • aux x : (a : n) → α) x_1 : α) ((aux y : (a : n) → α) x_1 : α)
i : n
h : HSMul.hSMul (β := β) (σ g) ((x : (a : n) → β) i : β) = (y : (a : n) → β) i
⊢ Eq.{u_4 + 1} (α := β) ((σ g • x : (a : n) → β) i : β) ((y : (a : n) → β) i : β)

Tactic:
rw [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 α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
inst_4 : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (x : n ↪ β) → n ↪ α := fun (x : n ↪ β) ↦ x.trans (Function.Embedding.ofSurjective (⇑f : (a : α) → β) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x : (a : n) → α) i) = (x : (a : n) → β) i
g : G
hg : ∀ (x_1 : n), Eq.{u_2 + 1} (α := α) ((g • aux x : (a : n) → α) x_1 : α) ((aux y : (a : n) → α) x_1 : α)
i : n
⊢ HSMul.hSMul (β := β) (σ g) ((x : (a : n) → β) i : β) = (y : (a : n) → β) i

Tactic:
simp [← aux_apply, ← hg, MulActionHom.map_smul']

Premises used: MulActionHom.map_smul'
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hσ : Function.Surjective σ
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ IsPretransitive G (n ↪ α) ↔ IsPretransitive H (n ↪ β)

Tactic:
isPretransitive_congr hσ hf.mulActionHom_embedding_isBijective

Premises used: Function.Bijective.mulActionHom_embedding_isBijective, MulAction.isPretransitive_congr
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
n : Type u_5
inst_2 : IsEmpty n
⊢ IsPretransitive G (n ↪ α)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
⊢ IsMultiplyPretransitive G α 0

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
one : Type u_5
inst_2 : Unique one
⊢ Function.Bijective (α := one ↪ α) (β := α) (⇑oneEmbeddingMap : (a : one ↪ α) → α)

Tactic:
oneEmbeddingEquiv.bijective

Premises used: Equiv.bijective, Function.Embedding.oneEmbeddingEquiv
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
one : Type u_5
inst_2 : Unique one
⊢ IsPretransitive G (one ↪ α) ↔ IsPretransitive G α

Tactic:
isPretransitive_congr Function.surjective_id oneEmbeddingMap_bijective

Premises used: MulAction.isPretransitive_congr, Function.surjective_id, MulActionHom.oneEmbeddingMap_bijective
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
⊢ IsMultiplyPretransitive G α 1 ↔ IsPretransitive G α

Tactic:
oneEmbedding_isPretransitive_iff

Premises used: MulAction.oneEmbedding_isPretransitive_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
mp : IsMultiplyPretransitive G α 2 → ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
mpr : (∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d) → IsMultiplyPretransitive G α 2
⊢ IsMultiplyPretransitive G α 2 ↔ ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h_1 : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
mp : ∀ (m : G) (e : m • embFinTwo h = embFinTwo h'), ∃ (g : G), g • a = c ∧ g • b = d
⊢ ∃ (g : G), g • a = c ∧ g • b = d

Tactic:
obtain ⟨m, e⟩ := exists_smul_eq (M := G) (embFinTwo h) (embFinTwo h')

Premises used: Function.Embedding.embFinTwo, MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h_1 : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
m : G
e : m • embFinTwo h = embFinTwo h'
rw : HSMul.hSMul (β := α) m ((embFinTwo h : (a : Fin 2) → α) 0 : α) = c
rw₁ : (m • embFinTwo h : (a : Fin 2) → α) 0 = c
rw₂ : (embFinTwo h' : (a : Fin 2) → α) 0 = c
rw₃ rw₄ : c = c
⊢ m • a = c

Tactic:
rw [← embFinTwo_apply_zero h, ← smul_apply, e, embFinTwo_apply_zero]

Premises used: Function.Embedding.smul_apply, Function.Embedding.embFinTwo_apply_zero
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h_1 : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
m : G
e : m • embFinTwo h = embFinTwo h'
rw : HSMul.hSMul (β := α) m ((embFinTwo h : (a : Fin 2) → α) 1 : α) = d
rw₁ : (m • embFinTwo h : (a : Fin 2) → α) 1 = d
rw₂ : (embFinTwo h' : (a : Fin 2) → α) 1 = d
rw₃ rw₄ : d = d
⊢ m • b = d

Tactic:
rw [← embFinTwo_apply_one h, ← smul_apply, e, embFinTwo_apply_one]

Premises used: Function.Embedding.smul_apply, Function.Embedding.embFinTwo_apply_one
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h_1 : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
m : G
e : m • embFinTwo h = embFinTwo h'
⊢ ∃ (g : G), g • a = c ∧ g • b = d

Tactic:
exact ⟨m,
      by rw [← embFinTwo_apply_zero h, ← smul_apply, e, embFinTwo_apply_zero],
      by rw [← embFinTwo_apply_one h, ← smul_apply, e, embFinTwo_apply_one]⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
mpr : ∀ (x y : Fin 2 ↪ α), ∃ (g : G), g • x = y
⊢ IsMultiplyPretransitive G α 2

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
j j' : Fin 2 ↪ α
mpr :
  ∀ (g : G) (h : HSMul.hSMul (β := α) g ((j : (a : Fin 2) → α) 0 : α) = (j' : (a : Fin 2) → α) 0)
    (h' : HSMul.hSMul (β := α) g ((j : (a : Fin 2) → α) 1 : α) = (j' : (a : Fin 2) → α) 1), ∃ (g : G), g • j = j'
⊢ ∃ (g : G), g • j = j'

Tactic:
obtain ⟨g, h, h'⟩ :=
      H (j.injective.ne_iff.mpr Fin.zero_ne_one) (j'.injective.ne_iff.mpr Fin.zero_ne_one)

Premises used: Iff.mpr, Function.Injective.ne_iff, Fin.zero_ne_one, Function.Embedding.injective
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
j j' : Fin 2 ↪ α
g : G
h : HSMul.hSMul (β := α) g ((j : (a : Fin 2) → α) 0 : α) = (j' : (a : Fin 2) → α) 0
h' : HSMul.hSMul (β := α) g ((j : (a : Fin 2) → α) 1 : α) = (j' : (a : Fin 2) → α) 1
h₁ : g • j = j'
⊢ ∃ (g : G), g • j = j'

Tactic:
use g
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
j j' : Fin 2 ↪ α
g : G
h : HSMul.hSMul (β := α) g ((j : (a : Fin 2) → α) 0 : α) = (j' : (a : Fin 2) → α) 0
h' : HSMul.hSMul (β := α) g ((j : (a : Fin 2) → α) 1 : α) = (j' : (a : Fin 2) → α) 1
h₁ : ∀ (i : Fin 2), Eq (α := α) ((g • j : (a : Fin 2) → α) i : α) ((j' : (a : Fin 2) → α) i : α)
⊢ g • j = j'

Tactic:
ext i
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
j j' : Fin 2 ↪ α
g : G
h : HSMul.hSMul (β := α) g ((j : (a : Fin 2) → α) 0 : α) = (j' : (a : Fin 2) → α) 0
h' : HSMul.hSMul (β := α) g ((j : (a : Fin 2) → α) 1 : α) = (j' : (a : Fin 2) → α) 1
i : Fin 2
pos : ∀ (hi : i = 0), Eq (α := α) ((g • j : (a : Fin 2) → α) i : α) ((j' : (a : Fin 2) → α) i : α)
neg : ∀ (hi : ¬i = 0), Eq (α := α) ((g • j : (a : Fin 2) → α) i : α) ((j' : (a : Fin 2) → α) i : α)
⊢ Eq (α := α) ((g • j : (a : Fin 2) → α) i : α) ((j' : (a : Fin 2) → α) i : α)

Tactic:
by_cases hi : i = 0
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
j j' : Fin 2 ↪ α
g : G
h : HSMul.hSMul (β := α) g ((j : (a : Fin 2) → α) 0 : α) = (j' : (a : Fin 2) → α) 0
h' : HSMul.hSMul (β := α) g ((j : (a : Fin 2) → α) 1 : α) = (j' : (a : Fin 2) → α) 1
i : Fin 2
hi : i = 0
⊢ Eq (α := α) ((g • j : (a : Fin 2) → α) i : α) ((j' : (a : Fin 2) → α) i : α)

Tactic:
simp [hi, h]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
j j' : Fin 2 ↪ α
g : G
h : HSMul.hSMul (β := α) g ((j : (a : Fin 2) → α) 0 : α) = (j' : (a : Fin 2) → α) 0
h' : HSMul.hSMul (β := α) g ((j : (a : Fin 2) → α) 1 : α) = (j' : (a : Fin 2) → α) 1
i : Fin 2
hi : ¬i = 0
⊢ Eq (α := α) ((g • j : (a : Fin 2) → α) i : α) ((j' : (a : Fin 2) → α) i : α)

Tactic:
simp [eq_one_of_ne_zero i hi, h']

Premises used: Fin.eq_one_of_ne_zero
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
a b : α
pos : ∀ (h : a = b), ∃ (g : G), g • a = b
neg : ∀ (h : ¬a = b), ∃ (g : G), g • a = b
⊢ ∃ (g : G), g • a = b

Tactic:
by_cases h : a = b
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
a b : α
h : a = b
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := G) 1 a = b

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
a b : α
h : a = b
⊢ ∃ (g : G), g • a = b

Tactic:
exact ⟨1, by simp [h]⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
a b : α
h : ¬a = b
neg :
  ∀ (h2 : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d) (a b : α) (h : ¬a = b),
    ∃ (g : G), g • a = b
⊢ ∃ (g : G), g • a = b

Tactic:
rw [is_two_pretransitive_iff] at h2

Premises used: MulAction.is_two_pretransitive_iff
-- 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
a b : α
h : ¬a = b
neg : ∀ (g : G) (h : g • a = b), g • b = a → ∃ (g : G), g • a = b
⊢ ∃ (g : G), g • a = b

Tactic:
obtain ⟨g, h, _⟩ := h2 h (Ne.symm h)

Premises used: Ne.symm
-- 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
a b : α
h_1 : ¬a = b
g : G
h : g • a = b
right : g • b = a
⊢ ∃ (g : G), g • a = b

Tactic:
⟨g, h⟩

Premises used: Exists.intro
-- 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
a b : α
h_1 : ¬a = b
g : G
h : g • a = b
right : g • b = a
⊢ ∃ (g : G), g • a = b

Tactic:
exact ⟨g, h⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
⊢ IsPretransitive G α

Tactic:
have : IsPretransitive G α := isPretransitive_of_is_two_pretransitive
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
isTrivialBlock_of_isBlock : ∀ {B : Set α}, IsBlock G B → IsTrivialBlock B
⊢ IsPreprimitive G α

Tactic:
apply IsPreprimitive.mk

Premises used: MulAction.IsPreprimitive.mk
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
isTrivialBlock_of_isBlock : ∀ (h : B.Subsingleton), IsTrivialBlock B
isTrivialBlock_of_isBlock₁ : ∀ (h : B.Nontrivial), IsTrivialBlock B
⊢ IsTrivialBlock B

Tactic:
rcases B.subsingleton_or_nontrivial with h | h

Premises used: Set.subsingleton_or_nontrivial
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
h isTrivialBlock_of_isBlock : B.Subsingleton
⊢ IsTrivialBlock B

Tactic:
left
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
h : B.Subsingleton
⊢ B.Subsingleton

Tactic:
h
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
h : B.Subsingleton
⊢ B.Subsingleton

Tactic:
exact h
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
h : B.Nontrivial
isTrivialBlock_of_isBlock : B = univ
⊢ IsTrivialBlock B

Tactic:
right
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
h : B.Nontrivial
isTrivialBlock_of_isBlock : ∀ (a : α) (ha : a ∈ B) (b : α) (hb : b ∈ B) (h : a ≠ b), B = univ
⊢ B = univ

Tactic:
obtain ⟨a, ha, b, hb, h⟩ := h
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
isTrivialBlock_of_isBlock : ⊤ ≤ B
⊢ B = univ

Tactic:
rw [← top_eq_univ, eq_top_iff]

Premises used: eq_top_iff, Set.top_eq_univ
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
isTrivialBlock_of_isBlock : Membership.mem (γ := Set α) ⊤ c → c ∈ B
⊢ Membership.mem (γ := Set α) ⊤ c → c ∈ B

Tactic:
_
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
h_1 : Membership.mem (γ := Set α) ⊤ c
pos : ∀ (h' : a = c), c ∈ B
neg : ∀ (h' : ¬a = c), c ∈ B
⊢ c ∈ B

Tactic:
by_cases h' : a = c
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
h_1 : Membership.mem (γ := Set α) ⊤ c
h' : a = c
pos : a ∈ B
⊢ c ∈ B

Tactic:
rw [← h']
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
h_1 : Membership.mem (γ := Set α) ⊤ c
h' : a = c
⊢ a ∈ B

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

Tactic:
rw [is_two_pretransitive_iff] at h2

Premises used: MulAction.is_two_pretransitive_iff
-- 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 : IsBlock G B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
h_1 : Membership.mem (γ := Set α) ⊤ c
h' : ¬a = c
neg : ∀ (g : G) (hga : g • a = a) (hgb : g • b = c), c ∈ B
⊢ c ∈ B

Tactic:
obtain ⟨g, hga, hgb⟩ := h2 h h'
-- 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 : IsBlock G 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 :
  ∀ (hB : ∀ ⦃g : G⦄ ⦃a : α⦄, a ∈ B → g • a ∈ B → g • B = B) (a : α) (ha : a ∈ B) (b : α) (hb : b ∈ B) (h : a ≠ b)
    ⦃c : α⦄, Membership.mem (γ := Set α) ⊤ c → ∀ (h' : ¬a = c) (g : G) (hga : g • a = a) (hgb : g • b = c), c ∈ B
⊢ c ∈ B

Tactic:
rw [MulAction.isBlock_iff_smul_eq_of_mem] at hB

Premises used: MulAction.isBlock_iff_smul_eq_of_mem
-- 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
rw : a ∈ B
⊢ g • a ∈ B

Tactic:
rw [hga]
-- 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:
ha