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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesLimit K F)

Tactic:
constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesColimit K F)

Tactic:
constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (PreservesLimitsOfShape J F)

Tactic:
constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (PreservesColimitsOfShape J F)

Tactic:
constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

Tactic:
constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

Tactic:
constructor; rintro ⟨a⟩ ⟨b⟩; congr!

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

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
h : f = 0
⊢ 𝟙 Y = 0

Tactic:
rw [← IsSplitEpi.id f]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
h : f = 0
⊢ section_ f ≫ f = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝³ : Category.{v, u} C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) = coequalizer.desc (G.map h) ⋯

Tactic:
apply coequalizer.hom_ext

Goal state after:
C : Type u
X Y : C
inst✝³ : Category.{v, u} C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) =
    coequalizer.π (G.map f) (G.map g) ≫ coequalizer.desc (G.map h) ⋯
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsLimit K F)

Tactic:
constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsColimit K F)

Tactic:
constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (ReflectsLimitsOfShape J F)

Tactic:
constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (ReflectsColimitsOfShape J F)

Tactic:
constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

Tactic:
constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

Tactic:
constructor; rintro ⟨a⟩ ⟨b⟩; congr!

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasLimit (parallelPair f 0)
w : kernel.ι f = 0
P✝ : C
g : P✝ ⟶ X
h : g ≫ f = 0
⊢ g = 0

Tactic:
rw [← kernel.lift_ι f g h, w, Limits.comp_zero]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero c.pt
R✝ : C
g : Y ⟶ R✝
hg : f ≫ g = 0
a : c.pt ⟶ R✝
ha : Cofork.π c ≫ a = g
⊢ Cofork.π c ≫ a = 0

Tactic:
h.eq_of_src a 0,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero c.pt
R✝ : C
g : Y ⟶ R✝
hg : f ≫ g = 0
a : c.pt ⟶ R✝
ha : Cofork.π c ≫ a = g
⊢ Cofork.π c ≫ 0 = 0
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P Q : ObjectProperty C
X : C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : Q.IsClosedUnderIsomorphisms
⊢ (P ⊔ Q).IsClosedUnderIsomorphisms

Tactic:
simp only [isClosedUnderIsomorphisms_iff_isoClosure_eq_self, isoClosure_sup, isoClosure_eq_self]

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✝
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hf : Epi f
h : IsZero c.pt
s : CokernelCofork f
⊢ Cofork.π c ≫ 0 = Cofork.π s

Tactic:
rw [comp_zero, ← cancel_epi f, comp_zero, s.condition]

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✝
inst✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasCokernel f
inst✝ : IsIso g
s : CokernelCofork (f ≫ g)
m : cokernel (?m.116 s) ⟶ ?m.118 s
w : Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m = Cofork.π s
⊢ m = cokernel.desc f (g ≫ Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m) ⋯

Tactic:
apply coequalizer.hom_ext

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasCokernel f
inst✝ : IsIso g
s : CokernelCofork (f ≫ g)
m : cokernel f ⟶ s.pt
w : Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m = Cofork.π s
⊢ coequalizer.π f 0 ≫ m =
    coequalizer.π f 0 ≫ cokernel.desc f (g ≫ Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m) ⋯
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
J : Type
x✝ : Finite J
val✝ : Fintype J
f✝ : J → C
b✝ : Bicone f✝
hb : b✝.IsBilimit
⊢ ∑ j, (F.mapBicone b✝).π j ≫ (F.mapBicone b✝).ι j = 𝟙 (F.mapBicone b✝).pt

Tactic:
F.mapBicone_π,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
J : Type
x✝ : Finite J
val✝ : Fintype J
f✝ : J → C
b✝ : Bicone f✝
hb : b✝.IsBilimit
⊢ ∑ x, F.map (b✝.π x) ≫ (F.mapBicone b✝).ι x = 𝟙 (F.mapBicone b✝).pt
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
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j : Subtype p
⊢ fromSubtype f p ≫ π f ↑j = 𝟙 (⨁ Subtype.restrict p f) ≫ π (Subtype.restrict p f) j

Tactic:
biproduct.fromSubtype_π_subtype,

Goal state after:
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)
j : Subtype p
⊢ π (Subtype.restrict p f) j = 𝟙 (⨁ Subtype.restrict p f) ≫ π (Subtype.restrict p f) j
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inl ≫ map f g = f ≫ inl

Tactic:
biprod.map_eq_map'

Goal state after:
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inl ≫ map' f g = f ≫ inl
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inr ≫ map f g = g ≫ inr

Tactic:
biprod.map_eq_map'

Goal state after:
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inr ≫ map' f g = g ≫ inr
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

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
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ desc b.inl b.inr ≫ lift b.fst b.snd = 𝟙 (X ⊞ Y)

Tactic:
rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ←
      biprod.conePointUniqueUpToIso_inv X Y hb, Iso.inv_hom_id]

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

Goal state before:
pp: case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : inv inl ≫ inl ≫ fst = inv inl ≫ 𝟙 X
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl

Tactic:
IsIso.inv_hom_id_assoc,

Goal state after:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : fst = inv inl ≫ 𝟙 X
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl
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
⊢ m = f ≫ b.inl + g ≫ b.inr

Tactic:
obtain ⟨q : T ⟶ Y, hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)⟩ :=
        KernelFork.IsLimit.lift' hb _ h₁'

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)
⊢ m = f ≫ b.inl + g ≫ b.inr
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
i : Fin n
hlt : i.castSucc < q
⊢ q.succAbove i < q

Tactic:
simp [succAbove_of_castSucc_lt, hlt]

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

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

Tactic:
sum_dite_of_true fun _ ↦ id

Goal state after:
case a.mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
e : ↥s ≃ Fin #s
f : Fin #s → μ
⊢ ∑ i, f (e ⟨↑i, ⋯⟩) = ∑ i, f i ∧ ∀ (i : ι), (fun i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0) i ≠ 0 → i ∈ s
Module: Mathlib.Algebra.Order.Antidiag.Pi

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

Tactic:
ext; simp [funext_iff]

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

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

Tactic:
hx

Goal state after:
case e_a
n x : ℕ
hx : x < n
⊢ antidiagonalTuple 0 (n - x) = []
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 : ι
⊢ x ∈ s → (Finsupp.erase a f) x = f x

Tactic:
hx

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 : ι
hx : x ∈ s
⊢ (Finsupp.erase a f) x = f x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
| n

Tactic:
rw [← c.blocks_sum, ← sum_take_add_sum_drop _ i]

Goal state after:
n : ℕ
c : Composition n
i : ℕ
| (take i c.blocks).sum + (drop i c.blocks).sum
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr
ι : 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
⊢ Function.update (⇑g) a n1 a + ∑ x ∈ s, Function.update (⇑g) a n1 x = n1 + s.sum ⇑g

Tactic:
apply congr_arg₂

Goal state after:
case mpr.hx
ι : 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
⊢ Function.update (⇑g) a n1 a = n1

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 = s.sum ⇑g
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 : ι
⊢ x ∈ s → Function.update (⇑g) a n1 x = g x

Tactic:
hx

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 : ι
hx : x ∈ s
⊢ Function.update (⇑g) a n1 x = g x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : (∀ f ∈ l, f x = x) → l.prod x = x
hx : ∀ f_1 ∈ f :: l, f_1 x = x
⊢ f x = x

pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : (∀ f ∈ l, f x = x) → l.prod x = x
hx : ∀ f_1 ∈ f :: l, f_1 x = x
⊢ ∀ f ∈ l, f x = x

Tactic:
hx

Goal state after:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : (∀ f ∈ l, f x = x) → l.prod x = x
hx : ∀ f_1 ∈ f :: l, f_1 x = x
⊢ x = x

case cons._
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : (∀ f ∈ l, f x = x) → l.prod x = x
hx : ∀ f_1 ∈ f :: l, f_1 x = x
⊢ f ∈ f :: l

case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : (∀ f ∈ l, f x = x) → l.prod x = x
hx : ∀ f_1 ∈ f :: l, f_1 x = x
⊢ ∀ f ∈ l, f x = x
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : Finite ↑{x | p x}
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ e.extendSubtype x = ↑(e.toCompl ⟨x, hx⟩)

Tactic:
by
  simp only [extendSubtype, subtypeCongr, Equiv.trans_apply,
    sumCompl_symm_apply_of_neg hx]
  rfl

Goal state after:
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 : α
⊢ x ∈ f.support ∩ g.support → (f ^ (k + 1)) x = (g ^ (k + 1)) x

Tactic:
hx

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 : α
hx : x ∈ f.support ∩ g.support
⊢ (f ^ (k + 1)) x = (g ^ (k + 1)) x
Module: Mathlib.GroupTheory.Perm.List

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

Tactic:
hx

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

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

Tactic:
hx

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
⊢ x ∈ l.toFinset
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.toCompositionAsSet.blocks = c.blocks

Tactic:
let d := c.toCompositionAsSet
  change d.blocks = c.blocks
  have length_eq : d.blocks.length = c.blocks.length := by simp [d, blocks_length]
  suffices H : ∀ i ≤ d.blocks.length, (d.blocks.take i).sum = (c.blocks.take i).sum from
    eq_of_sum_take_eq length_eq H
  intro i hi
  have i_lt : i < d.boundaries.card := by
    simpa [CompositionAsSet.blocks, length_ofFn,
      d.card_boundaries_eq_succ_length] using Nat.lt_succ_iff.2 hi
  have i_lt' : i < c.boundaries.card := i_lt
  have i_lt'' : i < c.length + 1 := by rwa [c.card_boundaries_eq_succ_length] at i_lt'
  have A :
    d.boundaries.orderEmbOfFin rfl ⟨i, i_lt⟩ =
      c.boundaries.orderEmbOfFin c.card_boundaries_eq_succ_length ⟨i, i_lt''⟩ :=
    rfl
  have B : c.sizeUpTo i = c.boundary ⟨i, i_lt''⟩ := rfl
  rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A,
    c.orderEmbOfFin_boundaries]

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

Goal state before:
pp: n✝ n : ℕ
c : CompositionAsSet n
⊢ (fun c ↦ c.toCompositionAsSet) ((fun c ↦ c.toComposition) c) = c

Tactic:
ext1
    exact c.toComposition_boundaries

Goal state after:
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 : α
⊢ x ∈ f.support → f x = (hd :: tl).prod x

Tactic:
hx

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 : α
hx : 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
x : α
⊢ x ∈ f.support → x ∈ l.prod.support

Tactic:
hx

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
x : α
hx : x ∈ f.support
⊢ x ∈ l.prod.support
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]
x : α
⊢ x ∈ ↑l.toFinset → x ∈ {x | l.formPerm x ≠ x}

Tactic:
hx

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
x : α
hx : 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:
hx

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.Cycle.Basic

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

Tactic:
apply_symm_apply

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