awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : (↑I : Type)
snd : X
h₁ : 1 - (↑t : ℝ) ≤ 1 / 2
h₂ : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 2 * (1 - (↑t : ℝ)) < 1 - (2 * (↑t : ℝ) - 1) → 2 / 2 = 1
linarith₁ : 2 * (1 - (↑t : ℝ)) < 1 - (2 * (↑t : ℝ) - 1) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * (1 - (↑t : ℝ)) < 1 - (2 * (↑t : ℝ) - 1) → GT.gt (α := ℝ) 2 0
linarith₃ : 2 * (1 - (↑t : ℝ)) < 1 - (2 * (↑t : ℝ) - 1) → 2 / 2 = 1
linarith₄ : 2 * (1 - (↑t : ℝ)) < 1 - (2 * (↑t : ℝ) - 1) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 2 * (1 - (↑t : ℝ)) < 1 - (2 * (↑t : ℝ) - 1) → GT.gt (α := ℝ) 2 0
linarith₆ : 2 * (1 - (↑t : ℝ)) < 1 - (2 * (↑t : ℝ) - 1) → 2 * (1 - (↑t : ℝ)) - (1 - (2 * (↑t : ℝ) - 1)) = 0
linarith₇ : 1 - (2 * (↑t : ℝ) - 1) < 2 * (1 - (↑t : ℝ)) → 2 / 2 = 1
linarith₈ : 1 - (2 * (↑t : ℝ) - 1) < 2 * (1 - (↑t : ℝ)) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : 1 - (2 * (↑t : ℝ) - 1) < 2 * (1 - (↑t : ℝ)) → GT.gt (α := ℝ) 2 0
linarith₁₀ : 1 - (2 * (↑t : ℝ) - 1) < 2 * (1 - (↑t : ℝ)) → 2 / 2 = 1
linarith₁₁ : 1 - (2 * (↑t : ℝ) - 1) < 2 * (1 - (↑t : ℝ)) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ : 1 - (2 * (↑t : ℝ) - 1) < 2 * (1 - (↑t : ℝ)) → GT.gt (α := ℝ) 2 0
linarith₁₃ : 1 - (2 * (↑t : ℝ) - 1) < 2 * (1 - (↑t : ℝ)) → 1 - (2 * (↑t : ℝ) - 1) - 2 * (1 - (↑t : ℝ)) = 0
⊢ 2 * (1 - (↑t : ℝ)) = 1 - (2 * (↑t : ℝ) - 1)

Tactic:
linarith
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : (↑I : Type)
snd : X
h₁ : ¬1 - (↑t : ℝ) ≤ 1 / 2
h₂ : (↑t : ℝ) ≤ 1 / 2
pos :
  Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ)) - 1) ⋯ =
    σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)
⊢ Eq.{v + 1} (α := Y)
    ((G : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ)) - 1) ⋯, snd) : Y)
    ((G : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯), snd) : Y)

Tactic:
congr 2
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : (↑I : Type)
snd : X
h₁ : ¬1 - (↑t : ℝ) ≤ 1 / 2
h₂ : (↑t : ℝ) ≤ 1 / 2
pos :
  (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ)) - 1) ⋯) : ℝ) =
    (↑(σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)) : ℝ)
⊢ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ)) - 1) ⋯ =
    σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : (↑I : Type)
snd : X
h₁ : ¬1 - (↑t : ℝ) ≤ 1 / 2
h₂ : (↑t : ℝ) ≤ 1 / 2
linarith : 2 * (1 - (↑t : ℝ)) - 1 < 1 - 2 * (↑t : ℝ) → 2 / 2 = 1
linarith₁ : 2 * (1 - (↑t : ℝ)) - 1 < 1 - 2 * (↑t : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * (1 - (↑t : ℝ)) - 1 < 1 - 2 * (↑t : ℝ) → GT.gt (α := ℝ) 2 0
linarith₃ : 2 * (1 - (↑t : ℝ)) - 1 < 1 - 2 * (↑t : ℝ) → 2 / 2 = 1
linarith₄ : 2 * (1 - (↑t : ℝ)) - 1 < 1 - 2 * (↑t : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 2 * (1 - (↑t : ℝ)) - 1 < 1 - 2 * (↑t : ℝ) → GT.gt (α := ℝ) 2 0
linarith₆ : 2 * (1 - (↑t : ℝ)) - 1 < 1 - 2 * (↑t : ℝ) → 2 * (1 - (↑t : ℝ)) - 1 - (1 - 2 * (↑t : ℝ)) = 0
linarith₇ : 1 - 2 * (↑t : ℝ) < 2 * (1 - (↑t : ℝ)) - 1 → 2 / 2 = 1
linarith₈ : 1 - 2 * (↑t : ℝ) < 2 * (1 - (↑t : ℝ)) - 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : 1 - 2 * (↑t : ℝ) < 2 * (1 - (↑t : ℝ)) - 1 → GT.gt (α := ℝ) 2 0
linarith₁₀ : 1 - 2 * (↑t : ℝ) < 2 * (1 - (↑t : ℝ)) - 1 → 2 / 2 = 1
linarith₁₁ : 1 - 2 * (↑t : ℝ) < 2 * (1 - (↑t : ℝ)) - 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ : 1 - 2 * (↑t : ℝ) < 2 * (1 - (↑t : ℝ)) - 1 → GT.gt (α := ℝ) 2 0
linarith₁₃ : 1 - 2 * (↑t : ℝ) < 2 * (1 - (↑t : ℝ)) - 1 → 1 - 2 * (↑t : ℝ) - (2 * (1 - (↑t : ℝ)) - 1) = 0
⊢ 2 * (1 - (↑t : ℝ)) - 1 = 1 - 2 * (↑t : ℝ)

Tactic:
linarith
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : (↑I : Type)
snd : X
h₁ : ¬1 - (↑t : ℝ) ≤ 1 / 2
h₂ : ¬(↑t : ℝ) ≤ 1 / 2
neg : False
⊢ Eq.{v + 1} (α := Y)
    ((G : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ)) - 1) ⋯, snd) : Y)
    ((F : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯), snd) : Y)

Tactic:
exfalso
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : (↑I : Type)
snd : X
h₁ : ¬1 - (↑t : ℝ) ≤ 1 / 2
h₂ : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : GT.gt (α := ℝ) 2 0
linarith₆ :
  HMul.hMul (α := ℝ) 1 1 - (HMul.hMul (α := ℝ) 2 1 - 2 * (↑t : ℝ)) + (HMul.hMul (α := ℝ) 1 1 - 2 * (↑t : ℝ)) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ g₀ g₁ : C(X, Y)
F : f₀.Homotopy f₁
h₀ : f₀ = g₀
h₁ : f₁ = g₁
⊢ ∀ (x : X), Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (0, x) : Y) ((g₀ : (a : X) → Y) x : Y)

Tactic:
simp [← h₀]
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ g₀ g₁ : C(X, Y)
F : f₀.Homotopy f₁
h₀ : f₀ = g₀
h₁ : f₁ = g₁
⊢ ∀ (x : X), Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (1, x) : Y) ((g₁ : (a : X) → Y) x : Y)

Tactic:
simp [← h₁]
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
g₀ g₁ : C(Y, Z)
G : g₀.Homotopy g₁
F : f₀.Homotopy f₁
⊢ ∀ (x : X),
    Eq.{w + 1} (α := Z)
      ((G : (a : (↑I : Type) × Y) → Z) (((0, x).1, (F : (a : (↑I : Type) × X) → Y) (0, x)) : (↑I : Type) × Y) : Z)
      ((g₀.comp f₀ : (a : X) → Z) x : Z)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
g₀ g₁ : C(Y, Z)
G : g₀.Homotopy g₁
F : f₀.Homotopy f₁
⊢ ∀ (x : X),
    Eq.{w + 1} (α := Z)
      ((G : (a : (↑I : Type) × Y) → Z) (((1, x).1, (F : (a : (↑I : Type) × X) → Y) (1, x)) : (↑I : Type) × Y) : Z)
      ((g₁.comp f₁ : (a : X) → Z) x : Z)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
⊢ f.Homotopic f

Tactic:
⟨Homotopy.refl f⟩

Premises used: Nonempty.intro, ContinuousMap.Homotopic, ContinuousMap.Homotopy.refl
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
h : f.Homotopic g
⊢ g.Homotopic f

Tactic:
h.map Homotopy.symm

Premises used: ContinuousMap.Homotopy.symm, ContinuousMap.Homotopic, Nonempty.map
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g h : C(X, Y)
h₀ : f.Homotopic g
h₁ : g.Homotopic h
⊢ f.Homotopic h

Tactic:
h₀.map2 Homotopy.trans h₁

Premises used: Nonempty.map2, ContinuousMap.Homotopy.trans, ContinuousMap.Homotopic
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
Z : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g₀ g₁ : C(Y, Z)
f₀ f₁ : C(X, Y)
hg : g₀.Homotopic g₁
hf : f₀.Homotopic f₁
⊢ (g₀.comp f₀).Homotopic (g₁.comp f₁)

Tactic:
hg.map2 Homotopy.comp hf

Premises used: Nonempty.map2, ContinuousMap.Homotopy.comp, ContinuousMap.Homotopic
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ ∀ {x y : C(X, Y)}, x.Homotopic y → y.Homotopic x

Tactic:
apply symm

Premises used: ContinuousMap.Homotopic.symm
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ ∀ {x y z : C(X, Y)}, x.Homotopic y → y.Homotopic z → x.Homotopic z

Tactic:
apply trans

Premises used: ContinuousMap.Homotopic.trans
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
ι : Type u_2
inst : TopologicalSpace X
Y : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (Y i)
f₀ f₁ : (i : ι) → ContinuousMap.{u, u_3} X (Y i)
F : ∀ (i : ι), (f₀ i).Homotopic (f₁ i)
⊢ (pi (X := Y) f₀).Homotopic (pi (X := Y) f₁)

Tactic:
⟨.pi fun i ↦ (F i).some⟩

Premises used: ContinuousMap.Homotopy.pi, Nonempty.some, Nonempty.intro, ContinuousMap.Homotopic
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
ι : Type u_2
X : ι → Type u_3
Y : ι → Type u_4
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → TopologicalSpace (Y i)
f₀ f₁ : (i : ι) → ContinuousMap.{u_3, u_4} (X i) (Y i)
F : ∀ (i : ι), (f₀ i).Homotopic (f₁ i)
⊢ (piMap (X := X) (Y := Y) f₀).Homotopic (piMap (X := X) (Y := Y) f₁)

Tactic:
.pi fun i ↦ .comp (F i) (.refl <| .eval i)

Premises used: ContinuousMap.eval, ContinuousMap.Homotopic.comp, ContinuousMap.Homotopic.pi, ContinuousMap.piMap, ContinuousMap.Homotopic.refl
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
P : C(X, Y) → Prop
toFun : (↑I : Type) × X → Y
continuous_toFun : Continuous toFun
toContinuousMap : ContinuousMap.{u, v} ((↑I : Type) × X) Y := { toFun := toFun, continuous_toFun := continuous_toFun }
map_zero_left : ∀ (x : X), toFun (0, x) = (f₀ : (a : X) → Y) x
map_one_left : ∀ (x : X), toFun (1, x) = (f₁ : (a : X) → Y) x
toHomotopy : f₀.Homotopy f₁ :=
  { toContinuousMap := toContinuousMap, map_zero_left := map_zero_left, map_one_left := map_one_left }
t : (↑I : Type)
⊢ Continuous.{u, u} (X := X) (Prod.mk t)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
P : C(X, Y) → Prop
⊢ Function.Injective (α := f₀.HomotopyWith f₁ P) (β := (↑I : Type) × X → Y)
    (DFunLike.coe (β := fun (x : (↑I : Type) × X) ↦ Y))

Tactic:
DFunLike.coe_injective'

Premises used: DFunLike.coe_injective'
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
P : C(X, Y) → Prop
F G : f₀.HomotopyWith f₁ P
h :
  ∀ (x : (↑I : Type) × X),
    Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) x : Y) ((G : (a : (↑I : Type) × X) → Y) x : Y)
⊢ F = G

Tactic:
DFunLike.ext F G h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
P : C(X, Y) → Prop
F : f₀.HomotopyWith f₁ P
⊢ Continuous.{u, v} (X := (↑I : Type) × X) (Y := Y) (⇑F : (a : (↑I : Type) × X) → Y)

Tactic:
F.continuous_toFun

Premises used: ContinuousMap.Homotopy.toContinuousMap, ContinuousMap.continuous_toFun, ContinuousMap.HomotopyWith.toHomotopy
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
P : C(X, Y) → Prop
F : f₀.HomotopyWith f₁ P
x : X
⊢ Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (0, x) : Y) ((f₀ : (a : X) → Y) x : Y)

Tactic:
F.map_zero_left x

Premises used: ContinuousMap.HomotopyWith.toHomotopy, ContinuousMap.Homotopy.map_zero_left
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
P : C(X, Y) → Prop
F : f₀.HomotopyWith f₁ P
x : X
⊢ Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (1, x) : Y) ((f₁ : (a : X) → Y) x : Y)

Tactic:
F.map_one_left x

Premises used: ContinuousMap.HomotopyWith.toHomotopy, ContinuousMap.Homotopy.map_one_left
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
P : C(X, Y) → Prop
F : f₀.HomotopyWith f₁ P
⊢ Eq (α := (a : (↑I : Type) × X) → Y) (⇑F.toHomotopy (P := P).toContinuousMap : (a : (↑I : Type) × X) → Y)
    (⇑F : (a : (↑I : Type) × X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
P : C(X, Y) → Prop
F : f₀.HomotopyWith f₁ P
⊢ Eq (α := (a : (↑I : Type) × X) → Y) (⇑(F.toHomotopy (P := P)) : (a : (↑I : Type) × X) → Y)
    (⇑F : (a : (↑I : Type) × X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
P : C(X, Y) → Prop
F : f₀.HomotopyWith f₁ P
t : (↑I : Type)
⊢ P ((F.toHomotopy (P := P).curry : (a : (↑I : Type)) → C(X, Y)) t)

Tactic:
F.prop' t

Premises used: ContinuousMap.HomotopyWith.prop'
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
P : C(X, Y) → Prop
F : f₀.HomotopyWith f₁ P
t : ℝ
⊢ P ((F.toHomotopy (P := P).extend : (a : ℝ) → C(X, Y)) t)

Tactic:
F.prop _

Premises used: ContinuousMap.HomotopyWith.prop, Set.IccExtend
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
P : C(X, Y) → Prop
f₀ f₁ : C(X, Y)
F : f₀.HomotopyWith f₁ P
⊢ F.symm (P := P).symm (P := P) = F

Tactic:
ext <| Homotopy.congr_fun <| Homotopy.symm_symm _

Premises used: ContinuousMap.Homotopy.symm_symm, ContinuousMap.HomotopyWith.ext, ContinuousMap.Homotopy.congr_fun
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
P : C(X, Y) → Prop
f₀ f₁ : C(X, Y)
⊢ Function.Bijective (α := f₀.HomotopyWith f₁ P) (symm (P := P))

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, ContinuousMap.HomotopyWith.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : (↑I : Type)
simp :
  P
    {
      toFun := fun (x : X) ↦
        if (↑t : ℝ) ≤ 1 / 2 then
          (((F.toHomotopy (P := P).extend : (a : ℝ) → C(X, Y)) (2 * (↑t : ℝ)) : C(X, Y)) : (a : X) → Y) x
        else (((G.toHomotopy (P := P).extend : (a : ℝ) → C(X, Y)) (2 * (↑t : ℝ) - 1) : C(X, Y)) : (a : X) → Y) x,
      continuous_toFun := ⋯ }
⊢ P { toFun := fun (x : X) ↦ (F.toHomotopy (P := P).trans (G.toHomotopy (P := P))).toFun (t, x), continuous_toFun := ⋯ }

Tactic:
simp only [Homotopy.trans]

Premises used: ContinuousMap.Homotopy.trans
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : (↑I : Type)
pos :
  ∀ (h : (↑t : ℝ) ≤ 1 / 2),
    P
      {
        toFun := fun (x : X) ↦
          (((F.toHomotopy (P := P).extend : (a : ℝ) → C(X, Y)) (2 * (↑t : ℝ)) : C(X, Y)) : (a : X) → Y) x,
        continuous_toFun := ⋯ }
neg :
  ∀ (h : ¬(↑t : ℝ) ≤ 1 / 2),
    P
      {
        toFun := fun (x : X) ↦
          (((G.toHomotopy (P := P).extend : (a : ℝ) → C(X, Y)) (2 * (↑t : ℝ) - 1) : C(X, Y)) : (a : X) → Y) x,
        continuous_toFun := ⋯ }
⊢ P
    {
      toFun := fun (x : X) ↦
        if (↑t : ℝ) ≤ 1 / 2 then
          (((F.toHomotopy (P := P).extend : (a : ℝ) → C(X, Y)) (2 * (↑t : ℝ)) : C(X, Y)) : (a : X) → Y) x
        else (((G.toHomotopy (P := P).extend : (a : ℝ) → C(X, Y)) (2 * (↑t : ℝ) - 1) : C(X, Y)) : (a : X) → Y) x,
      continuous_toFun := ⋯ }

Tactic:
split_ifs
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
⊢ P
    {
      toFun := fun (x : X) ↦
        (((F.toHomotopy (P := P).extend : (a : ℝ) → C(X, Y)) (2 * (↑t : ℝ)) : C(X, Y)) : (a : X) → Y) x,
      continuous_toFun := ⋯ }

Tactic:
F.extendProp _

Premises used: ContinuousMap.HomotopyWith.extendProp, Set.IccExtend
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
⊢ P
    {
      toFun := fun (x : X) ↦
        (((F.toHomotopy (P := P).extend : (a : ℝ) → C(X, Y)) (2 * (↑t : ℝ)) : C(X, Y)) : (a : X) → Y) x,
      continuous_toFun := ⋯ }

Tactic:
exact F.extendProp _

Premises used: ContinuousMap.HomotopyWith.extendProp
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ P
    {
      toFun := fun (x : X) ↦
        (((G.toHomotopy (P := P).extend : (a : ℝ) → C(X, Y)) (2 * (↑t : ℝ) - 1) : C(X, Y)) : (a : X) → Y) x,
      continuous_toFun := ⋯ }

Tactic:
G.extendProp _

Premises used: ContinuousMap.HomotopyWith.extendProp, Set.IccExtend
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ P
    {
      toFun := fun (x : X) ↦
        (((G.toHomotopy (P := P).extend : (a : ℝ) → C(X, Y)) (2 * (↑t : ℝ) - 1) : C(X, Y)) : (a : X) → Y) x,
      continuous_toFun := ⋯ }

Tactic:
exact G.extendProp _

Premises used: ContinuousMap.HomotopyWith.extendProp
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
x : (↑I : Type) × X
⊢ Eq.{v + 1} (α := Y) ((F.trans (P := P) G : (a : (↑I : Type) × X) → Y) x : Y)
    (if h : (↑x.1 : ℝ) ≤ 1 / 2 then
        (F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ)) ⋯, x.2)
      else (G : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ) - 1) ⋯, x.2) :
      Y)

Tactic:
Homotopy.trans_apply _ _ _

Premises used: ContinuousMap.Homotopy.trans_apply
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
⊢ (F.trans (P := P) G).symm (P := P) = G.symm (P := P).trans (P := P) (F.symm (P := P))

Tactic:
ext <| Homotopy.congr_fun <| Homotopy.symm_trans _ _

Premises used: ContinuousMap.Homotopy.symm_trans, ContinuousMap.HomotopyWith.ext, ContinuousMap.Homotopy.congr_fun
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
P : C(X, Y) → Prop
f : C(X, Y)
hf : P f
⊢ f.HomotopicWith f P

Tactic:
⟨HomotopyWith.refl f hf⟩

Premises used: Nonempty.intro, ContinuousMap.HomotopicWith, ContinuousMap.HomotopyWith.refl
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
P : C(X, Y) → Prop
f g : C(X, Y)
h : f.HomotopicWith g P
⊢ g.HomotopicWith f P

Tactic:
⟨h.some.symm⟩

Premises used: ContinuousMap.HomotopyWith.symm, Nonempty.some, Nonempty.intro, ContinuousMap.HomotopicWith
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
P : C(X, Y) → Prop
f g h : C(X, Y)
h₀ : f.HomotopicWith g P
h₁ : g.HomotopicWith h P
⊢ f.HomotopicWith h P

Tactic:
⟨h₀.some.trans h₁.some⟩

Premises used: Nonempty.some, Nonempty.intro, ContinuousMap.HomotopicWith, ContinuousMap.HomotopyWith.trans
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
t : (↑I : Type)
x : X
hx : x ∈ S
⊢ Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (t, x) : Y) ((f₀ : (a : X) → Y) x : Y)

Tactic:
F.prop t x hx

Premises used: ContinuousMap.HomotopyWith.prop
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
t : (↑I : Type)
x : X
hx : x ∈ S
rw : Eq.{v + 1} (α := Y) ((f₀ : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)
rw₁ : Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (1, x) : Y) ((f₁ : (a : X) → Y) x : Y)
rw₂ rw₃ : Eq.{v + 1} (α := Y) ((f₁ : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)
⊢ Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (t, x) : Y) ((f₁ : (a : X) → Y) x : Y)

Tactic:
rw [F.eq_fst t hx, ← F.eq_fst 1 hx, F.apply_one]

Premises used: ContinuousMap.HomotopyWith.apply_one, ContinuousMap.HomotopyRel.eq_fst, OfNat.ofNat
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
x : X
hx : x ∈ S
⊢ Eq.{v + 1} (α := Y) ((f₀ : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)

Tactic:
F.eq_fst 0 hx ▸ F.eq_snd 0 hx

Premises used: Eq.rec, ContinuousMap.HomotopyRel.eq_fst, OfNat.ofNat, ContinuousMap.HomotopyRel.eq_snd
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
⊢ F.symm (S := S).symm (S := S) = F

Tactic:
HomotopyWith.symm_symm F

Premises used: ContinuousMap.HomotopyRel.symm, ContinuousMap.HomotopyWith.symm_symm
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
S : Set X
⊢ Function.Bijective (α := f₀.HomotopyRel f₁ S) (symm (S := S))

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, ContinuousMap.HomotopyRel.symm_symm