mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (cyclesMap φ)
h₂ : Epi φ.τ₁
h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0
z : (CokernelCofork.ofπ S₂.homologyπ ⋯).pt ⟶ S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ S₁.homologyπ = S₁.homologyπ ≫ 𝟙 S₁.homology

Tactic:
comp_id

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (cyclesMap φ)
h₂ : Epi φ.τ₁
h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0
z : (CokernelCofork.ofπ S₂.homologyπ ⋯).pt ⟶ S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ S₁.homologyπ = S₁.homologyπ
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₁.f = S₁.f ≫ 𝟙 S₁.X₂

Tactic:
comp_id

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₁.f = S₁.f
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (leftHomologyMap' φ h₁ h₂')
eq : leftHomologyMap' (φ ≫ 𝟙 S₂) h₁ h₂ = leftHomologyMap' φ h₁ h₂' ≫ leftHomologyMap' (𝟙 S₂) h₂' h₂
⊢ IsIso (leftHomologyMap' φ h₁ h₂)

Tactic:
comp_id

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (leftHomologyMap' φ h₁ h₂')
eq : leftHomologyMap' φ h₁ h₂ = leftHomologyMap' φ h₁ h₂' ≫ leftHomologyMap' (𝟙 S₂) h₂' h₂
⊢ IsIso (leftHomologyMap' φ h₁ h₂)
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (cyclesMap φ)
h₂ : Epi φ.τ₁
h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0
z : (CokernelCofork.ofπ S₂.homologyπ ⋯).pt ⟶ S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ S₂.homologyπ = S₂.homologyπ ≫ 𝟙 S₂.homology

Tactic:
comp_id

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (cyclesMap φ)
h₂ : Epi φ.τ₁
h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0
z : (CokernelCofork.ofπ S₂.homologyπ ⋯).pt ⟶ S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ S₂.homologyπ = S₂.homologyπ
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
⊢ S.liftCycles k hk ≫ 𝟙 S.cycles = S.liftCycles k hk

Tactic:
comp_id

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
⊢ S.liftCycles k hk = S.liftCycles k hk
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (opcyclesMap φ)
h₂ : Mono φ.τ₃
h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0
z : S₂.homology ⟶ (KernelFork.ofι S₁.homologyι ⋯).pt
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ S₁.homologyι ≫ 𝟙 S₁.opcycles = S₁.homologyι

Tactic:
comp_id

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (opcyclesMap φ)
h₂ : Mono φ.τ₃
h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0
z : S₂.homology ⟶ (KernelFork.ofι S₁.homologyι ⋯).pt
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ S₁.homologyι = S₁.homologyι
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (rightHomologyMap' φ h₁ h₂')
eq : rightHomologyMap' (φ ≫ 𝟙 S₂) h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂
⊢ IsIso (rightHomologyMap' φ h₁ h₂)

Tactic:
comp_id

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (rightHomologyMap' φ h₁ h₂')
eq : rightHomologyMap' φ h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂
⊢ IsIso (rightHomologyMap' φ h₁ h₂)
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.g = S.g ≫ 𝟙 S.X₃

Tactic:
comp_id

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.g = S.g
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b c : S₁ ⟶ S₂
⊢ (a + b + c).τ₁ = (a + (b + c)).τ₁

Tactic:
apply add_assoc

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b c : S₁ ⟶ S₂
⊢ (a + b + c).τ₂ = (a + (b + c)).τ₂

Tactic:
apply add_assoc

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b c : S₁ ⟶ S₂
⊢ (a + b + c).τ₃ = (a + (b + c)).τ₃

Tactic:
apply add_assoc

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₂ : ∀ (j : J), (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) = (π₂.mapCocone s).ι.app j
eq₃ : ∀ (j : J), (π₃.mapCocone c).ι.app j ≫ h₃.desc (π₃.mapCocone s) = (π₃.mapCocone s).ι.app j
⊢ (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) ≫ s.pt.g =
    (π₂.mapCocone c).ι.app j ≫ c.pt.g ≫ h₃.desc (π₃.mapCocone s)

Tactic:
have eq₂₃ := fun j => (c.ι.app j).comm₂₃

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₂ : ∀ (j : J), (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) = (π₂.mapCocone s).ι.app j
eq₃ : ∀ (j : J), (π₃.mapCocone c).ι.app j ≫ h₃.desc (π₃.mapCocone s) = (π₃.mapCocone s).ι.app j
eq₂₃ : ∀ (j : J), (c.ι.app j).τ₂ ≫ (((const J).obj c.pt).obj j).g = (F.obj j).g ≫ (c.ι.app j).τ₃
⊢ (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) ≫ s.pt.g =
    (π₂.mapCocone c).ι.app j ≫ c.pt.g ≫ h₃.desc (π₃.mapCocone s)
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ (S₁.mapLeftHomologyIso F).hom ≫ F.map (leftHomologyMap φ) ≫ (S₂.mapLeftHomologyIso F).inv =
    (S₁.mapLeftHomologyIso F).hom ≫ (S₁.mapLeftHomologyIso F).inv ≫ leftHomologyMap (F.mapShortComplex.map φ)

Tactic:
← mapLeftHomologyIso_hom_naturality_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ leftHomologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapLeftHomologyIso F).hom ≫ (S₂.mapLeftHomologyIso F).inv =
    (S₁.mapLeftHomologyIso F).hom ≫ (S₁.mapLeftHomologyIso F).inv ≫ leftHomologyMap (F.mapShortComplex.map φ)
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.iCycles ≫ S.pOpcycles = 0
⊢ a ≫ b = 0

Tactic:
← S.liftCycles_i a ha,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.iCycles ≫ S.pOpcycles = 0
⊢ (S.liftCycles a ha ≫ S.iCycles) ≫ b = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ S.g ≫ hS.desc (CokernelCofork.ofπ S.pOpcycles ⋯) = S.pOpcycles ≫ 𝟙 S.opcycles

Tactic:
comp_id

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ S.g ≫ hS.desc (CokernelCofork.ofπ S.pOpcycles ⋯) = S.pOpcycles
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
⊢ Epi S.g

Tactic:
have := s.isSplitEpi_g

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
this : IsSplitEpi S.g
⊢ Epi S.g
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
x : Subobject X
⊢ (map (f ≫ g)).obj x = (map g).obj ((map f).obj x)

Tactic:
by
  induction x using Quotient.inductionOn' with | _ t
  exact Quotient.sound ⟨(MonoOver.mapComp _ _).app t⟩

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive C
inst✝ : Balanced C
S : ShortComplex C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
⊢ S.g = S.g ≫ 𝟙 S.X₃

Tactic:
comp_id

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive C
inst✝ : Balanced C
S : ShortComplex C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
⊢ S.g = S.g
Module: Mathlib.CategoryTheory.Abelian.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ ((evaluation C D).obj X).map (cokernel.π α) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).hom =
    (Iso.refl (((evaluation C D).obj X).obj G)).hom ≫ cokernel.π (α.app X)

Tactic:
apply (cancel_mono (PreservesCokernel.iso ((evaluation C D).obj X) α).inv).1
        simp only [Category.assoc, Iso.hom_inv_id]
        dsimp
        simp only [PreservesCokernel.iso_inv, Category.id_comp, Category.comp_id]
        exact (π_comp_cokernelComparison _ ((evaluation C D).obj X)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsInitial X
A : C
i : A ⟶ X
w✝ : Mono i
fac : hX.to A ≫ i = 𝟙 X
⊢ i ≫ 𝟙 X = i

Tactic:
comp_id

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsInitial X
A : C
i : A ⟶ X
w✝ : Mono i
fac : hX.to A ≫ i = 𝟙 X
⊢ i = i
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
X : C
⊢ (StructuredArrow.hom E ≫
          ((whiskeringLeft C D H).obj L).map { app := fun Y ↦ (h Y).desc (G.coconeAt Y), naturality := ⋯ }).app
      X =
    (StructuredArrow.hom G).app X

Tactic:
simpa using (h (L.obj X)).fac (LeftExtension.coconeAt G _) (CostructuredArrow.mk (𝟙 _))

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
a✝ : F''.IsLeftKanExtension α'
⊢ α ≫ 𝟙 (L ⋙ F') = α

Tactic:
comp_id

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
a✝ : F''.IsLeftKanExtension α'
⊢ α = α
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (L.map f ≫ 𝟙 (L.obj X₂))) =
    limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f

Tactic:
comp_id

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (L.map f)) =
    limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯)))
      (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) =
    YonedaCollection.snd (counitForward F (unop s) ((ConcreteCategory.hom (F.map f)) x)).val

Tactic:
have : F.map (CostructuredArrow.mkPrecomp
      (YonedaCollection.fst (counitForward F (unop t) x).val) f.unop.left).op
      (F.map (eqToHom (by simp; rfl)) x) = _ :=
    map_mkPrecomp_eqToHom (h := by simp)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this✝ : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
this :
  (ConcreteCategory.hom
        (F.map (CostructuredArrow.mkPrecomp (YonedaCollection.fst (counitForward F (unop t) x).val) f.unop.left).op))
      ((ConcreteCategory.hom (F.map (eqToHom ⋯))) x) =
    (ConcreteCategory.hom (F.map (eqToHom ⋯)))
      ((ConcreteCategory.hom (F.map (CostructuredArrow.mkPrecomp t.1.hom f.unop.left).op)) x)
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯)))
      (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) =
    YonedaCollection.snd (counitForward F (unop s) ((ConcreteCategory.hom (F.map f)) x)).val
Module: Mathlib.Algebra.Category.Grp.Injective

Goal state before:
pp: case inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n • m ∈ ℤ ∙ m
⊢ n • m • DivisibleBy.div gₘ m = g ⟨n • m, hn⟩

Tactic:
DivisibleBy.div_cancel gₘ h0,

Goal state after:
case inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n • m ∈ ℤ ∙ m
⊢ n • gₘ = g ⟨n • m, hn⟩
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ (-n).negOnePow = n.negOnePow

Tactic:
by
  dsimp [negOnePow]
  simp only [zpow_neg, ← inv_zpow, inv_neg, inv_one]

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
b : ExtensionOf i f
a : N →ₗ.[R] Q
a_le : i.range ≤ a.domain
e1 : ∀ (m : M), f m = ↑a ⟨i m, ⋯⟩
domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 }.domain = b.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.domain⦄ ⦃hb : x ∈ b.domain⦄,
    ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap ⟨x, ha⟩ = ↑b.toLinearPMap ⟨x, hb⟩
⊢ a = b.toLinearPMap

Tactic:
exact LinearPMap.ext domain_eq to_fun_eq

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℕ
⊢ f (x + (2 * k) • c) = (-1) ^ (2 * k) • f x

pp: case inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℕ
⊢ f (x + (2 * k + 1) • c) = (-1) ^ (2 * k + 1) • f x

Tactic:
· rw [h.even_nsmul_periodic]
    simp

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℕ
⊢ f (x + (2 * k + 1) • c) = (-1) ^ (2 * k + 1) • f x
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: case e_a
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(fst i x) = a + r • y - snd i x • y

Tactic:
← eq1

Goal state after:
case e_a
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(fst i x) = ↑x - snd i x • y
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mpr
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p ^ (n + 1)
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False

Tactic:
pow_succ'

Goal state after:
case mpr
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p * p ^ n
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
⊢ Fintype.card (ZMod p)ˣ ≤ p - 1

Tactic:
have : NeZero p := ⟨(pos_of_gt hp).ne'⟩
  rw [ZMod.card_units_eq_totient p]
  exact Nat.le_sub_one_of_lt (Nat.totient_lt p hp)

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mpr
m n : ℕ
⊢ (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2 → (φ m).Coprime (φ n)

Tactic:
simp_rw [← totient_eq_one_iff]
    rintro (h | h) <;> rw [h]
    exacts [Nat.coprime_one_left _, Nat.coprime_one_right _]

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b) / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) =
    a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
        ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b

Tactic:
eq_comm,

Goal state after:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
        ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b =
    a.gcd b * (a * b) / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1))
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inl
b : ℕ
h : 0 ∣ b
⊢ φ 0 ∣ φ b

pp: case inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
⊢ φ a ∣ φ b

Tactic:
· simp [zero_dvd_iff.1 h]

Goal state after:
case inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
⊢ φ a ∣ φ b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : 0 = φ b
ha : a = 0
⊢ a = b ∨ 2 * a = b

Tactic:
eq_comm,

Goal state after:
case pos
a b : ℕ
h : a ∣ b
h' : φ b = 0
ha : a = 0
⊢ a = b ∨ 2 * a = b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ a * φ c
hb : ¬a * c = 0
this : a.Coprime c
⊢ a = a * c ∨ 2 * a = a * c

Tactic:
eq_comm,

Goal state after:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a * φ c = φ a
hb : ¬a * c = 0
this : a.Coprime c
⊢ a = a * c ∨ 2 * a = a * c
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
ha : Even a
h' : 0 = φ b
ha' : a = 0
⊢ a = b

Tactic:
eq_comm,

Goal state after:
case pos
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ b = 0
ha' : a = 0
⊢ a = b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : ¬a = 0
⊢ a = b

Tactic:
refine (eq_or_eq_of_totient_eq_totient h h').resolve_right fun h ↦ ?_

Goal state after:
case neg
a b : ℕ
h✝ : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : ¬a = 0
h : 2 * a = b
⊢ False