mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∉ s
⊢ (ofSubtype (g.subtypePerm hg)) a = c a

Tactic:
ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha,

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∉ s
⊢ a = c a
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case nil
α : Type u_1
l : List α
⊢ (l.splitWrtCompositionAux []).length = [].length

pp: case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), (l.splitWrtCompositionAux tail✝).length = tail✝.length
l : List α
⊢ (l.splitWrtCompositionAux (head✝ :: tail✝)).length = (head✝ :: tail✝).length

Tactic:
·

Goal state after:
case nil
α : Type u_1
l : List α
⊢ (l.splitWrtCompositionAux []).length = [].length
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), (l.splitWrtCompositionAux tail✝).length = tail✝.length
l : List α
⊢ (l.splitWrtCompositionAux (head✝ :: tail✝)).length = (head✝ :: tail✝).length

Tactic:
·

Goal state after:
case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), (l.splitWrtCompositionAux tail✝).length = tail✝.length
l : List α
⊢ (l.splitWrtCompositionAux (head✝ :: tail✝)).length = (head✝ :: tail✝).length
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: α : Type u_1
ns : List ℕ
⊢ ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns

Tactic:
induction ns with
  | nil => simp [splitWrtCompositionAux]
  | cons n ns IH => grind [splitWrtCompositionAux_cons]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
hx : p x
⊢ (∀ (x_1 : p x), u ⟨x, ⋯⟩ = ⟨x, ⋯⟩) ↔ (ofSubtype u) x = x

pp: case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
hx : ¬p x
⊢ (∀ (x_1 : p x), u ⟨x, ⋯⟩ = ⟨x, ⋯⟩) ↔ (ofSubtype u) x = x

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
hx : p x
⊢ (∀ (x_1 : p x), u ⟨x, ⋯⟩ = ⟨x, ⋯⟩) ↔ (ofSubtype u) x = x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
hx : p x
⊢ (∀ (x_1 : p x), u ⟨x, ⋯⟩ = ⟨x, ⋯⟩) ↔ (ofSubtype u) x = x

Tactic:
simp only [forall_prop_of_true hx, ofSubtype_apply_of_mem u hx, ← Subtype.coe_inj]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
hx : ¬p x
⊢ (∀ (x_1 : p x), u ⟨x, ⋯⟩ = ⟨x, ⋯⟩) ↔ (ofSubtype u) x = x

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
hx : ¬p x
⊢ (∀ (x_1 : p x), u ⟨x, ⋯⟩ = ⟨x, ⋯⟩) ↔ (ofSubtype u) x = x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case cons.zero
α : Type u_1
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
    (l.splitWrtCompositionAux ns)[i] = drop (take i ns).sum (take (take (i + 1) ns).sum l)
l : List α
hi : 0 < (l.splitWrtCompositionAux (n :: ns)).length
⊢ (l.splitWrtCompositionAux (n :: ns))[0] = drop (take 0 (n :: ns)).sum (take (take (0 + 1) (n :: ns)).sum l)

pp: case cons.succ
α : Type u_1
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
    (l.splitWrtCompositionAux ns)[i] = drop (take i ns).sum (take (take (i + 1) ns).sum l)
l : List α
i : ℕ
hi : i + 1 < (l.splitWrtCompositionAux (n :: ns)).length
⊢ (l.splitWrtCompositionAux (n :: ns))[i + 1] =
    drop (take (i + 1) (n :: ns)).sum (take (take (i + 1 + 1) (n :: ns)).sum l)

Tactic:
·

Goal state after:
case cons.zero
α : Type u_1
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
    (l.splitWrtCompositionAux ns)[i] = drop (take i ns).sum (take (take (i + 1) ns).sum l)
l : List α
hi : 0 < (l.splitWrtCompositionAux (n :: ns)).length
⊢ (l.splitWrtCompositionAux (n :: ns))[0] = drop (take 0 (n :: ns)).sum (take (take (0 + 1) (n :: ns)).sum l)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case cons.succ
α : Type u_1
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
    (l.splitWrtCompositionAux ns)[i] = drop (take i ns).sum (take (take (i + 1) ns).sum l)
l : List α
i : ℕ
hi : i + 1 < (l.splitWrtCompositionAux (n :: ns)).length
⊢ (l.splitWrtCompositionAux (n :: ns))[i + 1] =
    drop (take (i + 1) (n :: ns)).sum (take (take (i + 1 + 1) (n :: ns)).sum l)

Tactic:
·

Goal state after:
case cons.succ
α : Type u_1
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
    (l.splitWrtCompositionAux ns)[i] = drop (take i ns).sum (take (take (i + 1) ns).sum l)
l : List α
i : ℕ
hi : i + 1 < (l.splitWrtCompositionAux (n :: ns)).length
⊢ (l.splitWrtCompositionAux (n :: ns))[i + 1] =
    drop (take (i + 1) (n :: ns)).sum (take (take (i + 1 + 1) (n :: ns)).sum l)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ {comm : (↑∅).Pairwise (Commute on f)}, (∀ a ∈ ∅, x ∉ (f a).support) → x ∉ (∅.noncommProd f comm).support

pp: case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support) →
        ∀ {comm : (↑(insert a s)).Pairwise (Commute on f)},
          (∀ a_3 ∈ insert a s, x ∉ (f a_3).support) → x ∉ ((insert a s).noncommProd f comm).support

Tactic:
·

Goal state after:
case empty
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ {comm : (↑∅).Pairwise (Commute on f)}, (∀ a ∈ ∅, x ∉ (f a).support) → x ∉ (∅.noncommProd f comm).support
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support) →
        ∀ {comm : (↑(insert a s)).Pairwise (Commute on f)},
          (∀ a_3 ∈ insert a s, x ∉ (f a_3).support) → x ∉ ((insert a s).noncommProd f comm).support

Tactic:
·

Goal state after:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support) →
        ∀ {comm : (↑(insert a s)).Pairwise (Commute on f)},
          (∀ a_3 ∈ insert a s, x ∉ (f a_3).support) → x ∉ ((insert a s).noncommProd f comm).support
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ take n l ++ drop n l = l

pp: case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ ns.sum = (drop n l).length

Tactic:
·

Goal state after:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ take n l ++ drop n l = l
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ ns.sum = (drop n l).length

Tactic:
·

Goal state after:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ ns.sum = (drop n l).length
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝ n : ℕ
c : CompositionAsSet n
i : Fin (n - 1)
⊢ 1 + ↑i < n.succ

Tactic:
by lia

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
⊢ (i = 0 ∨ i = Fin.last n ∨ ∃ j, ⟨↑j + 1, ⋯⟩ ∈ c.boundaries ∧ ↑i = ↑j + 1) → i ∈ c.boundaries

pp: case mpr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
⊢ i ∈ c.boundaries → i = 0 ∨ i = Fin.last n ∨ ∃ j, ⟨↑j + 1, ⋯⟩ ∈ c.boundaries ∧ ↑i = ↑j + 1

Tactic:
·

Goal state after:
case mp
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
⊢ (i = 0 ∨ i = Fin.last n ∨ ∃ j, ⟨↑j + 1, ⋯⟩ ∈ c.boundaries ∧ ↑i = ↑j + 1) → i ∈ c.boundaries
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp.inl
n✝ n : ℕ
c : CompositionAsSet n
⊢ 0 ∈ c.boundaries

pp: case mp.inr.inl
n✝ n : ℕ
c : CompositionAsSet n
⊢ Fin.last n ∈ c.boundaries

pp: case mp.inr.inr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
j : Fin (n - 1)
hj1 : ⟨↑j + 1, ⋯⟩ ∈ c.boundaries
hj2 : ↑i = ↑j + 1
⊢ i ∈ c.boundaries

Tactic:
·

Goal state after:
case mp.inl
n✝ n : ℕ
c : CompositionAsSet n
⊢ 0 ∈ c.boundaries
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp.inr.inl
n✝ n : ℕ
c : CompositionAsSet n
⊢ Fin.last n ∈ c.boundaries

pp: case mp.inr.inr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
j : Fin (n - 1)
hj1 : ⟨↑j + 1, ⋯⟩ ∈ c.boundaries
hj2 : ↑i = ↑j + 1
⊢ i ∈ c.boundaries

Tactic:
·

Goal state after:
case mp.inr.inl
n✝ n : ℕ
c : CompositionAsSet n
⊢ Fin.last n ∈ c.boundaries
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp.inr.inr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
j : Fin (n - 1)
hj1 : ⟨↑j + 1, ⋯⟩ ∈ c.boundaries
hj2 : ↑i = ↑j + 1
⊢ i ∈ c.boundaries

Tactic:
·

Goal state after:
case mp.inr.inr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
j : Fin (n - 1)
hj1 : ⟨↑j + 1, ⋯⟩ ∈ c.boundaries
hj2 : ↑i = ↑j + 1
⊢ i ∈ c.boundaries
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
⊢ i ∈ c.boundaries → i = 0 ∨ i = Fin.last n ∨ ∃ j, ⟨↑j + 1, ⋯⟩ ∈ c.boundaries ∧ ↑i = ↑j + 1

Tactic:
·

Goal state after:
case mpr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
⊢ i ∈ c.boundaries → i = 0 ∨ i = Fin.last n ∨ ∃ j, ⟨↑j + 1, ⋯⟩ ∈ c.boundaries ∧ ↑i = ↑j + 1
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ c.boundaries.min' ⋯ = 0

Tactic:
exact le_antisymm (Finset.min'_le _ _ c.zero_mem) (Fin.zero_le _)

Goal state after:
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ f.extendSubtype (σ x) = τ (f.extendSubtype x)

pp: case neg
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∉ σ.support
⊢ f.extendSubtype (σ x) = τ (f.extendSubtype x)

Tactic:
·

Goal state after:
case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ f.extendSubtype (σ x) = τ (f.extendSubtype x)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries → ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

pp: case mpr
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j) → j ∈ c.boundaries

Tactic:
·

Goal state after:
case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries → ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ ↑(f ⟨σ x, ?pos.hx✝⟩) = τ ↑(f ⟨x, ?pos.hx✝¹⟩)

pp: case pos.hx
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ x ∈ ↑σ.support

pp: case pos.hx
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ σ x ∈ ↑σ.support

Tactic:
·

Goal state after:
case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ ↑(f ⟨σ x, ?pos.hx✝⟩) = τ ↑(f ⟨x, ?pos.hx✝¹⟩)
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case neg
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∉ σ.support
⊢ f.extendSubtype (σ x) = τ (f.extendSubtype x)

Tactic:
·

Goal state after:
case neg
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∉ σ.support
⊢ f.extendSubtype (σ x) = τ (f.extendSubtype x)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j) → j ∈ c.boundaries

Tactic:
·

Goal state after:
case mpr
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j) → j ∈ c.boundaries
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ (swap x y * swap y z).support ⊆ {x, y, z}

pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ {x, y, z} ⊆ (swap x y * swap y z).support

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ (swap x y * swap y z).support ⊆ {x, y, z}
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ {x, y, z} ⊆ (swap x y * swap y z).support

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ {x, y, z} ⊆ (swap x y * swap y z).support
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : x ∈ []
⊢ [].formPerm x ∈ []

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : x ∈ y :: l
⊢ (y :: l).formPerm x ∈ y :: l

Tactic:
·

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : x ∈ []
⊢ [].formPerm x ∈ []
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mp.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inr → Sum.inl l ∈ Set.range Sum.inr

pp: case mp.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inr → Sum.inr r ∈ Set.range Sum.inr

pp: case mpr.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl

pp: case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl

Tactic:
·

Goal state after:
case mp.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inr → Sum.inl l ∈ Set.range Sum.inr
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∉ z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mp.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inr → Sum.inr r ∈ Set.range Sum.inr

pp: case mpr.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl

pp: case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl

Tactic:
·

Goal state after:
case mp.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inr → Sum.inr r ∈ Set.range Sum.inr
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝ : (z :: l).formPerm x = y
⊢ z ∈ y :: z :: l

pp: case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : (z :: l).formPerm x = z
⊢ y ∈ y :: z :: l

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : ¬(z :: l).formPerm x = z
⊢ (z :: l).formPerm x ∈ y :: z :: l

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝ : (z :: l).formPerm x = y
⊢ z ∈ y :: z :: l
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : (z :: l).formPerm x = z
⊢ y ∈ y :: z :: l

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : ¬(z :: l).formPerm x = z
⊢ (z :: l).formPerm x ∈ y :: z :: l

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : (z :: l).formPerm x = z
⊢ y ∈ y :: z :: l
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : ¬(z :: l).formPerm x = z
⊢ (z :: l).formPerm x ∈ y :: z :: l

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : ¬(z :: l).formPerm x = z
⊢ (z :: l).formPerm x ∈ y :: z :: l
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mpr.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl

pp: case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl

Tactic:
·

Goal state after:
case mpr.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl

Tactic:
·

Goal state after:
case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∉ z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∉ z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l