mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
⊢ HigherFacesVanish (n + 1) (((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)))

Tactic:
intro j

Goal state after:
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)
⊢ n + 1 ≤ ↑j + (n + 1) →
    ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫ (Γ₀.obj K).δ j.succ = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₁ : ∀ (i : ℕ), (N₁.map f ≫ inv (N₁.map f)).f.f i = (𝟙 (N₁.obj X)).f.f i
h₂ : ∀ (i : ℕ), (inv (N₁.map f) ≫ N₁.map f).f.f i = (𝟙 (N₁.obj Y)).f.f i
h₃ :
  ∀ (n : ℕ),
    (N₁.obj Y).p.f n ≫ (inv (N₁.map f)).f.f n ≫ f.app (op ⦋n⦌) =
      (inv (N₁.map f)).f.f n ≫ (N₁.obj X).p.f n ≫ f.app (op ⦋n⦌)
⊢ ∀ (n : ℕ), IsIso (f.app (op ⦋n⦌))

Tactic:
simp only [N₁_map_f, Karoubi.comp_f, HomologicalComplex.comp_f,
      AlternatingFaceMapComplex.map_f, N₁_obj_p, Karoubi.id_f, assoc] at h₁ h₂ h₃

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ : ∀ (i : ℕ), (inv (N₁.map f)).f.f i ≫ PInfty.f i ≫ f.app (op ⦋i⦌) = PInfty.f i
h₃ :
  ∀ (n : ℕ), PInfty.f n ≫ (inv (N₁.map f)).f.f n ≫ f.app (op ⦋n⦌) = (inv (N₁.map f)).f.f n ≫ PInfty.f n ≫ f.app (op ⦋n⦌)
h₁ : ∀ (i : ℕ), PInfty.f i ≫ f.app (op ⦋i⦌) ≫ (inv (N₁.map f)).f.f i = PInfty.f i
⊢ ∀ (n : ℕ), IsIso (f.app (op ⦋n⦌))
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ N₂Γ₂ToKaroubiIso.hom.app K ≫ N₁Γ₀.hom.app K =
    Preadditive.DoldKan.equivalence.functor.map (isoΓ₀.hom.app K) ≫ isoN₁.hom.app (Γ.obj K) ≫ N₁Γ₀.hom.app K

Tactic:
simp

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
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
⊢ K[X].d i j ≫ 𝟙 (X _⦋j⦌) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : ReflQuiver U
inst✝ : ReflQuiver V
F : U ⥤rq V
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = F.map f

Tactic:
simp

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

Goal state before:
pp: X Y Z : TopCat
f₀ f₁ : X ⟶ Y
g₀ g₁ : Y ⟶ Z
G : Homotopy g₀ g₁
F : Homotopy f₀ f₁
x✝ : ↑(X ⊗ I)
⊢ (ConcreteCategory.hom (G.comp F).h) x✝ =
    (ConcreteCategory.hom (X ◁ lift (𝟙 I) (𝟙 I) ≫ (α_ X I I).inv ≫ F.h ▷ I ≫ G.h)) x✝

Tactic:
simp

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 s.nondegComplex)).f = 𝟙 s.nondegComplex

Tactic:
simp

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
⊢ s.fromNondegComplex ≫ s.toNondegComplex = 𝟙 s.nondegComplex

Tactic:
simp

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
⊢ s.toNondegComplex ≫ s.fromNondegComplex = PInfty

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.SingleObj

Goal state before:
pp: case cons
α : Type u_1
x b✝ c✝ : SingleObj α
a✝¹ : Path (star α) b✝
a✝ : b✝ ⟶ c✝
ih : listToPath (pathToList a✝¹) = Path.cast ⋯ ⋯ a✝¹
⊢ listToPath (pathToList (a✝¹.cons a✝)) = Path.cast ⋯ ⋯ (a✝¹.cons a✝)

Tactic:
dsimp [pathToList] at *; rw [ih]

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
⊢ MonoidHom.id M = e.symm.toMonoidHom.comp e.toMonoidHom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
⊢ e.toMonoidHom.comp e.symm.toMonoidHom = MonoidHom.id N

Tactic:
simp

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₁ : C(X, Y)
F : f₀.Homotopy f₁
a✝ : X
⊢ (F.curry 0) a✝ = f₀ a✝

Tactic:
simp

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₁ : C(X, Y)
F : f₀.Homotopy f₁
a✝ : X
⊢ (F.curry 1) a✝ = f₁ a✝

Tactic:
simp

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₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ F.extend 0 = f₀

Tactic:
simp

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₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ F.extend 1 = f₁

Tactic:
simp

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)
F : f₀.Homotopy f₁
⊢ ∀ (x : X), F (σ (0, x).1, (0, x).2) = f₁ x

Tactic:
simp

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₁ : C(X, Y)
F : f₀.Homotopy f₁
x✝ : ↑I × X
⊢ F.symm.symm x✝ = F x✝

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.EilenbergSteenrod

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Limits.HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
HP HP' : HomologyPretheory C c
f : HP ⟶ HP'
i : ι
⊢ (HP.iso i).hom ≫ incl.whiskerLeft (f.homₚ i) ≫ (HP'.iso i).inv = f.hom i

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ (piLimitFan F).proj j = s.proj j
⊢ ∀ (i : J), m ⋙ Pi.eval (fun i ↦ ↑(F i)) i = (Functor.pi' fun j ↦ s.proj j) ⋙ Pi.eval (fun i ↦ ↑(F i)) i

Tactic:
intro j

Goal state after:
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ (piLimitFan F).proj j = s.proj j
j : J
⊢ m ⋙ Pi.eval (fun i ↦ ↑(F i)) j = (Functor.pi' fun j ↦ s.proj j) ⋙ Pi.eval (fun i ↦ ↑(F i)) j
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)
g₀ g₁ : C(Y, Z)
G : g₀.Homotopy g₁
F : f₀.Homotopy f₁
⊢ ∀ (x : X), G ((0, x).1, F (0, x)) = (g₀.comp f₀) x

Tactic:
simp

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)
g₀ g₁ : C(Y, Z)
G : g₀.Homotopy g₁
F : f₀.Homotopy f₁
⊢ ∀ (x : X), G ((1, x).1, F (1, x)) = (g₁.comp f₁) x

Tactic:
simp

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'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : ↑I
⊢ P { toFun := fun x ↦ (F.trans G.toHomotopy).toFun (t, x), continuous_toFun := ⋯ }

Tactic:
simp only [Homotopy.trans]
      change P ⟨fun _ => ite ((t : ℝ) ≤ _) _ _, _⟩
      split_ifs
      · exact F.extendProp _
      · exact G.extendProp _

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

Goal state before:
pp: I : Type u
X : I → TopCat
X✝ Y✝ : (i : I) → ↑(π.obj (X i))
f✝ : X✝ ⟶ Y✝
i✝ : I
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f✝ i✝ =
    (CategoryTheory.eqToHom ⋯ ≫ (𝟭 ((i : I) → ↑(π.obj (X i)))).map f✝ ≫ CategoryTheory.eqToHom ⋯) i✝

Tactic:
simp

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

Goal state before:
pp: case h_map
I : Type u
X : I → TopCat
X✝ Y✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
f : X✝ ⟶ Y✝
⊢ (Path.Homotopic.pi fun i ↦ (CategoryTheory.Functor.pi' (proj X)).map f i) = f

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (projLeft A B).obj { as := (X✝.1.as, X✝.2.as) } = X✝.1
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

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

Tactic:
simp

Goal state after:
case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (projRight A B).obj { as := (X✝.1.as, X✝.2.as) } = X✝.2
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

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

Tactic:
simp

Goal state after:
case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((projLeft A B).obj X✝).as = X✝.as.1
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

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

Tactic:
simp

Goal state after:
case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((projRight A B).obj X✝).as = X✝.as.2
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₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : ↑I
⊢ (F.curry t) 0 = x₀

Tactic:
simp

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₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : ↑I
⊢ (F.curry t) 1 = x₁

Tactic:
simp

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : ↑I
⊢ (F.eval 0) t = p₀ t

Tactic:
simp

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : ↑I
⊢ (F.eval 1) t = p₁ t

Tactic:
simp

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

Goal state before:
pp: case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y → (ContinuousMap.id Y).Nullhomotopic

Tactic:
intro
    apply id_nullhomotopic

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : IndiscreteTopology Y
f g : C(X, Y)
⊢ ∀ (x : X),
    {
            toFun := fun x ↦
              match x with
              | (t, a) => if t = 0 then f a else g a,
            continuous_toFun := ⋯ }.toFun
        (0, x) =
      f x

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : IndiscreteTopology Y
f g : C(X, Y)
⊢ ∀ (x : X),
    {
            toFun := fun x ↦
              match x with
              | (t, a) => if t = 0 then f a else g a,
            continuous_toFun := ⋯ }.toFun
        (1, x) =
      g x

Tactic:
simp

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
x : ↑I × ↑I
⊢ ↑(σ x.1) + ↑x.1 = 1

Tactic:
simp

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

Goal state before:
pp: case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : ↑I
hx : x = 0
⊢ { toFun := fun x ↦ F ((t, x).1, σ (t, x).2), continuous_toFun := ⋯ } 0 = p.symm.toContinuousMap 0

Tactic:
simp

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

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : ↑I
hx : x = 1
⊢ { toFun := fun x ↦ F ((t, x).1, σ (t, x).2), continuous_toFun := ⋯ } 1 = p.symm.toContinuousMap 1

Tactic:
simp

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₁
F : p.Homotopy q
f : C(X, Y)
⊢ ∀ (x : ↑I), (⇑f ∘ ⇑F) (0, x) = (p.map ⋯).toContinuousMap x

Tactic:
simp

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₁
F : p.Homotopy q
f : C(X, Y)
⊢ ∀ (x : ↑I), (⇑f ∘ ⇑F) (1, x) = (q.map ⋯).toContinuousMap x

Tactic:
simp

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

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
x y : Y
p₁ p₂ : Path x y
hloops : ∀ (x : Y) (γ : Path x x), ⟦γ⟧ = ⟦Path.refl x⟧
h : Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧) = Path.Homotopic.Quotient.refl x
⊢ ⟦p₁⟧ = (Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧)).trans ⟦p₂⟧

Tactic:
simp

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

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ f (p' t✝) = H (((Path.refl { down := 0 }) t✝).down, p' t✝)

Tactic:
simp

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

Goal state before:
pp: case e'_2
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₂ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ x₀ = p₁ 0

Tactic:
simp

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

Goal state before:
pp: case e'_3
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₂ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ x₂ = p₂ 0

Tactic:
simp

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

Goal state before:
pp: case e'_2
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ x₁ = p₁ 1

Tactic:
simp

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

Goal state before:
pp: case e'_3
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ x₃ = p₂ 1

Tactic:
simp

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

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ g (p' t✝) = H (((Path.refl { down := 1 }) t✝).down, p' t✝)

Tactic:
simp

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

Goal state before:
pp: case refine_1
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
inst✝ : Nonempty Y
inhabited_h : Inhabited Y
x✝ : (const Y x₀).Homotopic (const Y x₁)
H : (const Y x₀).Homotopy (const Y x₁)
⊢ ((H.comp prodSwap).curry default).toFun 0 = x₀

Tactic:
simp

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

Goal state before:
pp: case refine_2
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
inst✝ : Nonempty Y
inhabited_h : Inhabited Y
x✝ : (const Y x₀).Homotopic (const Y x₁)
H : (const Y x₀).Homotopy (const Y x₁)
⊢ ((H.comp prodSwap).curry default).toFun 1 = x₁

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)
x : { x // x ∈ s }
p : Path ↑x ↑x
hp : ∀ (t : ↑unitInterval), p t ∈ s
⊢ ⟨p 0, ⋯⟩ = x

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)
x : { x // x ∈ s }
p : Path ↑x ↑x
hp : ∀ (t : ↑unitInterval), p t ∈ s
⊢ ⟨p 1, ⋯⟩ = x

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
x : ↑s
p : Path x x
F : (p.map ⋯).Homotopy (Path.refl ↑x)
hF : ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
⊢ ∀ (x_1 : ↑unitInterval), ⟨F (0, x_1), ⋯⟩ = p.toContinuousMap x_1

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
x : ↑s
p : Path x x
F : (p.map ⋯).Homotopy (Path.refl ↑x)
hF : ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
⊢ ∀ (x_1 : ↑unitInterval), ⟨F (1, x_1), ⋯⟩ = (Path.refl x).toContinuousMap x_1

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
x : ↑s
p : Path x x
F : (p.map ⋯).Homotopy (Path.refl ↑x)
hF : ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
⊢ ∀ (t x_1 : ↑unitInterval),
    x_1 ∈ {0, 1} → { toFun := fun x_2 ↦ ⟨F (t, x_2), ⋯⟩, continuous_toFun := ⋯ } x_1 = p.toContinuousMap x_1

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ toHoCat.Full

Tactic:
by dsimp [toHoCat]; infer_instance

Goal state after:
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
⊢ initial.to (resolutionObj Y) ≫ pResolutionObj Y = initial.to (resolutionObj X) ≫ pResolutionObj X ≫ f

Tactic:
simp

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₁
⊢ (p.symm.trans (Path.refl x₀)).symm = (Path.refl x₀).trans p

Tactic:
simp

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₁
⊢ p.symm.symm = p

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
h : weakEquivalences C x✝
⊢ (weakEquivalences (HoCat C)).inverseImage resolution x✝

Tactic:
by
    simpa only [MorphismProperty.inverseImage_iff, ← weakEquivalence_iff, HoCat.resolution,
      weakEquivalence_toHoCat_map_iff, weakEquivalence_resolutionMap_iff,
      weakEquivalence_homMk_iff] using h

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
x✝¹ x✝ : CofibrantObject C
f : x✝¹ ⟶ x✝
⊢ homMk (resolutionMap (ι.map f)) ≫ { hom := pResolutionObj (ι.obj x✝) } = { hom := pResolutionObj (ι.obj x✝¹) } ≫ f

Tactic:
ext : 1
    exact HoCat.resolutionMap_fac f.hom

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
R₀ : (localizerMorphism C).LeftResolution X :=
  { X₁ := mk (HoCat.resolutionObj X), w := HoCat.pResolutionObj X, hw := ⋯ }
R : (localizerMorphism C).LeftResolution X
⊢ initial.to ((localizerMorphism C).functor.obj R₀.X₁) ≫ R₀.w =
    initial.to ((localizerMorphism C).functor.obj R.X₁) ≫ R.w

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f : X ⟶ Y
⊢ leftHomotopyClassToHom L (LeftHomotopyClass.mk f) =
    (rightHomotopyClassToHom L ∘ ⇑leftHomotopyClassEquivRightHomotopyClass) (LeftHomotopyClass.mk f)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ toHoCat.Full

Tactic:
by dsimp [toHoCat]; infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
this✝ : ∀ (Y : C) [IsFibrant Y], IsCofibrant Y → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsCofibrant Y
Y' : C
w✝ : IsCofibrant Y'
p : Y' ⟶ Y
left✝ : Fibration p
right✝ : WeakEquivalence p
x✝ : IsFibrant Y'
hY' : Function.Bijective (leftHomotopyClassToHom L)
this : IsIso (L.map p)
f : X ⟶ Y'
⊢ (leftHomotopyClassToHom L ∘ fun f ↦ f.postcomp p) (LeftHomotopyClass.mk f) =
    (⇑((Iso.refl (L.obj X)).homCongr (asIso (L.map p))) ∘ leftHomotopyClassToHom L) (LeftHomotopyClass.mk f)

Tactic:
simp

Goal state after: