mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
s : Cofan fun i ↦ J.yoneda.obj (X i)
Y : C
i j : ι
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
⊢ (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b

Tactic:
by_cases h : i = j

Goal state after:
case pos
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
s : Cofan fun i ↦ J.yoneda.obj (X i)
Y : C
i j : ι
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
h : i = j
⊢ (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b

case neg
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
s : Cofan fun i ↦ J.yoneda.obj (X i)
Y : C
i j : ι
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
h : ¬i = j
⊢ (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
inst✝³ : Category.{v'', u''} E
J : Type w
inst✝² : LinearOrder J
F : J ⥤ C
G : C ⥤ D
inst✝¹ : F.IsWellOrderContinuous
inst✝ : PreservesWellOrderContinuousOfShape J G
j : J
hj : Order.IsSuccLimit j
⊢ IsColimit ((Set.principalSegIio j).cocone (F ⋙ G))

Tactic:
have := preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape G j hj

Goal state after:
C : Type u
D : Type u'
E : Type u''
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
inst✝³ : Category.{v'', u''} E
J : Type w
inst✝² : LinearOrder J
F : J ⥤ C
G : C ⥤ D
inst✝¹ : F.IsWellOrderContinuous
inst✝ : PreservesWellOrderContinuousOfShape J G
j : J
hj : Order.IsSuccLimit j
this : PreservesColimitsOfShape (↑(Set.Iio j)) G
⊢ IsColimit ((Set.principalSegIio j).cocone (F ⋙ G))
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ (extendToSucc hj F τ).map (homOfLE hi) =
    (extendToSuccObjIso hj F τ i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (extendToSuccObjIso hj F τ i₂ hi₂).inv

Tactic:
by
  rw [← extendToSuccObjIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
⊢ Arrow.mk (colimit.ι (inductiveSystem iter) ⟨k, hk⟩) = arrowι (restrictionLT (functor hj iter) hij) hi k hk

Tactic:
← arrowι_def _ hi

Goal state after:
case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
⊢ arrowι (inductiveSystem iter) hi k hk = arrowι (restrictionLT (functor hj iter) hij) hi k hk
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 : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
⊢ (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (↑(Set.Iic j)) f

Tactic:
have := (Subobject.isIso_arrow_iff_eq_top t).2 hj

Goal state after:
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 : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
this : IsIso t.arrow
⊢ (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (↑(Set.Iic j)) f
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
conv_lhs => rw [← q.num_divInt_den]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ padicValRat p (q.num /. ↑q.den) ≤ padicValRat p (q + r)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : q ≠ p
⊢ padicValNat q (p ^ n * q ^ m) = m

Tactic:
by
  rw [mul_comm (p ^ n) (q ^ m)]
  exact padicValNat_mul_pow_left m n ne

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : Fact (Prime p)
h : log p n < log p (n + 1)
⊢ log p (n + 1) ≤ padicValNat p (n + 1)

Tactic:
replace h := le_antisymm (add_one_le_iff.mpr (lt_pow_of_log_lt hp.out.one_lt h))
    (pow_log_le_self p n.succ_ne_zero)

Goal state after:
p n : ℕ
hp : Fact (Prime p)
h : n + 1 = p ^ log p (n + 1)
⊢ log p (n + 1) ≤ padicValNat p (n + 1)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
⊢ x.valuation ≤ 0

Tactic:
rw [Padic.norm_le_one_iff_val_nonneg, not_le] at hx

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : x.valuation < 0
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
⊢ x.valuation ≤ 0
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
⊢ ∃ l,
    ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj.left),
      l ≫ Pi.π (fun x ↦ M) ((ConcreteCategory.hom (Φ.fiber.map j.obj.hom)) y) = s.π.app (op j) ≫ Pi.π (fun t ↦ M) y

Tactic:
suffices ∀ (x : Φ.fiber.obj X), ∃ (l : s.pt ⟶ M),
      ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R g) (y : Φ.fiber.obj Y) (hy : Φ.fiber.map g y = x),
        s.π.app (op (Presieve.categoryMk _ _ hg)) ≫ Pi.π _ y = l by
    choose l hl using this
    exact ⟨Pi.lift l, fun j y ↦ by simpa using! (hl _ j.obj.hom  j.property y rfl).symm⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
⊢ ∀ (x : Φ.fiber.obj X),
    ∃ l,
      ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y),
        (ConcreteCategory.hom (Φ.fiber.map g)) y = x → s.π.app (op (R.arrows.categoryMk g hg)) ≫ Pi.π (fun t ↦ M) y = l
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
have hcl : g.norm = 0 := (norm_zero_iff g).2 hg

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
⊢ (f + g).norm ≤ max f.norm g.norm
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case inr
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₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
⊢ Presheaf.IsLocallySurjective J f

Tactic:
refine ⟨fun {U} s ↦ ?_⟩

Goal state after:
case inr
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₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
U : C
s : ToType (F₂.obj (op U))
⊢ Presheaf.imageSieve f s ∈ J U
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (lim' f) - ↑(↑(lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ padicNormE (↑(↑(lim' f) i) - ↑f i) < ε / 2

Tactic:
rw [padicNormE.map_sub]
      exact hN _ (le_of_max_le_left hi)

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

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (Q 0).f (n + 1) = ∑ i with ↑i < 0, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
simp only [Q_zero, HomologicalComplex.zero_f_apply, Nat.not_lt_zero,
      Finset.filter_false, Finset.sum_empty]

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
K : ChainComplex C ℕ
n : ℕ
⊢ Isδ₀ (SimplexCategory.δ 0)

Tactic:
rw [Isδ₀.iff]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ ¬Isδ₀ (SimplexCategory.δ b)

Tactic:
rw [Isδ₀.iff]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ ¬b = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ (N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂.map (𝟙 (N₂.obj P)))) ≫
      𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ 𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ N₂.map (Γ₂N₂.natTrans.app P) =
    𝟙 (N₂.obj P)

Tactic:
rw [Γ₂.map_id, N₂.map_id, comp_id, id_comp, id_comp, identity_N₂_objectwise P]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
⊢ (F.trans G).symm (t, snd✝) = (G.symm.trans F.symm) (t, snd✝)

Tactic:
trans_apply,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
⊢ (F.trans G).symm (t, snd✝) =
    if h : ↑(t, snd✝).1 ≤ 1 / 2 then G.symm (⟨2 * ↑(t, snd✝).1, ⋯⟩, (t, snd✝).2)
    else F.symm (⟨2 * ↑(t, snd✝).1 - 1, ⋯⟩, (t, snd✝).2)
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a✝¹ : Path a₁ a₂
b✝¹ : Path b₁ b₂
a✝ : Path a₂ a₃
b✝ : Path b₂ b₃
⊢ prod (Quotient.mk a✝¹) (Quotient.mk b✝¹) ⬝ prod (Quotient.mk a✝) (Quotient.mk b✝) =
    prod (Quotient.mk a✝¹ ⬝ Quotient.mk a✝) (Quotient.mk b✝¹ ⬝ Quotient.mk b✝)

Tactic:
simp only [prod_lift, ← Path.Homotopic.Quotient.mk_trans, Path.trans_prod_eq_prod_trans]

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

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X✝ = (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝

Tactic:
ext <;> simp <;> rfl

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

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

Tactic:
refine ⟨hpc, fun {x y} p₁ p₂ => ?_⟩

Goal state after:
case mpr
Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
hloops : ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
x y : Y
p₁ p₂ : Path x y
⊢ p₁.Homotopic p₂
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : C
f : X ⟶ Y
⊢ ∃ g, g ≫ pResolutionObj Y = pResolutionObj X ≫ f

Tactic:
have sq : CommSq (initial.to _) (initial.to _) (pResolutionObj Y)
    (pResolutionObj X ≫ f) := ⟨by simp⟩
  exact ⟨sq.lift, sq.fac_right⟩

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst✝ : LinearOrder ι
i j : ι
⊢ V i j = V j i

Tactic:
h.eq_inf,

Goal state after:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst✝ : LinearOrder ι
i j : ι
⊢ U i ⊓ U j = V j i
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst✝ : LinearOrder ι
i j : ι
⊢ U i ⊓ U j = V j i

Tactic:
h.eq_inf,

Goal state after:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst✝ : LinearOrder ι
i j : ι
⊢ U i ⊓ U j = U j ⊓ U i
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case neg.inl
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd✝ : n ≤ d
S : Finset (Fin (n + 1 + 1))
hS : S.card = d + 1
hx : stdSimplex.face S ≤ A
hd : n < d
⊢ stdSimplex.face S ≤ Λ[n + 1, i]

pp: case neg.inr
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : S.card = n + 1
⊢ stdSimplex.face S ≤ Λ[n + 1, i]

Tactic:
· obtain rfl : S = .univ := by
          rw [← Finset.card_eq_iff_eq_univ, Fintype.card_fin]
          exact le_antisymm (card_finset_fin_le S) (by lia)
        exact (h (le_trans (by simp) hx)).elim

Goal state after:
case neg.inr
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : S.card = n + 1
⊢ stdSimplex.face S ≤ Λ[n + 1, i]
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
h₁ : ¬k = i
h₂ : ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = k
l : Fin (d + 1)
hl : j l = k.rev
⊢ False

Tactic:
by grind [h₂ l.rev]

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

Goal state before:
pp: case a
X : SSet
n : ℕ
⊢ X.skeleton (n + 1) ≤ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x

pp: case a
X : SSet
n : ℕ
⊢ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x ≤ X.skeleton (n + 1)

Tactic:
· conv_lhs => dsimp [skeleton]
    simp only [iSup_le_iff]
    rintro ⟨d, hd⟩ x
    rw [Nat.lt_succ_iff] at hd
    obtain hd | rfl := hd.lt_or_eq
    · exact (X.ofSimplex_le_skeleton _ hd).trans le_sup_left
    · exact le_trans (le_trans (by rfl) (le_iSup _ x)) le_sup_right

Goal state after:
case a
X : SSet
n : ℕ
⊢ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x ≤ X.skeleton (n + 1)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
⊢ ∀ {a b c d : CatEnriched C} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
    hComp η (𝟙 (g ≫ h)) = (eqToIso ⋯).inv ≫ hComp (hComp η (𝟙 g)) (𝟙 h) ≫ (eqToIso ⋯).hom

Tactic:
simp [hComp_assoc]

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

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
⊢ ∀ {a b c d : CatEnriched C} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
    hComp (hComp (𝟙 f) η) (𝟙 h) = (eqToIso ⋯).hom ≫ hComp (𝟙 f) (hComp η (𝟙 h)) ≫ (eqToIso ⋯).inv

Tactic:
simp [hComp_assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ hComp (hComp η θ) κ ≍ hComp η (hComp θ κ)

Tactic:
simp [hComp_assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b c d : CatEnrichedOrdinary C} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
    hComp η (𝟙 (g ≫ h)) = (eqToIso ⋯).inv ≫ hComp (hComp η (𝟙 g)) (𝟙 h) ≫ (eqToIso ⋯).hom

Tactic:
simp [hComp_assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b c d : CatEnrichedOrdinary C} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
    hComp (hComp (𝟙 f) η) (𝟙 h) = (eqToIso ⋯).hom ≫ hComp (𝟙 f) (hComp η (𝟙 h)) ≫ (eqToIso ⋯).inv

Tactic:
simp [hComp_assoc]

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

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).image (β_ X Y).hom = T.unionProd S

Tactic:
rw [← preimage_β_hom, preimage_image_of_isIso]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (ρ_ X).inv.f = (ρ_ X.fst).inv

Tactic:
apply Iso.inv_ext' -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`
  rw [← rightUnitor_hom_f, ← comp_f, Iso.hom_inv_id]; rfl

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

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homTo W (f ≫ g) =
    Functor.LaxMonoidal.ε F ≫
      F.map
        ((λ_ (𝟙_ V)).inv ≫
          ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f) ⊗ₘ
              (e (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W g)) ≫
            eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝))

Tactic:
simp only [ForgetEnrichment.homTo_comp, eComp_eq, Category.assoc, Functor.map_comp]

Goal state after:
V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (λ_ (𝟙_ W)).inv ≫
      (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g) ≫
        Functor.LaxMonoidal.μ F (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)
            (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝) ≫
          F.map (eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)) =
    Functor.LaxMonoidal.ε F ≫
      F.map (λ_ (𝟙_ V)).inv ≫
        F.map
            ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f) ⊗ₘ
              (e (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W g)) ≫
          F.map (eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝))