mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ C₂ ⥤ C₃
e : F ≅ F'
⊢ sq.inl ≫ (Iso.refl sq.pt).hom = ((e.app Y₁).app X₂).hom ≫ (e.inv.app Y₁).app X₂ ≫ sq.inl

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ C₂ ⥤ C₃
e : F ≅ F'
⊢ sq.inr ≫ (Iso.refl sq.pt).hom = ((e.app X₁).app Y₂).hom ≫ (e.inv.app X₁).app Y₂ ≫ sq.inr

Tactic:
by simp

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonempty
⊢ Classical.arbitrary (X _⦋0⦌) ∈ X.nonDegenerate 0

Tactic:
by simp

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

Goal state before:
pp: X : SSet
x✝ : X.HasDimensionLT 0
x : X _⦋0⦌
⊢ x ∈ X.nonDegenerate 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) ≫
      pushout.desc ((initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to X.left) (ρ_ X.left).hom ⋯ ≫
        (ρ_ X.left).inv ≫
          pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
            (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) =
    pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) ≫
      𝟙 (X □ Arrow.mk (initial.to (𝟙_ C))).left

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) ≫
      { hom := pushout.desc ((initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to X.left) (ρ_ X.left).hom ⋯,
            inv :=
              (ρ_ X.left).inv ≫
                pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
                  (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom),
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        X.hom =
    pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) ≫
      (X □ Arrow.mk (initial.to (𝟙_ C))).hom ≫ (ρ_ X.right).hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X : Arrow C
T : C
t : IsTerminal T
W : C
this✝ : IsIso ((MonoidalClosed.pre X.hom).app T)
this :
  IsPullback (𝟙 (X.left ⟹ W)) ((IsTerminal.isTerminalObj (ihom X.right) T t).from (X.left ⟹ W))
    ((ihom X.left).map (t.from W)) ((MonoidalClosed.pre X.hom).app T)
⊢ (((Iso.refl
              ((MonoidalClosed.internalHom.obj (Opposite.op (Opposite.unop (Opposite.op X)).right)).obj
                (Arrow.mk (t.from W)).left)).hom ≫
          (MonoidalClosed.pre X.hom).app W) ≫
        this.isoPullback.hom) ≫
      pullback.fst ((ihom X.left).map (t.from W)) ((MonoidalClosed.pre X.hom).app T) =
    (PullbackObjObj.ofHasPullback MonoidalClosed.internalHom (Opposite.unop (Opposite.op X)).hom
          (Arrow.mk (t.from W)).hom).π ≫
      pullback.fst ((ihom X.left).map (t.from W)) ((MonoidalClosed.pre X.hom).app T)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X : Arrow C
I : C
i : IsInitial I
W : C
this✝ : IsIso ((ihom I).map X.hom)
this :
  IsPullback ((isTerminalTensorUnit.ofIso (powZero i).symm).from (W ⟹ X.right)) (𝟙 (W ⟹ X.right)) ((ihom I).map X.hom)
    ((MonoidalClosed.pre (i.to W)).app X.right)
⊢ (((Iso.refl
              ((MonoidalClosed.internalHom.obj
                    (Opposite.op (Opposite.unop (Opposite.op (Arrow.mk (i.to W)))).right)).obj
                X.left)).hom ≫
          (ihom W).map X.hom) ≫
        this.isoPullback.hom) ≫
      pullback.snd ((ihom I).map X.hom) ((MonoidalClosed.pre (i.to W)).app X.right) =
    (PullbackObjObj.ofHasPullback MonoidalClosed.internalHom (Opposite.unop (Opposite.op (Arrow.mk (i.to W)))).hom
          X.hom).π ≫
      pullback.snd ((ihom I).map X.hom) ((MonoidalClosed.pre (i.to W)).app X.right)

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ (parallelPair ((sigmaConst.obj R).map (SimplicialObject.δ X 1) - (sigmaConst.obj R).map (SimplicialObject.δ X 0))
            0).map
        WalkingParallelPairHom.right ≫
      (Iso.refl
          ((parallelPair
                ((sigmaConst.obj R).map (SimplicialObject.δ X 1) - (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                0).obj
            WalkingParallelPair.one)).hom =
    (-Iso.refl
            ((parallelPair
                  ((sigmaConst.obj R).map (SimplicialObject.δ X 1) - (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                  0).obj
              WalkingParallelPair.zero)).hom ≫
      (parallelPair ((X.chainComplex R).d 1 0) 0).map WalkingParallelPairHom.right

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
inst✝ : CategoryWithHomology C
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
inst✝ : CategoryWithHomology C
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
inst✝ : CategoryWithHomology C
x : X _⦋0⦌
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
inst✝ : CategoryWithHomology C
x : X _⦋0⦌
⊢ X.ιChainComplex x ≫ (X.chainComplex R).d 0 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
inst✝ : X.IsConnected
x : X.π₀ := Classical.arbitrary X.π₀
⊢ (Sigma.ι (fun x ↦ R) x ≫ Sigma.desc fun x ↦ 𝟙 R) = 𝟙 R

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
pt : C₂
fst : pt ⟶ (G.obj (op X₁)).obj X₃
snd : pt ⟶ (G.obj (op Y₁)).obj Y₃
isPullback : IsPullback fst snd ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
⊢ (G.map f₁.op).app X₃ ≫ (G.obj (op X₁)).map f₃ = (G.obj (op Y₁)).map f₃ ≫ (G.map f₁.op).app Y₃

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
inst✝ : HasPullback ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
⊢ (G.map f₁.op).app X₃ ≫ (G.obj (op X₁)).map f₃ = (G.obj (op Y₁)).map f₃ ≫ (G.map f₁.op).app Y₃

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
hs✝ : (s₁, objMk₁ 0) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, objMk₁ 0) ⋯ = OrderHom.id
this : (orderHomOfSimplex (s₁, objMk₁ 0) ⋯) 0 = OrderHom.id 0
⊢ 0 ≤ Fin.castSucc 0

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
h : is.castSucc ∈ Ss
⊢ is.castSucc < is.succ

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
hs✝ : (s₁, objMk₁ (Fin.last (p + 1)).succ) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, objMk₁ (Fin.last (p + 1)).succ) ⋯ = OrderHom.id
this : (orderHomOfSimplex (s₁, objMk₁ (Fin.last (p + 1)).succ) ⋯) (Fin.last (p + 1)) = OrderHom.id (Fin.last (p + 1))
⊢ (Fin.last (p + 1)).castSucc < Fin.last (p + 2)

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
this : St = Finset.image it.succ.succAbove Sδ ∪ {it.succ}
⊢ Disjoint (Finset.image it.succ.succAbove Sδ) {it.succ}

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ i.castSucc.succ.castSucc < i.castSucc.succ.succ

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ i.castSucc.castSucc.succ ≤ i.castSucc.succ.castSucc

Tactic:
by simp

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

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] i.succ)) (stdSimplex.objMk₁ j.castSucc.castSucc.succ)).2
      k =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
          stdSimplex.objMk₁ j.castSucc.succ).2
      k

Tactic:
rw [stdSimplex.δ_objMk₁_of_le _ _ (by simpa using! Fin.le_of_lt hij)]
      rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
x✝ : X.op.PtSimplex n (opObjEquiv.symm x)
⊢ (fun g ↦ { map := yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map)), comm := ⋯ })
      ((fun f ↦ { map := yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map)), comm := ⋯ }) x✝) =
    x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
x✝ : X.PtSimplex n x
⊢ (fun f ↦ { map := yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map)), comm := ⋯ })
      ((fun g ↦ { map := yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map)), comm := ⋯ }) x✝) =
    x✝

Tactic:
by simp

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x✝ : X.N
⊢ SemiSimplexCategory.toSimplexCategory.map (SemiSimplexCategory.homOfMono (monoOfLE ⋯)) =
    SemiSimplexCategory.toSimplexCategory.map (𝟙 ⦋x✝.dim⦌ₛ)

Tactic:
by simp

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
X✝ Y✝ Z✝ : X.N
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ SemiSimplexCategory.toSimplexCategory.map (SemiSimplexCategory.homOfMono (monoOfLE ⋯)) =
    SemiSimplexCategory.toSimplexCategory.map
      (SemiSimplexCategory.homOfMono (monoOfLE ⋯) ≫ SemiSimplexCategory.homOfMono (monoOfLE ⋯))

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : f.RelStruct g i.castSucc
j : Fin (n + 2)
hj : i.succ.succ < j
⊢ i.castSucc.succ < i.succ.succ

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : f.RelStruct g i.succ
j : Fin (n + 2)
hj : j < i.castSucc.castSucc
⊢ i.castSucc.castSucc < i.succ.castSucc

Tactic:
by simp

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

Goal state before:
pp: X : TopCat
x✝ : C(↑(stdSimplex ℝ (Fin ((Opposite.unop (Opposite.op ⦋1⦌)).len + 1))), ↑X)
⊢ (fun f ↦ (Hom.hom f).comp ↑stdSimplexHomeomorphI) ((fun f ↦ ofHom (f.comp ↑stdSimplexHomeomorphI.symm)) x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: X : TopCat
x✝ : I ⟶ X
⊢ (fun f ↦ ofHom (f.comp ↑stdSimplexHomeomorphI.symm)) ((fun f ↦ (Hom.hom f).comp ↑stdSimplexHomeomorphI) x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
⊢ (sSetTopAdj.homEquiv Δ[0] X) f = SSet.const (TopCat.toSSetObj₀Equiv.symm ((ConcreteCategory.hom f) default))

Tactic:
by
  have : sSetTopAdj.unit.app Δ[0] =
      SSet.const (TopCat.toSSetObj₀Equiv.symm default) :=
    SSet.yonedaEquiv.injective (TopCat.toSSetObj₀Equiv.injective (by subsingleton))
  rw [Adjunction.homEquiv_unit, TopCat.toSSetObj₀Equiv_symm_apply, this]
  rfl

Goal state after:
Module: Mathlib.Analysis.Convex.Contractible

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x✝ : E
h : StarConvex ℝ x✝ s
hne : s.Nonempty
x : ↑s
⊢ { toFun := fun p ↦ ⟨↑p.1 • x✝ + (1 - ↑p.1) • ↑p.2, ⋯⟩, continuous_toFun := ?m.76 }.toFun (0, x) =
    (ContinuousMap.id ↑s) x

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Convex.Contractible

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x✝ : E
h : StarConvex ℝ x✝ s
hne : s.Nonempty
x : ↑s
⊢ { toFun := fun p ↦ ⟨↑p.1 • x✝ + (1 - ↑p.1) • ↑p.2, ⋯⟩, continuous_toFun := ?m.76 }.toFun (1, x) =
    (ContinuousMap.const ↑s ⟨x✝, ⋯⟩) x

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
H :
  ∀ (x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })) (y : Y.obj (op { obj := ⦋2⦌, property := _proof_14 })),
    f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x) =
        (ConcreteCategory.hom (Y.map (δ₂ 2 _proof_12 _proof_15).op)) y →
      f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_12 _proof_15).op)) y →
        f₁ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_12 _proof_15).op)) y
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })
⊢ 1 ≤ 1 + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
inst✝² : Semiring R
v : AbsoluteValue R S
T : Type u_3
U : Type u_4
inst✝¹ : Semiring T
inst✝ : Semiring U
w : AbsoluteValue T S
u : AbsoluteValue U S
f✝ : R →+* T
g✝ : T →+* U
f : R ≃+* T
g : T ≃+* U
x : WithAbs v
⊢ (map w v f.symm.toRingHom) ((↑↑(map v w f.toRingHom)).toFun x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
inst✝² : Semiring R
v : AbsoluteValue R S
T : Type u_3
U : Type u_4
inst✝¹ : Semiring T
inst✝ : Semiring U
w : AbsoluteValue T S
u : AbsoluteValue U S
f✝ : R →+* T
g✝ : T →+* U
f : R ≃+* T
g : T ≃+* U
x : WithAbs w
⊢ (↑↑(map v w f.toRingHom)).toFun ((map w v f.symm.toRingHom) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : Semiring R
v w : AbsoluteValue R S
x : WithAbs w
⊢ (equiv v) ((congr v w (RingEquiv.refl R)).symm x) = (equiv w) x

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : Semiring R
v w : AbsoluteValue R S
x : R
⊢ (congr v w (RingEquiv.refl R)) ((equiv v).symm x) = (equiv w).symm x

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : Semiring R
v w : AbsoluteValue R S
x : R
⊢ (congr v w (RingEquiv.refl R)).symm ((equiv w).symm x) = (equiv v).symm x

Tactic:
by simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ i, f i
⊢ (sum fun x ↦ a) = #ι * a

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddGroup E
inst✝³ : MulActionWithZero 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝²] s
h's : s.Nonempty
⊢ #↑s = #E

Tactic:
rcases h's with ⟨x, hx⟩

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddGroup E
inst✝³ : MulActionWithZero 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝²] s
x : E
hx : x ∈ s
⊢ #↑s = #E
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop
hcⱼ : ∀ (j : ι), j ≠ i → ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → ∃ a, ∀ (b : ℕ), a ≤ b → (v j) (c b) ∈ s
r₁ : ℕ
hr₁ : ∀ (a : ℕ), r₁ ≤ a → 2 ≤ (v i) (c a)
j : ι
hj : j ≠ i
⊢ 0 ∈ Set.Iio 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Complex.OperatorNorm

Goal state before:
pp: ⊢ 1 = ‖reCLM 1‖

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Complex.OperatorNorm

Goal state before:
pp: ⊢ ‖1‖ ≤ 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Complex.OperatorNorm

Goal state before:
pp: ⊢ 1 = ‖imCLM I‖

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Complex.OperatorNorm

Goal state before:
pp: ⊢ ‖I‖ ≤ 1

Tactic:
by simp

Goal state after: