mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + ↑(↑i + 1) ≠ 0
⊢ logDeriv (fun z ↦ 1 + sineTerm z i) x = cotTerm x i

Tactic:
have h2 : ((x : ℂ) - (i + 1)) ≠ 0 := by
    simpa [sub_eq_add_neg] using integerComplement_add_ne_zero hx (-(i + 1))

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + ↑(↑i + 1) ≠ 0
h2 : x - (↑i + 1) ≠ 0
⊢ logDeriv (fun z ↦ 1 + sineTerm z i) x = cotTerm x i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + ↑(↑i + 1) ≠ 0
h2 : x - (↑i + 1) ≠ 0
this : x ^ 2 ≠ ↑(↑i + 1) ^ 2
⊢ (↑i + 1) ^ 2 - x ^ 2 ≠ 0

Tactic:
sub_ne_zero

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + ↑(↑i + 1) ≠ 0
h2 : x - (↑i + 1) ≠ 0
this : x ^ 2 ≠ ↑(↑i + 1) ^ 2
⊢ (↑i + 1) ^ 2 ≠ x ^ 2
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ MinFacHelper n k'

Tactic:
rw [← e]
  refine ⟨Nat.lt_add_right _ h.1, ?_, ?_⟩
  · rw [add_mod, mod_self, add_zero, mod_mod]
    exact h.2.1
  rcases h.2.2.eq_or_lt with rfl | h2
  · exact (np rfl).elim
  rcases (succ_le_of_lt h2).eq_or_lt with h2|h2
  · refine ((h.1.trans_le h.2.2).ne ?_).elim
    have h3 : 2 ∣ minFac n := by
      rw [Nat.dvd_iff_mod_eq_zero, ← h2, succ_eq_add_one, add_mod, h.2.1]
    simpa [dvd_prime <| minFac_prime h.one_lt.ne'] using h3
  exact h2

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Icc 0 ↑N)
integrable : IntegrableOn f (Ioi 0) volume
nonneg : ∀ t ∈ Ioi 0, 0 ≤ f t
⊢ ∑ n ∈ Finset.range N, f ↑(n + 1) ≤ ∫ (x : ℝ) in Ioi 0, f x

Tactic:
rw [Finset.range_eq_Ico]

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Icc 0 ↑N)
integrable : IntegrableOn f (Ioi 0) volume
nonneg : ∀ t ∈ Ioi 0, 0 ≤ f t
⊢ ∑ n ∈ Finset.Ico 0 N, f ↑(n + 1) ≤ ∫ (x : ℝ) in Ioi 0, f x
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
⊢ ∑ i ∈ range N with j < c ^ i, 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2

Tactic:
have cpos : 0 < c := zero_lt_one.trans hc

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ ∑ i ∈ range N with j < c ^ i, 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ≤ c ^ 2

Tactic:
simpa using pow_right_mono₀ hc.le one_le_two

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: c : ℝ
hc : 1 < c
i : ℕ
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

Tactic:
have cpos : 0 < c := zero_lt_one.trans hc

Goal state after:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
⊢ ∑ i ∈ range N with j < ↑⌊c ^ i⌋₊, 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2

Tactic:
have cpos : 0 < c := zero_lt_one.trans hc

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ ∑ i ∈ range N with j < ↑⌊c ^ i⌋₊, 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : I ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom ((colimitYonedaHomIsoLimit' D F).hom ≫ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i)) f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }

Tactic:
simp only [colimitYonedaHomIsoLimit', Iso.trans_hom, Category.assoc, HasLimit.isoOfNatIso_hom_π]

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : I ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        ((colimitHomIsoLimitYoneda' (D.leftOp ⋙ yoneda) F).hom ≫
          limit.π ((D.leftOp ⋙ yoneda).rightOp ⋙ yoneda.obj F) i ≫
            ((D ⋙ Prod.sectL Cᵒᵖ F).isoWhiskerLeft (yonedaLemma C)).hom.app i))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X) ↔ IsZero (Ψ.r.obj (Φ.quotient.obj X))

Tactic:
constructor <;> intro h
  · exact IsZero.of_epi_eq_zero ((colonπ Φ Ψ).app X)
      (zero_of_epi_comp ((toColon Φ Ψ).hom.left.app X) (by simp))
  · obtain ⟨inv, hinv⟩ :=
      KernelFork.IsLimit.lift' (Φ.isLimitKernelForkObj X) ((colon Φ Ψ).ι.app X) (by
        rw [colon_ι_app_π_app, h.eq_zero_of_tgt ((colonπ Φ Ψ).app X), zero_comp])
    dsimp at hinv
    refine ⟨inv, ?_, ?_⟩
    · simp [← cancel_mono (Φ.ι.app X), hinv]
    · simp [← cancel_mono ((Φ.colon Ψ).ι.app X), hinv]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ {
        X₁ :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
              ((CochainComplex.single₀ C).obj Z)).X₂,
        X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
        X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
        f :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
              (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
        g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
        zero := ⋯ }.Exact ∧
    Mono
      ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
          (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂

Tactic:
refine (ShortComplex.exact_and_mono_f_iff_of_iso ?_).2
          ⟨exact_f_d (Injective.ι Z), by dsimp; infer_instance⟩
        exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp)
          (by simp [ofCocomplex])

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : Over P
x✝ : f ≈ Over.mk 0
R : C
p : R ⟶ f.left
q : R ⟶ (Over.mk 0).left
w✝¹ : Epi p
w✝ : Epi q
comm : p ≫ f.hom = q ≫ (Over.mk 0).hom
⊢ p ≫ f.hom = 0

Tactic:
by simp [comm]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : Over P
hf : f.hom = 0
⊢ biprod.fst ≫ 0 = biprod.snd ≫ 0

Tactic:
HasZeroMorphisms.comp_zero,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : Over P
hf : f.hom = 0
⊢ 0 = biprod.snd ≫ 0
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield

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✝⁵ : Abelian C
inst✝⁴ : Abelian D
G : D ⥤ C
inst✝³ : PreservesFiniteLimits G
inst✝² : PreservesFiniteColimits G
F : C ⥤ D
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.kernel.isoModSerre = (isomorphisms C).inverseImage G

Tactic:
isoModSerre_kernel_eq_inverseImage_isomorphisms

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✝⁵ : Abelian C
inst✝⁴ : Abelian D
G : D ⥤ C
inst✝³ : PreservesFiniteLimits G
inst✝² : PreservesFiniteColimits G
F : C ⥤ D
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (isomorphisms C).inverseImage G = (isomorphisms C).inverseImage G
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Injective X
⊢ IsZero ((InjectiveResolution.self X).cocomplex.X (n + 1))

Tactic:
apply isZero_zero

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
          ((ShiftedHom.map
                (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
                DerivedCategory.Q).comp
            (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
          ⋯).comp
      (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)) ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm
              (Cocycle.toSingleMk (((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ≫ g) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y')) ⋯)
      ⋯

Tactic:
Cocycle.toSingleMk_postcomp _ _ _ _
      (by simpa [cochainComplex_d _ _ _ m n rfl rfl]) g,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
          ((ShiftedHom.map
                (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
                DerivedCategory.Q).comp
            (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
          ⋯).comp
      (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)) ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm
              ((Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯).postcomp
                ((singleFunctor C 0).map g)))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y')) ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X : C
⊢ IsZero (L.obj X) ↔ P X

Tactic:
by
  simp only [IsZero.iff_id_eq_zero, ← L.map_id, ← L.map_zero,
    MorphismProperty.map_eq_iff_precomp L P.isoModSerre,
    Category.comp_id, comp_zero, exists_prop, exists_eq_right]
  refine ⟨?_, fun _ ↦ ⟨X, by simpa⟩⟩
  rintro ⟨Y, h⟩
  simpa using h.2

Goal state after:
Module: Mathlib.CategoryTheory.Action.Continuous

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁴ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝³ : ConcreteCategory V FV
inst✝² : HasForget₂ V TopCat
G : Type u_4
inst✝¹ : Monoid G
inst✝ : TopologicalSpace G
X : Action V G
g h : G
x : ↑((forget₂ (Action V G) TopCat).obj X)
⊢ (ConcreteCategory.hom ((forget₂ V TopCat).map (X.ρ (g * h)))) x =
    (ConcreteCategory.hom ((forget₂ V TopCat).map (X.ρ h ≫ X.ρ g))) x

Tactic:
map_mul

Goal state after:
V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁴ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝³ : ConcreteCategory V FV
inst✝² : HasForget₂ V TopCat
G : Type u_4
inst✝¹ : Monoid G
inst✝ : TopologicalSpace G
X : Action V G
g h : G
x : ↑((forget₂ (Action V G) TopCat).obj X)
⊢ (ConcreteCategory.hom ((forget₂ V TopCat).map (X.ρ g * X.ρ h))) x =
    (ConcreteCategory.hom ((forget₂ V TopCat).map (X.ρ h ≫ X.ρ g))) x
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F.obj X)ᘁ ◁ 𝟙 (F.obj X) ≫ ε_ (F.obj X) (F.obj X)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ

Tactic:
MonoidalCategory.whiskerLeft_id,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ 𝟙 ((F.obj X)ᘁ ⊗ F.obj X) ≫ ε_ (F.obj X) (F.obj X)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
⊢ PreservesFiniteColimits L

Tactic:
let := abelian L P
  rw [((Functor.preservesFiniteColimits_tfae L).out 3 2 :)]
  intro _ _ f
  exact preservesCokernel L P f

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
f : Y ⟶ U'.obj (F.obj X)
⊢ f ≫
        adj₂.unit.app (U'.1 (F.obj X)) ≫
          U'.map (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X)))) =
      f ≫ U'.map (F.map (adj₁.unit.app X)) ↔
    (adj₂.homEquiv Y (F.obj (U.obj (F.obj X))))
        (F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((adj₂.homEquiv Y (F.obj X)).symm f))) =
      (adj₂.homEquiv Y (F.obj (U.obj (F.obj X))))
        ((adj₂.homEquiv Y (F.obj ((F ⋙ U).obj X))).symm (f ≫ U'.map (F.map (adj₁.unit.app X))))

Tactic:
adj₂.homEquiv_unit,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
f : Y ⟶ U'.obj (F.obj X)
⊢ f ≫
        adj₂.unit.app (U'.1 (F.obj X)) ≫
          U'.map (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X)))) =
      f ≫ U'.map (F.map (adj₁.unit.app X)) ↔
    adj₂.unit.app Y ≫ U'.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((adj₂.homEquiv Y (F.obj X)).symm f))) =
      (adj₂.homEquiv Y (F.obj (U.obj (F.obj X))))
        ((adj₂.homEquiv Y (F.obj ((F ⋙ U).obj X))).symm (f ≫ U'.map (F.map (adj₁.unit.app X))))
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X)))) ≫
        (R ⋙ U).map f ≫ (adj₂.homEquiv ((R ⋙ U).obj Y) Y) (adj₂.counit.app Y) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj ((𝟭 B).obj X)) Y) f ↔
    U.map (F.map ((adj₂.homEquiv (U.obj X) Y) f) ≫ adj₁.counit.app (R.obj Y)) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) f

Tactic:
adj₂.homEquiv_unit,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X)))) ≫
        (R ⋙ U).map f ≫ adj₂.unit.app ((R ⋙ U).obj Y) ≫ (R ⋙ U).map (adj₂.counit.app Y) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj ((𝟭 B).obj X)) Y) f ↔
    U.map (F.map ((adj₂.homEquiv (U.obj X) Y) f) ≫ adj₁.counit.app (R.obj Y)) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) f
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (λ_ (𝟙_ V)).inv ≫
      (eHomEquiv V) f ▷ 𝟙_ V ≫
        (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
          (eHomWhiskerRight V α.inv Y ▷ Y ⟶[V] Z) ≫
            (eHomWhiskerLeft V X₁ β.hom ▷ Y ⟶[V] Z) ≫
              (X₁ ⟶[V] Y₁) ◁ eHomWhiskerRight V β.inv Z ≫ eComp V X₁ Y₁ Z ≫ eHomWhiskerLeft V X₁ γ.hom

Tactic:
eHom_whisker_cancel_assoc,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (λ_ (𝟙_ V)).inv ≫
      (eHomEquiv V) f ▷ 𝟙_ V ≫
        (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
          (eHomWhiskerRight V α.inv Y ▷ Y ⟶[V] Z) ≫ eComp V X₁ Y Z ≫ eHomWhiskerLeft V X₁ γ.hom
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst✝ : p.IsHomLift (𝟙 S) φ'.hom
⊢ ∀ {a' : 𝒳} (φ'_1 : a' ⟶ b') [p.IsHomLift f φ'_1], ∃! χ, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ ≫ φ'.hom = φ'_1

Tactic:
intro c

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst✝ : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
⊢ ∀ (φ'_1 : c ⟶ b') [p.IsHomLift f φ'_1], ∃! χ, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ ≫ φ'.hom = φ'_1
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ≅ S
φ : a ≅ b
inst✝ : p.IsHomLift f.hom φ.hom
⊢ p.IsHomLift f.inv φ.inv

Tactic:
apply of_commSq
  apply CommSq.horiz_inv (f := p.mapIso φ) (commSq p f.hom φ.hom)

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst✝ : p.IsHomLift (𝟙 R) φ'.hom
⊢ ∀ {a'_1 : 𝒳} (φ'_1 : a'_1 ⟶ b) [p.IsHomLift f φ'_1], ∃! χ, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = φ'_1

Tactic:
intro c

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst✝ : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
⊢ ∀ (φ'_1 : c ⟶ b) [p.IsHomLift f φ'_1], ∃! χ, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = φ'_1
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
⊢ ∀ (y : a' ⟶ a), (fun χ ↦ p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ) y → y = map p f φ ⋯ (map p g ψ ⋯ τ)

Tactic:
intro π' ⟨hπ'₁, hπ'₂⟩

Goal state after:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
π' : a' ⟶ a
hπ'₁ : p.IsHomLift h π'
hπ'₂ : π' ≫ φ ≫ ψ = τ
⊢ π' = map p f φ ⋯ (map p g ψ ⋯ τ)
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ ∀ (y : a' ⟶ a), (fun χ ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ)

Tactic:
intro π' ⟨hπ'₁, hπ'₂⟩

Goal state after:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
π' : a' ⟶ a
hπ'₁ : p.IsHomLift h π'
hπ'₂ : π' ≫ φ = τ
⊢ π' = map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ)
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
⊢ ∀ {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [p.IsHomLift (g ≫ f) φ'], ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
intro c

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
c : 𝒳
⊢ ∀ (g : p.obj c ⟶ R) (φ' : c ⟶ b) [p.IsHomLift (g ≫ f) φ'], ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
⊢ p.IsStronglyCartesian f φ

Tactic:
by
  constructor
  intro c g φ' hφ'
  subst_hom_lift p f φ; clear a b R S
  -- Let `ψ` be a Cartesian arrow lying over `g`
  obtain ⟨a', ψ, hψ⟩ := h _ _ (p.map φ)
  -- Let `τ' : c ⟶ a'` be the map induced by the universal property of `ψ`
  let τ' := IsStronglyCartesian.map p (p.map φ) ψ (f' := g ≫ p.map φ) rfl φ'
  -- Let `Φ : a' ≅ a` be natural isomorphism induced between `φ` and `ψ`.
  let Φ := domainUniqueUpToIso p (p.map φ) φ ψ
  -- The map induced by `φ` will be `τ' ≫ Φ.hom`
  use τ' ≫ Φ.hom
  -- It is easily verified that `τ' ≫ Φ.hom` lifts `g` and `τ' ≫ Φ.hom ≫ φ = φ'`
  refine ⟨⟨by simp only [Φ]; infer_instance, ?_⟩, ?_⟩
  · simp [τ', Φ]
  -- It remains to check that it is unique. This follows from the universal property of `ψ`.
  intro π ⟨hπ, hπ_comp⟩
  rw [← Iso.comp_inv_eq]
  apply IsStronglyCartesian.map_uniq p (p.map φ) ψ rfl φ'
  simp [hπ_comp, Φ]

Goal state after: