Theorem: nontrivial_on_equiv_perm_two (Jordan/Jordan.lean)

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
⊢ IsMultiplyPretransitive K α 2
Tactic:
classical
let φ := MulAction.toPermHom K α
let f : α →ₑ[φ] α :=
  { toFun := id
    map_smul' := fun k x => rfl }
have hf : Function.Bijective f := Function.bijective_id
suffices Function.Surjective φ by
  rw [isMultiplyPretransitive_of_bijective_map_iff this hf]
  rw [← hα]
  apply Equiv.Perm.isMultiplyPretransitive
rw [← MonoidHom.range_top_iff_surjective]
apply Subgroup.eq_top_of_card_eq
apply le_antisymm
apply Fintype.card_subtype_le
suffices hg : toPerm g ∈ φ.range by
  rw [Fintype.card_perm, hα, Nat.factorial_two, Nat.succ_le_iff, Subgroup.one_lt_card_iff_ne_bot]
  intro h; apply hga
  rw [h, Subgroup.mem_bot] at hg
  rw [← MulAction.toPerm_apply, hg, Equiv.Perm.coe_one, id_eq]
use g
rfl
State after:
no goals

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
⊢ IsMultiplyPretransitive K α 2
Tactic:
let φ := MulAction.toPermHom K α
State after:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
⊢ IsMultiplyPretransitive K α 2

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
⊢ IsMultiplyPretransitive K α 2
Tactic:
let f : α →ₑ[φ] α :=
  { toFun := id
    map_smul' := fun k x => rfl }
State after:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
⊢ IsMultiplyPretransitive K α 2

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
⊢ IsMultiplyPretransitive K α 2
Tactic:
have hf : Function.Bijective f := Function.bijective_id
State after:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsMultiplyPretransitive K α 2

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsMultiplyPretransitive K α 2
Tactic:
suffices Function.Surjective φ by
  rw [isMultiplyPretransitive_of_bijective_map_iff this hf]
  rw [← hα]
  apply Equiv.Perm.isMultiplyPretransitive
State after:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Function.Surjective ⇑φ

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Function.Surjective ⇑φ
Tactic:
rw [← MonoidHom.range_top_iff_surjective]
State after:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ MonoidHom.range φ = ⊤

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ MonoidHom.range φ = ⊤
Tactic:
apply Subgroup.eq_top_of_card_eq
State after:
case h
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Fintype.card ↥(MonoidHom.range φ) = Fintype.card (Equiv.Perm α)

State before:
case h
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Fintype.card ↥(MonoidHom.range φ) = Fintype.card (Equiv.Perm α)
Tactic:
apply le_antisymm
State after:
case h.a
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Fintype.card ↥(MonoidHom.range φ) ≤ Fintype.card (Equiv.Perm α)

case h.a
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥(MonoidHom.range φ)

State before:
case h.a
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Fintype.card ↥(MonoidHom.range φ) ≤ Fintype.card (Equiv.Perm α)

case h.a
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥(MonoidHom.range φ)
Tactic:
apply Fintype.card_subtype_le
State after:
case h.a
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥(MonoidHom.range φ)

State before:
case h.a
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥(MonoidHom.range φ)
Tactic:
suffices hg : toPerm g ∈ φ.range by
  rw [Fintype.card_perm, hα, Nat.factorial_two, Nat.succ_le_iff, Subgroup.one_lt_card_iff_ne_bot]
  intro h; apply hga
  rw [h, Subgroup.mem_bot] at hg
  rw [← MulAction.toPerm_apply, hg, Equiv.Perm.coe_one, id_eq]
State after:
case h.a
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ toPerm g ∈ MonoidHom.range φ

State before:
case h.a
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ toPerm g ∈ MonoidHom.range φ
Tactic:
use g
State after:
case h
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ φ g = toPerm g

State before:
case h
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ φ g = toPerm g
Tactic:
rfl
State after:
no goals

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
this : Function.Surjective ⇑φ
⊢ IsMultiplyPretransitive K α 2
Tactic:
rw [isMultiplyPretransitive_of_bijective_map_iff this hf]
State after:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
this : Function.Surjective ⇑φ
⊢ IsMultiplyPretransitive (Equiv.Perm α) α 2

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
this : Function.Surjective ⇑φ
⊢ IsMultiplyPretransitive (Equiv.Perm α) α 2
Tactic:
rw [← hα]
State after:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
this : Function.Surjective ⇑φ
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
this : Function.Surjective ⇑φ
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)
Tactic:
apply Equiv.Perm.isMultiplyPretransitive
State after:
no goals

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
hg : toPerm g ∈ MonoidHom.range φ
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥(MonoidHom.range φ)
Tactic:
rw [Fintype.card_perm, hα, Nat.factorial_two, Nat.succ_le_iff, Subgroup.one_lt_card_iff_ne_bot]
State after:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
hg : toPerm g ∈ MonoidHom.range φ
⊢ MonoidHom.range φ ≠ ⊥

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
hg : toPerm g ∈ MonoidHom.range φ
⊢ MonoidHom.range φ ≠ ⊥
Tactic:
intro h
State after:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
hg : toPerm g ∈ MonoidHom.range φ
h : MonoidHom.range φ = ⊥
⊢ False

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
hg : toPerm g ∈ MonoidHom.range φ
h : MonoidHom.range φ = ⊥
⊢ False
Tactic:
apply hga
State after:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
hg : toPerm g ∈ MonoidHom.range φ
h : MonoidHom.range φ = ⊥
⊢ g • a = a

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
hg : toPerm g ∈ MonoidHom.range φ
h : MonoidHom.range φ = ⊥
⊢ g • a = a
Tactic:
rw [h, Subgroup.mem_bot] at hg
State after:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
hg : toPerm g = 1
h : MonoidHom.range φ = ⊥
⊢ g • a = a

State before:
α : Type u_2
inst✝² : Fintype α
G : Subgroup (Equiv.Perm α)
K : Type u_1
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Fintype.card α = 2
g : K
a : α
hga : g • a ≠ a
φ : K →* Equiv.Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
hg : toPerm g = 1
h : MonoidHom.range φ = ⊥
⊢ g • a = a
Tactic:
rw [← MulAction.toPerm_apply, hg, Equiv.Perm.coe_one, id_eq]
State after:
no goals