awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
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 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
⊢ ∃ (g : ↥(alternatingGroup α)), g • x = y
have this₁ : Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2
Tactic: have : (Finset.univ.image x)ᶜ.card = 2 := by
      rw [Finset.card_compl, Finset.univ.card_image_of_injective (by exact x.2), Finset.card_univ,
        ← Nat.card_eq_fintype_card, Fintype.card_fin, tsub_tsub_cancel_of_le h2]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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 : 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
⊢ ∃ (g : ↥(alternatingGroup α)), g • x = y
have inr : ∀ (a b : α) (hab : a ≠ b)
  (hs :
    Eq (α := Finset α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ
      {a, b}),
  ∃ (g : ↥(alternatingGroup α)), g • x = y
Tactic: obtain ⟨a, b, hab, hs⟩ := Finset.card_eq_two.mp this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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 : 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}
⊢ HSMul.hSMul (α := ↥(alternatingGroup α))
      (Subtype.mk (p := fun (x : Equiv.Perm α) ↦ x ∈ alternatingGroup α) (g * Equiv.swap a b) ⋯) x =
    y
have inr : ∀ (i : Fin (Nat.card α - 2)),
  Eq (α := α)
    ((HSMul.hSMul (α := ↥(alternatingGroup α))
            (Subtype.mk (p := fun (x : Equiv.Perm α) ↦ x ∈ alternatingGroup α) (g * Equiv.swap a b) sorry) x :
          (a : Fin (Nat.card α - 2)) → α)
        i :
      α)
    ((y : (a : Fin (Nat.card α - 2)) → α) i : α)
Tactic: ext i
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
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 : 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)
⊢ 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 : α)
have h₁ : Membership.mem (α := α) (γ := Finset α)
  (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)
  ((x : (a : Fin (Nat.card α - 2)) → α) i : α)
Tactic: have h : x i ∈ Finset.univ.image x := Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
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 :
  Membership.mem (α := α) (γ := Finset α)
    (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)
    ((x : (a : Fin (Nat.card α - 2)) → α) i : α)
⊢ 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 : α)
have h₁ : ¬(x : (a : Fin (Nat.card α - 2)) → α) i = a ∧ ¬(x : (a : Fin (Nat.card α - 2)) → α) i = b
Tactic: rw [← Finset.notMem_compl, hs, Finset.mem_insert, Finset.mem_singleton, not_or] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
⊢ alternatingGroup α ≤ G
have inl : ∀ (hα1 : Nat.card α < 2), alternatingGroup α ≤ G
Tactic: rcases Nat.lt_or_ge (Nat.card α) 2 with hα1 | hα
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ alternatingGroup α ≤ G
have inr : ∀ (hα : Nat.card α ≥ 2), alternatingGroup α ≤ G
Tactic: rcases Nat.lt_or_ge (Nat.card α) 2 with hα1 | hα
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα1 : Nat.card α < 2
⊢ alternatingGroup α ≤ G
have inl : ⊥ ≤ G
Tactic: rw [eq_bot_of_card_le_two hα1.le]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα : Nat.card α ≥ 2
⊢ alternatingGroup α ≤ G
have inr : G.index ≤ 2
Tactic: apply Equiv.Perm.alternatingGroup_le_of_index_le_two
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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 ≤ ncard.{u_1} (α := α) univ
have rw : Nat.card α - 2 ≤ Nat.card α
Tactic: rw [Set.ncard_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα : Nat.card α ≥ 2
⊢ G.index ≤ 2
have inr : ∀ s ⊆ univ, ∀ (hs : s.ncard = Nat.card α - 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)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
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
⊢ G.index ≤ 2
have hmt₁ : IsMultiplyPretransitive (↥G) α s.ncard
Tactic: rw [← hs] at hmt
Cleared hypotheses: hmt, left, hs
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
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
⊢ G.index ≤ 2
have this : Subgroup.index (G := ↥G) (fixingSubgroup (↥G) s) * (Nat.card α - s.ncard)! = (Nat.card α)!
Tactic: have := hmt.index_of_fixingSubgroup_mul rfl
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
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 α)!
⊢ G.index ≤ 2
have this₁ : Subgroup.index (G := ↥G) (fixingSubgroup (↥G) s) * 2 = (Nat.card α)!
Tactic: rw [hs, Nat.sub_sub_self hα, factorial_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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 α)!
⊢ G.index ≤ 2
have inr : Nat.card.{u_1} (Equiv.Perm α) ≤
  Subgroup.index (G := ↥G) (fixingSubgroup (↥G) s) * 2 * Nat.card.{u_1} ↥(fixingSubgroup (↥G) s)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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.{u_1} (Equiv.Perm α) ≤
    Subgroup.index (G := ↥G) (fixingSubgroup (↥G) s) * 2 * Nat.card.{u_1} ↥(fixingSubgroup (↥G) s)
have inr : (Nat.card α)! ≤ (Nat.card α)! * Nat.card.{u_1} ↥(fixingSubgroup (↥G) s)
Tactic: rw [this, Nat.card_perm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : 3 ≤ Nat.card α
⊢ IsPretransitive (↥(alternatingGroup α)) α
have rw : IsMultiplyPretransitive (↥(alternatingGroup α)) α 1
Tactic: rw [← is_one_pretransitive_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : 3 ≤ Nat.card α
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2) := ⋯
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 1
have apply : 1 ≤ Nat.card α - 2
Tactic: apply isMultiplyPretransitive_of_le (n := Nat.card α - 2) _ (sub_le _ _)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : 3 ≤ Nat.card α
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2) := ⋯
⊢ 1 ≤ Nat.card α - 2
have rwa : HAdd.hAdd (α := ℕ) 1 2 ≤ Nat.card α - 2 + 2
Tactic: rwa [← add_le_add_iff_right 2, Nat.sub_add_cancel (le_trans (by norm_num) h)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
⊢ IsTrivialBlock B
have inl : ∀ (h2 : Nat.card α ≤ 2), IsTrivialBlock B
Tactic: rcases le_or_gt (Nat.card α) 2 with h2 | h2
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
inl : ∀ (h2 : Nat.card α ≤ 2), IsTrivialBlock B
⊢ IsTrivialBlock B
have inr : ∀ (h2 : 2 < Nat.card α), IsTrivialBlock B
Tactic: rcases le_or_gt (Nat.card α) 2 with h2 | h2
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
⊢ IsTrivialBlock B
have inr : ∀ (h3 : Nat.card α ≤ 3), IsTrivialBlock B
Tactic: rcases le_or_gt (Nat.card α) 3 with h3 | h4
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ IsTrivialBlock B
have inr₁ : ∀ (h4 : 3 < Nat.card α), IsTrivialBlock B
Tactic: rcases le_or_gt (Nat.card α) 3 with h3 | h4
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h3 : Nat.card α ≤ 3
⊢ IsTrivialBlock B
have h3₁ : Nat.card α = 3
Tactic: replace h3 : Nat.card α = 3 := le_antisymm h3 h2
Cleared hypotheses: h3
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h3 : Nat.card α = 3
⊢ IsTrivialBlock B
have this : IsPretransitive (↥(alternatingGroup α)) α
Tactic: have : IsPretransitive (alternatingGroup α) α := isPretransitive_of_three_le_card α h3.ge
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
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 α)) α
⊢ IsTrivialBlock B
have this₁ : IsPreprimitive (↥(alternatingGroup α)) α
Tactic: have : IsPreprimitive (alternatingGroup α) α := IsPreprimitive.of_prime_card (h3 ▸ prime_three)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h4 : 3 < Nat.card α
⊢ IsTrivialBlock B
have inr : IsPreprimitive (↥(alternatingGroup α)) α
Tactic: suffices IsPreprimitive (alternatingGroup α) α by
    apply IsPreprimitive.isTrivialBlock_of_isBlock hB
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h4 : 3 < Nat.card α
⊢ IsPreprimitive (↥(alternatingGroup α)) α
have inr : IsMultiplyPretransitive (↥(alternatingGroup α)) α 2
Tactic: apply isPreprimitive_of_is_two_pretransitive
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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) := ⋯
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 2
have apply : 2 ≤ Nat.card α - 2
Tactic: apply isMultiplyPretransitive_of_le (n := Nat.card α - 2) _ (sub_le _ _)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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) := ⋯
⊢ 2 ≤ Nat.card α - 2
have rwa : HAdd.hAdd (α := ℕ) 2 2 ≤ Nat.card α - 2 + 2
Tactic: rwa [← add_le_add_iff_right 2, Nat.sub_add_cancel (le_of_lt h2)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ 2 ≤ Nat.card α - 2
have rwa₁ : HAdd.hAdd (α := ℕ) 2 2 ≤ Nat.card α
Tactic: rwa [← add_le_add_iff_right 2, Nat.sub_add_cancel (le_of_lt h2)]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
⊢ HSMul.hSMul (β := Set G) g ((⇑(mk' N) : (a : G) → G ⧸ N) ⁻¹' U) = (⇑(mk' N) : (a : G) → G ⧸ N) ⁻¹' U
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
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
have 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)
Tactic: simp only [Set.mem_preimage, Set.mem_smul_set_iff_inv_smul_mem]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
⊢ 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)
have h : Eq (α := G ⧸ N) ((mk' N : (a : G) → G ⧸ N) (g⁻¹ • x) : G ⧸ N) ((mk' N : (a : G) → G ⧸ N) x : G ⧸ N)
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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)
⊢ (leftRel φ.ker : G → G → Prop) a b
have rw : a⁻¹ * b ∈ φ.ker
Tactic: rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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
⊢ (leftRel φ.ker : G → G → Prop) a b
have rw₁ : Eq.{v + 1} (α := H) ((φ : (a : G) → H) (a⁻¹ * b) : H) (1 : H)
Tactic: rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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)
⊢ (leftRel φ.ker : G → G → Prop) a b
have rw₂ : HMul.hMul (α := H) (β := H) ((φ : (a : G) → H) a⁻¹ : H) ((φ : (a : G) → H) b : H) = 1
Tactic: rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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
⊢ (leftRel φ.ker : G → G → Prop) a b
have rw₃ : HMul.hMul (α := H) (β := H) ((φ : (a : G) → H) a⁻¹ : H) ((φ : (a : G) → H) a : H) = 1
Tactic: rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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
⊢ (leftRel φ.ker : G → G → Prop) a b
have rw₄ : HMul.hMul (α := H) (β := H) (((φ : (a : G) → H) a)⁻¹ : H) ((φ : (a : G) → H) a : H) = 1
Tactic: rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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
⊢ (leftRel φ.ker : G → G → Prop) a b
have rw₅ : Eq.{v + 1} (α := H) 1 1
Tactic: rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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} (α := ↥φ.range) ((φ.rangeRestrict : (a : G) → ↥φ.range) a : ↥φ.range)
    ((φ.rangeRestrict : (a : G) → ↥φ.range) b : ↥φ.range)
⊢ (leftRel φ.ker : G → G → Prop) a b
have rw : a⁻¹ * b ∈ φ.ker
Tactic: rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
        φ.rangeRestrict.map_inv, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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} (α := ↥φ.range) ((φ.rangeRestrict : (a : G) → ↥φ.range) a : ↥φ.range)
    ((φ.rangeRestrict : (a : G) → ↥φ.range) b : ↥φ.range)
rw : a⁻¹ * b ∈ φ.ker
⊢ (leftRel φ.ker : G → G → Prop) a b
have rw₁ : a⁻¹ * b ∈ φ.rangeRestrict.ker
Tactic: rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
        φ.rangeRestrict.map_inv, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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} (α := ↥φ.range) ((φ.rangeRestrict : (a : G) → ↥φ.range) a : ↥φ.range)
    ((φ.rangeRestrict : (a : G) → ↥φ.range) b : ↥φ.range)
rw : a⁻¹ * b ∈ φ.ker
rw₁ : a⁻¹ * b ∈ φ.rangeRestrict.ker
⊢ (leftRel φ.ker : G → G → Prop) a b
have rw₂ : Eq.{v + 1} (α := ↥φ.range) ((φ.rangeRestrict : (a : G) → ↥φ.range) (a⁻¹ * b) : ↥φ.range) (1 : ↥φ.range)
Tactic: rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
        φ.rangeRestrict.map_inv, inv_mul_cancel]