awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this_2 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h_1 : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
this :
  Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2
a b : α
hab : a ≠ b
hs :
  Eq (α := Finset α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ
    {a, b}
i : Fin (Nat.card α - 2)
h : ¬(x : (a : Fin (Nat.card α - 2)) → α) i = a ∧ ¬(x : (a : Fin (Nat.card α - 2)) → α) i = b
⊢ Eq (α := α)
    ((HSMul.hSMul (α := ↥(alternatingGroup α))
            (Subtype.mk (p := fun (x : Equiv.Perm α) ↦ x ∈ alternatingGroup α) (g * Equiv.swap a b) ⋯) x :
          (a : Fin (Nat.card α - 2)) → α)
        i :
      α)
    ((y : (a : Fin (Nat.card α - 2)) → α) i : α)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne h.1 h.2, ← hg]

Premises used: Equiv.swap_apply_of_ne_of_ne, And.right, And.left
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
inl : ∀ (hα1 : Nat.card α < 2), alternatingGroup α ≤ G
inr : ∀ (hα : Nat.card α ≥ 2), alternatingGroup α ≤ G
⊢ alternatingGroup α ≤ G

Tactic:
rcases Nat.lt_or_ge (Nat.card α) 2 with hα1 | hα

Premises used: Nat.card, Nat.lt_or_ge, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα1 : Nat.card α < 2
inl : ⊥ ≤ G
⊢ alternatingGroup α ≤ G

Tactic:
rw [eq_bot_of_card_le_two hα1.le]

Premises used: alternatingGroup.eq_bot_of_card_le_two, LT.lt.le
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα1 : Nat.card α < 2
⊢ ⊥ ≤ G

Tactic:
bot_le

Premises used: Set.Mem, bot_le
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα1 : Nat.card α < 2
⊢ ⊥ ≤ G

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα : Nat.card α ≥ 2
inr : G.index ≤ 2
⊢ alternatingGroup α ≤ G

Tactic:
apply Equiv.Perm.alternatingGroup_le_of_index_le_two

Premises used: Equiv.Perm.alternatingGroup_le_of_index_le_two
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα : Nat.card α ≥ 2
rw : Nat.card α - 2 ≤ Nat.card α
⊢ Nat.card α - 2 ≤ ncard.{u_1} (α := α) univ

Tactic:
rw [Set.ncard_univ]

Premises used: Set.ncard_univ
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα : Nat.card α ≥ 2
⊢ Nat.card α - 2 ≤ Nat.card α

Tactic:
sub_le (Nat.card α) 2

Premises used: Nat.sub_le, Nat.card, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα : Nat.card α ≥ 2
⊢ Nat.card α - 2 ≤ Nat.card α

Tactic:
exact sub_le (Nat.card α) 2

Premises used: Nat.sub_le, Nat.card, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα : Nat.card α ≥ 2
inr : ∀ s ⊆ univ, ∀ (hs : s.ncard = Nat.card α - 2), G.index ≤ 2
⊢ G.index ≤ 2

Tactic:
obtain ⟨s, _, hs⟩ :=
    Set.exists_subset_card_eq (s := (Set.univ : Set α)) (n := Nat.card α - 2)
      (by rw [Set.ncard_univ]; exact sub_le (Nat.card α) 2)

Premises used: Set.exists_subset_card_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα : Nat.card α ≥ 2
s : Set α
left : s ⊆ univ
hs : s.ncard = Nat.card α - 2
⊢ IsMultiplyPretransitive (↥G) α s.ncard

Tactic:
rw [← hs] at hmt
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα : Nat.card α ≥ 2
s : Set α
left : s ⊆ univ
hs : s.ncard = Nat.card α - 2
hmt₁ : IsMultiplyPretransitive (↥G) α s.ncard
⊢ s ⊆ univ

Tactic:
rw [← hs] at hmt
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα : Nat.card α ≥ 2
s : Set α
left_1 : s ⊆ univ
hs : s.ncard = Nat.card α - 2
hmt₁ : IsMultiplyPretransitive (↥G) α s.ncard
left : s ⊆ univ
⊢ s.ncard = Nat.card α - 2

Tactic:
rw [← hs] at hmt
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Nat.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α s.ncard
left : s ⊆ univ
hs : s.ncard = Nat.card α - 2
⊢ Subgroup.index (G := ↥G) (fixingSubgroup (↥G) s) * (Nat.card α - s.ncard)! = (Nat.card α)!

Tactic:
have := hmt.index_of_fixingSubgroup_mul rfl
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Nat.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α s.ncard
left : s ⊆ univ
hs : s.ncard = Nat.card α - 2
this : Subgroup.index (G := ↥G) (fixingSubgroup (↥G) s) * (Nat.card α - s.ncard)! = (Nat.card α)!
⊢ Subgroup.index (G := ↥G) (fixingSubgroup (↥G) s) * 2 = (Nat.card α)!

Tactic:
rw [hs, Nat.sub_sub_self hα, factorial_two] at this

Premises used: Nat.sub_sub_self, Nat.factorial_two
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Nat.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α s.ncard
left : s ⊆ univ
hs : s.ncard = Nat.card α - 2
this : Subgroup.index (G := ↥G) (fixingSubgroup (↥G) s) * 2 = (Nat.card α)!
inr :
  Nat.card.{u_1} (Equiv.Perm α) ≤
    Subgroup.index (G := ↥G) (fixingSubgroup (↥G) s) * 2 * Nat.card.{u_1} ↥(fixingSubgroup (↥G) s)
⊢ G.index ≤ 2

Tactic:
rw [← mul_le_mul_iff_of_pos_left (a := Nat.card G) card_pos,
    Subgroup.card_mul_index, ← (fixingSubgroup G s).index_mul_card,
    mul_assoc, mul_comm _ 2, ← mul_assoc]

Premises used: Nat.card_pos, fixingSubgroup, mul_assoc, Subgroup.index_mul_card, Membership.mem, mul_le_mul_iff_of_pos_left, Subtype, mul_comm, OfNat.ofNat, Subgroup.card_mul_index
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Nat.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α s.ncard
left : s ⊆ univ
hs : s.ncard = Nat.card α - 2
this : Subgroup.index (G := ↥G) (fixingSubgroup (↥G) s) * 2 = (Nat.card α)!
inr : (Nat.card α)! ≤ (Nat.card α)! * Nat.card.{u_1} ↥(fixingSubgroup (↥G) s)
⊢ Nat.card.{u_1} (Equiv.Perm α) ≤
    Subgroup.index (G := ↥G) (fixingSubgroup (↥G) s) * 2 * Nat.card.{u_1} ↥(fixingSubgroup (↥G) s)

Tactic:
rw [this, Nat.card_perm]

Premises used: Nat.card_perm
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Nat.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α s.ncard
left : s ⊆ univ
hs : s.ncard = Nat.card α - 2
this : Subgroup.index (G := ↥G) (fixingSubgroup (↥G) s) * 2 = (Nat.card α)!
⊢ (Nat.card α)! ≤ (Nat.card α)! * Nat.card.{u_1} ↥(fixingSubgroup (↥G) s)

Tactic:
Nat.le_mul_of_pos_right (Nat.card α)! card_pos

Premises used: Nat.le_mul_of_pos_right, Nat.card_pos, Nat.card, Nat.factorial
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Nat.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α s.ncard
left : s ⊆ univ
hs : s.ncard = Nat.card α - 2
this : Subgroup.index (G := ↥G) (fixingSubgroup (↥G) s) * 2 = (Nat.card α)!
⊢ (Nat.card α)! ≤ (Nat.card α)! * Nat.card.{u_1} ↥(fixingSubgroup (↥G) s)

Tactic:
refine Nat.le_mul_of_pos_right (Nat.card α)! card_pos

Premises used: Nat.le_mul_of_pos_right, Nat.card_pos, Nat.card, Nat.factorial
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : 3 ≤ Nat.card α
rw : IsMultiplyPretransitive (↥(alternatingGroup α)) α 1
⊢ IsPretransitive (↥(alternatingGroup α)) α

Tactic:
rw [← is_one_pretransitive_iff]

Premises used: MulAction.is_one_pretransitive_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : 3 ≤ Nat.card α
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2) := ⋯
apply : 1 ≤ Nat.card α - 2
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 1

Tactic:
apply isMultiplyPretransitive_of_le (n := Nat.card α - 2) _ (sub_le _ _)

Premises used: Nat.sub_le, MulAction.isMultiplyPretransitive_of_le
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : 3 ≤ Nat.card α
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2) := ⋯
⊢ LE.le (α := ℕ) 2 3

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : 3 ≤ Nat.card α
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2) := ⋯
rwa : HAdd.hAdd (α := ℕ) 1 2 ≤ Nat.card α - 2 + 2
rwa₁ rwa₂ rwa₃ rwa₄ : HAdd.hAdd (α := ℕ) 1 2 ≤ Nat.card α
⊢ 1 ≤ Nat.card α - 2

Tactic:
rwa [← add_le_add_iff_right 2, Nat.sub_add_cancel (le_trans (by norm_num) h)]

Premises used: add_le_add_iff_right, Nat.sub_add_cancel, OfNat.ofNat, le_trans
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
inl : ∀ (h2 : Nat.card α ≤ 2), IsTrivialBlock B
inr : ∀ (h2 : 2 < Nat.card α), IsTrivialBlock B
⊢ IsTrivialBlock B

Tactic:
rcases le_or_gt (Nat.card α) 2 with h2 | h2

Premises used: Nat.card, le_or_gt, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : Nat.card α ≤ 2
⊢ IsTrivialBlock B

Tactic:
isTrivialBlock_of_card_le_two h2 B

Premises used: MulAction.isTrivialBlock_of_card_le_two
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : Nat.card α ≤ 2
⊢ IsTrivialBlock B

Tactic:
exact isTrivialBlock_of_card_le_two h2 B

Premises used: MulAction.isTrivialBlock_of_card_le_two
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
inr : ∀ (h3 : Nat.card α ≤ 3), IsTrivialBlock B
inr₁ : ∀ (h4 : 3 < Nat.card α), IsTrivialBlock B
⊢ IsTrivialBlock B

Tactic:
rcases le_or_gt (Nat.card α) 3 with h3 | h4

Premises used: Nat.card, le_or_gt, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h3 : Nat.card α ≤ 3
⊢ Nat.card α = 3

Tactic:
replace h3 : Nat.card α = 3 := le_antisymm h3 h2
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h3 : Nat.card α = 3
⊢ IsPretransitive (↥(alternatingGroup α)) α

Tactic:
have : IsPretransitive (alternatingGroup α) α := isPretransitive_of_three_le_card α h3.ge
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h3 : Nat.card α = 3
this : IsPretransitive (↥(alternatingGroup α)) α
⊢ IsPreprimitive (↥(alternatingGroup α)) α

Tactic:
have : IsPreprimitive (alternatingGroup α) α := IsPreprimitive.of_prime_card (h3 ▸ prime_three)
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h3 : Nat.card α = 3
this_1 : IsPretransitive (↥(alternatingGroup α)) α
this : IsPreprimitive (↥(alternatingGroup α)) α
⊢ IsTrivialBlock B

Tactic:
this.isTrivialBlock_of_isBlock hB

Premises used: MulAction.IsPreprimitive.isTrivialBlock_of_isBlock
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h3 : Nat.card α = 3
this_1 : IsPretransitive (↥(alternatingGroup α)) α
this : IsPreprimitive (↥(alternatingGroup α)) α
⊢ IsTrivialBlock B

Tactic:
exact this.isTrivialBlock_of_isBlock hB

Premises used: MulAction.IsPreprimitive.isTrivialBlock_of_isBlock
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h4 : 3 < Nat.card α
this : IsPreprimitive (↥(alternatingGroup α)) α
⊢ IsTrivialBlock B

Tactic:
apply IsPreprimitive.isTrivialBlock_of_isBlock hB

Premises used: MulAction.IsPreprimitive.isTrivialBlock_of_isBlock
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h4 : 3 < Nat.card α
inr : IsPreprimitive (↥(alternatingGroup α)) α
⊢ IsTrivialBlock B

Tactic:
suffices IsPreprimitive (alternatingGroup α) α by
    apply IsPreprimitive.isTrivialBlock_of_isBlock hB
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h4 : 3 < Nat.card α
inr : IsMultiplyPretransitive (↥(alternatingGroup α)) α 2
⊢ IsPreprimitive (↥(alternatingGroup α)) α

Tactic:
apply isPreprimitive_of_is_two_pretransitive

Premises used: MulAction.isPreprimitive_of_is_two_pretransitive
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h4 : 3 < Nat.card α
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2) := ⋯
apply : 2 ≤ Nat.card α - 2
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 2

Tactic:
apply isMultiplyPretransitive_of_le (n := Nat.card α - 2) _ (sub_le _ _)

Premises used: Nat.sub_le, MulAction.isMultiplyPretransitive_of_le
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h4 : 3 < Nat.card α
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2) := ⋯
rwa : HAdd.hAdd (α := ℕ) 2 2 ≤ Nat.card α - 2 + 2
rwa₁ rwa₂ rwa₃ rwa₄ : HAdd.hAdd (α := ℕ) 2 2 ≤ Nat.card α
⊢ 2 ≤ Nat.card α - 2

Tactic:
rwa [← add_le_add_iff_right 2, Nat.sub_add_cancel (le_of_lt h2)]

Premises used: le_of_lt, add_le_add_iff_right, Nat.sub_add_cancel, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : 3 ≤ Nat.card α
⊢ IsPreprimitive (↥(alternatingGroup α)) α

Tactic:
letI := isPretransitive_of_three_le_card α h
  { isTrivialBlock_of_isBlock := isTrivialBlock_of_isBlock α }

Premises used: alternatingGroup.isTrivialBlock_of_isBlock, MulAction.IsPreprimitive.mk
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
h :
  ∀ (x : G),
    x ∈ HSMul.hSMul (β := Set G) g ((⇑(mk' N) : (a : G) → G ⧸ N) ⁻¹' U) ↔
      Membership.mem (γ := Set G) ((⇑(mk' N) : (a : G) → G ⧸ N) ⁻¹' U) x
⊢ HSMul.hSMul (β := Set G) g ((⇑(mk' N) : (a : G) → G ⧸ N) ⁻¹' U) = (⇑(mk' N) : (a : G) → G ⧸ N) ⁻¹' U

Tactic:
ext x
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
h :
  Membership.mem (α := G ⧸ N) U ((mk' N : (a : G) → G ⧸ N) (g⁻¹ • x) : G ⧸ N) ↔
    Membership.mem (α := G ⧸ N) U ((mk' N : (a : G) → G ⧸ N) x : G ⧸ N)
⊢ x ∈ HSMul.hSMul (β := Set G) g ((⇑(mk' N) : (a : G) → G ⧸ N) ⁻¹' U) ↔
    Membership.mem (γ := Set G) ((⇑(mk' N) : (a : G) → G ⧸ N) ⁻¹' U) x

Tactic:
simp only [Set.mem_preimage, Set.mem_smul_set_iff_inv_smul_mem]

Premises used: Set.mem_smul_set_iff_inv_smul_mem, Set.mem_preimage
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
h : Eq (α := G ⧸ N) ((mk' N : (a : G) → G ⧸ N) (g⁻¹ • x) : G ⧸ N) ((mk' N : (a : G) → G ⧸ N) x : G ⧸ N)
⊢ Membership.mem (α := G ⧸ N) U ((mk' N : (a : G) → G ⧸ N) (g⁻¹ • x) : G ⧸ N) ↔
    Membership.mem (α := G ⧸ N) U ((mk' N : (a : G) → G ⧸ N) x : G ⧸ N)

Tactic:
congr! 1
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
⊢ Eq (α := G ⧸ N) ((mk' N : (a : G) → G ⧸ N) (g⁻¹ • x) : G ⧸ N) ((mk' N : (a : G) → G ⧸ N) x : G ⧸ N)

Tactic:
Quotient.sound ⟨g⁻¹, rfl⟩

Premises used: Inv.inv, Exists.intro, Quotient.sound, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
⊢ Eq (α := G ⧸ N) ((mk' N : (a : G) → G ⧸ N) (g⁻¹ • x) : G ⧸ N) ((mk' N : (a : G) → G ⧸ N) x : G ⧸ N)

Tactic:
exact Quotient.sound ⟨g⁻¹, rfl⟩
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u_1
ι : Type u_2
inst : CommGroup G
N : Subgroup G
s : Finset ι
f : ι → G
⊢ Eq (α := G ⧸ N) (↑(s.prod f) : G ⧸ N) (∏ i ∈ s, (↑(f i) : G ⧸ N))

Tactic:
map_prod (QuotientGroup.mk' N) _ _

Premises used: map_prod, QuotientGroup.mk'
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
⊢ StrictMono (β := Subgroup ↥N × Subgroup (G ⧸ N)) fun (H : Subgroup G) ↦
    (Subgroup.comap N.subtype H, Subgroup.map (mk' N) H)

Tactic:
strictMono_comap_prod_image N

Premises used: StrictMono, Subgroup.map, Set.Mem, setOf, Set.Subset, QuotientGroup.strictMono_comap_prod_image, Set.image
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst_1 : Group H
M : Type x
inst_2 : Monoid M
A : Subgroup G
B : Subgroup H
q : (G × H) ⧸ A.prod B
⊢ ∀ (a b : G × H),
    (leftRel (A.prod B) : G × H → G × H → Prop) a b →
      Eq (α := Prod.{u, v} (G ⧸ A) (H ⧸ B))
        ((fun (x : G × H) ↦
            (match (motive := G × H → Prod.{u, v} (G ⧸ A) (H ⧸ B)) x with
              | (g, h) => ((↑g : G ⧸ A), (↑h : H ⧸ B)) :
              Prod.{u, v} (G ⧸ A) (H ⧸ B)))
          a)
        ((fun (x : G × H) ↦
            (match (motive := G × H → Prod.{u, v} (G ⧸ A) (H ⧸ B)) x with
              | (g, h) => ((↑g : G ⧸ A), (↑h : H ⧸ B)) :
              Prod.{u, v} (G ⧸ A) (H ⧸ B)))
          b)

Tactic:
simp [QuotientGroup.leftRel_apply, Subgroup.mem_prod, QuotientGroup.eq]

Premises used: QuotientGroup.eq, Subgroup.mem_prod, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst_1 : Group H
M : Type x
inst_2 : Monoid M
A : Subgroup G
B : Subgroup H
q : Prod.{u, v} (G ⧸ A) (H ⧸ B)
⊢ ∀ (a₁ : G) (a₂ : H) (b₁ : G) (b₂ : H),
    (leftRel A : G → G → Prop) a₁ b₁ →
      (leftRel B : H → H → Prop) a₂ b₂ →
        Eq (α := (G × H) ⧸ A.prod B)
          ((fun (g : G) (h : H) ↦ ((↑(g, h) : (G × H) ⧸ A.prod B) : (G × H) ⧸ A.prod B)) a₁ a₂)
          ((fun (g : G) (h : H) ↦ ((↑(g, h) : (G × H) ⧸ A.prod B) : (G × H) ⧸ A.prod B)) b₁ b₂)

Tactic:
simp [QuotientGroup.leftRel_apply, Subgroup.mem_prod, QuotientGroup.eq, ← and_imp]

Premises used: and_imp, QuotientGroup.eq, Subgroup.mem_prod, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst_1 : Group H
M : Type x
inst_2 : Monoid M
A : Subgroup G
B : Subgroup H
q : (G × H) ⧸ A.prod B
⊢ ∀ (a : G × H),
    Eq (α := (G × H) ⧸ A.prod B)
      ((fun (q : Prod.{u, v} (G ⧸ A) (H ⧸ B)) ↦
          Quotient.liftOn₂' q.1 q.2 (fun (g : G) (h : H) ↦ (↑(g, h) : (G × H) ⧸ A.prod B)) ⋯)
        ((fun (q : (G × H) ⧸ A.prod B) ↦
            Quotient.liftOn' q
              (fun (x : G × H) ↦
                match (motive := G × H → Prod.{u, v} (G ⧸ A) (H ⧸ B)) x with
                | (g, h) => ((↑g : G ⧸ A), (↑h : H ⧸ B)))
              ⋯)
          (Quotient.mk'' a)))
      (Quotient.mk'' a)

Tactic:
simp
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst_1 : Group H
M : Type x
inst_2 : Monoid M
A : Subgroup G
B : Subgroup H
x : Prod.{u, v} (G ⧸ A) (H ⧸ B)
q₁ : G ⧸ A
q₂ : H ⧸ B
⊢ ∀ (a₁ : G) (a₂ : H),
    Eq (α := Prod.{u, v} (G ⧸ A) (H ⧸ B))
      ((fun (q : (G × H) ⧸ A.prod B) ↦
          Quotient.liftOn' q
            (fun (x : G × H) ↦
              match (motive := G × H → Prod.{u, v} (G ⧸ A) (H ⧸ B)) x with
              | (g, h) => ((↑g : G ⧸ A), (↑h : H ⧸ B)))
            ⋯)
        ((fun (q : Prod.{u, v} (G ⧸ A) (H ⧸ B)) ↦
            Quotient.liftOn₂' q.1 q.2 (fun (g : G) (h : H) ↦ (↑(g, h) : (G × H) ⧸ A.prod B)) ⋯)
          (Quotient.mk'' a₁, Quotient.mk'' a₂)))
      (Quotient.mk'' a₁, Quotient.mk'' a₂)

Tactic:
simp
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
φ : G →* H
g : G
⊢ Eq.{v + 1} (α := H) ((kerLift φ : (a : G ⧸ φ.ker) → H) (↑g : G ⧸ φ.ker) : H) ((φ : (a : G) → H) g : H)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
φ : G →* H
a_1 b_1 : G ⧸ φ.ker
a b : G
h : Eq.{v + 1} (α := H) ((φ : (a : G) → H) a : H) ((φ : (a : G) → H) b : H)
rw : a⁻¹ * b ∈ φ.ker
rw₁ : Eq.{v + 1} (α := H) ((φ : (a : G) → H) (a⁻¹ * b) : H) (1 : H)
rw₂ : HMul.hMul (α := H) (β := H) ((φ : (a : G) → H) a⁻¹ : H) ((φ : (a : G) → H) b : H) = 1
rw₃ : HMul.hMul (α := H) (β := H) ((φ : (a : G) → H) a⁻¹ : H) ((φ : (a : G) → H) a : H) = 1
rw₄ : HMul.hMul (α := H) (β := H) (((φ : (a : G) → H) a)⁻¹ : H) ((φ : (a : G) → H) a : H) = 1
rw₅ rw₆ : Eq.{v + 1} (α := H) 1 1
⊢ (leftRel φ.ker : G → G → Prop) a b

Tactic:
rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_cancel]

Premises used: inv_mul_cancel, MonoidHom.mem_ker, MonoidHom.map_inv, MonoidHom.map_mul, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst_1 : Group H
M : Type x
inst_2 : Monoid M
φ : G →* H
g : G
hg rwa rwa₁ rwa₂ rwa₃ : g ∈ φ.ker
⊢ g ∈ φ.rangeRestrict.ker

Tactic:
rwa [ker_rangeRestrict]

Premises used: MonoidHom.ker_rangeRestrict