Theorem: MulAction.isMultiplyPretransitive_of_bijective_map_iff (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 : α →ₑ[σ] β
hσ : Function.Surjective σ
hf : Function.Bijective ⇑f
⊢ IsMultiplyPretransitive M α n ↔ IsMultiplyPretransitive N β n
Tactic:
constructor
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

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

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

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

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

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'⟩
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

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'⟩
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

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

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

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

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

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

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

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

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

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