awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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'_1 : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : ¬Nat.card α < sᶜ.ncard * 2
inr : sᶜ.ncard + sᶜᶜ.ncard < sᶜ.ncard * 2
inr₁ : sᶜ.ncard + sᶜᶜ.ncard < sᶜ.ncard + sᶜ.ncard
inr₂ : sᶜᶜ.ncard < sᶜ.ncard
inr₃ inr₄ inr₅ inr₆ : s.ncard < sᶜ.ncard
⊢ Nat.card α < sᶜ.ncard * 2

Tactic:
rwa [← Set.ncard_add_ncard_compl sᶜ, mul_two, add_lt_add_iff_left, compl_compl]

Premises used: compl_compl, Compl.compl, Set.ncard_add_ncard_compl, mul_two, add_lt_add_iff_left
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
⊢ ¬IsBlock (↥G) sᶜ

Tactic:
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]
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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_1 : Set α
hB_1 : IsBlock (↥G) B_1
hB' : ¬B_1.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ B ≠ sᶜ

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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ᶜ
⊢ ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBsc : B ⊆ sᶜ), B.Subsingleton

Tactic:
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
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
⊢ ∀ (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
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
⊢ IsMultiplyPretransitive (Perm α) α (s.ncard + 1)

Tactic:
have _ := isMultiplyPretransitive α (s.ncard + 1)
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
isTrivialBlock_of_isBlock₁ : ¬B ⊆ sᶜ
isTrivialBlock_of_isBlock₂ : IsBlock (↥G) B
⊢ sᶜ ⊆ B

Tactic:
apply MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl hG.le

Premises used: MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl, LT.lt.le
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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)
⊢ ¬B ⊆ s

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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)
⊢ ¬B ⊆ sᶜ

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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)
⊢ IsBlock (↥G) B

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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)
inr₁ : ∀ (h : sᶜ.ncard < s.ncard), IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)

Tactic:
obtain h | h | h := Nat.lt_trichotomy s.ncard sᶜ.ncard

Premises used: Nat.lt_trichotomy, Compl.compl, Set.ncard
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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)

Tactic:
isCoatom_stabilizer_of_ncard_lt_ncard_compl hs_nonempty h

Premises used: Equiv.Perm.isCoatom_stabilizer_of_ncard_lt_ncard_compl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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)

Tactic:
exact isCoatom_stabilizer_of_ncard_lt_ncard_compl hs_nonempty h

Premises used: Equiv.Perm.isCoatom_stabilizer_of_ncard_lt_ncard_compl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
inr : ∀ (hα : ¬IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)), Nat.card α = 2 * s.ncard
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)

Tactic:
contrapose hα
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
inr₂ inr₃ : s.ncard + s.ncard = s.ncard + s.ncard
⊢ Nat.card α = 2 * s.ncard

Tactic:
rw [← Set.ncard_add_ncard_compl s, two_mul, ← h]

Premises used: two_mul, Set.ncard_add_ncard_compl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
inr : IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) sᶜ)
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)

Tactic:
rw [← stabilizer_compl]

Premises used: stabilizer_compl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
inr : sᶜ.ncard < sᶜᶜ.ncard
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) sᶜ)

Tactic:
apply isCoatom_stabilizer_of_ncard_lt_ncard_compl hsc_nonempty

Premises used: Equiv.Perm.isCoatom_stabilizer_of_ncard_lt_ncard_compl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
h inr inr₁ inr₂ inr₃ : sᶜ.ncard < s.ncard
⊢ sᶜ.ncard < sᶜᶜ.ncard

Tactic:
rwa [compl_compl]

Premises used: compl_compl
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Option α ≃ Option α) (optionCongr 1) 1

Tactic:
Equiv.optionCongr_refl

Premises used: Equiv.optionCongr_refl
-- Module: Mathlib.GroupTheory.Perm.Option
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
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
⊢ optionCongr (swap x y) = swap (some x) (some y)

Tactic:
ext (_ | i)
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
x y a : α
⊢ (optionCongr (swap x y) : (a : Option α) → Option α) none = some a ↔
    (swap (some x) (some y) : (a : Option α) → Option α) none = some a

Tactic:
simp [swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.GroupTheory.Perm.Option
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
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
⊢ (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
-- Module: Mathlib.GroupTheory.Perm.Option
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

Tactic:
simp only [hx, optionCongr_apply, Option.map_some, swap_apply_left,
             Option.some.injEq]

Premises used: Option.some.injEq, Equiv.optionCongr_apply, Option.map_some, Equiv.swap_apply_left
-- Module: Mathlib.GroupTheory.Perm.Option
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
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
⊢ (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
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
x y i a : α
hx : ¬i = x
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:
simp [hx, hy, swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
x y i a : α
hx : ¬i = x
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:
simp [hx, hy, swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Eq (α := ℤˣ) (((Perm.sign : Perm (Option α) →* ℤˣ) : (a : Perm (Option α)) → ℤˣ) (optionCongr 1) : ℤˣ)
    (((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1 : ℤˣ)

Tactic:
simp [Perm.one_def]

Premises used: Equiv.Perm.one_def
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
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:
simp [h, hne, Perm.mul_def]

Premises used: Equiv.Perm.mul_def
-- Module: Mathlib.GroupTheory.Perm.Option
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 : ℤˣ)
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) : ℤˣ)
⊢ Eq (α := ℤˣ) (((Perm.sign : Perm (Option α) →* ℤˣ) : (a : Perm (Option α)) → ℤˣ) (optionCongr e) : ℤˣ)
    (((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) e : ℤˣ)

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]

Premises used: Equiv.Perm.one_def, Equiv.Perm.mul_def
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
H :
  ∀ (x : Option α),
    Eq (α := Option α) (((removeNone σ).optionCongr : (a : Option α) → Option α) x : Option α)
      ((swap none ((σ : (a : Option α) → Option α) none) * σ : (a : Option α) → Option α) x : Option α)
⊢ (removeNone σ).optionCongr = swap none ((σ : (a : Option α) → Option α) none) * σ

Tactic:
ext1 x
-- Module: Mathlib.GroupTheory.Perm.Option
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 α))
some :
  ∀ (x : α),
    Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) (Option.some x))
      ((swap Option.none ((σ : (a : Option α) → Option α) Option.none) : (a : Option α) → Option α)
        ((σ : (a : Option α) → Option α) (Option.some x) : Option α))
⊢ Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) x)
    ((swap Option.none ((σ : (a : Option α) → Option α) Option.none) : (a : Option α) → Option α)
      ((σ : (a : Option α) → Option α) x : Option α))

Tactic:
obtain - | x := x
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
⊢ Eq (α := Option α) (Option.map (α := α) (⇑(removeNone σ) : (a : α) → α) none)
    ((swap none ((σ : (a : Option α) → Option α) none) : (a : Option α) → Option α)
      ((σ : (a : Option α) → Option α) none : Option α))

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Option
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)
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))
⊢ 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 α))

Tactic:
cases h : σ (some _)

Premises used: Option.some, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
x : α
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:
simp [removeNone_none _ h]

Premises used: Equiv.removeNone_none
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
x val : α
h : (σ : (a : Option α) → Option α) (some x) = some val
⊢ Ne (α := Option α) ((σ : (a : Option α) → Option α) (some x) : Option α) (none : Option α)

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
x val : α
h : (σ : (a : Option α) → Option α) (some x) = some val
⊢ Ne (α := Option α) ((σ : (a : Option α) → Option α) (some x) : Option α) (none : Option α)

Tactic:
have hn : σ (some x) ≠ none := by simp [h]
-- Module: Mathlib.GroupTheory.Perm.Option
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 α)
⊢ some x ≠ none

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Option
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 α)
⊢ Ne (α := Option α) ((σ : (a : Option α) → Option α) (some x) : Option α)
    ((σ : (a : Option α) → Option α) none : Option α)

Tactic:
have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)
-- Module: Mathlib.GroupTheory.Perm.Option
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 α)
hσn :
  Ne (α := Option α) ((σ : (a : Option α) → Option α) (some x) : Option α)
    ((σ : (a : Option α) → Option α) none : Option α)
⊢ Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) (some x))
    ((swap none ((σ : (a : Option α) → Option α) none) : (a : Option α) → Option α) (some val))

Tactic:
simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]

Premises used: Equiv.swap_apply_of_ne_of_ne, Exists.intro, Equiv.removeNone_some
-- Module: Mathlib.GroupTheory.Perm.Option
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 α))

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]
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
x : Option α
this :
  Eq (α := Option α) (Option.map (⇑(removeNone σ) : (a : α) → α) x)
    ((swap none ((σ : (a : Option α) → Option α) none) : (a : Option α) → Option α)
      ((σ : (a : Option α) → Option α) x : Option α))
⊢ Eq (α := Option α) (((removeNone σ).optionCongr : (a : Option α) → Option α) x : Option α)
    ((swap none ((σ : (a : Option α) → Option α) none) * σ : (a : Option α) → Option α) x : Option α)

Tactic:
simpa using this
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
σ : Perm (Option α)
⊢ (fun (i : Option α × Perm α) ↦ swap none i.1 * optionCongr i.2)
      ((fun (σ : Perm (Option α)) ↦ (((σ : (a : Option α) → Option α) none, removeNone σ) : Option α × Perm α)) σ) =
    σ

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
x_1 : Option α × Perm α
x : Option α
σ : Perm α
⊢ (removeNone (swap none x * optionCongr σ)).optionCongr = optionCongr σ

Tactic:
simp [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
x_1 : Option α × Perm α
x : Option α
σ : Perm α
⊢ removeNone (swap none x * optionCongr σ) = σ

Tactic:
have : removeNone (swap none x * σ.optionCongr) = σ :=
      Equiv.optionCongr_injective (by simp [← mul_assoc])
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
x_1 : Option α × Perm α
x : Option α
σ : Perm α
this : removeNone (swap none x * optionCongr σ) = σ
⊢ (fun (σ : Perm (Option α)) ↦ (((σ : (a : Option α) → Option α) none, removeNone σ) : Option α × Perm α))
      ((fun (i : Option α × Perm α) ↦ swap none i.1 * optionCongr i.2) (x, σ)) =
    (x, σ)

Tactic:
simp [this]
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
e : Perm α
i : Option α
⊢ Eq (α := Option α)
    ((((Equiv.symm decomposeOption : (a : Option α × Perm α) → Perm (Option α)) (none, e) : Perm (Option α)) :
          (a : Option α) → Option α)
        i :
      Option α)
    (Option.map (⇑e : (a : α) → α) i : Option α)

Tactic:
simp