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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯
wι : kernel.ι (cokernel.π γ) ≫ g' = 0
e : cokernel γ ≅ Abelian.coimage S.g :=
  (colimit.isColimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0)).coconePointUniqueUpToIso
    S.cokernelToAbelianCoimageIsCokernel
he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage
fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g
W'✝ : C
x : W'✝ ⟶ cokernel S.f
hx : x ≫ g' = 0
b : W'✝ ⟶ kernel (cokernel.π γ)
hb : b ≫ kernel.ι (cokernel.π γ) = x
⊢ b ≫ equalizer.ι (cokernel.π γ) 0 = kernel.lift (cokernel.π γ) x ⋯ ≫ equalizer.ι (cokernel.π γ) 0

Tactic:
simp only [hb, kernel.lift_ι]

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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ φ₁.τ₃ + φ₃.τ₃ = h.h₃ + h'.h₃ + (h.h₂ + h'.h₂) ≫ S₂.g + (φ₂.τ₃ + φ₄.τ₃)

Tactic:
h.comm₃,

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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ + φ₃.τ₃ = h.h₃ + h'.h₃ + (h.h₂ + h'.h₂) ≫ S₂.g + (φ₂.τ₃ + φ₄.τ₃)
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₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ (S₁.mapHomologyIso F).hom ≫ F.map (homologyMap φ) ≫ (S₂.mapHomologyIso F).inv =
    (S₁.mapHomologyIso F).hom ≫ (S₁.mapHomologyIso F).inv ≫ homologyMap (F.mapShortComplex.map φ)

Tactic:
← mapHomologyIso_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₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapHomologyIso F).hom ≫ (S₂.mapHomologyIso F).inv =
    (S₁.mapHomologyIso F).hom ≫ (S₁.mapHomologyIso F).inv ≫ homologyMap (F.mapShortComplex.map φ)
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 φ₃ φ₄
⊢ φ₁.τ₃ - φ₃.τ₃ = h.h₃ - h'.h₃ + (h.h₂ - h'.h₂) ≫ S₂.g + (φ₂.τ₃ - φ₄.τ₃)

Tactic:
h.comm₃,

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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ - φ₃.τ₃ = h.h₃ - h'.h₃ + (h.h₂ - h'.h₂) ≫ S₂.g + (φ₂.τ₃ - φ₄.τ₃)
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 φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ (ψ ≫ φ₁).τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃

Tactic:
comp_τ₃,

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 : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
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 φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃

Tactic:
comp_τ₃,

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 : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
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 φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₃ ≫ φ₁.τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃

Tactic:
h.comm₃,

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 : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₃ ≫ (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
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 φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ (φ₁ ≫ ψ).τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃

Tactic:
comp_τ₃,

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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
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 φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃

Tactic:
comp_τ₃,

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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
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 φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃

Tactic:
h.comm₃,

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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
Module: Mathlib.CategoryTheory.Subobject.MonoOver

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✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ («exists» f).obj Z ≅ (map f).obj Z

Tactic:
suffices (forget _).obj ((«exists» f).obj Z) ≅ (forget _).obj ((map f).obj Z) by
      apply (forget _).preimageIso this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ (forget Y).obj ((«exists» f).obj Z) ≅ (forget Y).obj ((map f).obj Z)
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
F : C ⥤ D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.PreservesHomology
X Y : C
f : X ⟶ Y
hf : Mono f
S : ShortComplex C := { X₁ := X, X₂ := X, X₃ := Y, f := 0, g := f, zero := ⋯ }
⊢ (S.map F).f = 0

Tactic:
simp [S]

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
F : C ⥤ D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.PreservesHomology
X Y : C
f : X ⟶ Y
hf : Epi f
S : ShortComplex C := { X₁ := X, X₂ := Y, X₃ := Y, f := f, g := 0, zero := ⋯ }
⊢ (S.map F).g = 0

Tactic:
simp [S]

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

Goal state before:
pp: case insert.inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
m : i✝ ∈ s✝
⊢ (P i✝).Factors (P a✝¹ ⊓ s✝.inf P).arrow

Tactic:
rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]

Goal state after:
case insert.inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
m : i✝ ∈ s✝
⊢ (P i✝).Factors ((s✝.inf P).factorThru (P a✝¹ ⊓ s✝.inf P).arrow ⋯ ≫ (s✝.inf P).arrow)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj f = underlying.obj ((equivShrink (Subobject A)).symm ↑⟨(equivShrink (Subobject A)) f, ⋯⟩)

Tactic:
exact (congr_arg (fun X : Subobject A => (X : C)) (Equiv.symm_apply_apply _ _).symm)

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.HasLeftKanExtension F
G : D ⥤ H
⊢ L.lanUnit.app (L ⋙ G) ≫ L.whiskerLeft ((L.lanAdjunction H).counit.app G) = 𝟙 (L ⋙ G)

Tactic:
simp [lanAdjunction_counit_app]

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

Goal state before:
pp: case mp
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
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
⊢ F''.IsLeftKanExtension α' → IsIso φ

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
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
⊢ IsIso φ → F''.IsLeftKanExtension α'

Tactic:
· intro
    rw [F'.hom_ext_of_isLeftKanExtension α φ (leftKanExtensionUnique _ α _ α').hom
      (by simp [comm])]
    infer_instance

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
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
⊢ IsIso φ → F''.IsLeftKanExtension α'
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
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
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : F ⟶ L ⋙ F'
⊢ F'.IsLeftKanExtension α ↔ F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv)

Tactic:
let eq : (LeftExtension.mk _ α).IsUniversal ≃ (LeftExtension.mk _
      (whiskerLeft G α ≫ (associator _ _ _).inv)).IsUniversal :=
    (LeftExtension.isUniversalPrecompEquiv L F G _).trans
    (IsInitial.equivOfIso (StructuredArrow.isoMk (Iso.refl _)))
  constructor
  · exact fun _ => ⟨⟨eq (isUniversalOfIsLeftKanExtension _ _)⟩⟩
  · exact fun _ => ⟨⟨eq.symm (isUniversalOfIsLeftKanExtension _ _)⟩⟩

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₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
⊢ StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ ((whiskeringLeft C D' H).obj (L ⋙ L')).map (hb.desc u) =
    StructuredArrow.hom y

Tactic:
by
          ext x
          have hb_fac_app := congr_app (hb.fac u) (L.obj x)
          have hα_fac_app :=
            congr_app (hα.fac <| LeftExtension.mk _ <|
              y.hom ≫ (L.associator L' y.right).hom) x
          dsimp at hα_fac_app hb_fac_app
          simp [hb_fac_app, u, hα_fac_app]

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

Goal state before:
pp: J : Type w
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | none => Arrow.mk (𝟙 zero)
      | some none => Arrow.mk (𝟙 one)
      | some (some t) => Arrow.mk (line t))
    fun f ↦
    match f.left, f.right, f.hom with
    | zero, .(zero), Hom.id .(zero) => none
    | one, .(one), Hom.id .(one) => some none
    | zero, one, line t => some (some t)

Tactic:
rintro (_ | (_ | _))

Goal state after:
case none
J : Type w
⊢ (fun f ↦
        match f.left, f.right, f.hom with
        | zero, .(zero), Hom.id .(zero) => none
        | one, .(one), Hom.id .(one) => some none
        | zero, one, line t => some (some t))
      ((fun x ↦
          match x with
          | none => Arrow.mk (𝟙 zero)
          | some none => Arrow.mk (𝟙 one)
          | some (some t) => Arrow.mk (line t))
        none) =
    none

case some.none
J : Type w
⊢ (fun f ↦
        match f.left, f.right, f.hom with
        | zero, .(zero), Hom.id .(zero) => none
        | one, .(one), Hom.id .(one) => some none
        | zero, one, line t => some (some t))
      ((fun x ↦
          match x with
          | none => Arrow.mk (𝟙 zero)
          | some none => Arrow.mk (𝟙 one)
          | some (some t) => Arrow.mk (line t))
        (some none)) =
    some none

case some.some
J : Type w
val✝ : J
⊢ (fun f ↦
        match f.left, f.right, f.hom with
        | zero, .(zero), Hom.id .(zero) => none
        | one, .(one), Hom.id .(one) => some none
        | zero, one, line t => some (some t))
      ((fun x ↦
          match x with
          | none => Arrow.mk (𝟙 zero)
          | some none => Arrow.mk (𝟙 one)
          | some (some t) => Arrow.mk (line t))
        (some (some val✝))) =
    some (some val✝)
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
⊢ IsColimit (coconeπOpCompShrinkYonedaObj F X)

Tactic:
refine Nonempty.some ((Types.isColimit_iff_coconeTypesIsColimit _).2
    ⟨?_, fun x ↦ ?_⟩)

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
⊢ Function.Injective
    (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X)))

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
x :
  (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
      (coconeπOpCompShrinkYonedaObj F X)).pt
⊢ ∃ a,
    ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
        (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
          (coconeπOpCompShrinkYonedaObj F X))
        a =
      x
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
i j : C
f : { as := i } ⟶ { as := j }
⊢ i = j

Tactic:
simpa using Discrete.eq_of_hom f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case left
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
⊢ Function.Injective ((Discrete.functor F).descColimitType c)

pp: case right
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
⊢ Function.Surjective ((Discrete.functor F).descColimitType c)

Tactic:
· intro x y h
      obtain ⟨⟨i⟩, x, rfl⟩ := (Discrete.functor F).ιColimitType_jointly_surjective x
      obtain ⟨⟨j⟩, y, rfl⟩ := (Discrete.functor F).ιColimitType_jointly_surjective y
      obtain rfl := h₃ _ _ _ _ h
      obtain rfl := h₂ _ h
      rfl

Goal state after:
case right
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
⊢ Function.Surjective ((Discrete.functor F).descColimitType c)
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: case neg
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : Nonempty X
hf : Function.Injective ⇑(ConcreteCategory.hom f)
g : (fun X ↦ X) Y → (fun X ↦ X) X
hg : Function.LeftInverse g ⇑(ConcreteCategory.hom f)
⊢ Mono (free.map f)

Tactic:
have : IsSplitMono f := IsSplitMono.mk' { retraction := ↾g }

Goal state after:
case neg
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : Nonempty X
hf : Function.Injective ⇑(ConcreteCategory.hom f)
g : (fun X ↦ X) Y → (fun X ↦ X) X
hg : Function.LeftInverse g ⇑(ConcreteCategory.hom f)
this : IsSplitMono f
⊢ Mono (free.map f)
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
i j : C
f : { as := i } ⟶ { as := j }
⊢ i = j

Tactic:
simpa using Discrete.eq_of_hom f

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

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

Tactic:
rw [negOnePow_even _ h'] at h

Goal state after:
case mp
n : ℤ
h : 1 = -1
h' : Even n
⊢ False
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddGroup α
h : Periodic f c
x : α ⧸ AddSubgroup.zmultiples c
a b : α
h' : (QuotientAddGroup.leftRel (AddSubgroup.zmultiples c)) a b
⊢ f a = f b

Tactic:
by
    rw [QuotientAddGroup.leftRel_apply] at h'
    obtain ⟨k, hk⟩ := h'
    exact (h.zsmul k _).symm.trans (congr_arg f (add_eq_of_eq_neg_add hk))

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
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
r : R
x : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨r • x, ⋯⟩ = (RingHom.id R) r • ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩

Tactic:
rw [← LinearPMap.map_smul]

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
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
r : R
x : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨r • x, ⋯⟩ = ↑(extensionOfMax f g).toLinearPMap ((RingHom.id R) r • ⟨x, ⋯⟩)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
e : ↑{m | m < n ∧ n.Coprime m} ≃ ↥({x ∈ range n | n.Coprime x}) :=
  { toFun := fun m ↦ ⟨↑m, ⋯⟩, invFun := fun m ↦ ⟨↑m, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ φ n = Nat.card ↑{m | m < n ∧ n.Coprime m}

Tactic:
totient_eq_card_coprime,

Goal state after:
n : ℕ
e : ↑{m | m < n ∧ n.Coprime m} ≃ ↥({x ∈ range n | n.Coprime x}) :=
  { toFun := fun m ↦ ⟨↑m, ⋯⟩, invFun := fun m ↦ ⟨↑m, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ #({a ∈ range n | n.Coprime a}) = Nat.card ↑{m | m < n ∧ n.Coprime m}
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a → ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)

Tactic:
intro hap b h; rcases h with ⟨_, rfl⟩
            exact hap (dvd_mul_left _ _)

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

Goal state before:
pp: p : ℕ
h : φ p = p - 1
hp : 1 < p
⊢ Prime p

Tactic:
totient_eq_card_coprime,

Goal state after:
p : ℕ
h : #({a ∈ range p | p.Coprime a}) = p - 1
hp : 1 < p
⊢ Prime p
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg.refine_1
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ φ a < φ (a * p)

Tactic:
rw [mul_comm, totient_mul_of_prime_of_dvd hp hap, Nat.lt_mul_iff_one_lt_left]

Goal state after:
case neg.refine_1
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ 1 < p

case neg.refine_1
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ 0 < φ a
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier s = closure s ∩ closure sᶜ

Tactic:
rw [closure_compl, frontier, sdiff_eq]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier s ⊆ s ↔ IsClosed s

Tactic:
by
  rw [frontier, sdiff_subset_iff, union_eq_right.mpr interior_subset, closure_subset_iff_isClosed]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Tactic:
simp_rw [isClosed_iff_clusterPt]
  exact ⟨fun hs x F F_ne FS Fx ↦ hs _ <| NeBot.mono F_ne (le_inf Fx FS),
         fun hs x hx ↦ hs x (𝓝 x ⊓ 𝓟 s) hx inf_le_right inf_le_left⟩

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ 𝓝ˢ s = 𝓟 s ↔ IsOpen[inst✝] s

Tactic:
rw [← principal_le_nhdsSet.ge_iff_eq', le_principal_iff, mem_nhdsSet_iff_forall,
    isOpen_iff_mem_nhds]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case basic
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ : Set α
hs : s✝ ∈ g
ha : a ∈ s✝
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 s✝

Tactic:
| basic _ hs =>

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X✝ : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s : Set (Set X)
h : ∀ t ∈ s, t.Nonempty → tᶜ.Finite
x : X
t : Set X
hts : t ∈ s
hzt : x ∈ t
⊢ (⋂₀ (compl '' s)).Finite

Tactic:
exact Finite.sInter (mem_image_of_mem _ hts) (h t hts ⟨x, hzt⟩)

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : s ∈ 𝓝 x
⊢ ContinuousWithinAt f s x ↔ ContinuousAt f x

Tactic:
by
  rw [← univ_inter s, continuousWithinAt_inter h, continuousWithinAt_univ]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
⊢ range Subtype.val ∈ 𝓝 ↑⟨x, hx⟩

Tactic:
by rw [Subtype.range_val]; exact h

Goal state after: