internlm/Lean-Github huggingface dataset:
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
x : Fin n ↪ β
i : Fin n
⊢ f.toFun ((aux x) i) = x i
Tactic:
simp only [toFun_eq_coe, coeFn_mk, Function.comp_apply, aux]
Proof state after:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
x : Fin n ↪ β
i : Fin n
⊢ f.toFun (Function.surjInv hf (x i)) = x i
Theorem: MulAction.isMultiplyPretransitive_of_surjective_map
Proof state before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
aux : (Fin n ↪ β) → Fin n ↪ α := fun x => { toFun := Function.surjInv hf ∘ x.toFun, inj' := ⋯ }
x : Fin n ↪ β
i : Fin n
⊢ f.toFun (Function.surjInv hf (x i)) = x i
Tactic:
apply Function.surjInv_eq
Proof state after:
no goals
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
⊢ IsMultiplyPretransitive M α n ↔ IsMultiplyPretransitive N β n
Tactic:
constructor
Proof state after:
case mp
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
⊢ IsMultiplyPretransitive M α n → IsMultiplyPretransitive N β n

case mpr
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
⊢ IsMultiplyPretransitive N β n → IsMultiplyPretransitive M α n
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case mpr
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
⊢ IsMultiplyPretransitive N β n → IsMultiplyPretransitive M α n
Tactic:
intro hN
Proof state after:
case mpr
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
⊢ IsMultiplyPretransitive M α n
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case mpr
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
⊢ IsMultiplyPretransitive M α n
Tactic:
let hN_heq := hN.exists_smul_eq
Proof state after:
case mpr
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsMultiplyPretransitive M α n
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case mpr
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsMultiplyPretransitive M α n
Tactic:
apply IsPretransitive.mk
Proof state after:
case mpr.exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : Fin n ↪ α), ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case mpr.exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : Fin n ↪ α), ∃ g, g • x = y
Tactic:
intro x y
Proof state after:
case mpr.exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
⊢ ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case mpr.exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
⊢ ∃ g, g • x = y
Tactic:
let x' : Fin n ↪ β := ⟨f ∘ x, hf.injective.comp x.inj'⟩
Proof state after:
case mpr.exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
⊢ ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case mpr.exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
⊢ ∃ g, g • x = y
Tactic:
let y' : Fin n ↪ β := ⟨f ∘ y, hf.injective.comp y.inj'⟩
Proof state after:
case mpr.exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
⊢ ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case mpr.exists_smul_eq
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g', hg'⟩ := hN_heq x' y'
Proof state after:
case mpr.exists_smul_eq.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
⊢ ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case mpr.exists_smul_eq.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g, hg⟩ := hσ g'
Proof state after:
case mpr.exists_smul_eq.intro.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
g : M
hg : σ g = g'
⊢ ∃ g, g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case mpr.exists_smul_eq.intro.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
g : M
hg : σ g = g'
⊢ ∃ g, g • x = y
Tactic:
use g
Proof state after:
case h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
g : M
hg : σ g = g'
⊢ g • x = y
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
g : M
hg : σ g = g'
⊢ g • x = y
Tactic:
ext i
Proof state after:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
g : M
hg : σ g = g'
i : Fin n
⊢ (g • x) i = y i
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case h.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
g : M
hg : σ g = g'
i : Fin n
⊢ (g • x) i = y i
Tactic:
apply hf.injective
Proof state after:
case h.h.a
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
g : M
hg : σ g = g'
i : Fin n
⊢ f ((g • x) i) = f (y i)
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case h.h.a
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
g : M
hg : σ g = g'
i : Fin n
⊢ f ((g • x) i) = f (y i)
Tactic:
simp only [smul_apply, map_smulₛₗ, hg]
Proof state after:
case h.h.a
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
g : M
hg : σ g = g'
i : Fin n
⊢ g' • f (x i) = f (y i)
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case h.h.a
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
g : M
hg : σ g = g'
i : Fin n
⊢ g' • f (x i) = f (y i)
Tactic:
change g' • (x' i) = y' i
Proof state after:
case h.h.a
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
g : M
hg : σ g = g'
i : Fin n
⊢ g' • x' i = y' i
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case h.h.a
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
hN : IsMultiplyPretransitive N β n
hN_heq : ∀ (x y : Fin n ↪ β), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ α
x' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑x, inj' := ⋯ }
y' : Fin n ↪ β := { toFun := ⇑f ∘ ⇑y, inj' := ⋯ }
g' : N
hg' : g' • x' = y'
g : M
hg : σ g = g'
i : Fin n
⊢ g' • x' i = y' i
Tactic:
simp only [← hg, coeFn_mk, Function.comp_apply, ← hg', smul_apply]
Proof state after:
no goals
Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff
Proof state before:
case mp
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
n : ℕ
σ : M → N
f : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
⊢ IsMultiplyPretransitive M α n → IsMultiplyPretransitive N β n
Tactic:
apply isMultiplyPretransitive_of_surjective_map hf.surjective
Proof state after:
no goals
Theorem: MulAction.is_zero_pretransitive
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPretransitive M α 0
Tactic:
apply IsPretransitive.mk
Proof state after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ ∀ (x y : Fin 0 ↪ α), ∃ g, g • x = y
Theorem: MulAction.is_zero_pretransitive
Proof state before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ ∀ (x y : Fin 0 ↪ α), ∃ 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 α
x y : Fin 0 ↪ α
⊢ ∃ g, g • x = y
Theorem: MulAction.is_zero_pretransitive
Proof state before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
⊢ ∃ g, g • x = y
Tactic:
use 1
Proof state after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
⊢ 1 • x = y
Theorem: MulAction.is_zero_pretransitive
Proof state before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
⊢ 1 • x = y
Tactic:
rw [one_smul]
Proof state after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
⊢ x = y
Theorem: MulAction.is_zero_pretransitive
Proof state before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
⊢ x = y
Tactic:
ext i
Proof state after:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
i : Fin 0
⊢ x i = y i
Theorem: MulAction.is_zero_pretransitive
Proof state before:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
i : Fin 0
⊢ x i = y i
Tactic:
exfalso
Proof state after:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
i : Fin 0
⊢ False
Theorem: MulAction.is_zero_pretransitive
Proof state before:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 0 ↪ α
i : Fin 0
⊢ False
Tactic:
exact IsEmpty.false i
Proof state after:
no goals
Theorem: MulAction.isPretransitive_iff_is_one_pretransitive
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPretransitive M α ↔ IsMultiplyPretransitive M α 1
Tactic:
unfold IsMultiplyPretransitive
Proof state after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPretransitive M α ↔ IsPretransitive M (Fin 1 ↪ α)
Theorem: MulAction.isPretransitive_iff_is_one_pretransitive
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPretransitive M α ↔ IsPretransitive M (Fin 1 ↪ α)
Tactic:
rw [isPretransitive.of_bijective_map_iff Function.surjective_id (finOneToMap_bijective M α)]
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 α
⊢ IsMultiplyPretransitive M α 2 ↔ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
Tactic:
have : ∀ i : Fin 2, i = 0 ∨ i = 1 := by
  rintro ⟨i, hi⟩
  by_cases hi' : i = 0
  apply Or.intro_left
  apply Fin.eq_of_val_eq
  simp only [Fin.val_zero, hi']
  apply Or.intro_right
  apply Fin.eq_of_val_eq
  simp only [Fin.val_one]
  apply Nat.eq_of_lt_succ_of_not_lt
  exact hi; simp only [lt_one_iff]; exact hi'
Proof state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
⊢ IsMultiplyPretransitive M α 2 ↔ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
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
⊢ IsMultiplyPretransitive M α 2 ↔ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
Tactic:
let f : ∀ (a b : α) (_ : a ≠ b), Fin 2 ↪ α := fun a b hab =>
  ⟨fun i => ite (i = 0) a b, by
    intro i j hij
    by_cases hi : i = 0
    by_cases hj : j = 0
    rw [hi, hj]
    simp only [if_pos hi, if_neg hj] at hij ; exfalso; exact hab hij
    by_cases hj : j = 0
    simp only [if_neg hi, if_pos hj] at hij ; exfalso; exact hab hij.symm
    rw [Or.resolve_left (this i) hi, Or.resolve_left (this j) hj]⟩
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' := ⋯ }
⊢ IsMultiplyPretransitive M α 2 ↔ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
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' := ⋯ }
⊢ IsMultiplyPretransitive M α 2 ↔ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
Tactic:
constructor
Proof state after:
case mp
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' := ⋯ }
⊢ IsMultiplyPretransitive M α 2 → ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d

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
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ ∀ (i : Fin 2), i = 0 ∨ i = 1
Tactic:
rintro ⟨i, hi⟩
Proof state after:
case mk
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1
Theorem: MulAction.is_two_pretransitive_iff
Proof state before:
case mk
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1
Tactic:
by_cases hi' : i = 0
Proof state after:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : i = 0
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1