mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.Ordered

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
⊢ ⇑(s.sup' H f) = s.sup' H fun i ↦ ⇑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Ordered

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
⊢ ⇑(s.inf' H f) = s.inf' H fun i ↦ ⇑(f i)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ homeomorph 0 = 0

Tactic:
by

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

Goal state before:
pp: ⊢ homeomorph 1 = 1

Tactic:
by

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

Goal state before:
pp: ⊢ (ConcreteCategory.hom symm) 1 = 0

Tactic:
by

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

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ ∀ b ∈ Finset.univ,
    b ≠ IndexSet.id (op ⦋i⦌) →
      ((s.πSummand b ≫ (s.cofan (op ⦋i⦌)).inj b) ≫ K[X].d i j) ≫ s.πSummand (IndexSet.id (op ⦋j⦌)) = 0

Tactic:
intro A _ hA
              simp only [assoc, s.ιSummand_comp_d_comp_πSummand_eq_zero _ _ _ hA, comp_zero]

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

Goal state before:
pp: ⊢ (ConcreteCategory.hom symm) 0 = 1

Tactic:
by

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 : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ s.πSummand (IndexSet.id (op ⦋i⦌)) ≫ ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex).X.d i j =
    (N₁.obj X).X.d i j ≫ s.πSummand (IndexSet.id (op ⦋j⦌))

Tactic:
by

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
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
⊢ (((N₁ ⋙ Γ₂).obj X).X.map θ ≫ (Γ₀.splitting K[X]).desc Δ' fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op) =
    ((Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op) ≫
      ((toKaroubi (SimplicialObject C)).obj X).X.map θ

Tactic:
by

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
⊢ (N₁.obj X).p ≫
      { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ } ≫
        ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex).p =
    { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
⊢ ι₀ ≫ F.h = f₀

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
⊢ ι₁ ≫ F.h = f₁

Tactic:
by

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
⊢ { f := { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ }, comm := ⋯ } ≫
      { f := { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ } =
    𝟙 ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex)

Tactic:
by

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
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ ((N₁ ⋙ Γ₂).obj X).p ≫
      { app := fun Δ ↦ (Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op, naturality := ⋯ } ≫
        ((toKaroubi (SimplicialObject C)).obj X).p =
    { app := fun Δ ↦ (Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op, naturality := ⋯ }

Tactic:
by

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₁
⊢ (G.comp F).h = X ◁ lift (𝟙 I) (𝟙 I) ≫ (α_ X I I).inv ≫ F.h ▷ I ≫ G.h

Tactic:
by

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
⊢ { f := { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ } ≫
      { f := { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ }, comm := ⋯ } =
    𝟙 (N₁.obj X)

Tactic:
by

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.toKaroubiNondegComplexIsoN₁.hom.f ≫ PInfty = s.toKaroubiNondegComplexIsoN₁.hom.f

Tactic:
by

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.toKaroubiNondegComplexIsoN₁.hom.f ≫ s.toKaroubiNondegComplexIsoN₁.inv.f = 𝟙 s.nondegComplex

Tactic:
by

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
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
f : X ⟶ Y
⊢ (N₁ ⋙ Γ₂).map f ≫
      {
        f :=
          { app := fun Δ ↦ (Γ₀.splitting K[Y]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ Y.map A.e.op,
            naturality := ⋯ },
        comm := ⋯ } =
    {
        f :=
          { app := fun Δ ↦ (Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op,
            naturality := ⋯ },
        comm := ⋯ } ≫
      (toKaroubi (SimplicialObject C)).map f

Tactic:
by

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

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 ℕ)).map (PInfty ≫ s.toNondegComplex) = (toKaroubi (ChainComplex C ℕ)).map s.toNondegComplex

Tactic:
by

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 ℕ)).map (s.fromNondegComplex ≫ s.toNondegComplex) =
    (toKaroubi (ChainComplex C ℕ)).map (𝟙 s.nondegComplex)

Tactic:
by

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
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ natTrans.app P = (N₂ ⋙ Γ₂).map P.decompId_i ≫ (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p

Tactic:
by

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
n : ℕ
⊢ s.toNondegComplex.f n = PInfty.f n ≫ s.toKaroubiNondegComplexIsoN₁.inv.f.f n

Tactic:
by

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
n : ℕ
⊢ s.fromNondegComplex.f n = s.ι n ≫ PInfty.f n

Tactic:
by

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:
by

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 ℕ)).map (s.toNondegComplex ≫ s.fromNondegComplex) =
    (toKaroubi (ChainComplex C ℕ)).map PInfty

Tactic:
by

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:
by

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
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X = (Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)

Tactic:
by

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
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ Φ.f i ≫ S₂.s.nondegComplex.d i j = S₁.s.nondegComplex.d i j ≫ Φ.f j

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X✝ Y✝ : Split C
Φ : X✝ ⟶ Y✝
⊢ (nondegComplexFunctor ⋙ toKaroubi (ChainComplex C ℕ)).map Φ ≫ Y✝.s.toKaroubiNondegComplexIsoN₁.hom =
    X✝.s.toKaroubiNondegComplexIsoN₁.hom ≫ (forget C ⋙ N₁).map Φ

Tactic:
by

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
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
      (N₂.map (Γ₂N₂.natTrans.app P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)

Tactic:
by

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
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂N₂.natTrans.app P) = 𝟙 (N₂.obj P)

Tactic:
by

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
inst✝ : HasFiniteCoproducts C
⊢ (𝟙 N₂ ◫ N₂Γ₂.inv) ≫ (N₂.associator Γ₂ N₂).inv ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂ = 𝟙 N₂

Tactic:
by

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
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ IsIso (N₂.map (Γ₂N₂.natTrans.app P))

Tactic:
by

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
inst✝ : HasFiniteCoproducts C
⊢ ∀ (P : Karoubi (SimplicialObject C)), IsIso (Γ₂N₂.natTrans.app P)

Tactic:
by

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
inst✝ : HasFiniteCoproducts C
⊢ IsIso Γ₂N₂.natTrans

Tactic:
by

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
inst✝ : HasFiniteCoproducts C
⊢ ∀ (X : SimplicialObject C), IsIso (Γ₂N₁.natTrans.app X)

Tactic:
by

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
inst✝ : HasFiniteCoproducts C
⊢ IsIso Γ₂N₁.natTrans

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ (u ⟶ v) = (u' ⟶ v')

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ cast hu hv e = _root_.cast ⋯ e

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' u'' v'' : U
e : u ⟶ v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ cast hu' hv' (cast hu hv e) = cast ⋯ ⋯ e

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ cast hu hv e ≍ e

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ cast hu hv e = e' ↔ e ≍ e'

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ e' = cast hu hv e ↔ e' ≍ e

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ Path u v = Path u' v'

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ cast hu hv p = _root_.cast ⋯ p

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' u'' v'' : U
p : Path u v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ cast hu' hv' (cast hu hv p) = cast ⋯ ⋯ p

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u u' : U
hu : u = u'
⊢ cast hu hu nil = nil

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ cast hu hv p ≍ p

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
p' : Path u' v'
⊢ cast hu hv p = p' ↔ p ≍ p'

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v w u' w' : U
p : Path u v
e : v ⟶ w
hu : u = u'
hw : w = w'
⊢ cast hu hw (p.cons e) = (cast hu ⋯ p).cons (Hom.cast ⋯ hw e)

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ p ≍ p'

Tactic:
exact heq_of_cons_eq_cons h

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ Path.cast ⋯ ⋯ p = p'

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ Hom.cast ⋯ ⋯ e = e'

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v : U
p : Path u v
hzero : p.length = 0
⊢ Path.cast ⋯ ⋯ p = nil

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : SingleObj α ⥤q SingleObj β
g : SingleObj β ⥤q SingleObj γ
⊢ toPrefunctor.symm (f ⋙q g) = toPrefunctor.symm g ∘ toPrefunctor.symm f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : SingleObj α
p : Path (star α) x
⊢ listToPath (pathToList p) = Path.cast ⋯ ⋯ p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ pathToList (listToPath l) = l

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: G : Type u
inst✝ : Group G
x y : SingleObj G
f : x ⟶ y
⊢ inv f = f⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝² : Monoid M
inst✝¹ : Group G
N : Type v
inst✝ : Monoid N
⊢ Function.LeftInverse (fun f ↦ { toFun := fun x ↦ f.map ((toEnd M) x), map_one' := ⋯, map_mul' := ⋯ }) fun f ↦
    { obj := id, map := fun {X Y} ↦ ⇑f, map_id := ⋯, map_comp := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝² : Monoid M
inst✝¹ : Group G
N : Type v
inst✝ : Monoid N
⊢ Function.RightInverse (fun f ↦ { toFun := fun x ↦ f.map ((toEnd M) x), map_one' := ⋯, map_mul' := ⋯ }) fun f ↦
    { obj := id, map := fun {X Y} ↦ ⇑f, map_id := ⋯, map_comp := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝³ : Monoid M
inst✝² : Group G
N : Type v
inst✝¹ : Monoid N
C : Type v
inst✝ : Category.{w, v} C
f : C → G
⊢ ∀ (X : C), f X * (f X)⁻¹ = 𝟙 ()

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝³ : Monoid M
inst✝² : Group G
N : Type v
inst✝¹ : Monoid N
C : Type v
inst✝ : Category.{w, v} C
f : C → G
⊢ ∀ {X Y Z : C} (f_1 : X ⟶ Y) (g : Y ⟶ Z), f Z * (f X)⁻¹ = (f Y * (f X)⁻¹) ≫ (f Z * (f Y)⁻¹)

Tactic:
by

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
⊢ 𝟭 (SingleObj M) = e.toMonoidHom.toFunctor ⋙ e.symm.toMonoidHom.toFunctor

Tactic:
by

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.symm.toMonoidHom.toFunctor ⋙ e.toMonoidHom.toFunctor = 𝟭 (SingleObj N)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: X✝ Y✝ : MonCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : toCat.map a₁✝ = toCat.map a₂✝
⊢ Hom.hom a₁✝ = Hom.hom a₂✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X✝¹ Y✝¹ X Y Z : TopPair
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
⊢ 𝟙 snd ≫ map = map ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X✝¹ Y✝¹ X✝ Y✝ Z : TopPair
X Y : TopPair
f : X ⟶ Y
⊢ ((𝟭 TopPair).map f ≫ ofHom (𝟙 fst) map ⋯).right = (ofHom (𝟙 fst) map ⋯ ≫ (proj₁ ⋙ diag).map f).right

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X Y : TopPair
f g : X ⟶ Y
H : Homotopy f g
x : ↑TopPair.snd
t : ↑unitInterval
⊢ H.fst (t, (ConcreteCategory.hom map) x) = (ConcreteCategory.hom map) (H.snd (t, x))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X Y : TopPair
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
⊢ F.symm.symm = F

Tactic:
by

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 : f₀.Homotopy f₁
toFun✝ : ↑I × X → Y
continuous_toFun✝ : Continuous toFun✝
map_zero_left✝ : ∀ (x : X), { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun (0, x) = f₀ x
map_one_left✝ : ∀ (x : X), { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun (1, x) = f₁ x
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_zero_left := map_zero_left✝,
        map_one_left := map_one_left✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_zero_left := map_zero_left✝,
      map_one_left := map_one_left✝ } =
    g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g

Goal state after:
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)
toFun✝¹ : ↑I × X → Y
continuous_toFun✝¹ : Continuous toFun✝¹
map_zero_left✝¹ : ∀ (x : X), { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ }.toFun (0, x) = f₀ x
map_one_left✝¹ : ∀ (x : X), { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ }.toFun (1, x) = f₁ x
toFun✝ : ↑I × X → Y
continuous_toFun✝ : Continuous toFun✝
map_zero_left✝ : ∀ (x : X), { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun (0, x) = f₀ x
map_one_left✝ : ∀ (x : X), { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun (1, x) = f₁ x
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹, map_zero_left := map_zero_left✝¹,
        map_one_left := map_one_left✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_zero_left := map_zero_left✝,
        map_one_left := map_one_left✝ }
⊢ { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹, map_zero_left := map_zero_left✝¹,
      map_one_left := map_one_left✝¹ } =
    { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_zero_left := map_zero_left✝,
      map_one_left := map_one_left✝ }
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 g : f₀.Homotopy f₁
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X✝ Y✝ X Y Z : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ map ▷ I ≫ Homotopy.h (F.fst.trans G.fst) = Homotopy.h (F.snd.trans G.snd) ≫ map

Tactic:
by

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.curry 0 = f₀

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm = G.symm.trans F.symm

Tactic:
by

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.curry 1 = f₁

Tactic:
by

Goal state after: