mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ Y✝ : C ⥤ D
e : X✝ ≅ Y✝
h : rightExactFunctor C D X✝
⊢ rightExactFunctor C D Y✝

Tactic:
simp only [rightExactFunctor_iff] at h ⊢
    exact preservesFiniteColimits_of_natIso e

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
inst✝ : Mono f
this : Mono (Fork.ι c)
⊢ 0 = 0 ≫ 0

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
inst✝ : Mono f
this : Mono (Fork.ι c)
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ : HasZeroObject C
inst✝ : Mono f
s : Fork f 0
⊢ 0 ≫ Fork.ι (zeroKernelFork f) = s.ι

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ : HasZeroObject C
inst✝ : Mono f
s : Fork f 0
⊢ 0 = s.ι
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0
s : Fork f 0
⊢ 0 ≫ Fork.ι (KernelFork.ofι 0 ⋯) = 0

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0
s : Fork f 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : CokernelCofork f
⊢ 0 ≫ Cofork.π s = 0

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : CokernelCofork f
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
π : Y ⟶ Z
w : f ≫ π = 0
⊢ 0 = 0 ≫ π

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
π : Y ⟶ Z
w : f ≫ π = 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m✝ : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π (CokernelCofork.ofπ (Cofork.π c) ⋯) ≫ m✝ = s.π
⊢ m✝ = ↑l

Tactic:
apply Cofork.IsColimit.hom_ext i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
s' : CokernelCofork f := ⋯
l : { l // Cofork.π c ≫ l = Cofork.π s' } := ⋯
m✝ : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π (CokernelCofork.ofπ (Cofork.π c) ⋯) ≫ m✝ = s.π
⊢ Cofork.π c ≫ m✝ = Cofork.π c ≫ ↑l
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
W : C
g : W ⟶ X
h✝ : W ⟶ Y
c : CokernelCofork h✝
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h✝
s : Cofork f 0
m : (CokernelCofork.ofπ (Cofork.π c) hf).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π c) hf) ≫ m = s.π
⊢ m = i.desc (CokernelCofork.ofπ s.π ⋯)

Tactic:
apply Cofork.IsColimit.hom_ext i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
W : C
g : W ⟶ X
h✝ : W ⟶ Y
c : CokernelCofork h✝
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h✝
s : Cofork f 0
m : (CokernelCofork.ofπ (Cofork.π c) hf).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π c) hf) ≫ m = s.π
⊢ Cofork.π c ≫ m = Cofork.π c ≫ i.desc (CokernelCofork.ofπ s.π ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
hf : f = 0
⊢ 0 ≫ 𝟙 Y = 0

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
hf : f = 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ 0 ≫ 𝟙 c.pt = 0

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j j' : J
w : j = j'
⊢ π f j ≫ eqToHom ⋯ = π f j'

Tactic:
simp [*]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ (w j).inv ≫ 0 = ι f j ≫ π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯

pp: case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ e j ≠ k

Tactic:
biproduct.ι_π_ne_assoc

Goal state after:
case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ (w j).inv ≫ 0 = 0 ≫ (w (e.symm k)).inv ≫ eqToHom ⋯

case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ j ≠ e.symm k

case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ e j ≠ k
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ 0 = ι g k ≫ π g (e j) ≫ (w j).hom

pp: case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ e.symm k ≠ j

Tactic:
biproduct.ι_π_ne_assoc

Goal state after:
case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ 0 = 0 ≫ (w j).hom

case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ k ≠ e j

case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ e.symm k ≠ j
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : ¬p j
⊢ 0 = 0 ≫ π (Subtype.restrict p f) i

Tactic:
zero_comp

Goal state after:
case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : ¬p j
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type u_1
inst✝¹ : Finite J
f : J → C
inst✝ : HasCoproduct f
⊢ HasBiproduct f

Tactic:
by
  cases nonempty_fintype J
  exact HasBiproduct.mk
    { bicone := _
      isBilimit := biconeIsBilimitOfColimitCoconeOfIsColimit (colimit.isColimit _) }

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
⊢ ∀ {Z' : C} (g' : ⨁ f ⟶ Z'),
    biproduct.fromSubtype f p ≫ g' = 0 → biproduct.toSubtype f pᶜ ≫ biproduct.fromSubtype f pᶜ ≫ g' = g'

Tactic:
intro W

Goal state after:
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W : C
⊢ ∀ (g' : ⨁ f ⟶ W), biproduct.fromSubtype f p ≫ g' = 0 → biproduct.toSubtype f pᶜ ≫ biproduct.fromSubtype f pᶜ ≫ g' = g'
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ X
hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)
⊢ 0 ≫ b.inl = 0

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ X
hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ Y
hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)
⊢ 0 ≫ b.inr = 0

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ Y
hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)
⊢ 0 = 0
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.right.succ.refine_1
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a : ℕ × ℕ
x₁ x₂ : Fin k → ℕ
h : Fin.cons (Prod.map Nat.succ id a).1 x₂ = Fin.cons (0, n + 1).1 x₁
⊢ False

Tactic:
Fin.cons_inj

Goal state after:
case succ.right.succ.refine_1
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a : ℕ × ℕ
x₁ x₂ : Fin k → ℕ
h : (Prod.map Nat.succ id a).1 = (0, n + 1).1 ∧ x₂ = x₁
⊢ False
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
e : ↥s ≃ Fin #s
f : Fin #s → μ
⊢ ∀ (i : ι), (fun i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0) i ≠ 0 → i ∈ s

Tactic:
by simp +contextual

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

Goal state before:
pp: case pos
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : n = 0
⊢ ∅.piAntidiag n = {0}

Tactic:
simp [*]

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

Goal state before:
pp: case neg
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : ¬n = 0
⊢ ∅.piAntidiag n = ∅

Tactic:
simp [*]

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

Goal state before:
pp: case pos
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : n = 0
⊢ ∅.finsuppAntidiag n = {0}

Tactic:
simp [*]

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

Goal state before:
pp: case neg
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : ¬n = 0
⊢ ∅.finsuppAntidiag n = ∅

Tactic:
simp [*]

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

Goal state before:
pp: k : ℕ
⊢ map (fun x ↦ Fin.cons (0, 0).1 x) [0] = [0]

Tactic:
List.map_singleton

Goal state after:
k : ℕ
⊢ [Fin.cons (0, 0).1 0] = [0]
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case pos
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
hi : i ∈ s
⊢ n ∣ f i

Tactic:
exact hfdvd _ hi

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

Goal state before:
pp: n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) [![ni.2]]) (antidiagonal n) =
    map (fun i ↦ ![i.1, i.2]) (antidiagonal n)

Tactic:
List.map_singleton

Goal state after:
n : ℕ
⊢ flatMap (fun ni ↦ [Fin.cons ni.1 ![ni.2]]) (antidiagonal n) = map (fun i ↦ ![i.1, i.2]) (antidiagonal n)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case inl.inl
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ : f x = x
h✝ : g x = x
⊢ (f * g) x = x ∨ h x = x

Tactic:
simp [*]

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

Goal state before:
pp: case inl.inr
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ : f x = x
h✝ : h x = x
⊢ (f * g) x = x ∨ h x = x

Tactic:
simp [*]

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

Goal state before:
pp: case inr.inl
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ : h x = x
h✝ : g x = x
⊢ (f * g) x = x ∨ h x = x

Tactic:
simp [*]

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

Goal state before:
pp: case inr.inr
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ h✝ : h x = x
⊢ (f * g) x = x ∨ h x = x

Tactic:
simp [*]

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

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

Tactic:
rw [← mem_range_embedding_iff']

Goal state after:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ (c.embedding i) j ∈ Set.range ⇑(c.embedding i)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
m : ℕ
c₁ : Composition m
c₂ : Composition n
⊢ ∀ {i : ℕ}, i ∈ c₁.blocks ++ c₂.blocks → 0 < i

Tactic:
by
    intro i hi
    rw [mem_append] at hi
    exact hi.elim c₁.blocks_pos c₂.blocks_pos

Goal state after:
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:
simp [*]

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ (e.viaFintypeEmbedding f) b = f (e (f.invOfMemRange ⟨b, h⟩))

Tactic:
by
  simp only [viaFintypeEmbedding, Function.Embedding.invOfMemRange]
  rw [Equiv.Perm.extendDomain_apply_subtype _ _ h]
  congr

Goal state after:
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:
simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
⊢ (x :: y :: l).dedup.length = (x' :: y' :: l').length

Tactic:
← dedup_eq_self.mpr hd',

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
⊢ (x :: y :: l).dedup.length = (x' :: y' :: l').dedup.length
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case pos
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
hg : g b < g a
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ l.formPerm x ≠ x ↔ 2 ≤ l.length

Tactic:
rw [Ne, formPerm_apply_mem_eq_self_iff _ hl x hx, not_le]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ 1 < l.length ↔ 2 ≤ l.length
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
⊢ ∃ i, (f ^ i) x = y

Tactic:
by
  obtain ⟨i, _, hi⟩ := h.exists_pow_eq'
  exact ⟨i, hi⟩

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

Goal state before:
pp: α : Type u_2
f g : Perm α
x : α
hx : f x ≠ x
h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
⊢ (g * f * g⁻¹) (g x) ≠ g x

Tactic:
by simp [coe_mul, hx]

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

Goal state before:
pp: case e'_2
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x) = (Equiv.symm f) b
⊢ (swap x (f⁻¹ x) * f⁻¹) (((swap x (f x) * f) ^ (-i)) (f x)) =
    ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x)

Tactic:
rw [zpow_neg, ← inv_zpow, ← mul_apply, mul_inv_rev, swap_inv, mul_swap_eq_swap_mul]
      simp [swap_comm _ x, ← mul_apply, -coe_mul, ← inv_def, -coe_inv, ← inv_def, mul_assoc _ f⁻¹,
        ← mul_zpow_mul, mul_assoc _ _ f]
      simp

Goal state after:
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: case zero
α : Type u_1
f : α → α
a : α
⊢ (iterate f a 0).length = 0

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n✝ : ℕ
a✝ : ∀ (a : α), (iterate f a n✝).length = n✝
a : α
⊢ (iterate f a (n✝ + 1)).length = n✝ + 1

Tactic:
simp [*]

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

Goal state before:
pp: case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ f ^ n = 1 → ∃ x, f x ≠ x ∧ (f ^ n) x = x

pp: case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ (∃ x, f x ≠ x ∧ (f ^ n) x = x) → f ^ n = 1

Tactic:
· intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩

Goal state after:
case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ (∃ x, f x ≠ x ∧ (f ^ n) x = x) → f ^ n = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
⊢ f ^ a = f ^ b → ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

pp: case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
⊢ (∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x) → f ^ a = f ^ b

Tactic:
· intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩

Goal state after:
case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
⊢ (∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x) → f ^ a = f ^ b
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case left.swap_mul
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih : sign (σa'.sumCongr 1) = sign σa'
⊢ sign ((swap a₁ a₂ * σa').sumCongr 1) = sign (swap a₁ a₂ * σa')

Tactic:
← one_mul (1 : Perm β),

Goal state after:
case left.swap_mul
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih : sign (σa'.sumCongr 1) = sign σa'
⊢ sign ((swap a₁ a₂ * σa').sumCongr (1 * 1)) = sign (swap a₁ a₂ * σa')
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inl
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : f.IsCycleOn ↑{a}
ha : a ∈ {a}
⊢ (f ^ n) a = a ↔ #{a} ∣ n

pp: case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
⊢ (f ^ n) a = a ↔ #s ∣ n

Tactic:
· rw [coe_singleton, isCycleOn_singleton] at hf
    simpa using! IsFixedPt.iterate hf n

Goal state after:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
⊢ (f ^ n) a = a ↔ #s ∣ n