awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBsc : B ⊆ sᶜ), B.Subsingleton
⊢ sᶜ ⊆ B
have hB_not_le_s : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBs : B ⊆ s), B.Subsingleton
Tactic: have hB_not_le_s (B : Set α) (hB : IsBlock G B) (hBs : B ⊆ s) : B.Subsingleton :=
    have := isPreprimitive_stabilizer_subgroup hG.le
    hB.subsingleton_of_stabilizer_lt_of_subset hB_not_le_sc hG hBs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBsc : B ⊆ sᶜ), B.Subsingleton
hB_not_le_s : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBs : B ⊆ s), B.Subsingleton
⊢ sᶜ ⊆ B
have x : IsMultiplyPretransitive (Perm α) α (s.ncard + 1)
Tactic: have _ := isMultiplyPretransitive α (s.ncard + 1)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBsc : B ⊆ sᶜ), B.Subsingleton
hB_not_le_s : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBs : B ⊆ s), B.Subsingleton
h : IsMultiplyPretransitive (Perm α) α (s.ncard + 1)
⊢ sᶜ ⊆ B
have isTrivialBlock_of_isBlock : ¬B ⊆ s
Tactic: apply MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl hG.le
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBsc : B ⊆ sᶜ), B.Subsingleton
hB_not_le_s : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBs : B ⊆ s), B.Subsingleton
h : IsMultiplyPretransitive (Perm α) α (s.ncard + 1)
isTrivialBlock_of_isBlock : ¬B ⊆ s
⊢ sᶜ ⊆ B
have isTrivialBlock_of_isBlock₁ : ¬B ⊆ sᶜ
Tactic: apply MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl hG.le
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
have have : ∀ (h1 : sᶜ.Nonempty), IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
Tactic: classical
  have h1 : sᶜ.Nonempty := nonempty_iff_ne_empty.mpr (by aesop)
  have : Fintype α := Fintype.ofFinite α
  -- To prove that `stabilizer (Perm α) s` is maximal,
  -- we need to prove that it is `≠ ⊤`
  refine ⟨stabilizer_ne_top_of_nonempty_of_nonempty_compl h0 h1, fun G hG ↦ ?_⟩
  have hG' : stabilizer (Perm α) sᶜ < G := by rwa [stabilizer_compl]
  -- … and that every strict over-subgroup `G` is equal to `⊤`
  -- We know that `G` contains a swap
  obtain ⟨g, hg_swap, hg⟩ := has_swap_mem_of_lt_stabilizer s G hG
  -- By Jordan's theorem `subgroup_eq_top_of_isPreprimitive_of_isSwap_mem`,
  -- it suffices to prove that `G` acts primitively
  apply subgroup_eq_top_of_isPreprimitive_of_isSwap_mem _ g hg_swap hg
  -- First, we prove that `G` acts transitively
  have := G.isPretransitive_of_stabilizer_lt hG exists_mem_stabilizer_smul_eq
  apply IsPreprimitive.mk
  -- We now have to prove that all blocks of `G` are trivial
  -- We reduce to proving that a block which is not a subsingleton is `univ`.
  intro B hB
  unfold IsTrivialBlock
  rw [or_iff_not_imp_left]
  intro hB'
  suffices sᶜ ⊆ B by
    apply hB.eq_univ_of_card_lt
    have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
    rw [← Set.ncard_add_ncard_compl s]
    lia
  -- The proof needs 4 steps
  /- Step 1 : `sᶜ` is not a block.
       This uses that `Nat.card s < Nat.card sᶜ`.
       In the equality case, `Nat.card s` = Nat.card sᶜ`,
       it would be possible that `sᶜ` is a block,
       and then `G` would be a wreath product,
       — this is case (b) of the O'Nan-Scott classification
       of maximal subgroups of the symmetric group -/
  have not_isBlock_sc : ¬ IsBlock G sᶜ := fun hsc ↦ by
    rcases lt_or_ge (Nat.card α) (sᶜ.ncard * 2) with hB' | hB'
    · apply h0.ne_empty
      rw [← compl_univ_iff]
      exact hsc.eq_univ_of_card_lt hB'
    · rw [← not_lt] at hB'
      apply hB'
      rwa [← Set.ncard_add_ncard_compl sᶜ, mul_two, add_lt_add_iff_left, compl_compl]
  -- Step 2 : A block contained in sᶜ is a subsingleton
  have hB_not_le_sc (B : Set α) (hB : IsBlock G B) (hBsc : B ⊆ sᶜ) :
      B.Subsingleton :=
    -- uses Step 1
    hB.subsingleton_of_ssubset_of_stabilizer_Perm_le (hBsc.ssubset_of_ne (by lia)) hG'.le
  -- Step 3 : A block contained in `s` is a subsingleton
  have hB_not_le_s (B : Set α) (hB : IsBlock G B) (hBs : B ⊆ s) : B.Subsingleton :=
    have := isPreprimitive_stabilizer_subgroup hG.le
    hB.subsingleton_of_stabilizer_lt_of_subset hB_not_le_sc hG hBs
  -- Step 4 : `sᶜ ⊆ B`
  have _ := isMultiplyPretransitive α (s.ncard + 1)
  apply MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl hG.le <;>
    grind
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
have have₁ have₂ : ∀ (h1 : sᶜ.Nonempty), IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
have have₃ : ∀ (h1 : sᶜ.Nonempty) (this : Fintype α), IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
Tactic: classical
  have h1 : sᶜ.Nonempty := nonempty_iff_ne_empty.mpr (by aesop)
  have : Fintype α := Fintype.ofFinite α
  -- To prove that `stabilizer (Perm α) s` is maximal,
  -- we need to prove that it is `≠ ⊤`
  refine ⟨stabilizer_ne_top_of_nonempty_of_nonempty_compl h0 h1, fun G hG ↦ ?_⟩
  have hG' : stabilizer (Perm α) sᶜ < G := by rwa [stabilizer_compl]
  -- … and that every strict over-subgroup `G` is equal to `⊤`
  -- We know that `G` contains a swap
  obtain ⟨g, hg_swap, hg⟩ := has_swap_mem_of_lt_stabilizer s G hG
  -- By Jordan's theorem `subgroup_eq_top_of_isPreprimitive_of_isSwap_mem`,
  -- it suffices to prove that `G` acts primitively
  apply subgroup_eq_top_of_isPreprimitive_of_isSwap_mem _ g hg_swap hg
  -- First, we prove that `G` acts transitively
  have := G.isPretransitive_of_stabilizer_lt hG exists_mem_stabilizer_smul_eq
  apply IsPreprimitive.mk
  -- We now have to prove that all blocks of `G` are trivial
  -- We reduce to proving that a block which is not a subsingleton is `univ`.
  intro B hB
  unfold IsTrivialBlock
  rw [or_iff_not_imp_left]
  intro hB'
  suffices sᶜ ⊆ B by
    apply hB.eq_univ_of_card_lt
    have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
    rw [← Set.ncard_add_ncard_compl s]
    lia
  -- The proof needs 4 steps
  /- Step 1 : `sᶜ` is not a block.
       This uses that `Nat.card s < Nat.card sᶜ`.
       In the equality case, `Nat.card s` = Nat.card sᶜ`,
       it would be possible that `sᶜ` is a block,
       and then `G` would be a wreath product,
       — this is case (b) of the O'Nan-Scott classification
       of maximal subgroups of the symmetric group -/
  have not_isBlock_sc : ¬ IsBlock G sᶜ := fun hsc ↦ by
    rcases lt_or_ge (Nat.card α) (sᶜ.ncard * 2) with hB' | hB'
    · apply h0.ne_empty
      rw [← compl_univ_iff]
      exact hsc.eq_univ_of_card_lt hB'
    · rw [← not_lt] at hB'
      apply hB'
      rwa [← Set.ncard_add_ncard_compl sᶜ, mul_two, add_lt_add_iff_left, compl_compl]
  -- Step 2 : A block contained in sᶜ is a subsingleton
  have hB_not_le_sc (B : Set α) (hB : IsBlock G B) (hBsc : B ⊆ sᶜ) :
      B.Subsingleton :=
    -- uses Step 1
    hB.subsingleton_of_ssubset_of_stabilizer_Perm_le (hBsc.ssubset_of_ne (by lia)) hG'.le
  -- Step 3 : A block contained in `s` is a subsingleton
  have hB_not_le_s (B : Set α) (hB : IsBlock G B) (hBs : B ⊆ s) : B.Subsingleton :=
    have := isPreprimitive_stabilizer_subgroup hG.le
    hB.subsingleton_of_stabilizer_lt_of_subset hB_not_le_sc hG hBs
  -- Step 4 : `sᶜ ⊆ B`
  have _ := isMultiplyPretransitive α (s.ncard + 1)
  apply MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl hG.le <;>
    grind
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
have inl : ∀ (h : s.ncard < sᶜ.ncard), IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
Tactic: obtain h | h | h := Nat.lt_trichotomy s.ncard sᶜ.ncard
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
inl : ∀ (h : s.ncard < sᶜ.ncard), IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
have inr : ∀ (h : s.ncard = sᶜ.ncard), IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
Tactic: obtain h | h | h := Nat.lt_trichotomy s.ncard sᶜ.ncard
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
inl : ∀ (h : s.ncard < sᶜ.ncard), IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
inr : ∀ (h : s.ncard = sᶜ.ncard), IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
have inr₁ : ∀ (h : sᶜ.ncard < s.ncard), IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
Tactic: obtain h | h | h := Nat.lt_trichotomy s.ncard sᶜ.ncard
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
h : s.ncard = sᶜ.ncard
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
have inr : ∀ (hα : ¬IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)), Nat.card α = 2 * s.ncard
Tactic: contrapose hα
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
h : s.ncard = sᶜ.ncard
hα : ¬IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
⊢ Nat.card α = 2 * s.ncard
have inr : s.ncard + sᶜ.ncard = 2 * s.ncard
Tactic: rw [← Set.ncard_add_ncard_compl s, two_mul, ← h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
h : s.ncard = sᶜ.ncard
hα : ¬IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
inr : s.ncard + sᶜ.ncard = 2 * s.ncard
⊢ Nat.card α = 2 * s.ncard
have inr₁ : s.ncard + sᶜ.ncard = s.ncard + s.ncard
Tactic: rw [← Set.ncard_add_ncard_compl s, two_mul, ← h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
h : s.ncard = sᶜ.ncard
hα : ¬IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
inr : s.ncard + sᶜ.ncard = 2 * s.ncard
inr₁ : s.ncard + sᶜ.ncard = s.ncard + s.ncard
⊢ Nat.card α = 2 * s.ncard
have inr₂ : s.ncard + s.ncard = s.ncard + s.ncard
Tactic: rw [← Set.ncard_add_ncard_compl s, two_mul, ← h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
h : sᶜ.ncard < s.ncard
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
have inr : IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) sᶜ)
Tactic: rw [← stabilizer_compl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
h : sᶜ.ncard < s.ncard
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) sᶜ)
have inr : sᶜ.ncard < sᶜᶜ.ncard
Tactic: apply isCoatom_stabilizer_of_ncard_lt_ncard_compl hsc_nonempty
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
⊢ optionCongr (swap x y) = swap (some x) (some y)
have H : ∀ (a : α),
  (optionCongr (swap x y) : (a : Option α) → Option α) none = some a ↔
    (swap (some x) (some y) : (a : Option α) → Option α) none = some a
Tactic: ext (_ | i)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
H :
  ∀ (a : α),
    (optionCongr (swap x y) : (a : Option α) → Option α) none = some a ↔
      (swap (some x) (some y) : (a : Option α) → Option α) none = some a
⊢ optionCongr (swap x y) = swap (some x) (some y)
have H₁ : ∀ (i a : α),
  (optionCongr (swap x y) : (a : Option α) → Option α) (some i) = some a ↔
    (swap (some x) (some y) : (a : Option α) → Option α) (some i) = some a
Tactic: ext (_ | i)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y i a : α
⊢ (optionCongr (swap x y) : (a : Option α) → Option α) (some i) = some a ↔
    (swap (some x) (some y) : (a : Option α) → Option α) (some i) = some a
have pos : ∀ (hx : i = x),
  (optionCongr (swap x y) : (a : Option α) → Option α) (some i) = some a ↔
    (swap (some x) (some y) : (a : Option α) → Option α) (some i) = some a
Tactic: by_cases hx : i = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y i a : α
pos :
  ∀ (hx : i = x),
    (optionCongr (swap x y) : (a : Option α) → Option α) (some i) = some a ↔
      (swap (some x) (some y) : (a : Option α) → Option α) (some i) = some a
⊢ (optionCongr (swap x y) : (a : Option α) → Option α) (some i) = some a ↔
    (swap (some x) (some y) : (a : Option α) → Option α) (some i) = some a
have neg : ∀ (hx : ¬i = x),
  (optionCongr (swap x y) : (a : Option α) → Option α) (some i) = some a ↔
    (swap (some x) (some y) : (a : Option α) → Option α) (some i) = some a
Tactic: by_cases hx : i = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y i a : α
hx : ¬i = x
⊢ (optionCongr (swap x y) : (a : Option α) → Option α) (some i) = some a ↔
    (swap (some x) (some y) : (a : Option α) → Option α) (some i) = some a
have pos : ∀ (hy : i = y),
  (optionCongr (swap x y) : (a : Option α) → Option α) (some i) = some a ↔
    (swap (some x) (some y) : (a : Option α) → Option α) (some i) = some a
Tactic: by_cases hy : i = y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y i a : α
hx : ¬i = x
pos :
  ∀ (hy : i = y),
    (optionCongr (swap x y) : (a : Option α) → Option α) (some i) = some a ↔
      (swap (some x) (some y) : (a : Option α) → Option α) (some i) = some a
⊢ (optionCongr (swap x y) : (a : Option α) → Option α) (some i) = some a ↔
    (swap (some x) (some y) : (a : Option α) → Option α) (some i) = some a
have neg : ∀ (hy : ¬i = y),
  (optionCongr (swap x y) : (a : Option α) → Option α) (some i) = some a ↔
    (swap (some x) (some y) : (a : Option α) → Option α) (some i) = some a
Tactic: by_cases hy : i = y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
e : Perm α
⊢ Eq (α := ℤˣ) (((Perm.sign : Perm (Option α) →* ℤˣ) : (a : Perm (Option α)) → ℤˣ) (optionCongr e) : ℤˣ)
    (((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) e : ℤˣ)
have one : Eq (α := ℤˣ) (((Perm.sign : Perm (Option α) →* ℤˣ) : (a : Perm (Option α)) → ℤˣ) (optionCongr 1) : ℤˣ)
  (((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1 : ℤˣ)
Tactic: induction e using Perm.swap_induction_on with
  | one => simp [Perm.one_def]
  | swap_mul f x y hne h =>
    simp [h, hne, Perm.mul_def]
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
e : Perm α
one :
  Eq (α := ℤˣ) (((Perm.sign : Perm (Option α) →* ℤˣ) : (a : Perm (Option α)) → ℤˣ) (optionCongr 1) : ℤˣ)
    (((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1 : ℤˣ)
⊢ Eq (α := ℤˣ) (((Perm.sign : Perm (Option α) →* ℤˣ) : (a : Perm (Option α)) → ℤˣ) (optionCongr e) : ℤˣ)
    (((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) e : ℤˣ)
have swap_mul : ∀ (f : Perm α) (x y : α) (hne : x ≠ y)
  (h :
    Eq (α := ℤˣ) (((Perm.sign : Perm (Option α) →* ℤˣ) : (a : Perm (Option α)) → ℤˣ) (optionCongr f) : ℤˣ)
      (((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)),
  Eq (α := ℤˣ) (((Perm.sign : Perm (Option α) →* ℤˣ) : (a : Perm (Option α)) → ℤˣ) (optionCongr (swap x y * f)) : ℤˣ)
    (((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap x y * f) : ℤˣ)
Tactic: induction e using Perm.swap_induction_on with
  | one => simp [Perm.one_def]
  | swap_mul f x y hne h =>
    simp [h, hne, Perm.mul_def]
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
⊢ (removeNone σ).optionCongr = swap none ((σ : (a : Option α) → Option α) none) * σ
have H : ∀ (x : Option α),
  Eq (α := Option α) (((removeNone σ).optionCongr : (a : Option α) → Option α) x : Option α)
    ((swap none ((σ : (a : Option α) → Option α) none) * σ : (a : Option α) → Option α) x : Option α)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
x : Option α
⊢ Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) x)
    ((swap none ((σ : (a : Option α) → Option α) none) : (a : Option α) → Option α)
      ((σ : (a : Option α) → Option α) x : Option α))
have none : Eq (α := Option α) (Option.map (α := α) (⇑(removeNone σ) : (a : α) → α) none)
  ((swap none ((σ : (a : Option α) → Option α) none) : (a : Option α) → Option α)
    ((σ : (a : Option α) → Option α) none : Option α))
Tactic: obtain - | x := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
x : Option α
none :
  Eq (α := Option α) (Option.map (α := α) (⇑(removeNone σ) : (a : α) → α) Option.none)
    ((swap Option.none ((σ : (a : Option α) → Option α) Option.none) : (a : Option α) → Option α)
      ((σ : (a : Option α) → Option α) Option.none : Option α))
⊢ Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) x)
    ((swap Option.none ((σ : (a : Option α) → Option α) Option.none) : (a : Option α) → Option α)
      ((σ : (a : Option α) → Option α) x : Option α))
have some : ∀ (x : α),
  Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) (some x))
    ((swap Option.none ((σ : (a : Option α) → Option α) Option.none) : (a : Option α) → Option α)
      ((σ : (a : Option α) → Option α) (some x) : Option α))
Tactic: obtain - | x := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
x : α
⊢ Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) (some x))
    ((swap none ((σ : (a : Option α) → Option α) none) : (a : Option α) → Option α)
      ((σ : (a : Option α) → Option α) (some x) : Option α))
have some : ∀ (h : Eq (α := Option α) ((σ : (a : Option α) → Option α) (some x) : Option α) (none : Option α)),
  Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) (some x))
    ((swap none ((σ : (a : Option α) → Option α) none) : (a : Option α) → Option α) none)
Tactic: cases h : σ (some _)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
x : α
some :
  ∀ (h : Eq (α := Option α) ((σ : (a : Option α) → Option α) (Option.some x) : Option α) (none : Option α)),
    Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) (Option.some x))
      ((swap none ((σ : (a : Option α) → Option α) none) : (a : Option α) → Option α) none)
⊢ Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) (Option.some x))
    ((swap none ((σ : (a : Option α) → Option α) none) : (a : Option α) → Option α)
      ((σ : (a : Option α) → Option α) (Option.some x) : Option α))
have some₁ : ∀ (val : α) (h : (σ : (a : Option α) → Option α) (Option.some x) = Option.some val),
  Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) (Option.some x))
    ((swap none ((σ : (a : Option α) → Option α) none) : (a : Option α) → Option α) (Option.some val))
Tactic: cases h : σ (some _)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
x val : α
h : (σ : (a : Option α) → Option α) (some x) = some val
⊢ Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) (some x))
    ((swap none ((σ : (a : Option α) → Option α) none) : (a : Option α) → Option α) (some val))
have hn : Ne (α := Option α) ((σ : (a : Option α) → Option α) (some x) : Option α) (none : Option α)
Tactic: have hn : σ (some x) ≠ none := by simp [h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
x val : α
h : (σ : (a : Option α) → Option α) (some x) = some val
hn : Ne (α := Option α) ((σ : (a : Option α) → Option α) (some x) : Option α) (none : Option α)
⊢ Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) (some x))
    ((swap none ((σ : (a : Option α) → Option α) none) : (a : Option α) → Option α) (some val))
have hσn : Ne (α := Option α) ((σ : (a : Option α) → Option α) (some x) : Option α)
  ((σ : (a : Option α) → Option α) none : Option α)
Tactic: have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
x : Option α
⊢ Eq (α := Option α) (((removeNone σ).optionCongr : (a : Option α) → Option α) x : Option α)
    ((swap none ((σ : (a : Option α) → Option α) none) * σ : (a : Option α) → Option α) x : Option α)
have this : Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) x)
  ((swap none ((σ : (a : Option α) → Option α) none) : (a : Option α) → Option α)
    ((σ : (a : Option α) → Option α) x : Option α))
Tactic: have : Option.map (⇑(removeNone σ)) x = (swap none (σ none)) (σ x) := by
    obtain - | x := x
    · simp
    · cases h : σ (some _)
      · simp [removeNone_none _ h]
      · have hn : σ (some x) ≠ none := by simp [h]
        have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)
        simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Option (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
x_1 : Option α × Perm α
x : Option α
σ : Perm α
⊢ (fun (σ : Perm (Option α)) ↦ (((σ : (a : Option α) → Option α) none, removeNone σ) : Option α × Perm α))
      ((fun (i : Option α × Perm α) ↦ swap none i.1 * optionCongr i.2) (x, σ)) =
    (x, σ)
have this : removeNone (swap none x * optionCongr σ) = σ
Tactic: have : removeNone (swap none x * σ.optionCongr) = σ :=
      Equiv.optionCongr_injective (by simp [← mul_assoc])