mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
eq₂ : ∀ (j : J), h₂.lift (π₂.mapCone s) ≫ (c.π.app j).τ₂ = (s.π.app j).τ₂
eq₃ : ∀ (j : J), h₃.lift (π₃.mapCone s) ≫ (c.π.app j).τ₃ = (s.π.app j).τ₃
eq₂₃ : ∀ (j : J), (c.π.app j).τ₂ ≫ (F.obj j).g = c.pt.g ≫ (c.π.app j).τ₃
eq₂₃' : ∀ (j : J), (s.π.app j).τ₂ ≫ (F.obj j).g = s.pt.g ≫ (s.π.app j).τ₃
⊢ h₂.lift (π₂.mapCone s) ≫ c.pt.g ≫ (c.π.app j).τ₃ = s.pt.g ≫ h₃.lift (π₃.mapCone s) ≫ (c.π.app j).τ₃

Tactic:
← eq₂₃,

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 : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
eq₂ : ∀ (j : J), h₂.lift (π₂.mapCone s) ≫ (c.π.app j).τ₂ = (s.π.app j).τ₂
eq₃ : ∀ (j : J), h₃.lift (π₃.mapCone s) ≫ (c.π.app j).τ₃ = (s.π.app j).τ₃
eq₂₃ : ∀ (j : J), (c.π.app j).τ₂ ≫ (F.obj j).g = c.pt.g ≫ (c.π.app j).τ₃
eq₂₃' : ∀ (j : J), (s.π.app j).τ₂ ≫ (F.obj j).g = s.pt.g ≫ (s.π.app j).τ₃
⊢ h₂.lift (π₂.mapCone s) ≫ (c.π.app j).τ₂ ≫ (F.obj j).g = s.pt.g ≫ h₃.lift (π₃.mapCone s) ≫ (c.π.app j).τ₃
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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
A' : C
α : A ⟶ A'
⊢ S.f ≫ k ≫ α = 0

Tactic:
rw [reassoc_of% hk, zero_comp]

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 : S₁ ⟶ S₂
⊢ (a - b).τ₁ = (a + -b).τ₁

Tactic:
apply sub_eq_add_neg

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 : S₁ ⟶ S₂
⊢ (a - b).τ₂ = (a + -b).τ₂

Tactic:
apply sub_eq_add_neg

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 : S₁ ⟶ S₂
⊢ (a - b).τ₃ = (a + -b).τ₃

Tactic:
apply sub_eq_add_neg

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ π ≫ (isoHomology S hkf hcc fac).hom = (S.isoCyclesOfIsLimit hkf).hom ≫ S.homologyπ

Tactic:
by
  dsimp [isoHomology]
  simp [← cancel_mono (S.homologyIsoImageICyclesCompPOpcycles.hom),
    ← cancel_mono (image.ι (S.iCycles ≫ S.pOpcycles)),
    ← reassoc_of% fac]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Type u₁
⊢ Mono (↾WithBot.some)

Tactic:
by
          rw [mono_iff_injective]
          exact WithBot.coe_injective

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

Goal state before:
pp: case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : EnoughInjectives C
X : C
h : IsZero X
⊢ ∃ p, IsZero X → IsZero p.J

Tactic:
have := h.injective
    exact ⟨{ J := X, f := 𝟙 X}, by tauto⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ = S₁.f ≫ h₁ + h₀ + Hom.τ₁ 0

Tactic:
nullHomotopic_τ₁,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ h₀ + S₁.f ≫ h₁ = S₁.f ≫ h₁ + h₀ + Hom.τ₁ 0
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ S₁.f ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i

Tactic:
nullHomotopic_τ₁,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ S₁.f ≫ h₁ ≫ S₂.f = ((h₀ + S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝² : Mono S₁.f
this✝¹ : Mono S₂.f
this✝ : Epi S₁.g
this : Epi S₂.g
⊢ IsIso φ.τ₂

Tactic:
have := mono_τ₂_of_exact_of_mono φ h₁.exact

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝³ : Mono S₁.f
this✝² : Mono S₂.f
this✝¹ : Epi S₁.g
this✝ : Epi S₂.g
this : Mono φ.τ₂
⊢ IsIso φ.τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
⊢ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact ∧ Mono φ.τ₂

Tactic:
have : Mono φ.τ₂ := by
      rw [← S₂.liftCycles_i φ.τ₂ w]
      apply mono_comp

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact ∧ Mono φ.τ₂
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ ((pullback X✝.arrow ⋙ map X✝.arrow).obj g).obj.left ⟶ ((pullback Y✝.arrow ⋙ map Y✝.arrow).obj g).obj.left

Tactic:
apply pullback.lift (pullback.fst _ _) (pullback.snd _ _ ≫ k.hom.left) _

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ pullback.fst ((forget A).obj g).hom X✝.arrow ≫ ((forget A).obj g).hom =
    (pullback.snd ((forget A).obj g).hom X✝.arrow ≫ Over.Hom.left k.hom) ≫ Y✝.arrow
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case some
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val✝ : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ (u ≫ limit.π (wideCospan s) (some val✝)) ≫ ((equivShrink (Subobject A)).symm ↑val✝).arrow =
    (v ≫ limit.π (wideCospan s) (some val✝)) ≫ ((equivShrink (Subobject A)).symm ↑val✝).arrow

Tactic:
rw [assoc, assoc]

Goal state after:
case some
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val✝ : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ u ≫ limit.π (wideCospan s) (some val✝) ≫ ((equivShrink (Subobject A)).symm ↑val✝).arrow =
    v ≫ limit.π (wideCospan s) (some val✝) ≫ ((equivShrink (Subobject A)).symm ↑val✝).arrow
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 : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
⊢ (L ⋙ E.functor).HasPointwiseRightKanExtensionAt F (E.functor.obj Y)

Tactic:
let Φ := StructuredArrow.post Y L E.functor

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
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
Φ : StructuredArrow Y L ⥤ StructuredArrow (E.functor.obj Y) (L ⋙ E.functor) := StructuredArrow.post Y L E.functor
⊢ (L ⋙ E.functor).HasPointwiseRightKanExtensionAt F (E.functor.obj Y)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
inst✝ : HasColimit (CostructuredArrow.proj L Y ⋙ F)
g : CostructuredArrow L Y
⊢ (StructuredArrow.hom E).app g.left ≫ (StructuredArrow.right E).map g.hom ≫ h.isoColimit.hom =
    colimit.ι (CostructuredArrow.proj L Y ⋙ F) g

Tactic:
by
  simpa using! h.comp_coconePointUniqueUpToIso_hom (colimit.isColimit _) g

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

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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : D ⥤ H
G₁ G₂ : C ⥤ H
β : ((whiskeringLeft C D H).obj L).obj F ⟶ G₁
f : G₁ ⟶ G₂
X : C
h : (L.ran.map f).app (L.obj X) ≫ (L.ranCounit.app G₂).app X = (L.ranCounit.app G₁).app X ≫ f.app X
⊢ β.app X ≫ f.app X =
    ((L.ran.obj G₁).liftOfIsRightKanExtension (L.ranCounit.app G₁) F β).app (L.obj X) ≫
      (L.ran.map f).app (L.obj X) ≫ (L.ranCounit.app G₂).app X

Tactic:
rw [h, liftOfIsRightKanExtension_fac_app_assoc]

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
ex : L'.RightExtension F
⊢ CostructuredArrow.IsUniversal ex ≃ CostructuredArrow.IsUniversal ((postcomp₁ G e.hom F).obj ex)

Tactic:
apply IsTerminal.isTerminalIffObj (RightExtension.postcomp₁ G e.hom F)

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

Goal state before:
pp: J✝ : Type u_2
inst✝⁵ : Countable J✝
inst✝⁴ : Preorder J✝
inst✝³ : IsCofiltered J✝
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this : Nonempty (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h : unop i.left ≤ unop j.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
· right
      exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasLimitsOfShape K C
inst✝ : PreservesColimitsOfShape J lim
d : D
F G : K ⥤ D ⥤ C
η : F ⟶ G
j : K
⊢ ((lim ⋙ (evaluation D C).obj d).map η ≫
        (limitObjIsoLimitCompEvaluation G d ≪≫
            HasLimit.isoOfNatIso (Iso.refl (G ⋙ (evaluation D C).obj d)) ≪≫
              (limitObjIsoLimitCompEvaluation ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip
                  G).symm).hom) ≫
      (limit.π ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip j).app G =
    ((limitObjIsoLimitCompEvaluation F d ≪≫
            HasLimit.isoOfNatIso (Iso.refl (F ⋙ (evaluation D C).obj d)) ≪≫
              (limitObjIsoLimitCompEvaluation ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip
                  F).symm).hom ≫
        (limit ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip).map η) ≫
      (limit.π ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip j).app G

Tactic:
simp [← NatTrans.comp_app]

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ := ⋯
a : (precomp₂ L' α).obj b ⟶ y
⊢ StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (StructuredArrow.Hom.right a) =
    StructuredArrow.hom b ≫
      ((whiskeringLeft D D' H).obj L').map (StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) ⋯))

Tactic:
apply hα.hom_ext

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ := ⋯
a : (precomp₂ L' α).obj b ⟶ y
⊢ StructuredArrow.hom (mk F₁ α) ≫
      ((whiskeringLeft C D H).obj L).map
        (StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (StructuredArrow.Hom.right a)) =
    StructuredArrow.hom (mk F₁ α) ≫
      ((whiskeringLeft C D H).obj L).map
        (StructuredArrow.hom b ≫
          ((whiskeringLeft D D' H).obj L').map (StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) ⋯)))
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
⊢ StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (StructuredArrow.Hom.right u) = StructuredArrow.hom y

Tactic:
apply hα.hom_ext

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := ⋯
⊢ StructuredArrow.hom (mk F₁ α) ≫
      ((whiskeringLeft C D H).obj L).map
        (StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (StructuredArrow.Hom.right u)) =
    StructuredArrow.hom (mk F₁ α) ≫ ((whiskeringLeft C D H).obj L).map (StructuredArrow.hom y)
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  uliftYoneda.{w, v₁, u₁}.map f.unop ≫ s.ι.app (op (P.elementsMk X x)) =
    s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))
⊢ uliftYonedaEquiv (s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))) =
    (hom (s.pt.map f)) (uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))))

Tactic:
rw [← this, uliftYonedaEquiv_comp]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  uliftYoneda.{w, v₁, u₁}.map f.unop ≫ s.ι.app (op (P.elementsMk X x)) =
    s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))
⊢ (hom ((s.ι.app (op (P.elementsMk X x))).app (op (unop Y)))) (uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map f.unop)) =
    (hom (s.pt.map f)) (uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))))
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (uliftYoneda.{max w v₂, v₁, u₁}.obj X)
Z : Cᵒᵖ
f : (yoneda.obj X).obj Z
⊢ (hom
          ((StructuredArrow.hom
                  (Functor.LeftExtension.mk (uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)) (uliftYonedaMap F X)) ≫
                ((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))).obj F.op).map
                  (uliftYonedaEquiv.symm (uliftYonedaEquiv (StructuredArrow.hom Y)))).app
            Z)).toFun
      { down := f } =
    (hom ((StructuredArrow.hom Y).app Z)).toFun { down := f }

Tactic:
simpa [uliftYonedaEquiv, uliftYoneda] using
        ConcreteCategory.congr_hom (CC := fun X ↦ X) (Y.hom.naturality f.op).symm (ULift.up (𝟙 _))

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.limitsOfShape J X
⊢ P.IsCoseparating

Tactic:
by
  intro X Y f g h
  obtain ⟨J, _, ⟨p⟩⟩ := hP Y
  exact p.isLimit.hom_ext (fun j ↦ h _ (p.prop_diag_obj _) _)

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

Goal state before:
pp: case mp
n : ℤ
h : n.negOnePow = 1
⊢ ¬Odd n

Tactic:
intro h'

Goal state after:
case mp
n : ℤ
h : n.negOnePow = 1
h' : Odd n
⊢ False
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case mp
n : ℤ
h : n.negOnePow = -1
⊢ Odd n

Tactic:
rw [← Int.not_even_iff_odd]

Goal state after:
case mp
n : ℤ
h : n.negOnePow = -1
⊢ ¬Even n
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case mp
n : ℤ
h : n.negOnePow = -1
⊢ ¬Even n

Tactic:
intro h'

Goal state after:
case mp
n : ℤ
h : n.negOnePow = -1
h' : Even n
⊢ False
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
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : Q ≃ₗ[R] M
h : Baer R Q
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] Q
h' : ∀ (x : R) (mem : x ∈ I), g' x = (↑e.symm ∘ₗ g) ⟨x, mem⟩
⊢ ∀ (x : R) (mem : x ∈ I), (↑e ∘ₗ g') x = g ⟨x, mem⟩

Tactic:
by simpa [LinearEquiv.eq_symm_apply] using h'

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
c : Set (ExtensionOf i f)
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
pf✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ((fun x ↦ x.toLinearPMap) '' c)
pf✝ : i m ∈ (LinearPMap.sSup ((fun x ↦ x.toLinearPMap) '' c) pf✝¹).domain
h1 : i m ∈ hnonempty.some.domain
⊢ ↑(LinearPMap.sSup ((fun x ↦ x.toLinearPMap) '' c) pf✝¹) ⟨i m, pf✝⟩ = ↑hnonempty.some.toLinearPMap ⟨i m, h1⟩

Tactic:
exact
        LinearPMap.sSup_apply (IsChain.directedOn <| chain_linearPMap_of_chain_extensionOf hchain)
          ((Set.mem_image _ _ _).mpr ⟨hnonempty.some, hnonempty.choose_spec, rfl⟩) ⟨i m, h1⟩

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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
a : ↥(extensionOfMax i f).domain
r : R
eq1 : ↑x = ↑a + r • y
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap a + (extendIdealTo i f h y) r

Tactic:
obtain ⟨a, ha⟩ := a
  have eq2 :
    (ExtensionOfMaxAdjoin.fst i x - a : N) = (r - ExtensionOfMaxAdjoin.snd i x) • y := by
    change x = a + r • y at eq1
    rwa [ExtensionOfMaxAdjoin.eqn, ← sub_eq_zero, ← sub_sub_sub_eq, sub_eq_zero, ← sub_smul]
      at eq1
  have eq3 :=
    ExtensionOfMaxAdjoin.extendIdealTo_eq i f h (r - ExtensionOfMaxAdjoin.snd i x)
      (by rw [← eq2]; exact Submodule.sub_mem _ (ExtensionOfMaxAdjoin.fst i x).2 ha)
  simp only [map_sub, sub_smul, sub_eq_iff_eq_add] at eq3
  unfold ExtensionOfMaxAdjoin.extensionToFun
  rw [eq3, ← add_assoc, ← (extensionOfMax i f).toLinearPMap.map_add, AddMemClass.mk_add_mk]
  congr
  ext
  dsimp
  rw [Subtype.coe_mk, add_sub, ← eq1]
  exact eq_sub_of_add_eq (ExtensionOfMaxAdjoin.eqn i x).symm

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ x < p ^ (n + 1), ¬p ∣ x ↔ ∀ (x_1 : ℕ), ¬(x_1 < p ^ n ∧ x_1 * p = x)

Tactic:
intro a ha

Goal state after:
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a ↔ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
h : #({a ∈ insert 0 (Ico (0 + 1) p) | p.Coprime a}) = p - 1
hp : 1 < p
⊢ Prime p

Tactic:
Finset.filter_insert,

Goal state after:
p : ℕ
h : #(if p.Coprime 0 then insert 0 ({a ∈ Ico (0 + 1) p | p.Coprime a}) else {a ∈ Ico (0 + 1) p | p.Coprime a}) = p - 1
hp : 1 < p
⊢ Prime p
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2

Tactic:
by
    have : 3 ≤ n + 3 := le_add_self
    simp only [succ_succ_ne_one, false_or]
    exact ⟨fun h => not_even_one.elim <| h ▸ totient_even this, by rintro ⟨⟩⟩

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
φ : ℕ → ℕ
hφ : StrictMono φ
hrφ : ∀ (m n : ℕ), m < n → r (φ m) (φ n)
⊢ ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)

pp: α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)

Tactic:
· exact ⟨φ, hφ, hrφ, hs.comp_strictMono hφ⟩

Goal state after:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)