mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case pos
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ (F.eval x.1).extend (2 * ↑x.2) = (F.eval x.1) ⟨2 * ↑x.2, ⋯⟩

pp: case neg
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ (G.eval x.1).extend (2 * ↑x.2 - 1) = (G.eval x.1) ⟨2 * ↑x.2 - 1, ⋯⟩

Tactic:
<;>

Goal state after:
case pos
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ (F.eval x.1).extend (2 * ↑x.2) = (F.eval x.1) ⟨2 * ↑x.2, ⋯⟩

case neg
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ (G.eval x.1).extend (2 * ↑x.2 - 1) = (G.eval x.1) ⟨2 * ↑x.2 - 1, ⋯⟩
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: case left
Y : Type u_2
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y

pp: case right
Y : Type u_2
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)

Tactic:
<;>

Goal state after:
case left
Y : Type u_2
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y

case right
Y : Type u_2
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: case e'_2
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ x₀ = p 0

pp: case e'_3
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ x₂ = q 0

Tactic:
<;>

Goal state after:
case e'_2
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ x₀ = p 0

case e'_3
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ x₂ = q 0
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: case e'_2
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ x₁ = p 1

pp: case e'_3
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ x₃ = q 1

Tactic:
<;>

Goal state after:
case e'_2
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ x₁ = p 1

case e'_3
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ x₃ = q 1
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

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

Goal state after:
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

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

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

Goal state after:
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

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
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₀

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

Goal state after:
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₀

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₁
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case pos.left.ha
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1 * 2

pp: case hb
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.2

Tactic:
<;>

Goal state after:
case pos.left.ha
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1 * 2

case hb
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.2
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case pos.right.ha
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 ≤ 1

pp: case hb₀
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 * ↑x.2

pp: case hb
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 2 * ↑x.2 ≤ 1

Tactic:
<;>

Goal state after:
case pos.right.ha
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 ≤ 1

case hb₀
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 * ↑x.2

case hb
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 2 * ↑x.2 ≤ 1
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case neg.left.ha
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1

pp: case hb
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.2

Tactic:
<;>

Goal state after:
case neg.left.ha
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1

case hb
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.2
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case neg.right.ha
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 ≤ 1

pp: case hb₀
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.2

pp: case hb
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 2 - 2 * ↑x.2 ≤ 1

Tactic:
<;>

Goal state after:
case neg.right.ha
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 ≤ 1

case hb₀
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.2

case hb
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 2 - 2 * ↑x.2 ≤ 1
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ∈ I

pp: case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ∈ I

Tactic:
<;>

Goal state after:
case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ∈ I

case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ∈ I
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case pos.left
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ 2 * ↑t

pp: case pos.right
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ≤ 1

pp: case neg.left
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1

pp: case neg.right
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 1

Tactic:
<;>

Goal state after:
case pos.left
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ 2 * ↑t

case pos.right
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ≤ 1

case neg.left
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1

case neg.right
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 1
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:
by
  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.FundamentalGroupoid.Basic

Goal state before:
pp: case pos
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 2 * ↑t ∈ I

pp: case pos
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ ↑t + 1 / 4 ∈ I

pp: case neg
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 / 2 * (↑t + 1) ∈ I

Tactic:
<;>

Goal state after:
case pos
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 2 * ↑t ∈ I

case pos
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ ↑t + 1 / 4 ∈ I

case neg
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 / 2 * (↑t + 1) ∈ I
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case pos.left
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 0 ≤ 2 * ↑t

pp: case pos.right
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 2 * ↑t ≤ 1

pp: case pos.left
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ ↑t + 1 / 4

pp: case pos.right
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ ↑t + 1 / 4 ≤ 1

pp: case neg.left
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1 / 2 * (↑t + 1)

pp: case neg.right
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 / 2 * (↑t + 1) ≤ 1

Tactic:
<;>

Goal state after:
case pos.left
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 0 ≤ 2 * ↑t

case pos.right
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 2 * ↑t ≤ 1

case pos.left
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ ↑t + 1 / 4

case pos.right
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ ↑t + 1 / 4 ≤ 1

case neg.left
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1 / 2 * (↑t + 1)

case neg.right
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 / 2 * (↑t + 1) ≤ 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
U✝ V✝ : SimplexCategoryᵒᵖ
φ : U✝ ⟶ V✝
s : Δ[n].obj U✝
hs : s ∈ {s | Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}
h : Set.range ⇑(stdSimplex.asOrderHom ((ConcreteCategory.hom (Δ[n].map φ)) s)) ∪ {i} = Set.univ
⊢ Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} = Set.univ

Tactic:
Set.eq_univ_iff_forall

Goal state after:
n : ℕ
i : Fin (n + 1)
U✝ V✝ : SimplexCategoryᵒᵖ
φ : U✝ ⟶ V✝
s : Δ[n].obj U✝
hs : s ∈ {s | Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ⇑(stdSimplex.asOrderHom ((ConcreteCategory.hom (Δ[n].map φ)) s)) ∪ {i}
⊢ ∀ (x : Fin (n + 1)), x ∈ Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i}
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this : ∀ (j : Fin (n + 1)), j ≠ i → j ∈ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
k : Fin (⦋n⦌.len + 1)
h✝ : k = i
⊢ k ∈ Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} ↔ k ∈ ⊤

pp: case neg
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this : ∀ (j : Fin (n + 1)), j ≠ i → j ∈ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
k : Fin (⦋n⦌.len + 1)
h✝ : ¬k = i
⊢ k ∈ Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} ↔ k ∈ ⊤

Tactic:
<;>

Goal state after:
case pos
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this : ∀ (j : Fin (n + 1)), j ≠ i → j ∈ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
k : Fin (⦋n⦌.len + 1)
h✝ : k = i
⊢ k ∈ Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} ↔ k ∈ ⊤

case neg
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this : ∀ (j : Fin (n + 1)), j ≠ i → j ∈ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
k : Fin (⦋n⦌.len + 1)
h✝ : ¬k = i
⊢ k ∈ Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} ↔ k ∈ ⊤
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case false
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ false ∈ {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} ↔
    false ∈ Set.univ

pp: case true
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ true ∈ {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} ↔
    true ∈ Set.univ

Tactic:
<;>

Goal state after:
case false
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ false ∈ {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} ↔
    false ∈ Set.univ

case true
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ true ∈ {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} ↔
    true ∈ Set.univ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case neg.inl
n k : ℕ
h : k < n + 2
hk : ¬k = 0
hi : 0 < n + 4
h₀ : 0 < ⟨0, hi⟩
hₙ : ⟨0, hi⟩ < Fin.last (n + 3)
hS : {⟨0, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
⊢ False

pp: case neg.inr
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
hk : ¬0 = 0
⊢ False

Tactic:
<;>

Goal state after:
case neg.inl
n k : ℕ
h : k < n + 2
hk : ¬k = 0
hi : 0 < n + 4
h₀ : 0 < ⟨0, hi⟩
hₙ : ⟨0, hi⟩ < Fin.last (n + 3)
hS : {⟨0, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
⊢ False

case neg.inr
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
hk : ¬0 = 0
⊢ False
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s s' : S
hs' : (ConcreteCategory.hom g) s = (ConcreteCategory.hom g) s'
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inl ((ConcreteCategory.hom f) s'))

Tactic:
exact Rel'.inl_inl _ _ hs'

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
⊢ ∀ (a b : X₁ ⊕ X₂), Rel' f g a b → Quot.mk (Rel f g) a = Quot.mk (Rel f g) b

Tactic:
rintro a b (_ | ⟨x₀, y₀, h⟩ | _ | _)
    · rfl
    · have h₀ : Rel f g _ _ := Rel.inl_inr x₀
      rw [Quot.sound h₀, h]
      symm
      apply Quot.sound
      apply Rel.inl_inr
    · apply Quot.sound
      apply Rel.inl_inr
    · symm
      apply Quot.sound
      apply Rel.inl_inr

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

Goal state before:
pp: X : SSet
i n : ℕ
hi : i < n
j : ℕ
f : ⦋i⦌ ⟶ ⦋j⦌
w✝ : Epi f
y : ↑(X.nonDegenerate j)
⊢ (ConcreteCategory.hom (X.map f.op)) ↑y ∈ (X.skeleton n).obj (op ⦋i⦌)

Tactic:
suffices Subcomplex.ofSimplex y.1 ≤ X.skeleton n from
    (X.skeleton n).map _ (this _ (Subcomplex.mem_ofSimplex_obj _))

Goal state after:
X : SSet
i n : ℕ
hi : i < n
j : ℕ
f : ⦋i⦌ ⟶ ⦋j⦌
w✝ : Epi f
y : ↑(X.nonDegenerate j)
⊢ Subcomplex.ofSimplex ↑y ≤ X.skeleton n
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
y₃ : X₄
x₂ : X₂
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom r) x₂) = (ConcreteCategory.hom k) y₃
⊢ (ConcreteCategory.hom r) x₂ = y₃

pp: case inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
y₃ : X₄
x₃ : X₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) y₃
⊢ (ConcreteCategory.hom b) x₃ = y₃

Tactic:
<;>

Goal state after:
case inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
y₃ : X₄
x₂ : X₂
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom r) x₂) = (ConcreteCategory.hom k) y₃
⊢ (ConcreteCategory.hom r) x₂ = y₃

case inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
y₃ : X₄
x₃ : X₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) y₃
⊢ (ConcreteCategory.hom b) x₃ = y₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case e'_2
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 1

pp: case e'_3
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 2).inv =
    stdSimplex.δ 0

Tactic:
<;>

Goal state after:
case e'_2
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 1

case e'_3
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 2).inv =
    stdSimplex.δ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case e'_2
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 2

pp: case e'_3
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 0

Tactic:
<;>

Goal state after:
case e'_2
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 2

case e'_3
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «1»
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ (((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv) ≫ f₀ =
    (((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv) ≫ f₃

Tactic:
convert! h₁₂ <;> decide

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

Goal state before:
pp: case e'_2
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 0 1 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 2).inv =
    stdSimplex.δ 2

pp: case e'_3
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 0 1 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 2

Tactic:
<;>

Goal state after:
case e'_2
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 0 1 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 2).inv =
    stdSimplex.δ 2

case e'_3
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 0 1 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 2
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ.inr
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
hl : j = Fin.last (m + 1)
⊢ f.vertex (Fin.last m).succ = g.vertex (Fin.last m).succ

Tactic:
← f.arrow_tgt (Fin.last m),

Goal state after:
case hᵥ.inr
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
hl : j = Fin.last (m + 1)
⊢ (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 0) ⋯ ⋯).op)) (f.arrow (Fin.last m)) = g.vertex (Fin.last m).succ