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

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.Icc (-1) 1)
⊢ ContinuousOn f (Set.uIcc (-1) 1)

Tactic:
Set.uIcc_of_lt (by norm_num)

Goal state after:
f : ℝ → ℝ
hf : ContinuousOn f (Set.Icc (-1) 1)
⊢ ContinuousOn f (Set.Icc (-1) 1)
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: n : ℕ
x✝ : n + 1 ≠ 0
⊢ (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) = 8 * (n + 1) + (n + 1 + n) * (n + 1 + n)

Tactic:
zify

Goal state after:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ (↑n + 1 + 1 + (↑n + 1)) * (↑n + 1 + 1 + (↑n + 1)) = 8 * (↑n + 1) + (↑n + 1 + ↑n) * (↑n + 1 + ↑n)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case refine_1
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2

pp: case refine_2
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ 1 ≤ (↑(x 1) / ‖x‖) ^ 2

Tactic:
· have : x 0 ≠ 0 := by
      rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
    simp only [norm_eq_max_natAbs, H0, Nat.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
      le_refl]

Goal state after:
case refine_2
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ 1 ≤ (↑(x 1) / ‖x‖) ^ 2
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b b n = b * (1 - a ^ (n + 1)) / (1 - a)

Tactic:
rw [arithGeom_eq ha n]
  field [sub_ne_zero.mpr ha.symm]

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: m n : ℤ
⊢ (fib m).gcd (fib n) = Nat.fib (m.gcd n)

Tactic:
obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg
    <;> obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg

Goal state after:
case inl.inl
m n : ℕ
⊢ (fib ↑m).gcd (fib ↑n) = Nat.fib ((↑m).gcd ↑n)

case inl.inr
m n : ℕ
⊢ (fib ↑m).gcd (fib (-↑n)) = Nat.fib ((↑m).gcd (-↑n))

case inr.inl
m n : ℕ
⊢ (fib (-↑m)).gcd (fib ↑n) = Nat.fib ((-↑m).gcd ↑n)

case inr.inr
m n : ℕ
⊢ (fib (-↑m)).gcd (fib (-↑n)) = Nat.fib ((-↑m).gcd (-↑n))
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
⊢ ∑ i ∈ Finset.Ico a b, f ↑i * g ↑i ≤ ∫ (x : ℝ) in ↑a..↑b, f x * g (x - 1)

Tactic:
apply sum_Ico_le_integral_of_le (f := fun x ↦ f x * g x) hab

Goal state after:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
⊢ ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i * g ↑i ≤ f x * g (x - 1)

case hg
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
⊢ IntegrableOn (fun x ↦ f x * g (x - 1)) (Ico ↑a ↑b) volume
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case base.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure f 0).fst

pp: case base.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨0, ?base.refine_1⟩ = { obj := f x, property := ⋯ }.obj

Tactic:
· simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      exact ULift.up x

Goal state after:
case base.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨0, id { down := x }⟩ =
    { obj := f x, property := ⋯ }.obj
Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P : IndParallelPairPresentation f g
j : P.I
⊢ { pt := A, ι := P.ι₁ }.ι.app j ≫
      (parallelPair f g).map WalkingParallelPairHom.left ≫
        (P.isColimit₂.coconePointUniqueUpToIso (colimit.isColimit (P.F₂ ⋙ yoneda))).hom =
    { pt := A, ι := P.ι₁ }.ι.app j ≫
      (P.isColimit₁.coconePointUniqueUpToIso (colimit.isColimit (P.F₁ ⋙ yoneda))).hom ≫
        (parallelPair P.φ P.ψ ⋙ (whiskeringRight P.I C (Cᵒᵖ ⥤ Type v₁)).obj yoneda ⋙ colim).map
          WalkingParallelPairHom.left

Tactic:
by
      simp [P.hf, P.isColimit₁.ι_map_assoc, P.isColimit₁.comp_coconePointUniqueUpToIso_hom_assoc,
        P.isColimit₂.comp_coconePointUniqueUpToIso_hom]

Goal state after:
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 ≫ limit.π (F.op ⋙ coyoneda) (op i)).app A =
    (yoneda.obj A).map (colimit.ι F i).op

Tactic:
coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π,

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
⊢ (coyoneda.map (colimit.ι F i).op).app A = (yoneda.obj A).map (colimit.ι F i).op
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
h : G ⟶ pullback (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g))
r : ↥F → (End G)ᵐᵒᵖ :=
  fun x ↦
    MulOpposite.op
      (h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun x ↦ G) x)
⊢ (ModuleCat.Hom.hom f) (∑ x ∈ F.attach, r x • (↑x).as) = 0

Tactic:
suffices ∑ x ∈ F.attach, r x • x.1.as = 0 by simp [this]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
h : G ⟶ pullback (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g))
r : ↥F → (End G)ᵐᵒᵖ :=
  fun x ↦
    MulOpposite.op
      (h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun x ↦ G) x)
⊢ ∑ x ∈ F.attach, r x • (↑x).as = 0
Module: Mathlib.CategoryTheory.Abelian.Preradical.Radical

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
Φ : Preradical C
⊢ IsIso (Φ.toColon Φ) ↔ IsZero (Φ.quotient ⋙ Φ.r)

Tactic:
isIso_toColon_iff

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
Φ : Preradical C
⊢ IsZero (Φ.quotient ⋙ Φ.r) ↔ IsZero (Φ.quotient ⋙ Φ.r)
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : ProjectiveResolution X
⊢ R.cochainComplex.IsGE 0

Tactic:
by
  simp only [HomologicalComplex.isSupported_iff_of_quasiIso R.π']
  infer_instance

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 Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst✝¹ : Epi f
inst✝ : Mono g
⊢ P (Abelian.image (f ≫ g)) ↔ P Z

Tactic:
have := strongEpi_of_epi f

Goal state after:
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 Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst✝¹ : Epi f
inst✝ : Mono g
this : StrongEpi f
⊢ P (Abelian.image (f ≫ g)) ↔ P Z
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
a b : ActionCategory G X
f : a ⟶ b
⊢ P f

Tactic:
refine cast ?_ (hyp b.back f.val)

Goal state after:
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
a b : ActionCategory G X
f : a ⟶ b
⊢ P (homOfPair b.back ↑f) = P f
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
v g : G
x : G ⧸ N
⊢ (ConcreteCategory.hom
        ((ofMulAction G (FintypeCat.of (G ⧸ N))).ρ g ≫ FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * v⁻¹⟧) ⋯)))
      x =
    (ConcreteCategory.hom
        (FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * v⁻¹⟧) ⋯) ≫ (ofMulAction G (FintypeCat.of (G ⧸ N))).ρ g))
      x

Tactic:
induction x using Quotient.inductionOn with | h x

Goal state after:
case h
G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
v g x : G
⊢ (ConcreteCategory.hom
        ((ofMulAction G (FintypeCat.of (G ⧸ N))).ρ g ≫ FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * v⁻¹⟧) ⋯)))
      ⟦x⟧ =
    (ConcreteCategory.hom
        (FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * v⁻¹⟧) ⋯) ≫ (ofMulAction G (FintypeCat.of (G ⧸ N))).ρ g))
      ⟦x⟧
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : B
f : Discrete (Path a b)
⊢ (inclusionPath a b ⋙ (normalize B).mapFunctor a b).obj f = (𝟭 (Discrete (Path a b))).obj f

Tactic:
by
      obtain ⟨f⟩ := f
      induction f with
      | nil => rfl
      | cons _ _ ih =>
        ext1 -- Porting note: `tidy` closes the goal in mathlib3 but `aesop` doesn't here.
        injection ih with ih
        conv_rhs => rw [← ih]
        rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
hB : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
sA : A ≌ AsSmall A := ⋯
sB : B ≌ AsSmall B := ⋯
sT : T ≌ AsSmall T := ⋯
L' : AsSmall A ⥤ AsSmall T := ⋯
R' : AsSmall B ⥤ AsSmall T := ⋯
this✝ : ∀ (b : AsSmall B), (CostructuredArrow.toOver L' (R'.obj b)).Final
this : L'.Final
⊢ sA.functor ⋙ L' ⋙ sT.inverse ≅ L

Tactic:
exact (sA.functor.associator (sA.inverse ⋙ L ⋙ sT.functor) sT.inverse).symm ≪≫
    ((sA.functor.associator sA.inverse (L ⋙ sT.functor)).symm ≪≫
      isoWhiskerRight sA.unitIso.symm _ ≪≫ (L ⋙ sT.functor).leftUnitor).compInverseIso

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ curry.obj F₁ = curry.obj F₂

Tactic:
apply Construction.uniq

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ W₁.Q ⋙ curry.obj F₁ = W₁.Q ⋙ curry.obj F₂
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ (W₁.Q ⋙ curry.obj F₁).flip = (W₁.Q ⋙ curry.obj F₂).flip

Tactic:
apply Construction.uniq

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₁).flip = W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₂).flip
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ V₁.str ≫ F.map (inv f.f) = inv f.f ≫ V₀.str

Tactic:
rw [IsIso.eq_inv_comp f.1, ← Category.assoc, ← f.h, Category.assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ V₀.str ≫ F.map f.f ≫ F.map (inv f.f) = V₀.str
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 c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
T : 𝒮
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 T) ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
obtain rfl : S = T := by rw [← codomain_eq p f φ, domain_eq p (𝟙 T) ψ]
  infer_instance

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.IsStronglyCartesian f φ
R' : 𝒮
a' : 𝒳
g : R' ⟶ R
f' : R' ⟶ S
hf' : f' = g ≫ f
φ' : a' ⟶ b
inst✝ : p.IsHomLift f' φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
subst_hom_lift p f' φ'; clear a b R S
  have : p.IsHomLift (g ≫ f) φ' := (hf' ▸ inferInstance)
  apply IsStronglyCartesian.universal_property' f

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

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.IsCocartesian f φ
b' : 𝒳
φ' : a ⟶ b'
inst✝ : p.IsCocartesian f φ'
⊢ IsCocartesian.map p f φ φ' ≫ IsCocartesian.map p f φ' φ = 𝟙 b

Tactic:
by
    subst_hom_lift p f φ
    apply IsCocartesian.ext p (p.map φ) φ
    simp only [fac_assoc, fac, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasFunctorEnrichedHom V F₁ F₂
inst✝¹ : HasFunctorEnrichedHom V F₂ F₃
inst✝ : HasFunctorEnrichedHom V F₁ F₃
j j' : J
f : j ⟶ j'
k : Under j'
⊢ (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂)) ⊗ₘ
        precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃))) ≫
      (end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂)) k ⊗ₘ
          end_.π (diagram V (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃)) k) ≫
        eComp V (F₁.obj k.right) (F₂.obj k.right) (F₃.obj k.right) =
    enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ≫
      precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)) ≫
        end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) k

Tactic:
rw [tensorHom_comp_tensorHom_assoc]

Goal state after:
V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasFunctorEnrichedHom V F₁ F₂
inst✝¹ : HasFunctorEnrichedHom V F₂ F₃
inst✝ : HasFunctorEnrichedHom V F₁ F₃
j j' : J
f : j ⟶ j'
k : Under j'
⊢ (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
            (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂)) ≫
          end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂)) k ⊗ₘ
        precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂))
            (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)) ≫
          end_.π (diagram V (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃)) k) ≫
      eComp V (F₁.obj k.right) (F₂.obj k.right) (F₃.obj k.right) =
    enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ≫
      precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)) ≫
        end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) k
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case ind
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
⊢ ∀ (X : C), n = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
| _ n hi
   => 

Goal state after:
case ind
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
⊢ ∀ (X : C), n = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
A : C
f : A ⟶ ∏ᶜ fun X ↦ ↑X
hgal : IsGalois A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
h1 : ∀ σ ∈ U, σ.hom.app A = 𝟙 (F.obj A)
σ : Aut F
σinU : σ ∈ U
⊢ ∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)

Tactic:
intro ⟨X, hX⟩

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
A : C
f : A ⟶ ∏ᶜ fun X ↦ ↑X
hgal : IsGalois A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
h1 : ∀ σ ∈ U, σ.hom.app A = 𝟙 (F.obj A)
σ : Aut F
σinU : σ ∈ U
X : C
hX : X ∈ I
⊢ σ.hom.app ↑⟨X, hX⟩ = 𝟙 (F.obj ↑⟨X, hX⟩)
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (P.decompId_i ≫ P.complement.decompId_p).f = Hom.f 0

Tactic:
simp only [comp_f, toKaroubi_obj_X, decompId_i_f, decompId_p_f,
        complement_p, comp_sub, comp_id, idem, sub_self, zero_def]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ {x | Map.Arrows φ hφ S d d x}.Nonempty → ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

pp: case mpr
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ (∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d) → {x | Map.Arrows φ hφ S d d x}.Nonempty

Tactic:
· rintro ⟨f, hf⟩
    change Map.Arrows φ hφ S d d f at hf; rw [Map.arrows_iff] at hf
    obtain ⟨c, d, g, ec, ed, eg, gS, eg⟩ := hf
    exact ⟨c, ⟨mem_objs_of_src S eg, ec⟩⟩

Goal state after:
case mpr
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ (∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d) → {x | Map.Arrows φ hφ S d d x}.Nonempty
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b c : Cat} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (η ▷ h).toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C f.toFunctor h.toFunctor)).hom ≫
        NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) η.toNatTrans) ▷ (mapPair (𝟭 C) h.toFunctor).toCatHom ≫
          (Cat.Hom.isoMk (mapCompRight C g.toFunctor h.toFunctor)).inv

Tactic:
intros; exact congr($(mapWhiskerLeft_whiskerRight C _ _).toCatHom₂)

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

Goal state before:
pp: case left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' : C ⋆ D ⥤ E
α β : F ⟶ F'
h₁ : (inclLeft C D).whiskerLeft α = (inclLeft C D).whiskerLeft β
h₂ : (inclRight C D).whiskerLeft α = (inclRight C D).whiskerLeft β
t : C
⊢ α.app (left t) = β.app (left t)

Tactic:
| left t =>

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this✝ : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
⊢ IsClosedUnderColimitsOfShape (fun f ↦ Coequifibered f.hom) J

Tactic:
rw [isClosedUnderColimitsOfShape_iff_op, ← isClosedUnderLimitsOfShape_inverseImage_iff _ _ e]

Goal state after:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this✝ : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
⊢ ((ObjectProperty.op fun f ↦ Coequifibered f.hom).inverseImage e.functor).IsClosedUnderLimitsOfShape Jᵒᵖ
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ #(X ⟶ yp) ≤ α

Tactic:
· apply Cardinal.mk_le_of_injective _
      · intro f
        exact ⟨_, _, f⟩
      · rintro f g k
        cases k
        rfl

Goal state after: