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

Goal state before:
pp: case refine_1
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ ∀ (i : ℕ), IntegrableOn f (Ioc (↑N) (↑i + ↑N)) volume

pp: case refine_2
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ ∀ᶠ (i : ℕ) in atTop, ∫ (x : ℝ) in ↑N..↑i + ↑N, ‖f x‖ ≤ ∑' (n : ℕ), f ↑(n + N)

Tactic:
· intro n
    rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le (by grind)]
    exact (anti.mono <| by grind [uIcc_of_le]).intervalIntegrable

Goal state after:
case refine_2
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ ∀ᶠ (i : ℕ) in atTop, ∫ (x : ℝ) in ↑N..↑i + ↑N, ‖f x‖ ≤ ∑' (n : ℕ), f ↑(n + N)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
integrable : IntegrableOn f (Ioi ↑N) volume
⊢ ∫ (x : ℝ) in Ioi ↑N, f x ≤ ∑' (n : ℕ), f ↑(n + N)

Tactic:
refine le_of_tendsto_of_tendsto (intervalIntegral_tendsto_integral_Ioi N integrable this) lim ?_

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
integrable : IntegrableOn f (Ioi ↑N) volume
⊢ (fun i ↦ ∫ (x : ℝ) in ↑N..↑i + ↑N, f x) ≤ᶠ[atTop] fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)
Module: Mathlib.CategoryTheory.Comma.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✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
j₁ j₂ : Comma L R
Q : CostructuredArrow L (R.obj (IsCofiltered.min j₁.right j₂.right))
ia : A
va₁ : ia ⟶ Q.left
va₂ : ia ⟶ j₁.left
heqa : L.map va₁ ≫ Q.hom ≫ R.map (IsCofiltered.minToLeft j₁.right j₂.right) = L.map va₂ ≫ j₁.hom
ib : A
vb₁ : ib ⟶ Q.left
vb₂ : ib ⟶ j₂.left
heqb : L.map vb₁ ≫ Q.hom ≫ R.map (IsCofiltered.minToRight j₁.right j₂.right) = L.map vb₂ ≫ j₂.hom
i₀ : A
il₀ : i₀ ⟶ ia
ir₀ : i₀ ⟶ ib
heq : il₀ ≫ va₁ = ir₀ ≫ vb₁
⊢ L.map (il₀ ≫ va₂) ≫ j₁.hom =
    { left := i₀, right := IsCofiltered.min j₁.right j₂.right, hom := L.map (il₀ ≫ va₁) ≫ Q.hom }.hom ≫
      R.map (IsCofiltered.minToLeft j₁.right j₂.right)

Tactic:
by simp [← heqa]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type v
inst✝¹ : Finite α
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ Ind C
I : α → Type v := fun s ↦ (F.obj { as := s }).presentation.I
G : (s : α) → I s ⥤ C := fun s ↦ (F.obj { as := s }).presentation.F
⊢ (Discrete.functor fun s ↦ Pi.eval I s ⋙ G s) ⋙ (whiskeringRight ((i : α) → I i) C (Ind C)).obj Ind.yoneda ⋙ colim ≅ F

Tactic:
refine Discrete.natIso (fun s => ?_)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
α : Type v
inst✝¹ : Finite α
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ Ind C
I : α → Type v := fun s ↦ (F.obj { as := s }).presentation.I
G : (s : α) → I s ⥤ C := fun s ↦ (F.obj { as := s }).presentation.F
s : Discrete α
⊢ ((Discrete.functor fun s ↦ Pi.eval I s ⋙ G s) ⋙
          (whiskeringRight ((i : α) → I i) C (Ind C)).obj Ind.yoneda ⋙ colim).obj
      s ≅
    F.obj s
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
inst✝² : HasProductsOfShape ι C
ι' : Type u_3
inst✝¹ : HasProductsOfShape ι' C
inst✝ : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x✝¹ : (i : ι') → SmallCategory (J i)
x✝ : ∀ (i : ι'), IsFiltered (J i)
F : (i : ι') → J i ⥤ C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
⊢ Nonempty (IsColimit (coconePointwiseProduct c))

Tactic:
obtain ⟨h⟩ := nonempty_isColimit fun i : ι ↦ hc (e i)

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
inst✝² : HasProductsOfShape ι C
ι' : Type u_3
inst✝¹ : HasProductsOfShape ι' C
inst✝ : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x✝¹ : (i : ι') → SmallCategory (J i)
x✝ : ∀ (i : ι'), IsFiltered (J i)
F : (i : ι') → J i ⥤ C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
h : IsColimit (coconePointwiseProduct fun i ↦ c (e i))
⊢ Nonempty (IsColimit (coconePointwiseProduct c))
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
⊢ HasCoseparator C

Tactic:
suffices HasCoseparator (ShrinkHoms C) from
    HasCoseparator.of_equivalence (ShrinkHoms.equivalence.{w} C).symm
  obtain ⟨G, -, hG⟩ := Abelian.has_injective_coseparator (separator (ShrinkHoms C))
    (isSeparator_separator _)
  exact ⟨G, hG⟩

Goal state after:
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
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (I.isoRightDerivedObj F n).inv ≫ (F.rightDerived n).map f ≫ (J.isoRightDerivedObj F n).hom =
    (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ ≫
      (J.isoRightDerivedObj F n).inv ≫ (J.isoRightDerivedObj F n).hom

Tactic:
InjectiveResolution.isoRightDerivedObj_hom_naturality f I J φ comm F n,

Goal state after:
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
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (I.isoRightDerivedObj F n).inv ≫
      (I.isoRightDerivedObj F n).hom ≫
        (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
          φ =
    (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ ≫
      (J.isoRightDerivedObj F n).inv ≫ (J.isoRightDerivedObj F n).hom
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 : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Epi (L.map f)
⊢ P.epiModSerre f

Tactic:
have hf : L.map (cokernel.π f) = 0 := by
      rw [← cancel_epi (L.map f), comp_zero, ← L.map_comp,
        cokernel.condition, L.map_zero]

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 Y : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Epi (L.map f)
hf : L.map (cokernel.π f) = 0
⊢ P.epiModSerre 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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
Z : C
z : Z ⟶ X
Z' : C
t : Z' ⟶ Z
ht : P.isoModSerre t
fac : t ≫ z ≫ f = 0
this : IsIso (L.map t)
⊢ ∃ l, l ≫ L.map (kernel.ι f) = eqToHom ⋯ ≫ L.map z

Tactic:
rw [← Category.assoc] at fac

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 Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
Z : C
z : Z ⟶ X
Z' : C
t : Z' ⟶ Z
ht : P.isoModSerre t
fac : (t ≫ z) ≫ f = 0
this : IsIso (L.map t)
⊢ ∃ l, l ≫ L.map (kernel.ι f) = eqToHom ⋯ ≫ L.map z
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]

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✝ 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' ≫ NormalMono.g) = 0
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]

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✝ 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 ≫ f') = 0
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s : BinaryCofan a b
⊢ pullback.fst a.arrow b.arrow ≫ underlying.map (s.ι.app { as := WalkingPair.left }) =
    pullback.snd a.arrow b.arrow ≫ underlying.map (s.ι.app { as := WalkingPair.right })

Tactic:
by ext; simp [pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
e₁ : x = y
⊢ eqToHomTransIso e₁ ⋯ = (ρ_ (eqToHom e₁)).symm

Tactic:
by
  ext
  subst e₁
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
e₁ : x = y
⊢ eqToHomTransIso ⋯ e₁ = (λ_ (eqToHom e₁)).symm

Tactic:
by
  ext
  subst e₁
  simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t✝ : RightLift f g
t : RightLift f (𝟙 c ≫ g)
P : t.IsKan
⊢ ∀ (s : RightLift f g) (τ : s ⟶ t.ofIdComp), τ = t.whiskerIdCancel (Limits.IsTerminal.from P (s.whisker (𝟙 c)))

Tactic:
by
    intro s τ
    ext
    apply P.hom_ext
    simp [← RightLift.w τ]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case mp.inr.refl
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
h' : Sum.inr a' ∈ f a
e' : b ∈ f.fix a'
⊢ b ∈ f.fix a'

Tactic:
exact e'

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 : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
⊢ W₁.Q.prod W₂.Q ⋙ prodLift F hF = F

Tactic:
by
  rw [← Functor.uncurry_obj_curry_obj_flip_flip', prod_fac₂, Functor.flip_flip, prod_fac₁,
    Functor.uncurry_obj_curry_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: case inr.inr
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C'
f✝¹ f✝ : x✝ ⟶ y✝
⊢ (Sum.inr_ C C').map f✝¹ = (Sum.inr_ C C').map f✝

Tactic:
case inr x y f g => rw [((by assumption : IsDiscrete C').subsingleton x y).allEq f g]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X : C
⊢ (ρ_ (L'.obj X)).hom = L'.obj X ◁ (ε' L W ε).inv ≫ (μ L W ε X (𝟙_ C)).hom ≫ L'.map (ρ_ X).hom

Tactic:
by
  dsimp +instances [monoidalCategoryStruct, rightUnitor]
  rw [liftNatTrans_app]
  dsimp
  rw [assoc]
  change _ ≫ (μ L W ε _ _).hom ≫ _ ≫ 𝟙 _ ≫ 𝟙 _ = _
  simp only [comp_id]

Goal state after:
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:
IsIso.eq_inv_comp f.1,

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
⊢ f.f ≫ V₁.str ≫ F.map (inv f.f) = V₀.str
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 A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom
        ((Types.pullbackIsoPullback ((cospan f g ⋙ F ⋙ FintypeCat.incl).map WalkingCospan.Hom.inl)
              ((cospan f g ⋙ F ⋙ FintypeCat.incl).map WalkingCospan.Hom.inr)).inv ≫
          pullback.fst ((F ⋙ FintypeCat.incl).map f) ((F ⋙ FintypeCat.incl).map g)))
      ⟨(a, b), h⟩ =
    a

Tactic:
Types.pullbackIsoPullback_inv_fst

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom (↾fun p ↦ (↑p).1)) ⟨(a, b), h⟩ = a
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).obj
Z : C
f : Z ⟶ X
z : (F.obj Z).obj
hz : (ConcreteCategory.hom (F.map f)) z = (ConcreteCategory.hom i.hom) y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu : (ConcreteCategory.hom ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).map u.hom)) y = z
⊢ i = u.hom ≫ (functorToAction F).map f

Tactic:
apply evaluation_injective_of_isConnected
    (forget₂ (Action FintypeCat (Aut F)) FintypeCat) Y ((functorToAction F).obj X) y

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).obj
Z : C
f : Z ⟶ X
z : (F.obj Z).obj
hz : (ConcreteCategory.hom (F.map f)) z = (ConcreteCategory.hom i.hom) y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu : (ConcreteCategory.hom ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).map u.hom)) y = z
⊢ (fun f ↦ (ConcreteCategory.hom ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).map f)) y) i =
    (fun f ↦ (ConcreteCategory.hom ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).map f)) y)
      (u.hom ≫ (functorToAction F).map f)
Module: Mathlib.CategoryTheory.Galois.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X : ContAction FintypeCat (Aut F')
⊢ Continuous fun p ↦
    (ConcreteCategory.hom
        ((forget₂ FintypeCat TopCat).map
          (((FintypeCat.uSwitchEquivalence.functor.mapAction (Aut F')).obj X.obj).ρ p.1)))
      p.2

Tactic:
change Continuous ((fun p ↦ (FintypeCat.uSwitchEquiv X.obj.V).symm p) ∘
              (fun p : Aut F' × _ ↦ (X.obj.ρ p.1).hom p.2) ∘
              (fun p : Aut F' × _ ↦ (p.1, FintypeCat.uSwitchEquiv _ p.2)))

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X : ContAction FintypeCat (Aut F')
⊢ Continuous
    ((fun p ↦ X.obj.V.uSwitchEquiv.symm p) ∘
      (fun p ↦ (ConcreteCategory.hom (X.obj.ρ p.1).hom) p.2) ∘ fun p ↦ (p.1, X.obj.V.uSwitchEquiv p.2))
Module: Mathlib.CategoryTheory.Galois.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X : ContAction FintypeCat (Aut F')
⊢ Continuous fun p ↦
    (ConcreteCategory.hom
        ((forget₂ FintypeCat TopCat).map
          (((FintypeCat.uSwitchEquivalence.inverse.mapAction (Aut F')).obj X.obj).ρ p.1)))
      p.2

Tactic:
change Continuous ((fun p ↦ (FintypeCat.uSwitchEquiv X.obj.V).symm p) ∘
              (fun p : Aut F' × _ ↦ (X.obj.ρ p.1).hom p.2) ∘
              (fun p : Aut F' × _ ↦ (p.1, FintypeCat.uSwitchEquiv _ p.2)))

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X : ContAction FintypeCat (Aut F')
⊢ Continuous
    ((fun p ↦ X.obj.V.uSwitchEquiv.symm p) ∘
      (fun p ↦ (ConcreteCategory.hom (X.obj.ρ p.1).hom) p.2) ∘ fun p ↦ (p.1, X.obj.V.uSwitchEquiv p.2))
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun i ↦ ⋯.some
P : C := ∏ᶜ X
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).obj), g • x = (ConcreteCategory.hom (t.hom.app (X i))) x

Tactic:
let is₁ : F.obj P ≅ ∏ᶜ fun i ↦ (F.obj (X i)) := PreservesProduct.iso F X

Goal state after:
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun i ↦ ⋯.some
P : C := ∏ᶜ X
is₁ : F.obj P ≅ ∏ᶜ fun i ↦ F.obj (X i) := PreservesProduct.iso F X
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).obj), g • x = (ConcreteCategory.hom (t.hom.app (X i))) x
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X✝² Y✝¹ X✝¹ Y✝ X Y : Paths (Symmetrify V)
X✝ Z✝ : Symmetrify V
f : X✝ ⟶ Z✝
XW : X✝² ⟶ (Paths.of (Symmetrify V)).obj X✝
WY : (Paths.of (Symmetrify V)).obj X✝ ⟶ Y✝¹
⊢ HomRel.CompClosure redStep (Path.reverse (XW ≫ 𝟙 ((Paths.of (Symmetrify V)).obj X✝) ≫ WY))
    (Path.reverse (XW ≫ (f.toPath ≫ (reverse f).toPath) ≫ WY))

Tactic:
have : HomRel.CompClosure redStep (WY.reverse ≫ 𝟙 _ ≫ XW.reverse)
      (WY.reverse ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ XW.reverse) := by
    constructor
    constructor

Goal state after:
V : Type u
inst✝ : Quiver V
X✝² Y✝¹ X✝¹ Y✝ X Y : Paths (Symmetrify V)
X✝ Z✝ : Symmetrify V
f : X✝ ⟶ Z✝
XW : X✝² ⟶ (Paths.of (Symmetrify V)).obj X✝
WY : (Paths.of (Symmetrify V)).obj X✝ ⟶ Y✝¹
this :
  HomRel.CompClosure redStep (Path.reverse WY ≫ 𝟙 ((Paths.of (Symmetrify V)).obj X✝) ≫ Path.reverse XW)
    (Path.reverse WY ≫ (f.toPath ≫ (reverse f).toPath) ≫ Path.reverse XW)
⊢ HomRel.CompClosure redStep (Path.reverse (XW ≫ 𝟙 ((Paths.of (Symmetrify V)).obj X✝) ≫ WY))
    (Path.reverse (XW ≫ (f.toPath ≫ (reverse f).toPath) ≫ WY))
Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
A B K L X Y : C
g : K ⟶ L
h : X ⟶ Y
i : IsInitial A
this :
  HasLiftingProperty (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom).ι h ↔
    HasLiftingProperty (B ◁ (Arrow.mk g).hom) h
⊢ HasLiftingProperty (pushout.desc (B ◁ g) (i.to B ▷ L) ⋯) h ↔ HasLiftingProperty g ((ihom B).map h)

Tactic:
rw [dsimp% this]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
A B K L X Y : C
g : K ⟶ L
h : X ⟶ Y
i : IsInitial A
this :
  HasLiftingProperty (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom).ι h ↔
    HasLiftingProperty (B ◁ (Arrow.mk g).hom) h
⊢ HasLiftingProperty (B ◁ g) h ↔ HasLiftingProperty g ((ihom B).map h)