internlm/Lean-Github huggingface dataset:
Theorem: eq_s2_of_nontrivial
Proof state before:
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ G = ⊤
Tactic:
apply Subgroup.eq_top_of_card_eq
Proof state after:
case h
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card ↥G = Fintype.card (Equiv.Perm α)
Theorem: eq_s2_of_nontrivial
Proof state before:
case h
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card ↥G = Fintype.card (Equiv.Perm α)
Tactic:
apply le_antisymm
Proof state after:
case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card ↥G ≤ Fintype.card (Equiv.Perm α)

case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥G
Theorem: eq_s2_of_nontrivial
Proof state before:
case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card ↥G ≤ Fintype.card (Equiv.Perm α)

case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥G
Tactic:
apply Fintype.card_subtype_le
Proof state after:
case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥G
Theorem: eq_s2_of_nontrivial
Proof state before:
case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥G
Tactic:
rw [Fintype.card_equiv (Equiv.cast rfl)]
Proof state after:
case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial (Fintype.card α) ≤ Fintype.card ↥G
Theorem: eq_s2_of_nontrivial
Proof state before:
case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial (Fintype.card α) ≤ Fintype.card ↥G
Tactic:
refine' le_trans _ _
Proof state after:
case h.a.refine'_1
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ ℕ

case h.a.refine'_2
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial (Fintype.card α) ≤ ?h.a.refine'_1

case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ ?h.a.refine'_1 ≤ Fintype.card ↥G
Theorem: eq_s2_of_nontrivial
Proof state before:
case h.a.refine'_1
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ ℕ

case h.a.refine'_2
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial (Fintype.card α) ≤ ?h.a.refine'_1

case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ ?h.a.refine'_1 ≤ Fintype.card ↥G
Tactic:
exact (2 : ℕ).factorial
Proof state after:
case h.a.refine'_2
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial (Fintype.card α) ≤ Nat.factorial 2

case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial 2 ≤ Fintype.card ↥G
Theorem: eq_s2_of_nontrivial
Proof state before:
case h.a.refine'_2
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial (Fintype.card α) ≤ Nat.factorial 2

case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial 2 ≤ Fintype.card ↥G
Tactic:
exact Nat.factorial_le hα
Proof state after:
case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial 2 ≤ Fintype.card ↥G
Theorem: eq_s2_of_nontrivial
Proof state before:
case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial 2 ≤ Fintype.card ↥G
Tactic:
rw [Nat.factorial_two]
Proof state after:
case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ 2 ≤ Fintype.card ↥G
Theorem: eq_s2_of_nontrivial
Proof state before:
case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ 2 ≤ Fintype.card ↥G
Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial] at hG
Proof state after:
case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : 1 < Fintype.card ↥G
⊢ 2 ≤ Fintype.card ↥G
Theorem: eq_s2_of_nontrivial
Proof state before:
case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : 1 < Fintype.card ↥G
⊢ 2 ≤ Fintype.card ↥G
Tactic:
exact hG
Proof state after:
no goals
Theorem: nontrivial_on_equiv_perm_two
Proof 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
Proof state after:
no goals
Theorem: nontrivial_on_equiv_perm_two
Proof 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 α
Proof 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
Theorem: nontrivial_on_equiv_perm_two
Proof 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 }
Proof 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
Theorem: nontrivial_on_equiv_perm_two
Proof 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
Proof 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
Theorem: nontrivial_on_equiv_perm_two
Proof 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
Proof 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 ⇑φ
Theorem: nontrivial_on_equiv_perm_two
Proof 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]
Proof 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 φ = ⊤
Theorem: nontrivial_on_equiv_perm_two
Proof 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
Proof 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 α)
Theorem: nontrivial_on_equiv_perm_two
Proof 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
Proof 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 φ)
Theorem: nontrivial_on_equiv_perm_two
Proof 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
Proof 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 φ)
Theorem: nontrivial_on_equiv_perm_two
Proof 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]
Proof 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 φ
Theorem: nontrivial_on_equiv_perm_two
Proof 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
Proof 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
Theorem: nontrivial_on_equiv_perm_two
Proof 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
Proof state after:
no goals
Theorem: nontrivial_on_equiv_perm_two
Proof 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]
Proof 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
Theorem: nontrivial_on_equiv_perm_two
Proof 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α]
Proof 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 α)
Theorem: nontrivial_on_equiv_perm_two
Proof 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
Proof state after:
no goals
Theorem: nontrivial_on_equiv_perm_two
Proof 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]
Proof 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 φ ≠ ⊥
Theorem: nontrivial_on_equiv_perm_two
Proof 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
Proof 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
Theorem: nontrivial_on_equiv_perm_two
Proof 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
Proof 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
Theorem: nontrivial_on_equiv_perm_two
Proof 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
Proof 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
Theorem: nontrivial_on_equiv_perm_two
Proof 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]
Proof state after:
no goals
Theorem: isPretransitive_of_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
hgc : Equiv.Perm.IsCycle g
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
Tactic:
obtain ⟨a, _, hgc⟩ := hgc
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
Theorem: isPretransitive_of_cycle
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
Tactic:
have hs : ∀ x : α, g • x ≠ x ↔
  x ∈ SubMulAction.ofFixingSubgroup G ((↑g.support : Set α)ᶜ) := by
  intro x
  rw [SubMulAction.mem_ofFixingSubgroup_iff]
  simp only [Set.mem_compl_iff, Finset.mem_coe, Equiv.Perm.not_mem_support]
  rfl
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
Theorem: isPretransitive_of_cycle
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
Tactic:
suffices ∀ x ∈ SubMulAction.ofFixingSubgroup G ((↑g.support : Set α)ᶜ),
    ∃ k : fixingSubgroup G ((↑g.support : Set α)ᶜ), x = k • a
  by
  apply IsPretransitive.mk
  rintro ⟨x, hx⟩ ⟨y, hy⟩
  obtain ⟨k, hk⟩ := this x hx
  obtain ⟨k', hk'⟩ := this y hy
  use k' * k⁻¹
  rw [← SetLike.coe_eq_coe]
  simp only [SetLike.mk_smul_mk]
  rw [hk, hk', smul_smul, inv_mul_cancel_right]
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
⊢ ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a