Theorem: MulAction.isMultiplyPretransitive_of_surjective_map (Jordan/MultipleTransitivity.lean)

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
⊢ IsMultiplyPretransitive N β n
Tactic:
let h_eq := h.exists_smul_eq
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
⊢ IsMultiplyPretransitive N β n

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
⊢ IsMultiplyPretransitive N β n
Tactic:
apply IsPretransitive.mk
State after:
case 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 : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : Fin n ↪ β), ∃ g, g • x = y

State before:
case 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 : α →ₑ[σ] β
hf : Function.Surjective ⇑f
h : IsMultiplyPretransitive M α n
h_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : Fin n ↪ β), ∃ g, g • x = y
Tactic:
let aux : (Fin n ↪ β) → (Fin n ↪ α) := fun x =>
  { toFun := (Function.surjInv hf) ∘ x.toFun
    inj' := fun u v huv => by
      let huv' :=congr_arg f huv
      simp only [Function.comp_apply, Function.surjInv_eq] at huv'
      exact x.inj' huv' }
State after:
case 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 : α →ₑ[σ] β
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 y : Fin n ↪ β), ∃ g, g • x = y

State before:
case 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 : α →ₑ[σ] β
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 y : Fin n ↪ β), ∃ g, g • x = y
Tactic:
have aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun (aux x i) = x i := fun x i => by
  simp only [toFun_eq_coe, coeFn_mk, Function.comp_apply, aux]
  apply Function.surjInv_eq
State after:
case 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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
⊢ ∀ (x y : Fin n ↪ β), ∃ g, g • x = y

State before:
case 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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
⊢ ∀ (x y : Fin n ↪ β), ∃ g, g • x = y
Tactic:
intro x y
State after:
case 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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
⊢ ∃ g, g • x = y

State before:
case 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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g, hg⟩ := h_eq (aux x) (aux y)
State after:
case 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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : g • aux x = aux y
⊢ ∃ g, g • x = y

State before:
case 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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : g • aux x = aux y
⊢ ∃ g, g • x = y
Tactic:
use σ g
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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : g • aux x = aux y
⊢ σ g • x = y

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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : g • aux x = aux y
⊢ σ g • x = y
Tactic:
ext i
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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : g • aux x = aux y
i : Fin n
⊢ (σ g • x) i = y i

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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : g • aux x = aux y
i : Fin n
⊢ (σ g • x) i = y i
Tactic:
rw [DFunLike.ext_iff] at hg
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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : ∀ (x_1 : Fin n), (g • aux x) x_1 = (aux y) x_1
i : Fin n
⊢ (σ g • x) i = y i

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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : ∀ (x_1 : Fin n), (g • aux x) x_1 = (aux y) x_1
i : Fin n
⊢ (σ g • x) i = y i
Tactic:
simp only [smul_apply]
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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : ∀ (x_1 : Fin n), (g • aux x) x_1 = (aux y) x_1
i : Fin n
⊢ σ g • x i = y i

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 : α →ₑ[σ] β
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' := ⋯ }
aux_apply : ∀ (x : Fin n ↪ β) (i : Fin n), f.toFun ((aux x) i) = x i
x y : Fin n ↪ β
g : M
hg : ∀ (x_1 : Fin n), (g • aux x) x_1 = (aux y) x_1
i : Fin n
⊢ σ g • x i = y i
Tactic:
simp only [← aux_apply, ← hg, smul_apply, MulActionHom.map_smul']
State after:
no goals

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
x : Fin n ↪ β
u v : Fin n
huv : (Function.surjInv hf ∘ x.toFun) u = (Function.surjInv hf ∘ x.toFun) v
⊢ u = v
Tactic:
let huv' :=congr_arg f huv
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
x : Fin n ↪ β
u v : Fin n
huv : (Function.surjInv hf ∘ x.toFun) u = (Function.surjInv hf ∘ x.toFun) v
huv' : f ((Function.surjInv hf ∘ x.toFun) u) = f ((Function.surjInv hf ∘ x.toFun) v) := congr_arg (⇑f) huv
⊢ u = v

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
x : Fin n ↪ β
u v : Fin n
huv : (Function.surjInv hf ∘ x.toFun) u = (Function.surjInv hf ∘ x.toFun) v
huv' : f ((Function.surjInv hf ∘ x.toFun) u) = f ((Function.surjInv hf ∘ x.toFun) v) := congr_arg (⇑f) huv
⊢ u = v
Tactic:
simp only [Function.comp_apply, Function.surjInv_eq] at huv'
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
x : Fin n ↪ β
u v : Fin n
huv : (Function.surjInv hf ∘ x.toFun) u = (Function.surjInv hf ∘ x.toFun) v
huv' : x.toFun u = x.toFun v
⊢ u = v

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
x : Fin n ↪ β
u v : Fin n
huv : (Function.surjInv hf ∘ x.toFun) u = (Function.surjInv hf ∘ x.toFun) v
huv' : x.toFun u = x.toFun v
⊢ u = v
Tactic:
exact x.inj' huv'
State after:
no goals

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]
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

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
State after:
no goals