internlm/Lean-Github huggingface dataset:
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
case h.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
m : M
hm : ∀ (x : Fin 2), (m • f a b hab) x = (f c d hcd) x
⊢ m • b = d
Tactic:
simpa only [smul_apply, coeFn_mk, eq_self_iff_true, if_true] using hm 1
Proof state after:
no goals
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
⊢ (∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d) → IsMultiplyPretransitive M α 2
Tactic:
intro h
Proof state after:
case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
⊢ IsMultiplyPretransitive M α 2
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
⊢ IsMultiplyPretransitive M α 2
Tactic:
apply IsPretransitive.mk
Proof state after:
case mpr.exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
⊢ ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
case mpr.exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
⊢ ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y
Tactic:
intro u v
Proof state after:
case mpr.exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
u v : Fin 2 ↪ α
⊢ ∃ g, g • u = v
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
case mpr.exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
u v : Fin 2 ↪ α
⊢ ∃ g, g • u = v
Tactic:
specialize h (u 0) (u 1) (v 0) (v 1)
Proof state after:
case mpr.exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ∃ g, g • u = v
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
case mpr.exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ∃ g, g • u = v
Tactic:
obtain ⟨m, hm⟩ := h
  (by rw [Ne.def, Function.Embedding.apply_eq_iff_eq]; exact zero_ne_one)
  (by rw [Ne.def, Function.Embedding.apply_eq_iff_eq]; exact zero_ne_one)
Proof state after:
case mpr.exists_smul_eq.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ∃ g, g • u = v
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
case mpr.exists_smul_eq.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ∃ g, g • u = v
Tactic:
use m
Proof state after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ m • u = v
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ m • u = v
Tactic:
ext x
Proof state after:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
⊢ (m • u) x = v x
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
⊢ (m • u) x = v x
Tactic:
cases' this x with hx hx
Proof state after:
case h.h.inl
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
hx : x = 0
⊢ (m • u) x = v x

case h.h.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
hx : x = 1
⊢ (m • u) x = v x
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
case h.h.inl
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
hx : x = 0
⊢ (m • u) x = v x

case h.h.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
hx : x = 1
⊢ (m • u) x = v x
Tactic:
simpa only [hx] using hm.left
Proof state after:
case h.h.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
hx : x = 1
⊢ (m • u) x = v x
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
case h.h.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
hx : x = 1
⊢ (m • u) x = v x
Tactic:
simpa only [hx] using hm.right
Proof state after:
no goals
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ u 0 ≠ u 1
Tactic:
rw [Ne.def, Function.Embedding.apply_eq_iff_eq]
Proof state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ¬0 = 1
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ¬0 = 1
Tactic:
exact zero_ne_one
Proof state after:
no goals
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ v 0 ≠ v 1
Tactic:
rw [Ne.def, Function.Embedding.apply_eq_iff_eq]
Proof state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ¬0 = 1
Theorem: MulAction.isMultiplyPretransitive_of_higher
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
⊢ IsMultiplyPretransitive M α m
Tactic:
unfold IsMultiplyPretransitive
Proof state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
⊢ IsPretransitive M (Fin m ↪ α)
Theorem: MulAction.isMultiplyPretransitive_of_higher
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
⊢ IsPretransitive M (Fin m ↪ α)
Tactic:
let hn_eq := hn.exists_smul_eq
Proof state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive M (Fin m ↪ α)
Theorem: MulAction.isMultiplyPretransitive_of_higher
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive M (Fin m ↪ α)
Tactic:
apply IsPretransitive.mk
Proof state after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : Fin m ↪ α), ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_higher
Proof state before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : Fin m ↪ α), ∃ g, g • x = y
Tactic:
intro x y
Proof state after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
⊢ ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_higher
Proof state before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨x', hx'⟩ := may_extend hmn hα x
Proof state after:
case exists_smul_eq.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
⊢ ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_higher
Proof state before:
case exists_smul_eq.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨y', hy'⟩ := may_extend hmn hα y
Proof state after:
case exists_smul_eq.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
⊢ ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_higher
Proof state before:
case exists_smul_eq.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g, hg⟩ := hn_eq x' y'
Proof state after:
case exists_smul_eq.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
⊢ ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_higher
Proof state before:
case exists_smul_eq.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
⊢ ∃ g, g • x = y
Tactic:
use g
Proof state after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
⊢ g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_higher
Proof state before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
⊢ g • x = y
Tactic:
ext
Proof state after:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
x✝ : Fin m
⊢ (g • x) x✝ = y x✝
Theorem: MulAction.isMultiplyPretransitive_of_higher
Proof state before:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
x✝ : Fin m
⊢ (g • x) x✝ = y x✝
Tactic:
rw [← hy', ← hx', ← hg]
Proof state after:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
x✝ : Fin m
⊢ (g • Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x') x✝ =
    (Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding (g • x')) x✝
Theorem: MulAction.isMultiplyPretransitive_of_higher
Proof state before:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
x✝ : Fin m
⊢ (g • Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x') x✝ =
    (Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding (g • x')) x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: MulAction.exists_extends_with_last_eq
Proof state before:
M : Type ?u.67011
α : Type ?u.67014
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x✝ : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x y : ↥(SubMulAction.ofStabilizer M a)
hxy : (fun u => id ↑u) x = (fun u => id ↑u) y
⊢ x = y
Tactic:
simpa using hxy
Proof state after:
no goals
Theorem: MulAction.exists_extends_with_last_eq
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
⊢ let j := { toFun := fun u => id ↑u, inj' := ⋯ };
  ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x j ∧
      x' { val := n, isLt := ⋯ } = a
Tactic:
intro _
Proof state after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
⊢ ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x j✝ ∧
      x' { val := n, isLt := ⋯ } = a
Theorem: MulAction.exists_extends_with_last_eq
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
⊢ ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x j✝ ∧
      x' { val := n, isLt := ⋯ } = a
Tactic:
refine' may_extend_with (x.trans (subtype _)) a _
Proof state after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
⊢ a ∉ Set.range (Function.Embedding.trans x (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)).toFun
Theorem: MulAction.exists_extends_with_last_eq
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
⊢ a ∉ Set.range (Function.Embedding.trans x (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)).toFun
Tactic:
rintro ⟨u, hu⟩
Proof state after:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : (Function.Embedding.trans x (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)).toFun u = a
⊢ False
Theorem: MulAction.exists_extends_with_last_eq
Proof state before:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : (Function.Embedding.trans x (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)).toFun u = a
⊢ False
Tactic:
simp only [toFun_eq_coe, trans_apply, Function.Embedding.coe_subtype] at hu
Proof state after:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : ↑(x u) = a
⊢ False