mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
inst✝¹ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
z : X ⟶ c.pt
⊢ ∃ j₀ y, z = y ≫ c.ι.app j₀

Tactic:
by
  have := isFiltered_of_isCardinalFiltered J κ
  have := hc.mono_ι_app_of_isFiltered
  have := NatTrans.mono_of_mono_app c.ι
  obtain ⟨j, _⟩ := exists_isIso_of_functor_from_monoOver (F z) hXκ _
    (colimit.isColimit _) (f z) (hf z) (epi_f hc z)
  refine ⟨j, inv ((F z).obj j).obj.hom ≫ (pullback.fst c.ι _).app j, ?_⟩
  dsimp
  rw [Category.assoc, IsIso.eq_inv_comp, ← NatTrans.comp_app, pullback.condition,
    NatTrans.comp_app, Functor.const_map_app]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ transfiniteCompositions.{w, v, u} W f ↔ ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J f

Tactic:
by
  simp only [transfiniteCompositions, iSup_iff]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case inl
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
⊢ (ConcreteCategory.hom (F.map (homOfLE hij✝).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val),
        ⋯⟩

Tactic:
have := congr_arg (F.map (homOfLE hij').op) (d.map_succ j hj e.val)

Goal state after:
case inl
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE hij').op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val)) =
    (ConcreteCategory.hom (F.map (homOfLE hij').op)) e.val
⊢ (ConcreteCategory.hom (F.map (homOfLE hij✝).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val),
        ⋯⟩
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
s : ↑(sqFunctor c p f g).sections
hs : (↑s (Opposite.op ⊥)).f' = f
t : Cocone F := { pt := X, ι := { app := fun j ↦ (↑s (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
hl : ∀ (j : J), c.ι.app j ≫ l = (↑s (Opposite.op j)).f'
⊢ c.ι.app ⊥ ≫ l = f

Tactic:
by rw [hl, hs]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (F.map (homOfLE ⋯)) p
f✝ : F.obj ⊥ ⟶ X
g✝ : ((Functor.const J).obj c.pt).obj ⊥ ⟶ Y
sq : CommSq f✝ (c.ι.app ⊥) p g✝
j : J
hj : ¬IsMax j
x✝¹ : F.obj j ⟶ X
x✝ : CommSq x✝¹ (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g✝)
⊢ x✝.HasLift

Tactic:
have := hF j hj; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ W.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
have := W.rlp.isStableUnderTransfiniteCompositionOfShape_llp J

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
this : W.rlp.llp.IsStableUnderTransfiniteCompositionOfShape J
⊢ W.transfiniteCompositionsOfShape J ≤ W.rlp.llp
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: case left
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this✝² : LocallySmall.{w, v, u} C
this✝¹ : IsSmall.{w, v, u} I
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
X✝ Y✝ : Arrow C ⥤ Arrow C
f✝ : X✝ ⟶ Y✝
F : Arrow C ⥤ Arrow C
f : Arrow C
⊢ (coproducts.{w, v, u} I).pushouts (Arrow.Hom.left (((succStruct I κ).toSucc F).app f))

Tactic:
nth_rw 1 [← I.ofHoms_homFamily]
    apply pushouts_mk _ (functorObj_isPushout I.homFamily (F.obj f).hom)
    exact coproducts_of_small _ _ (colimitsOfShape_colimMap _ (by rintro ⟨j⟩; constructor))

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
⊢ IsColimit ((Set.principalSegIio m).cocone (functor hG A₀ J))

Tactic:
by
    have := hm.nonempty_Iio.to_subtype
    let c := (Set.principalSegIio m).cocone (functorToMonoOver hG A₀ J ⋙ MonoOver.forget _)
    have : Mono c.pt.hom := by dsimp [c]; infer_instance
    apply IsGrothendieckAbelian.isColimitMapCoconeOfSubobjectMkEqISup
      ((Set.principalSegIio m).monotone.functor ⋙ functorToMonoOver hG A₀ J) c
    dsimp [c]
    simp only [Subobject.mk_arrow]
    exact transfiniteIterate_limit (largerSubobject hG) A₀ m hm

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
⊢ False

Tactic:
apply CauSeq.not_limZero_of_not_congr_zero hf

Goal state after:
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
⊢ LimZero f
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝ : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → C ⥤ D i
h : JointlyFaithful F
X Y : C
f : X ⟶ Y
x✝ : ∀ (i : I), Epi ((F i).map f)
Z : C
g₁ g₂ : Y ⟶ Z
hg : f ≫ g₁ = f ≫ g₂
i : I
⊢ (F i).map g₁ = (F i).map g₂

Tactic:
by
    simp only [← cancel_epi ((F i).map f), ← Functor.map_comp, hg]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
⊢ ∃ Y g,
    ∃ (_ : (Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U))).arrows g),
      ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = u

Tactic:
obtain ⟨t, ht⟩ := shrinkYonedaObjObjEquiv.symm.surjective (f.app _ y)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
t : unop (op V) ⟶ U
ht : shrinkYonedaObjObjEquiv.symm t = (ConcreteCategory.hom (f.app (op V))) y
⊢ ∃ Y g,
    ∃ (_ : (Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U))).arrows g),
      ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = u
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (limSeq f j - limSeq f i) < ε

Tactic:
by
  have hε3 : 0 < ε / 3 := div_pos hε (by simp)
  let ⟨N, hN⟩ := exi_rat_seq_conv f hε3
  let ⟨N2, hN2⟩ := f.cauchy₂ hε3
  exists max N N2
  intro j hj
  suffices
    padicNormE (limSeq f j - f (max N N2) + (f (max N N2) - limSeq f (max N N2)) : ℚ_[p]) < ε by
    ring_nf at this
    rw [← padicNormE.eq_padic_norm']
    exact mod_cast this
  apply lt_of_le_of_lt
  · apply padicNormE.add_le
  · rw [← add_thirds ε]
    apply _root_.add_lt_add
    · suffices padicNormE (limSeq f j - f j + (f j - f (max N N2)) : ℚ_[p]) < ε / 3 + ε / 3 by
        simpa only [sub_add_sub_cancel]
      apply lt_of_le_of_lt
      · apply padicNormE.add_le
      · apply _root_.add_lt_add
        · rw [padicNormE.map_sub]
          apply mod_cast hN j
          exact le_of_max_le_left hj
        · exact hN2 _ (le_of_max_le_right hj) _ (le_max_right _ _)
    · apply mod_cast hN (max N N2)
      apply le_max_left

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
h : Isδ₀ (SimplexCategory.δ j.succ)
⊢ j.succ = 0

Tactic:
by simpa only [Isδ₀.iff] using h

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Monoidal

Goal state before:
pp: ⊢ Continuous (⇑homeomorph.symm ∘ unitInterval.symm ∘ ⇑homeomorph)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
⊢ ((toKaroubi (ChainComplex C ℕ)).obj K[X]).X ⟶ (N₁.obj X).X

Tactic:
by exact PInfty

Goal state after:
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
⊢ Continuous fun x ↦ ↑x.1

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
⊢ Continuous fun x ↦ (Set.projIcc 0 1 extend._proof_1 (2 * ↑x.1), x.2)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
⊢ Continuous fun x ↦ (Set.projIcc 0 1 extend._proof_1 (2 * ↑x.1 - 1), x.2)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: F : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
P : C(X, Y) → Prop
toFun : ↑I × X → Y
continuous_toFun : Continuous toFun
toContinuousMap : C(↑I × X, Y) := { toFun := toFun, continuous_toFun := continuous_toFun }
map_zero_left : ∀ (x : X), toFun (0, x) = f₀ x
map_one_left : ∀ (x : X), toFun (1, x) = f₁ x
toHomotopy : f₀.Homotopy f₁ :=
  { toContinuousMap := toContinuousMap, map_zero_left := map_zero_left, map_one_left := map_one_left }
t : ↑I
⊢ Continuous (Prod.mk t)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
⊢ Continuous fun x ↦ (x.1, Set.projIcc 0 1 extend._proof_2 (2 * ↑x.2))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
⊢ Continuous fun x ↦ (x.1, Set.projIcc 0 1 extend._proof_2 (2 * ↑x.2 - 1))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ Continuous fun x ↦ p ⟨↑(σ x.1) * ↑x.2 + ↑x.1 * ↑(f x.2), ⋯⟩

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂

Tactic:
convert! simply_connected_iff_paths_homotopic (Y := Y)
  simp [Path.Homotopic.Quotient, Setoid.eq_top_iff]; rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: case mp
Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ (PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂) →
    PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

Tactic:
intro ⟨hpc, hall⟩

Goal state after:
case mp
Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
hall : ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂
⊢ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ Continuous fun x ↦ ↑x.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ Continuous fun x ↦ 1 / 2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ ↑x.1 * 2 * ↑x.2) {x | ↑x.2 ≤ 1 / 2}

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ ↑x.1 * (2 - 2 * ↑x.2)) {x | 1 / 2 ≤ ↑x.2}

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Continuous fun x ↦ p ⟨reflTransSymmAux x, ⋯⟩

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ Continuous Subtype.val

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ 2 * ↑x) {x | ↑x ≤ 1 / 2}

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ 1) {x | 1 / 2 ≤ ↑x}

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Continuous fun t ↦ ⟨transReflReparamAux t, ⋯⟩

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ Continuous fun x ↦ 1 / 4

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ 2 * ↑x) {x | ↑x ≤ 1 / 4}

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ ↑x + 1 / 4) {x | ↑x ≤ 1 / 2}

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ 1 / 2 * (↑x + 1)) {x | 1 / 2 ≤ ↑x}

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
⊢ Continuous fun t ↦ ⟨transAssocReparamAux t, ⋯⟩

Tactic:
fun_prop

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ yonedaEquiv (yonedaEquiv.symm (face i j hij)) = face i j hij

Tactic:
Equiv.apply_symm_apply

Goal state after:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ face i j hij = face i j hij
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
x₂ : X₂
⊢ (∃ s, x₁ = (ConcreteCategory.hom f) s ∧ x₂ = (ConcreteCategory.hom g) s) → Rel' f g (Sum.inl x₁) (Sum.inr x₂)

Tactic:
· rintro ⟨s, rfl, rfl⟩
    exact Rel'.inl_inr _

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : Y.Quasicategory
⊢ X.Quasicategory

Tactic:
rw [quasicategory_iff_innerFibration] at hY ⊢

Goal state after:
X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : InnerFibration (terminal.from Y)
⊢ InnerFibration (terminal.from X)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ Subcomplex.range c.map ≤ (skeletonOfMono i) (d + 1)

Tactic:
simp [map, Subcomplex.range_eq_ofSimplex, mem_skeletonOfMono_obj_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) (spineToSimplex h p) = spineToSimplex h (p.interval 1 n ⋯)

Tactic:
rw [spineToSimplex_succ, δ₀_concat]

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

Goal state before:
pp: V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
G : EnrichedFunctor W D E
X✝ Y✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
⊢ (comp W F G).forget.map f ≫ (Iso.refl ((comp W F G).forget.obj Y✝)).hom =
    (Iso.refl ((comp W F G).forget.obj X✝)).hom ≫ (F.forget ⋙ G.forget).map f

Tactic:
by simp [comp, forget]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : (X ⊗ Y).obj n
⊢ x ∈ (S.unionProd T).obj n ↔ x.2 ∈ T.obj n ∨ x.1 ∈ S.obj n

Tactic:
by
  dsimp [unionProd, Set.prod]
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: X'✝ X✝ : ReflQuiv
Y✝ : Cat
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ forget.obj Y✝
⊢ ((Cat.Hom.equivFunctor (Cat.freeRefl.obj X'✝) Y✝).trans adj.homEquiv).symm (x✝¹ ≫ x✝) =
    Cat.freeRefl.map x✝¹ ≫ ((Cat.Hom.equivFunctor (Cat.freeRefl.obj X✝) Y✝).trans adj.homEquiv).symm x✝

Tactic:
by ext1; exact adj.homEquiv_naturality_left_symm _ _

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: y : OneTruncation₂ ((truncation 2).obj Δ[0])
⊢ default ⟶ y

Tactic:
obtain rfl : y = default := Unique.uniq _ _

Goal state after:
⊢ default ⟶ default
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X Y Z : Truncated 2
xyz : (X.HomotopyCategory × Y.HomotopyCategory) × Z.HomotopyCategory
⊢ (associativityIso X Y Z).hom.app xyz =
    𝟙 (((inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙ inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom).obj xyz)

Tactic:
dsimp [associativityIso]
  rw [associativity'Iso_hom_app _]
  dsimp
  rw [CategoryTheory.Functor.map_id, Category.id_comp, Category.comp_id,
    Category.comp_id, ← prod_id, CategoryTheory.Functor.map_id,
    CategoryTheory.Functor.map_id]

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
h : b ∈ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t

Tactic:
| inr h =>

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
h : b ∈ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t

Tactic:
| inr h =>

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg.«_@».Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne.3003013004._hygCtx._hyg.53.«1»
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
hj : (ConcreteCategory.hom f) i = (fun i ↦ i) ⟨1, ⋯⟩
⊢ 0 = (ConcreteCategory.hom f) i

Tactic:
exact (hS ⟨i, by simpa [S]⟩).elim

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right.inr
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
ht : t.Nonempty
h : t = {v}
⊢ t ∈ {s | ∃ v, s = {v}}

Tactic:
| inr h =>

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right.inr
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
ht : t.Nonempty
h : t = {v}
⊢ t ∈ {t | ∃ v, t = {v}}

Tactic:
| inr h =>

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right.inr
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
ht : t.Nonempty
h : t = {v}
⊢ t ∈ {s | ∃ v, s = {v}}

Tactic:
| inr h =>

Goal state after: