mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₀.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ (biprod.inl ≫
        (biprod.fst ≫ f₁₁ ≫ biprod.inl + biprod.fst ≫ f₁₂ ≫ biprod.inr + biprod.snd ≫ f₂₁ ≫ biprod.inl +
            biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
          (biprod.fst ≫ g₁₁ ≫ biprod.inl + biprod.fst ≫ g₁₂ ≫ biprod.inr + biprod.snd ≫ g₂₁ ≫ biprod.inl +
            biprod.snd ≫ g₂₂ ≫ biprod.inr)) ≫
      biprod.fst =
    (biprod.inl ≫
        (biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl + biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr +
            biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
          biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr)) ≫
      biprod.fst

Tactic:
simp only [add_comp, comp_add, add_zero, zero_add, biprod.inl_fst,
      biprod.inl_snd, biprod.inr_fst, biprod.inr_snd, biprod.inl_fst_assoc, biprod.inl_snd_assoc,
      biprod.inr_fst_assoc, biprod.inr_snd_assoc, comp_zero, zero_comp, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ (biprod.inl ≫
        (biprod.fst ≫ f₁₁ ≫ biprod.inl + biprod.fst ≫ f₁₂ ≫ biprod.inr + biprod.snd ≫ f₂₁ ≫ biprod.inl +
            biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
          (biprod.fst ≫ g₁₁ ≫ biprod.inl + biprod.fst ≫ g₁₂ ≫ biprod.inr + biprod.snd ≫ g₂₁ ≫ biprod.inl +
            biprod.snd ≫ g₂₂ ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inl ≫
        (biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl + biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr +
            biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
          biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr)) ≫
      biprod.snd

Tactic:
simp only [add_comp, comp_add, add_zero, zero_add, biprod.inl_fst,
      biprod.inl_snd, biprod.inr_fst, biprod.inr_snd, biprod.inl_fst_assoc, biprod.inl_snd_assoc,
      biprod.inr_fst_assoc, biprod.inr_snd_assoc, comp_zero, zero_comp, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₁.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ (biprod.inr ≫
        (biprod.fst ≫ f₁₁ ≫ biprod.inl + biprod.fst ≫ f₁₂ ≫ biprod.inr + biprod.snd ≫ f₂₁ ≫ biprod.inl +
            biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
          (biprod.fst ≫ g₁₁ ≫ biprod.inl + biprod.fst ≫ g₁₂ ≫ biprod.inr + biprod.snd ≫ g₂₁ ≫ biprod.inl +
            biprod.snd ≫ g₂₂ ≫ biprod.inr)) ≫
      biprod.fst =
    (biprod.inr ≫
        (biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl + biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr +
            biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
          biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr)) ≫
      biprod.fst

Tactic:
simp only [add_comp, comp_add, add_zero, zero_add, biprod.inl_fst,
      biprod.inl_snd, biprod.inr_fst, biprod.inr_snd, biprod.inl_fst_assoc, biprod.inl_snd_assoc,
      biprod.inr_fst_assoc, biprod.inr_snd_assoc, comp_zero, zero_comp, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ (biprod.inr ≫
        (biprod.fst ≫ f₁₁ ≫ biprod.inl + biprod.fst ≫ f₁₂ ≫ biprod.inr + biprod.snd ≫ f₂₁ ≫ biprod.inl +
            biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
          (biprod.fst ≫ g₁₁ ≫ biprod.inl + biprod.fst ≫ g₁₂ ≫ biprod.inr + biprod.snd ≫ g₂₁ ≫ biprod.inl +
            biprod.snd ≫ g₂₂ ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inr ≫
        (biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl + biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr +
            biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
          biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr)) ≫
      biprod.snd

Tactic:
simp only [add_comp, comp_add, add_zero, zero_add, biprod.inl_fst,
      biprod.inl_snd, biprod.inr_fst, biprod.inr_snd, biprod.inl_fst_assoc, biprod.inl_snd_assoc,
      biprod.inr_fst_assoc, biprod.inr_snd_assoc, comp_zero, zero_comp, Category.assoc]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ flatMap (fun a ↦ map (fun x ↦ Fin.cons a x) (antidiagonalTuple 0 (n - a))) (range n) ++
      map (fun x ↦ Fin.cons n x) (antidiagonalTuple 0 0) =
    [![n]]

Tactic:
conv_rhs => rw [← List.nil_append [![n]]]

Goal state after:
n : ℕ
⊢ flatMap (fun a ↦ map (fun x ↦ Fin.cons a x) (antidiagonalTuple 0 (n - a))) (range n) ++
      map (fun x ↦ Fin.cons n x) (antidiagonalTuple 0 0) =
    [] ++ [![n]]
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case e_a
n : ℕ
⊢ ∀ x < n, antidiagonalTuple 0 (n - x) = []

Tactic:
intro x

Goal state after:
case e_a
n x : ℕ
⊢ x < n → antidiagonalTuple 0 (n - x) = []
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case e_a
x m : ℕ
hx : x < x + m + 1
⊢ antidiagonalTuple 0 (x + m + 1 - x) = []

Tactic:
rw [add_assoc, add_tsub_cancel_left, antidiagonalTuple_zero_succ]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mp.refine_2
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ ∀ x ∈ s, (Finsupp.erase a f) x = f x

Tactic:
intro x

Goal state after:
case mp.refine_2
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
x : ι
⊢ x ∈ s → (Finsupp.erase a f) x = f x
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
⊢ Function.LeftInverse (fun x ↦ ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩) fun x ↦ ⟨(Sym.equivCongr e) ↑x, ⋯⟩

Tactic:
intro x

Goal state after:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
x : { x // ofSym x = μ }
⊢ (fun x ↦ ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩) ((fun x ↦ ⟨(Sym.equivCongr e) ↑x, ⋯⟩) x) = x
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
⊢ Function.RightInverse (fun x ↦ ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩) fun x ↦ ⟨(Sym.equivCongr e) ↑x, ⋯⟩

Tactic:
intro x

Goal state after:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
x : { x // ofSym x = μ }
⊢ (fun x ↦ ⟨(Sym.equivCongr e) ↑x, ⋯⟩) ((fun x ↦ ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩) x) = x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.length ≤ c.blocks.sum

Tactic:
exact length_le_sum_of_one_le _ fun i hi => c.one_le_blocks hi

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

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
⊢ False

Tactic:
have i_pos : (0 : ℕ) < i := by
    by_contra! i_pos
    revert H
    simp [nonpos_iff_eq_zero.1 i_pos, c.sizeUpTo_zero]

Goal state after:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
⊢ False
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr.hy
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ ∀ x ∈ s, Function.update (⇑g) a n1 x = g x

Tactic:
intro x

Goal state after:
case mpr.hy
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
x : ι
⊢ x ∈ s → Function.update (⇑g) a n1 x = g x
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
p : μ × μ
x✝¹ x✝ : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf✝ : f ∈ s.finsuppAntidiag p.2
g : ι →₀ μ
hg✝ : g ∈ s.finsuppAntidiag p.2
hf : s.sum ⇑f = p.2 ∧ f.support ⊆ s
hg : s.sum ⇑g = p.2 ∧ g.support ⊆ s
hfg : ∀ (x : ι), (f.update a p.1) x = (g.update a p.1) x
⊢ ∀ (x : ι), f x = g x

Tactic:
intro x

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
p : μ × μ
x✝¹ x✝ : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf✝ : f ∈ s.finsuppAntidiag p.2
g : ι →₀ μ
hg✝ : g ∈ s.finsuppAntidiag p.2
hf : s.sum ⇑f = p.2 ∧ f.support ⊆ s
hg : s.sum ⇑g = p.2 ∧ g.support ⊆ s
hfg : ∀ (x : ι), (f.update a p.1) x = (g.update a p.1) x
x : ι
⊢ f x = g x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f g : Perm α
h : f.Disjoint g
⊢ f⁻¹.Disjoint g

Tactic:
intro x

Goal state after:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ f⁻¹ x = x ∨ g x = x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ j ∈ Set.range ⇑(c.embedding i) → i = c.index j

Tactic:
← not_imp_not

Goal state after:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ ¬i = c.index j → j ∉ Set.range ⇑(c.embedding i)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ ↑(c.invEmbedding ((c.embedding i) j)) = ↑j

Tactic:
simp_rw [coe_invEmbedding, index_embedding, coe_embedding, add_tsub_cancel_left]

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

Goal state before:
pp: α : Type u_1
p : Perm α
n : ℤ
⊢ {x | (p ^ n) x ≠ x} ⊆ {x | p x ≠ x}

Tactic:
intro x

Goal state after:
α : Type u_1
p : Perm α
n : ℤ
x : α
⊢ x ∈ {x | (p ^ n) x ≠ x} → x ∈ {x | p x ≠ x}
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
⊢ ∀ x ∈ f.support ∩ g.support, (f ^ (k + 1)) x = (g ^ (k + 1)) x

Tactic:
intro x

Goal state after:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
x : α
⊢ x ∈ f.support ∩ g.support → (f ^ (k + 1)) x = (g ^ (k + 1)) x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ⊆ List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support tl)
⊢ (hd * tl.prod).support ⊆ List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (hd.support :: List.map support tl)

Tactic:
List.foldr_cons

Goal state after:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ⊆ List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support tl)
⊢ (hd * tl.prod).support ⊆ hd.support ⊔ List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support tl)
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mp
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)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)

Tactic:
intro x

Goal state after:
case mp
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
⊢ x ∈ Set.range Sum.inr → σ x ∈ Set.range Sum.inr
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
⊢ (zipWith Equiv.swap l l').prod.support ⊆ l.toFinset ⊔ l'.toFinset

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
x : α
⊢ x ∈ (zipWith Equiv.swap l l').prod.support → x ∈ l.toFinset ⊔ l'.toFinset
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mpr
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)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)

Tactic:
intro x

Goal state after:
case mpr
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
⊢ x ∈ Set.range Sum.inl → σ x ∈ Set.range Sum.inl
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
⊢ l.formPerm.support ⊆ l.toFinset

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
⊢ x ∈ l.formPerm.support → x ∈ l.toFinset
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

Tactic:
formPerm_cons_cons,

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
⊢ (Equiv.swap y z * (z :: l).formPerm) x ∈ y :: z :: l
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
h : f ∈ hd :: tl
hl : List.Pairwise Disjoint (hd :: tl)
⊢ ∀ x ∈ f.support, f x = (hd :: tl).prod x

Tactic:
intro x

Goal state after:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
h : f ∈ hd :: tl
hl : List.Pairwise Disjoint (hd :: tl)
x : α
⊢ x ∈ f.support → f x = (hd :: tl).prod x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
⊢ f.support ⊆ l.prod.support

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
x : α
⊢ x ∈ f.support → x ∈ l.prod.support
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ #(f * g).support = #f.support + #g.support

Tactic:
rw [← Finset.card_union_of_disjoint]
  · congr
    ext
    simp [h.support_mul]
  · simpa using h.disjoint_support

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ ↑l.toFinset ⊆ {x | l.formPerm x ≠ x}

Tactic:
intro x

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
x : α
⊢ x ∈ ↑l.toFinset → x ∈ {x | l.formPerm x ≠ x}
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
⊢ ∀ (x : α) (hx : x ∈ ↑(σ * τ).support),
    ↑((((setCongr hd1').trans (Set.union hd1'')).trans
            (((subtypeEquiv f ⋯).sumCongr (subtypeEquiv g ⋯)).trans ((setCongr hd2').trans (Set.union hd2'')).symm))
          ⟨(σ * τ) x, ⋯⟩) =
      (f * σ * f⁻¹ * (g * τ * g⁻¹))
        ↑((((setCongr hd1').trans (Set.union hd1'')).trans
              (((subtypeEquiv f ⋯).sumCongr (subtypeEquiv g ⋯)).trans ((setCongr hd2').trans (Set.union hd2'')).symm))
            ⟨x, hx⟩)

Tactic:
intro x

Goal state after:
case intro.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
⊢ ∀ (hx : x ∈ ↑(σ * τ).support),
    ↑((((setCongr hd1').trans (Set.union hd1'')).trans
            (((subtypeEquiv f ⋯).sumCongr (subtypeEquiv g ⋯)).trans ((setCongr hd2').trans (Set.union hd2'')).symm))
          ⟨(σ * τ) x, ⋯⟩) =
      (f * σ * f⁻¹ * (g * τ * g⁻¹))
        ↑((((setCongr hd1').trans (Set.union hd1'')).trans
              (((subtypeEquiv f ⋯).sumCongr (subtypeEquiv g ⋯)).trans ((setCongr hd2').trans (Set.union hd2'')).symm))
            ⟨x, hx⟩)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
| 1

Tactic:
← @Finset.prod_const_one _ _ (finPairsLT n)

Goal state after:
n : ℕ
| ∏ _x ∈ finPairsLT n, 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle y x ↔ f.SameCycle x y

Tactic:
sameCycle_comm

Goal state after:
α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle x y ↔ f.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
n : ℤ
⊢ f.SameCycle y x ↔ f.SameCycle x y

Tactic:
sameCycle_comm

Goal state after:
α : Type u_2
f : Perm α
x y : α
n : ℤ
⊢ f.SameCycle x y ↔ f.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
y : α
hy : σ y = y
⊢ (σ ^ m) y = (σ ^ n) y

Tactic:
zpow_apply_eq_self_of_apply_eq_self hy

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
⊢ ∀ (x : α), (ofSubtype u) x = x ∨ g x = x

Tactic:
intro x

Goal state after:
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
⊢ (ofSubtype u) x = x ∨ g x = x
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
⊢ H ⊓ K ≤ ⊥

Tactic:
intro x

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
x : Perm α
⊢ x ∈ H ⊓ K → x ∈ ⊥
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ Pairwise fun x y ↦ signAux2 l (swap x y) = -1

Tactic:
intro x

Goal state after:
case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
x : α
⊢ ∀ ⦃j : α⦄, x ≠ j → (fun x y ↦ signAux2 l (swap x y) = -1) x j
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
hx' : g x ≠ x
m : ℕ
hm : (g ^ m) x = z
⊢ ∀ x ∈ f.support ∩ g.support, f x = g x

Tactic:
intro x

Goal state after:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x✝ : α
hx : f x✝ ≠ x✝
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x✝ y
hx' : g x✝ ≠ x✝
m : ℕ
hm : (g ^ m) x✝ = z
x : α
⊢ x ∈ f.support ∩ g.support → f x = g x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support, f x = g x
hx : f x = g x
hx' : x ∈ f.support
hx'' : x ∈ g.support
this : f.support ⊆ g.support
⊢ f = g

Tactic:
exact hf.support_congr hg this h

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
H : ¬f ^ n = 1
⊢ f.support ⊆ (f ^ n).support

Tactic:
intro x

Goal state after:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
H : ¬f ^ n = 1
x : α
⊢ x ∈ f.support → x ∈ (f ^ n).support
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → f x ≠ x → β
h : ∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), g y ≠ y → ∃ x, ∃ (hx : f x ≠ x), i x hx = y
x : { x // f x ≠ x }
this : f (f ↑x) ≠ f ↑x
⊢ g (i ↑x ⋯) ≠ i ↑x ⋯

Tactic:
← h _ x.2 this

Goal state after:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → f x ≠ x → β
h : ∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), g y ≠ y → ∃ x, ∃ (hx : f x ≠ x), i x hx = y
x : { x // f x ≠ x }
this : f (f ↑x) ≠ f ↑x
⊢ i (f ↑x) this ≠ i ↑x ⋯
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → f x ≠ x → β
h : ∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), g y ≠ y → ∃ x, ∃ (hx : f x ≠ x), i x hx = y
x : { x // f x ≠ x }
this : f (f ↑x) ≠ f ↑x
⊢ i (f ↑x) this ≠ i ↑x ⋯

Tactic:
exact mt (hi _ _ this x.2) x.2

Goal state after: