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 α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
y : ι ↪ β
g : β → α
left : LeftInverse g (⇑f : (a : α) → β)
hfg : RightInverse g (⇑f : (a : α) → β)
⊢ (Injective.mulActionHom_embedding ι ⋯ : (a : ι ↪ α) → ι ↪ β) { toFun := g ∘ (⇑y : (a : ι) → β), inj' := ⋯ } = y
have h : ∀ (x : ι),
  Eq.{u_4 + 1} (α := β)
    ((((Injective.mulActionHom_embedding ι sorry : (a : ι ↪ α) → ι ↪ β) { toFun := g ∘ (⇑y : (a : ι) → β), inj' := sorry } :
            ι ↪ β) :
          (a : ι) → β)
        x :
      β)
    ((y : (a : ι) → β) x : β)
Tactic: ext
-- 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 α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
y : ι ↪ β
g : β → α
left : LeftInverse g (⇑f : (a : α) → β)
hfg : RightInverse g (⇑f : (a : α) → β)
x : ι
⊢ Eq.{u_4 + 1} (α := β)
    ((((Injective.mulActionHom_embedding ι ⋯ : (a : ι ↪ α) → ι ↪ β) { toFun := g ∘ (⇑y : (a : ι) → β), inj' := ⋯ } :
            ι ↪ β) :
          (a : ι) → β)
        x :
      β)
    ((y : (a : ι) → β) x : β)
have h : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (g ((y : (a : ι) → β) x)) : β) ((y : (a : ι) → β) x : β)
Tactic: simp only [hf.injective.mulActionHom_embedding_apply, coeFn_mk, comp_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 α
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_1 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
have simp : f.toFun ((Function.Embedding.ofSurjective (⇑f : (a : α) → β) hf : (a : β) → α) ((x : (a : n) → β) i : β)) =
  (x : (a : n) → β) i
Tactic: simp only [trans_apply, aux]
-- 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 α
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)
⊢ ∃ (g : H), g • x = y
have aux_apply : ∀ (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
-- 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 α
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 : H), g • x = y
have obtain : ∀ (g : G) (hg : g • aux x = aux y), ∃ (g : H), g • x = y
Tactic: obtain ⟨g, hg⟩ := exists_smul_eq (M := G) (aux x) (aux 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 α
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
⊢ ∃ (g : H), g • x = y
have h : σ g • x = y
Tactic: use σ g
-- 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 α
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
⊢ σ g • x = y
have h : ∀ (i : n), Eq.{u_4 + 1} (α := β) ((σ g • x : (a : n) → β) i : β) ((y : (a : n) → β) 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 α
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
⊢ Eq.{u_4 + 1} (α := β) ((σ g • x : (a : n) → β) i : β) ((y : (a : n) → β) i : β)
have 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 : β)
Tactic: rw [DFunLike.ext_iff] at hg
Cleared hypotheses: hg, 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 α
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
⊢ Eq.{u_4 + 1} (α := β) ((σ g • x : (a : n) → β) i : β) ((y : (a : n) → β) i : β)
have h : HSMul.hSMul (β := β) (σ g) ((x : (a : n) → β) i : β) = (y : (a : n) → β) i
Tactic: rw [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 α
⊢ IsMultiplyPretransitive G α 2 ↔ ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
have mp : IsMultiplyPretransitive G α 2 → ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
Tactic: constructor
-- 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 α
mp : IsMultiplyPretransitive G α 2 → ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
⊢ IsMultiplyPretransitive G α 2 ↔ ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
have mpr : (∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d) → IsMultiplyPretransitive G α 2
Tactic: constructor
-- 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 α
h_1 : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
⊢ ∃ (g : G), g • a = c ∧ g • b = d
have mp : ∀ (m : G) (e : m • embFinTwo h = embFinTwo h'), ∃ (g : G), g • a = c ∧ g • b = d
Tactic: obtain ⟨m, e⟩ := exists_smul_eq (M := G) (embFinTwo h) (embFinTwo h')
-- 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 α
h_1 : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
m : G
e : m • embFinTwo h = embFinTwo h'
⊢ m • a = c
have rw : HSMul.hSMul (β := α) m ((embFinTwo h : (a : Fin 2) → α) 0 : α) = c
Tactic: rw [← embFinTwo_apply_zero h, ← smul_apply, e, embFinTwo_apply_zero]
-- 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 α
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
⊢ m • a = c
have rw₁ : (m • embFinTwo h : (a : Fin 2) → α) 0 = c
Tactic: rw [← embFinTwo_apply_zero h, ← smul_apply, e, embFinTwo_apply_zero]
-- 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 α
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
⊢ m • a = c
have rw₂ : (embFinTwo h' : (a : Fin 2) → α) 0 = c
Tactic: rw [← embFinTwo_apply_zero h, ← smul_apply, e, embFinTwo_apply_zero]
-- 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 α
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
⊢ m • a = c
have rw₃ : c = c
Tactic: rw [← embFinTwo_apply_zero h, ← smul_apply, e, embFinTwo_apply_zero]
-- 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 α
h_1 : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
m : G
e : m • embFinTwo h = embFinTwo h'
⊢ m • b = d
have rw : HSMul.hSMul (β := α) m ((embFinTwo h : (a : Fin 2) → α) 1 : α) = d
Tactic: rw [← embFinTwo_apply_one h, ← smul_apply, e, embFinTwo_apply_one]
-- 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 α
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
⊢ m • b = d
have rw₁ : (m • embFinTwo h : (a : Fin 2) → α) 1 = d
Tactic: rw [← embFinTwo_apply_one h, ← smul_apply, e, embFinTwo_apply_one]
-- 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 α
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
⊢ m • b = d
have rw₂ : (embFinTwo h' : (a : Fin 2) → α) 1 = d
Tactic: rw [← embFinTwo_apply_one h, ← smul_apply, e, embFinTwo_apply_one]
-- 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 α
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
⊢ m • b = d
have rw₃ : d = d
Tactic: rw [← embFinTwo_apply_one h, ← smul_apply, e, embFinTwo_apply_one]
-- 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 α
H : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
⊢ IsMultiplyPretransitive G α 2
have mpr : ∀ (x y : Fin 2 ↪ α), ∃ (g : G), g • x = y
Tactic: constructor
-- 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 α
H : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d
j j' : Fin 2 ↪ α
⊢ ∃ (g : G), g • j = j'
have 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'
Tactic: obtain ⟨g, h, h'⟩ :=
      H (j.injective.ne_iff.mpr Fin.zero_ne_one) (j'.injective.ne_iff.mpr Fin.zero_ne_one)
-- 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 α
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
⊢ ∃ (g : G), g • j = j'
have h₁ : g • j = j'
Tactic: use g
-- 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 α
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
⊢ g • j = j'
have h₁ : ∀ (i : Fin 2), Eq (α := α) ((g • j : (a : Fin 2) → α) i : α) ((j' : (a : Fin 2) → α) 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 α
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
⊢ Eq (α := α) ((g • j : (a : Fin 2) → α) i : α) ((j' : (a : Fin 2) → α) i : α)
have pos : ∀ (hi : i = 0), Eq (α := α) ((g • j : (a : Fin 2) → α) i : α) ((j' : (a : Fin 2) → α) i : α)
Tactic: by_cases hi : i = 0
-- 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 α
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 : α)
⊢ Eq (α := α) ((g • j : (a : Fin 2) → α) i : α) ((j' : (a : Fin 2) → α) i : α)
have neg : ∀ (hi : ¬i = 0), Eq (α := α) ((g • j : (a : Fin 2) → α) i : α) ((j' : (a : Fin 2) → α) i : α)
Tactic: by_cases hi : i = 0
-- 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 α
h2 : IsMultiplyPretransitive G α 2
a b : α
⊢ ∃ (g : G), g • a = b
have pos : ∀ (h : a = b), ∃ (g : G), g • a = b
Tactic: by_cases h : a = b
-- 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 α
h2 : IsMultiplyPretransitive G α 2
a b : α
pos : ∀ (h : a = b), ∃ (g : G), g • a = b
⊢ ∃ (g : G), g • a = b
have neg : ∀ (h : ¬a = b), ∃ (g : G), g • a = b
Tactic: by_cases h : a = b
-- 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 α
h2 : IsMultiplyPretransitive G α 2
a b : α
h : ¬a = b
⊢ ∃ (g : G), g • a = b
have 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
Tactic: rw [is_two_pretransitive_iff] at h2
Cleared hypotheses: h2, a, b, h
-- 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 α
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
have neg : ∀ (g : G) (h : g • a = b), g • b = a → ∃ (g : G), g • a = b
Tactic: obtain ⟨g, h, _⟩ := h2 h (Ne.symm h)
-- 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 α
h2 : IsMultiplyPretransitive G α 2
⊢ IsPreprimitive G α
have this : IsPretransitive G α
Tactic: have : IsPretransitive G α := isPretransitive_of_is_two_pretransitive
-- 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 α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
⊢ IsPreprimitive G α
have isTrivialBlock_of_isBlock : ∀ {B : Set α}, IsBlock G B → IsTrivialBlock B
Tactic: apply IsPreprimitive.mk
-- 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 α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
⊢ IsTrivialBlock B
have isTrivialBlock_of_isBlock : ∀ (h : B.Subsingleton), IsTrivialBlock B
Tactic: rcases B.subsingleton_or_nontrivial with h | h
-- 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 α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
isTrivialBlock_of_isBlock : ∀ (h : B.Subsingleton), IsTrivialBlock B
⊢ IsTrivialBlock B
have isTrivialBlock_of_isBlock₁ : ∀ (h : B.Nontrivial), IsTrivialBlock B
Tactic: rcases B.subsingleton_or_nontrivial with h | h
-- 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 α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
h : B.Nontrivial
⊢ IsTrivialBlock B
have isTrivialBlock_of_isBlock : B = univ
Tactic: right
-- 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 α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
h : B.Nontrivial
⊢ B = univ
have isTrivialBlock_of_isBlock : ∀ (a : α) (ha : a ∈ B) (b : α) (hb : b ∈ B) (h : a ≠ b), B = univ
Tactic: obtain ⟨a, ha, b, hb, h⟩ := h
Cleared hypotheses: h
-- 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 α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
⊢ B = univ
have isTrivialBlock_of_isBlock : ⊤ ≤ B
Tactic: rw [← top_eq_univ, eq_top_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 α
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
⊢ c ∈ B
have pos : ∀ (h' : a = c), c ∈ B
Tactic: by_cases h' : a = c
-- 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 α
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
⊢ c ∈ B
have neg : ∀ (h' : ¬a = c), c ∈ B
Tactic: by_cases h' : a = c
-- 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 α
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
⊢ c ∈ B
have 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
Tactic: rw [is_two_pretransitive_iff] at h2
Cleared hypotheses: h2, this, B, hB, a, ha, b, hb, h, c, h_1, h'
-- 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 α
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
⊢ c ∈ B
have neg : ∀ (g : G) (hga : g • a = a) (hgb : g • b = c), c ∈ B
Tactic: obtain ⟨g, hga, hgb⟩ := h2 h h'
-- 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 α
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
⊢ c ∈ B
have 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
Tactic: rw [MulAction.isBlock_iff_smul_eq_of_mem] at hB
Cleared hypotheses: hB, a, ha, b, hb, h, c, h_1, h', g, hga, hgb
-- 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 α
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
⊢ c ∈ B
have neg : g • b ∈ g • B
Tactic: rw [← hB (g := g) ha (by rw [hga]; exact ha), ← hgb]
-- 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 : ℕ
inst_2 : IsMultiplyPretransitive G α n
hmn : m ≤ n
hα : (↑n : ℕ∞) ≤ ENat.card α
⊢ IsMultiplyPretransitive G α m
have obtain : ∀ (p : ℕ) [IsMultiplyPretransitive G α (m + p)] (hmn : m ≤ m + p) (hα : (↑(m + p) : ℕ∞) ≤ ENat.card α),
  IsMultiplyPretransitive G α m
Tactic: obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hmn
Cleared hypotheses: n, inst_2, hmn, hα
-- 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 : ℕ
inst_2 : IsMultiplyPretransitive G α n
hmn : m ≤ n
hα : n ≤ Nat.card α
inst_3 : Finite α
⊢ IsMultiplyPretransitive G α m
have obtain : ∀ (p : ℕ) [IsMultiplyPretransitive G α (m + p)] (hmn : m ≤ m + p) (hα : m + p ≤ Nat.card α),
  IsMultiplyPretransitive G α m
Tactic: obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hmn
Cleared hypotheses: n, inst_2, hmn, hα