mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
⊢ ∀ᶠ (p : ℕ) in atTop, u p / ↑p < L

Tactic:
refine .atTop_of_arithmetic hn fun r _ => ?_
  /- `(k * u n + u r) / (k * n + r)` tends to `u n / n < L`, hence
  `(k * u n + u r) / (k * n + r) < L` for sufficiently large `k`. -/
  have A : Tendsto (fun x : ℝ => (u n + u r / x) / (n + r / x)) atTop (𝓝 ((u n + 0) / (n + 0))) :=
    (tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id).div
      (tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id) <| by simpa
  have B : Tendsto (fun x => (x * u n + u r) / (x * n + r)) atTop (𝓝 (u n / n)) := by
    rw [add_zero, add_zero] at A
    refine A.congr' <| (eventually_ne_atTop 0).mono fun x hx => ?_
    simp only [add_div' _ _ _ hx, div_div_div_cancel_right₀ hx, mul_comm]
  refine ((B.comp tendsto_natCast_atTop_atTop).eventually (gt_mem_nhds hL)).mono fun k hk => ?_
  /- Finally, we use an upper estimate on `u (k * n + r)` to get an estimate on
  `u (k * n + r) / (k * n + r)`. -/
  rw [mul_comm]
  refine lt_of_le_of_lt ?_ hk
  simp only [(· ∘ ·), ← Nat.cast_add, ← Nat.cast_mul]
  gcongr
  apply h.apply_mul_add_le

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

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
⊢ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n

Tactic:
intro ε

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
⊢ 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ IntervalIntegrable g volume ↑i ↑(i + 1)

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ico_of_le (by simp)]

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ IntegrableOn g (Ico ↑i ↑(i + 1)) volume
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
⊢ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n

Tactic:
intro ε

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
⊢ 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
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
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).hom.app A ≫
      (limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) A).hom ≫ limit.π (F.op ⋙ yoneda.obj A) (op i) =
    (yoneda.obj A).map (colimit.ι F i).op

Tactic:
limitObjIsoLimitCompEvaluation_hom_π

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).hom.app A ≫ (limit.π (F.op ⋙ coyoneda) (op i)).app A =
    (yoneda.obj A).map (colimit.ι F i).op
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
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).hom.app A ≫
      (limitObjIsoLimitCompEvaluation (F.rightOp ⋙ coyoneda) A).hom ≫ limit.π (F.rightOp ⋙ yoneda.obj A) i =
    (yoneda.obj A).map (colimit.ι F (op i)).op

Tactic:
limitObjIsoLimitCompEvaluation_hom_π

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).hom.app A ≫ (limit.π (F.rightOp ⋙ coyoneda) i).app A =
    (yoneda.obj A).map (colimit.ι F (op i)).op
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = 0
⊢ g ≫ f = 0

Tactic:
suffices g ≫ f = 0 ≫ f by simpa
  exact hc.pushout_hom_ext (by simpa using hf)

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

Goal state before:
pp: case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
inst✝ : Injective Z
n✝ : ℕ
⊢ Injective (((single₀ C).obj Z).X (n✝ + 1))

Tactic:
apply IsZero.injective

Goal state after:
case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
inst✝ : Injective Z
n✝ : ℕ
⊢ IsZero (((single₀ C).obj Z).X (n✝ + 1))
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
n : ℤ
hn : n ≤ 0
⊢ Projective (R.cochainComplex.X n)

Tactic:
obtain ⟨k, rfl⟩ := Int.exists_eq_neg_ofNat hn
    exact Projective.of_iso (R.cochainComplexXIso (-k) k).symm inferInstance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
p : ℕ
hp : p + 1 = n
⊢ (∃ g, g ≫ R.cochainComplex.d ↑p ↑n = f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ↔ ∃ g, g ≫ R.cocomplex.d p n = f

Tactic:
R.cochainComplex_d _ _ _ _ rfl rfl

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
p : ℕ
hp : p + 1 = n
⊢ (∃ g,
      g ≫ (R.cochainComplexXIso (↑p) p ⋯).hom ≫ R.cocomplex.d p n ≫ (R.cochainComplexXIso (↑n) n ⋯).inv =
        f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ↔
    ∃ g, g ≫ R.cocomplex.d p n = f
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
p : ℕ
hp : p + 1 = n
⊢ (∃ g, R.cochainComplex.d (-↑n) (-↑p) ≫ g = (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ↔ ∃ g, R.complex.d n p ≫ g = f

Tactic:
R.cochainComplex_d _ _ _ _ rfl rfl

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
p : ℕ
hp : p + 1 = n
⊢ (∃ g,
      ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-↑p) p ⋯).inv) ≫ g =
        (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ↔
    ∃ g, R.complex.d n p ≫ g = f
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.monoModSerre s
eq : f ≫ s = 0
this : P.monoModSerre (Abelian.factorThruCoimage f ≫ s)
⊢ P (Abelian.coimage f)

Tactic:
show Abelian.factorThruCoimage f ≫ s = 0 by cat_disch,

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.monoModSerre s
eq : f ≫ s = 0
this : P.monoModSerre 0
⊢ P (Abelian.coimage f)
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
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ ∃ Y' t, ∃ (_ : P.isoModSerre t), f₁ ≫ t = f₂ ≫ t

Tactic:
by
    refine ⟨_, cokernel.π (f₁ - f₂), ?_, ?_⟩
    · rw [isoModSerre_iff_of_epi]
      exact (exists_isoModSerre_comp_eq_zero_iff P _).1 ⟨_, s, hs, by simpa [sub_eq_zero]⟩
    · simpa only [Preadditive.sub_comp, sub_eq_zero] using cokernel.condition (f₁ - f₂)

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Group N
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ →* N₂
fg : G₁ →* G₂
h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
x y : N₁ ⋊[φ₁] G₁
⊢ ⟨fn (x * y).left, fg (x * y).right⟩ = ⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩

Tactic:
replace h := DFunLike.ext_iff.1 (h x.right) y.left
    ext <;> simp_all

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Group N
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ ≃* N₂
fg : G₁ ≃* G₂
h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))
x y : N₁ ⋊[φ₁] G₁
⊢ ⟨fn (x * y).left, fg (x * y).right⟩ = ⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩

Tactic:
replace h := DFunLike.ext_iff.1 (h x.right) y.left
    ext <;> simp_all

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

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ Action V G
J : Type u_4
inst✝ : Category.{v_3, u_4} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ forget V G)
⊢ PreservesColimit K F

Tactic:
by
  let F' : C ⥤ SingleObj G ⥤ V := F ⋙ (Action.functorCategoryEquivalence V G).functor
  have : PreservesColimit K F' := SingleObj.preservesColimit _ _ h
  apply preservesColimit_of_reflects_of_preserves F (Action.functorCategoryEquivalence V G).functor

Goal state after:
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✝ Y✝ : D
f : X✝ ⟶ Y✝
X' Y' : C
f' : X' ⟶ Y'
w✝ : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
this : PreservesLimit (parallelPair NormalMono.g 0) L
⊢ L.map f' ≫ L.map NormalMono.g = 0

Tactic:
rw [← L.map_comp]; simp [hf'.w]

Goal state after:
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✝ Y✝ : D
f : X✝ ⟶ Y✝
X' Y' : C
f' : X' ⟶ Y'
w✝ : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
this : PreservesColimit (parallelPair NormalEpi.g 0) L
⊢ L.map NormalEpi.g ≫ L.map f' = 0

Tactic:
rw [← L.map_comp]; simp [hf'.w]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
⊢ T.map (𝟙 X.A) = 𝟙 (T.obj X.A)

Tactic:
Functor.map_id

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
⊢ 𝟙 (T.obj X.A) = 𝟙 (T.obj X.A)
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 =
      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:
Functor.comp_map,

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)))) ≫ U.map (R.map f) =
      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.Adjunction.Triple

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
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.whiskerLeft t.leftToRight = t.adj₁.counit ≫ t.adj₂.unit

Tactic:
ext X; exact t.leftToRight_app_obj

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
⊢ leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv

Tactic:
simpa [leftZigzag, bicategoricalComp] using H'.fac <| .mk _ <| (λ_ f).hom ≫ (ρ_ f).inv

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᴸ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ F.mapComp' f₀₂ f₂₃ f ⋯ =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃ ≫ F.mapComp' f₀₁ f₁₃ f ⋯

Tactic:
rw [whiskerLeft_mapComp'_comp_mapComp' _ _ _ _ _ _ f h₀₂ h₁₃,
    Iso.hom_inv_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ ∀ {X Y : Decomposed J}, Function.Surjective (decomposedTo J).map

Tactic:
rintro ⟨j', X, hX⟩ ⟨k', Y, hY⟩ f
    dsimp at f
    have : j' = k' := by
      rw [← hX, ← hY, Quotient.eq'']
      exact Relation.ReflTransGen.single (Or.inl ⟨f⟩)
    subst this
    exact ⟨Sigma.SigmaHom.mk (ObjectProperty.homMk f), rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
⊢ ∀ (s : LeftExtension f (g ≫ h)) (τ : t.whisker h ⟶ s),
    τ =
      let k := s.extension;
      let θ := s.unit;
      let sτ := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u));
      let τ := H.desc sτ;
      let sσ := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ);
      let σ := H'.desc sσ;
      homMk σ ⋯

Tactic:
intro s' τ₀'
    let τ' : t.extension ≫ h ⟶ s'.extension := τ₀'.right
    have Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit := by simpa [bicategoricalComp] using τ₀'.w
    ext
    apply (H' _).hom_ext
    dsimp only [StructuredArrow.homMk_right]
    rw [(H' _).fac]
    apply (cancel_epi (ρ_ _).inv).mp
    apply H.hom_ext
    dsimp only [LeftLift.whisker_lift, StructuredArrow.mk_right, LeftLift.whisker_unit,
      StructuredArrow.mk_hom_eq_self]
    let σs' := LeftExtension.mk (s'.extension ≫ u)
      (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
    calc _
      _ = 𝟙 _ ⊗≫ (t.unit ▷ (𝟙 c) ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u := by
        bicategory
      _ = 𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 _ := by
        rw [← whisker_exchange]; bicategory
      _ = t.unit ≫ f ◁ H.desc σs' := by
        rw [Hτ', IsKan.fac]
        dsimp only [StructuredArrow.mk_hom_eq_self, σs']
      _ = _ := by
        bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
inst✝¹⁰ : Category.{v_1, u_1} C₁
inst✝⁹ : Category.{v_2, u_2} C₂
inst✝⁸ : Category.{v_3, u_3} D₁
inst✝⁷ : Category.{v_4, u_4} D₂
inst✝⁶ : Category.{v_5, u_5} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
⊢ ((lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂) =
    ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫
      (τ.app X₁).app X₂ ≫ ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂

Tactic:
dsimp [lift₂NatTrans, fullyFaithfulUncurry, Equivalence.fullyFaithfulFunctor]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
inst✝¹⁰ : Category.{v_1, u_1} C₁
inst✝⁹ : Category.{v_2, u_2} C₂
inst✝⁸ : Category.{v_3, u_3} D₁
inst✝⁷ : Category.{v_4, u_4} D₂
inst✝⁶ : Category.{v_5, u_5} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
⊢ 𝟙 ((F₁'.obj (L₁.obj X₁)).obj (L₂.obj X₂)) ≫
      (liftNatTrans (L₁.prod L₂) (W₁.prod W₂) (uncurry.obj F₁) (uncurry.obj F₂) (uncurry.obj F₁') (uncurry.obj F₂')
              (uncurry.map τ)).app
          (L₁.obj X₁, L₂.obj X₂) ≫
        𝟙 ((F₂'.obj (L₁.obj X₁)).obj (L₂.obj X₂)) =
    ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫
      (τ.app X₁).app X₂ ≫ ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMultiplicative
h : ∀ {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂), W f → W g → W (f ⊗ₘ g)
X₁✝ X₂✝ : C
f : X₁✝ ⟶ X₂✝
hf : W f
Y : C
⊢ W (f ▷ Y)

Tactic:
by simpa using h f (𝟙 Y) hf (W.id_mem _)

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

Goal state before:
pp: case h
𝒮 : 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 : 𝒳
ψ : c ⟶ b'
hψ : p.IsHomLift f ψ
τ : c ⟶ a
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ ≫ φ'.hom = ψ
⊢ (τ ≫ φ) ≫ φ'.hom = ψ

Tactic:
simp only [assoc, hτ₂]

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

Goal state before:
pp: case h
𝒮 : 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 : 𝒳
ψ : c ⟶ b
hψ : p.IsHomLift f ψ
τ : c ⟶ a'
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ'.hom ≫ φ = ψ
⊢ (τ ≫ φ'.hom) ≫ φ = ψ

Tactic:
simp only [assoc, hτ₂]

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₁} 𝒮
inst✝ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
S : 𝒮
⊢ (Fiber.inducedFunctor ⋯).IsEquivalence

Tactic:
by exact isEquivalence_of_iso (F := 𝟭 (Fiber p S)) (Iso.refl _)

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: case refine_1
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.obj
inst✝ : MulAction.IsPretransitive G X.obj
h : Nonempty X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
this : Mono i.hom
⊢ Function.Injective ⇑(ConcreteCategory.hom i.hom)

Tactic:
exact ConcreteCategory.injective_of_mono_of_preservesPullback i.hom

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj
⊢ Function.Injective ⇑(ConcreteCategory.hom (F.map f)) ∧
    Fintype.card ((fun X ↦ X.obj) (F.obj X)) = Fintype.card ((fun X ↦ X.obj) (F.obj Y))

Tactic:
refine ⟨injective_of_mono_of_preservesPullback (F.map f), ?_⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj
⊢ Fintype.card ((fun X ↦ X.obj) (F.obj X)) = Fintype.card ((fun X ↦ X.obj) (F.obj Y))
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inl
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₁
⊢ (IsLimit.lift h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt)) i
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) ⋯) ≫
      (mk bc.pt (c₁.combPairHoms c₂ bc)).proj (Sum.inl val✝) =
    s.proj (Sum.inl val✝)

Tactic:
· simp only [fan_mk_proj, combPairHoms]
        erw [← Category.assoc, h.fac]
        simp only [pair_obj_left, mk_π_app, IsLimit.fac]

Goal state after: