mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: V : Type u
inst✝¹ : ReflQuiver V
W : Type u₂
inst✝ : ReflQuiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : V), { obj := F_obj, map := map✝¹ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝¹ }.obj X)
map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : V), { obj := F_obj, map := map✝ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝ }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.obj X = { obj := F_obj, map := map✝, map_id := map_id✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.map f =
      Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := F_obj, map := map✝, map_id := map_id✝ }.map f))
X Y : V
f : X ⟶ Y
⊢ map✝¹ f = map✝ f

Tactic:
simpa using h_map X Y f

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

Goal state before:
pp: V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
Fpre : V ⥤q W
Fid Gid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
h_obj : ∀ (X : V), { toPrefunctor := Fpre, map_id := Fid }.obj X = { toPrefunctor := Fpre, map_id := Gid }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { toPrefunctor := Fpre, map_id := Fid }.map f = Quiver.homOfEq ({ toPrefunctor := Fpre, map_id := Gid }.map f) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid } = { toPrefunctor := Fpre, map_id := Gid }

Tactic:
rfl

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

Goal state before:
pp: case refl
U : Type u_1
V : Type u_2
inst✝¹ : ReflQuiver U
inst✝ : ReflQuiver V
F : U ⥤rq V
X : U
⊢ F.obj X = F.obj X

Tactic:
rfl

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 : ℕ
⊢ 𝟙 (summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌))) = (𝟙 ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex)).f.f n

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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'
⊢ cast ⋯ ⋯ p = _root_.cast ⋯ p

Tactic:
rfl

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''
⊢ cast ⋯ ⋯ (cast ⋯ ⋯ p) = cast ⋯ ⋯ p

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
⊢ pathToList (listToPath []) = []

Tactic:
rfl

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

Goal state before:
pp: W✝ X✝ Y✝ Z✝ : Grpd
f✝ : ↑W✝ ⥤ ↑X✝
g✝ : ↑X✝ ⥤ ↑Y✝
h✝ : ↑Y✝ ⥤ ↑Z✝
⊢ (f✝ ⋙ g✝) ⋙ h✝ = f✝ ⋙ g✝ ⋙ h✝

Tactic:
rfl

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

Goal state before:
pp: J : Type u
f : J → Grpd
j : J
⊢ (piLimitFan f).π.app { as := j } = Pi.eval (fun i ↦ ↑(f i)) j

Tactic:
rfl

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

Goal state before:
pp: case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ↑x.1 ≤ 1 / 2
⊢ (F.curry ⟨2 * ↑x.1, ?pos.hx✝⟩) x.2 = F (⟨2 * ↑x.1, ⋯⟩, x.2)

pp: case pos.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ↑x.1 ≤ 1 / 2
⊢ 2 * ↑x.1 ∈ Set.Icc 0 1

Tactic:
rfl

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

Goal state before:
pp: case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ¬↑x.1 ≤ 1 / 2
⊢ (G.curry ⟨2 * ↑x.1 - 1, ?neg.hx✝⟩) x.2 = G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)

pp: case neg.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ¬↑x.1 ≤ 1 / 2
⊢ 2 * ↑x.1 - 1 ∈ Set.Icc 0 1

Tactic:
rfl

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

Goal state before:
pp: case h.h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ (pi fun i ↦ Quotient.mk ((a✝ i).trans (a i))) = pi fun i ↦ Quotient.mk (a✝ i) ⬝ Quotient.mk (a i)

Tactic:
rfl

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

Goal state before:
pp: I : Type u
X : I → TopCat
x : (i : I) → ↑(π.obj (X i))
⊢ Path.Homotopic.Quotient.mk (Path.pi fun i ↦ Path.refl (x i).as) = 𝟙 { as := fun i ↦ (x i).as }

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case h_obj
I : Type u
X : I → TopCat
X✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
⊢ (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj X✝ = (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj X✝

Tactic:
rfl

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

Goal state before:
pp: A : TopCat
B : TopCat
x₀ : ↑(π.obj A)
x₁ : ↑(π.obj B)
⊢ (match (x₀, x₁), (x₀, x₁), 𝟙 (x₀, x₁) with
    | (fst, snd), (fst_1, snd_1), (p₀, p₁) => Path.Homotopic.prod p₀ p₁) =
    𝟙 { as := (x₀.as, x₁.as) }

Tactic:
rfl

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)
⊢ (projLeft A B).obj { as := (X✝.1.as, X✝.2.as) } = X✝.1

Tactic:
rfl

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

Goal state before:
pp: 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

Tactic:
rfl

Goal state after:
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).obj X✝).as = X✝.as.1

Tactic:
rfl

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

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

Tactic:
rfl

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
y : Y
⊢ (const X y).Homotopic (const X y)

Tactic:
rfl

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

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y → PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)

Tactic:
intro; constructor <;> infer_instance

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

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), p₁.Homotopic p₂) ↔ ∀ (x y : Path a✝¹ a✝), (Path.Homotopic.setoid a✝¹ a✝) x y

Tactic:
rfl

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

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

Tactic:
rw [simply_connected_iff_paths_homotopic']

Goal state after:
Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ (PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂) ↔
    PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case mk
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ (mk γ).cast ⋯ ⋯ = mk γ

Tactic:
rfl

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

Goal state before:
pp: case mk
X : Type u
inst✝ : TopologicalSpace X
x y x' y' : X
hx : x' = x
hy : y' = y
x'' y'' : X
hx' : x'' = x'
hy' : y'' = y'
γ : Path x y
⊢ ((mk γ).cast hx hy).cast hx' hy' = (mk γ).cast ⋯ ⋯

Tactic:
rfl

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

Goal state before:
pp: case mk
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
Z : Type u_1
inst✝ : TopologicalSpace Z
p : Homotopic.Quotient x₀ x₁
f : C(X, Y)
g : C(Y, Z)
a✝ : Path x₀ x₁
⊢ map (Quot.mk (⇑(Homotopic.setoid x₀ x₁)) a✝) (g.comp f) = (map (Quot.mk (⇑(Homotopic.setoid x₀ x₁)) a✝) f).map g

Tactic:
rfl

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

Goal state before:
pp: case mk
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
p : Homotopic.Quotient x y
x' y' : X
hx : x' = x
hy : y' = y
f : C(X, Y)
a✝ : Path x y
⊢ (cast (Quot.mk (⇑(Homotopic.setoid x y)) a✝) hx hy).map f = (map (Quot.mk (⇑(Homotopic.setoid x y)) a✝) f).cast ⋯ ⋯

Tactic:
rfl

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
⊢ (Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧)).trans ⟦p₂⟧ = ⟦p₂⟧

Tactic:
grind

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
t✝ : ↑I
⊢ (H.evalAt x) t✝ = ((fun q ↦ q.map ⋯) (unitInterval.upath01.prod (Path.refl (fromTop x).as))) t✝

Tactic:
rfl

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

Goal state before:
pp: ⊢ ∀ (x : ↑I × ↑I), ↑x.2 = 1 / 2 → ↑x.1 * 2 * ↑x.2 = ↑x.1 * (2 - 2 * ↑x.2)

Tactic:
grind

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

Goal state before:
pp: case left
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ hcast ⋯ ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (Prod.mkHom uhpath01 p)) ≫
        hcast ⋯ =
    H.diagonalPath' p

Tactic:
rfl

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: ⊢ ∀ (x : ↑I), ↑x = 1 / 2 → 2 * ↑x = 1

Tactic:
grind

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

Goal state before:
pp: case right
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ hcast ⋯ ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (Prod.mkHom uhpath01 p)) ≫
        hcast ⋯ =
    H.diagonalPath' p

Tactic:
rfl

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (p.trans (Path.refl x₁)) x✝ = (⇑p ∘ fun t ↦ ⟨if ↑t ≤ 1 / 2 then 2 * ↑t else 1, ⋯⟩) x✝

Tactic:
grind

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

Goal state before:
pp: ⊢ ∀ (x : ↑I), ↑x = 1 / 2 → ↑x + 1 / 4 = 1 / 2 * (↑x + 1)

Tactic:
grind

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

Goal state before:
pp: ⊢ ∀ (x : ↑I), ↑x = 1 / 4 → 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)

Tactic:
grind

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
⊢ weakEquivalences (CofibrantObject C) ≤ (weakEquivalences C).inverseImage ι

Tactic:
rfl

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

Goal state before:
pp: case mk
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
x✝ : RightHomotopyClass X Y
f : X ⟶ Y
⊢ Quot.lift (fun f ↦ RightHomotopyClass.mk f.hom) ⋯
      (Quot.lift (fun f ↦ toHoCat.map (homMk f)) ⋯ (Quot.mk RightHomotopyRel f)) =
    Quot.mk RightHomotopyRel f

Tactic:
rfl

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

Goal state before:
pp: case mk
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
x✝ : toHoCat.obj (mk X) ⟶ toHoCat.obj (mk Y)
f : (toHoCat.obj (mk X)).as ⟶ (toHoCat.obj (mk Y)).as
⊢ Quot.lift (fun f ↦ toHoCat.map (homMk f)) ⋯
      (Quot.lift (fun f ↦ RightHomotopyClass.mk f.hom) ⋯ (Quot.mk (HomRel.CompClosure (homRel C)) f)) =
    Quot.mk (HomRel.CompClosure (homRel C)) f

Tactic:
rfl

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

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝² : ¬↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : 2 * ↑x ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = p ⟨2 * (2 * ↑x), ⋯⟩

pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : 2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = q ⟨2 * (2 * (2 * ↑x) - 1), ⋯⟩

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (2 * ↑x) - 1) - 1, ⋯⟩

pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝² : ¬↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : 1 / 2 * (↑x + 1) ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = p ⟨2 * (1 / 2 * (↑x + 1)), ⋯⟩

pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : 2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = q ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1), ⋯⟩

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : ¬2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1) - 1, ⋯⟩

Tactic:
grind

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : 2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = q ⟨2 * (2 * (2 * ↑x) - 1), ⋯⟩

case neg
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (2 * ↑x) - 1) - 1, ⋯⟩

case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝² : ¬↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : 1 / 2 * (↑x + 1) ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = p ⟨2 * (1 / 2 * (↑x + 1)), ⋯⟩

case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : 2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = q ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1), ⋯⟩

case neg
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : ¬2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1) - 1, ⋯⟩
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : 2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = q ⟨2 * (2 * (2 * ↑x) - 1), ⋯⟩

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (2 * ↑x) - 1) - 1, ⋯⟩

pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝² : ¬↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : 1 / 2 * (↑x + 1) ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = p ⟨2 * (1 / 2 * (↑x + 1)), ⋯⟩

pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : 2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = q ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1), ⋯⟩

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : ¬2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1) - 1, ⋯⟩

Tactic:
grind

Goal state after:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (2 * ↑x) - 1) - 1, ⋯⟩

case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝² : ¬↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : 1 / 2 * (↑x + 1) ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = p ⟨2 * (1 / 2 * (↑x + 1)), ⋯⟩

case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : 2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = q ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1), ⋯⟩

case neg
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : ¬2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1) - 1, ⋯⟩
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (2 * ↑x) - 1) - 1, ⋯⟩

pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝² : ¬↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : 1 / 2 * (↑x + 1) ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = p ⟨2 * (1 / 2 * (↑x + 1)), ⋯⟩

pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : 2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = q ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1), ⋯⟩

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : ¬2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1) - 1, ⋯⟩

Tactic:
grind

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝² : ¬↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : 1 / 2 * (↑x + 1) ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = p ⟨2 * (1 / 2 * (↑x + 1)), ⋯⟩

case pos
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : 2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = q ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1), ⋯⟩

case neg
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : ¬2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1) - 1, ⋯⟩
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ weakEquivalences (BifibrantObject C) ≤ (weakEquivalences C).inverseImage ι

Tactic:
rfl

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

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : ¬2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1) - 1, ⋯⟩

Tactic:
grind

Goal state after: