mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit (KernelFork.ofι 0 ⋯)
Z✝ : C
u v : Z✝ ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : w ≫ coequalizer.π u v = 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
⊢ w ≫ f = 0

Tactic:
← hm,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit (KernelFork.ofι 0 ⋯)
Z✝ : C
u v : Z✝ ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : w ≫ coequalizer.π u v = 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
⊢ w ≫ coequalizer.π u v ≫ m = 0
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ b • ↑(Hom.hom f).range = ↑(Hom.hom f).range

Tactic:
show (f.hom.range : Set B) = (1 : B) • f.hom.range from (one_leftCoset _).symm

Goal state after:
A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ b • ↑(Hom.hom f).range = 1 • ↑(Hom.hom f).range
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : b • ↑(Hom.hom f).range = ↑(Hom.hom f).range
⊢ False

Tactic:
show (f.hom.range : Set B) = (1 : B) • f.hom.range from (one_leftCoset _).symm

Goal state after:
A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : b • ↑(Hom.hom f).range = 1 • ↑(Hom.hom f).range
⊢ False
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
h : HomologyMapData φ h₁ h₂
⊢ h.left.φH ≫ h₂.iso.hom = h₁.iso.hom ≫ h.right.φH

Tactic:
simp only [← cancel_epi h₁.left.π, ← cancel_mono h₂.right.ι, assoc,
    LeftHomologyMapData.commπ_assoc, HomologyData.comm, LeftHomologyMapData.commi_assoc,
    RightHomologyMapData.commι, HomologyData.comm_assoc, RightHomologyMapData.commp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ ∀ (a b : HomologyMapData φ h₁ h₂), a = b

Tactic:
rintro ⟨left₁, right₁⟩ ⟨left₂, right₂⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
left₁ : LeftHomologyMapData φ h₁.left h₂.left
right₁ : RightHomologyMapData φ h₁.right h₂.right
left₂ : LeftHomologyMapData φ h₁.left h₂.left
right₂ : RightHomologyMapData φ h₁.right h₂.right
⊢ { left := left₁, right := right₁ } = { left := left₂, right := right₂ }
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
⊢ h₁.i ≫ S₁.g ≫ φ.τ₃ = 0

Tactic:
h₁.wi_assoc,

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
⊢ 0 ≫ φ.τ₃ = 0
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₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃

Tactic:
rw [γ₁.leftHomologyMap'_eq, γ₂.leftHomologyMap'_eq, (γ₁.comp γ₂).leftHomologyMap'_eq,
    LeftHomologyMapData.comp_φH]

Goal state after:
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 Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ ∀ (j : WalkingParallelPair),
    ((Cone.postcompose (parallelPair.ext eQ.symm (Iso.refl S.X₃) ⋯ ⋯).hom).obj (KernelFork.ofι h.ι ⋯)).π.app j =
      eH.symm.hom ≫ (KernelFork.ofι (eH.hom ≫ h.ι ≫ eQ.inv) ⋯).π.app j

Tactic:
by rintro (_ | _) <;> simp [IsCokernel.cokernelIso]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : Epi φ.τ₁
h₂ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
⊢ IsIso (homologyMap φ)

Tactic:
by
  dsimp only [homologyMap]
  infer_instance

Goal state after:
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₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ (leftHomologyMap' φ h₁ h₂).op = rightHomologyMap' (opMap φ) h₂.op h₁.op

Tactic:
let γ : LeftHomologyMapData φ h₁ h₂ := leftHomologyMapData φ h₁ h₂
  simp only [γ.leftHomologyMap'_eq, γ.op.rightHomologyMap'_eq,
    LeftHomologyMapData.op_φH]

Goal state after:
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₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
⊢ F.map γ.φQ = opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

Tactic:
(γ.map F).opcyclesMap'_eq,

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₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
⊢ F.map γ.φQ = (γ.map F).φQ
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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ (φ₁ + φ₃).τ₁ = S₁.f ≫ (h.h₁ + h'.h₁) + (h.h₀ + h'.h₀) + (φ₂ + φ₄).τ₁

Tactic:
by rw [add_τ₁, add_τ₁, h.comm₁, h'.comm₁, comp_add]; abel

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.PreservesMonomorphisms
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ ∃ h, g ≫ h = f

Tactic:
use adj.unit.app Y ≫ G.map w

Goal state after:
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.PreservesMonomorphisms
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ g ≫ adj.unit.app Y ≫ G.map w = f
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
⊢ Mono φ.τ₂

Tactic:
by
  rw [mono_iff_cancel_zero]
  intro A x₂ hx₂
  obtain ⟨x₁, hx₁⟩ : ∃ x₁, x₁ ≫ S₁.f = x₂ := ⟨_, h₁.lift_f x₂
    (by simp only [← cancel_mono φ.τ₃, assoc, zero_comp, ← φ.comm₂₃, reassoc_of% hx₂])⟩
  suffices x₁ = 0 by rw [← hx₁, this, zero_comp]
  simp only [← cancel_mono φ.τ₁, ← cancel_mono S₂.f, assoc, φ.comm₁₂, zero_comp,
    reassoc_of% hx₁, hx₂]

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

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
⊢ Epi φ.τ₂

Tactic:
have : Mono S₁.op.f := by dsimp; infer_instance
  have : Mono S₂.op.f := by dsimp; infer_instance
  have : Mono (opMap φ).τ₁ := by dsimp; infer_instance
  have : Mono (opMap φ).τ₃ := by dsimp; infer_instance
  have := mono_τ₂_of_exact_of_mono (opMap φ) h₂.op
  exact unop_epi_of_mono (opMap φ).τ₂

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasPullbacks C
f : X ⟶ Y
y : Subobject Y
⊢ ∃ φ, IsPullback φ ((pullback f).obj y).arrow y.arrow f

Tactic:
obtain ⟨A, i, ⟨_, rfl⟩⟩ := mk_surjective y

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasPullbacks C
f : X ⟶ Y
A : C
i : A ⟶ Y
w✝ : Mono i
⊢ ∃ φ, IsPullback φ ((pullback f).obj (mk i)).arrow (mk i).arrow f
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ≈ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)

Tactic:
apply ThinSkeleton.equiv_of_both_ways

Goal state after:
case f
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ⟶ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)

case g
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (MonoOver.pullback k).obj ((MonoOver.map h).obj a) ⟶ (MonoOver.map g).obj ((MonoOver.pullback f).obj a)
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasColimitsOfShape (Discrete α) C
X✝ Y✝ : Discrete α ⥤ C
β : X✝ ⟶ Y✝
J : Finset (Discrete α)
⊢ colimit.ι ((liftToFinset C α).obj X✝) J ≫
      colimMap ((liftToFinset C α).map β) ≫ (colimit.isoColimitCocone (liftToFinsetColimitCocone Y✝)).inv =
    colimit.ι ((liftToFinset C α).obj X✝) J ≫ (colimit.isoColimitCocone (liftToFinsetColimitCocone X✝)).inv ≫ colimMap β

Tactic:
simp only [liftToFinset_obj_obj]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasColimitsOfShape (Discrete α) C
X✝ Y✝ : Discrete α ⥤ C
β : X✝ ⟶ Y✝
J : Finset (Discrete α)
⊢ colimit.ι ((liftToFinset C α).obj X✝) J ≫
      colimMap ((liftToFinset C α).map β) ≫ (colimit.isoColimitCocone (liftToFinsetColimitCocone Y✝)).inv =
    colimit.ι ((liftToFinset C α).obj X✝) J ≫ (colimit.isoColimitCocone (liftToFinsetColimitCocone X✝)).inv ≫ colimMap β
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.HasPointwiseLeftKanExtensionAt F Y
Φ : CostructuredArrow L Y ⥤ CostructuredArrow (L ⋙ E.functor) (E.functor.obj Y) := CostructuredArrow.post L E.functor Y
⊢ (L ⋙ E.functor).HasPointwiseLeftKanExtensionAt F (E.functor.obj Y)

Tactic:
have : HasColimit ((asEquivalence Φ).functor ⋙
    CostructuredArrow.proj (L ⋙ E.functor) (E.functor.obj Y) ⋙ F) :=
    (inferInstance : HasPointwiseLeftKanExtensionAt L F Y)

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.HasPointwiseLeftKanExtensionAt F Y
Φ : CostructuredArrow L Y ⥤ CostructuredArrow (L ⋙ E.functor) (E.functor.obj Y) := CostructuredArrow.post L E.functor Y
this : HasColimit (Φ.asEquivalence.functor ⋙ CostructuredArrow.proj (L ⋙ E.functor) (E.functor.obj Y) ⋙ F)
⊢ (L ⋙ E.functor).HasPointwiseLeftKanExtensionAt F (E.functor.obj 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)
m : (coconeOfRepresentable P).pt ⟶ s.pt
hm : ∀ (j : P.Elementsᵒᵖ), uliftYonedaEquiv.symm (unop j).snd ≫ m = s.ι.app j
X : Cᵒᵖ
x : (coconeOfRepresentable P).pt.obj X
⊢ (hom (m.app X)) x = uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x)))

Tactic:
← hm,

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)
m : (coconeOfRepresentable P).pt ⟶ s.pt
hm : ∀ (j : P.Elementsᵒᵖ), uliftYonedaEquiv.symm (unop j).snd ≫ m = s.ι.app j
X : Cᵒᵖ
x : (coconeOfRepresentable P).pt.obj X
⊢ (hom (m.app X)) x = uliftYonedaEquiv (uliftYonedaEquiv.symm (unop (op (P.elementsMk X x))).snd ≫ m)
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
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
eq : f ≫ F.op.lanUnit.app Q = F.op.lanUnit.app P ≫ F.op.whiskerLeft (F.op.lan.map f)
⊢ F.op.lanUnit.app P ≫
      F.op.whiskerLeft (F.op.lan.map f) ≫
        F.op.whiskerLeft ((F.op.lan.obj Q).descOfIsLeftKanExtension (F.op.lanUnit.app Q) (G.obj Q) (presheafHom φ Q)) =
    F.op.lanUnit.app P ≫
      F.op.whiskerLeft ((F.op.lan.obj P).descOfIsLeftKanExtension (F.op.lanUnit.app P) (G.obj P) (presheafHom φ P)) ≫
        F.op.whiskerLeft (G.map f)

Tactic:
Functor.descOfIsLeftKanExtension_fac_assoc,

Goal state after:
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
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
eq : f ≫ F.op.lanUnit.app Q = F.op.lanUnit.app P ≫ F.op.whiskerLeft (F.op.lan.map f)
⊢ F.op.lanUnit.app P ≫
      F.op.whiskerLeft (F.op.lan.map f) ≫
        F.op.whiskerLeft ((F.op.lan.obj Q).descOfIsLeftKanExtension (F.op.lanUnit.app Q) (G.obj Q) (presheafHom φ Q)) =
    presheafHom φ P ≫ F.op.whiskerLeft (G.map f)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
⊢ (fun h' ↦ h' ≫ P.ofLE Q h₁ = f) (P.factorThru (f ≫ Q.arrow) this)

pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
g : G ⟶ underlying.obj P
hg : g ≫ P.ofLE Q h₁ = f
⊢ g = P.factorThru (f ≫ Q.arrow) this

Tactic:
· simp only [← cancel_mono Q.arrow, Category.assoc, ofLE_arrow, factorThru_arrow]

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
g : G ⟶ underlying.obj P
hg : g ≫ P.ofLE Q h₁ = f
⊢ g = P.factorThru (f ≫ Q.arrow) this
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
⊢ P = Q

Tactic:
by
  suffices IsIso (ofLE _ _ h₁) by exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp))
  refine h𝒢 _ fun G hG f => ?_
  have : P.Factors (f ≫ Q.arrow) := h₂ _ hG ((factors_iff _ _).2 ⟨_, rfl⟩)
  refine ⟨factorThru _ _ this, ?_, fun g (hg : g ≫ _ = f) => ?_⟩
  · simp only [← cancel_mono Q.arrow, Category.assoc, ofLE_arrow, factorThru_arrow]
  · simp only [← cancel_mono (Subobject.ofLE _ _ h₁), ← cancel_mono Q.arrow, hg, Category.assoc,
      ofLE_arrow, factorThru_arrow]

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)
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ ↑(extensionOfMax i f).domain
b : N
eq1 : (fun x1 x2 ↦ x1 + x2) a b = ↑x
z : R
eq2 : z • y = b
⊢ (fun x1 x2 ↦ x1 + x2) a b = ↑⟨a, a_mem⟩ + z • y

Tactic:
← eq2

Goal state after:
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)
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ ↑(extensionOfMax i f).domain
b : N
eq1 : (fun x1 x2 ↦ x1 + x2) a b = ↑x
z : R
eq2 : z • y = b
⊢ (fun x1 x2 ↦ x1 + x2) a (z • y) = ↑⟨a, a_mem⟩ + z • y
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)
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
⊢ (r - snd i x) • ?m.277 ∈ (extensionOfMax i f).domain

Tactic:
← eq2

Goal state after:
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
⊢ ↑(fst i x) - a ∈ (extensionOfMax i f).domain
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : Small.{v, u} R
S : Type u'
inst✝⁴ : Ring S
M : Type v
N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inj : Injective R M
⊢ Injective S N

Tactic:
apply Module.Baer.injective (fun I g ↦ ?_)

Goal state after:
R : Type u
inst✝⁶ : Ring R
inst✝⁵ : Small.{v, u} R
S : Type u'
inst✝⁴ : Ring S
M : Type v
N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
⊢ ∃ g', ∀ (x : S) (mem : x ∈ I), g' x = g ⟨x, mem⟩
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α₁ : Type u_6
α₂ : Type u_7
β₁ : Type u_8
β₂ : Type u_9
inst✝¹ : Preorder β₁
inst✝ : Preorder β₂
u₁ : β₁ → α₁
u₂ : β₂ → α₂
⊢ map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop

Tactic:
rw [prod_map_map_eq, prod_atTop_atTop_eq, Prod.map_def]

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
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)

Tactic:
rcases seq_of_forall_finite_exists fun t ht => (this t ht).exists with ⟨φ, 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
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n
φ : ℕ → ℕ
hφ : ∀ (n m : ℕ), m ∈ φ '' Iio n → m < φ n ∧ r m (φ n)
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
H : ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l
s : Set β
hs : s ∈ l
⊢ s ∈ map f k

Tactic:
contrapose! H

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι : Type u_3
g : Filter ι
inst✝¹ : g.IsCountablyGenerated
u : ι → α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : (f ⊓ map u g).NeBot
⊢ ∃ θ, Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f

Tactic:
rw [← Filter.push_pull', map_neBot_iff] at hx
  obtain ⟨θ, hθ⟩ := exists_seq_tendsto (comap u f ⊓ g)
  exact ⟨θ, (tendsto_inf.1 hθ).2, tendsto_comap_iff.1 (tendsto_inf.1 hθ).1⟩

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIcoMod hp a b = toIcoDiv hp a b • p

Tactic:
rw [toIcoMod, sub_sub_cancel]

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
t : Set Y
⊢ closure[inst✝¹] (f ⁻¹' t) ⊆ f ⁻¹' closure[inst✝] t

Tactic:
rw [← (isClosed_closure.preimage hf).closure_eq]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
t : Set Y
⊢ closure[inst✝¹] (f ⁻¹' t) ⊆ closure[inst✝¹] (f ⁻¹' closure[inst✝] t)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = b ↔ b ∈ Set.Ioc a (a + p)

Tactic:
rw [toIocMod_eq_iff, and_iff_left]
  exact ⟨0, by simp⟩

Goal state after: