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₁ : C(X, Y)
F : f₀.Homotopy f₁
h :
  ∀ (a : X),
    Eq.{v + 1} (α := Y) ((((F.curry : (a : (↑I : Type)) → C(X, Y)) 1 : C(X, Y)) : (a : X) → Y) a : Y)
      ((f₁ : (a : X) → Y) a : Y)
⊢ (F.curry : (a : (↑I : Type)) → C(X, Y)) 1 = f₁

Tactic:
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)
F : f₀.Homotopy f₁
a : X
⊢ Eq.{v + 1} (α := Y) ((((F.curry : (a : (↑I : Type)) → C(X, Y)) 1 : C(X, Y)) : (a : X) → Y) a : Y)
    ((f₁ : (a : X) → Y) a : Y)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : t ≤ 0
x : X
rw :
  Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y)
    ((F : (a : (↑I : Type) × X) → Y) (0, x) : Y)
⊢ Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)

Tactic:
rw [← F.apply_zero]

Premises used: ContinuousMap.Homotopy.apply_zero
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : t ≤ 0
x : X
⊢ Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y)
    ((F : (a : (↑I : Type) × X) → Y) (0, x) : Y)

Tactic:
ContinuousMap.congr_fun (Set.IccExtend_of_le_left (zero_le_one' ℝ) F.curry ht) x

Premises used: Real, Set.Mem, ContinuousMap.Homotopy.curry, zero_le_one', Set.IccExtend_of_le_left, ContinuousMap.congr_fun, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : t ≤ 0
x : X
⊢ Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y)
    ((F : (a : (↑I : Type) × X) → Y) (0, x) : Y)

Tactic:
exact ContinuousMap.congr_fun (Set.IccExtend_of_le_left (zero_le_one' ℝ) F.curry ht) x

Premises used: Real, ContinuousMap.Homotopy.curry, zero_le_one', Set.IccExtend_of_le_left, ContinuousMap.congr_fun, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : 1 ≤ t
x : X
rw :
  Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y)
    ((F : (a : (↑I : Type) × X) → Y) (1, x) : Y)
⊢ Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)

Tactic:
rw [← F.apply_one]

Premises used: ContinuousMap.Homotopy.apply_one
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : 1 ≤ t
x : X
⊢ Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y)
    ((F : (a : (↑I : Type) × X) → Y) (1, x) : Y)

Tactic:
ContinuousMap.congr_fun (Set.IccExtend_of_right_le (zero_le_one' ℝ) F.curry ht) x

Premises used: Real, Set.Mem, ContinuousMap.Homotopy.curry, zero_le_one', ContinuousMap.congr_fun, Set.IccExtend_of_right_le, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : 1 ≤ t
x : X
⊢ Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y)
    ((F : (a : (↑I : Type) × X) → Y) (1, x) : Y)

Tactic:
exact ContinuousMap.congr_fun (Set.IccExtend_of_right_le (zero_le_one' ℝ) F.curry ht) x

Premises used: Real, ContinuousMap.Homotopy.curry, zero_le_one', ContinuousMap.congr_fun, Set.IccExtend_of_right_le, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : (↑I : Type)
x : X
⊢ Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) (↑t : ℝ) : C(X, Y)) : (a : X) → Y) x : Y)
    ((F : (a : (↑I : Type) × X) → Y) (t, x) : Y)

Tactic:
ContinuousMap.congr_fun (Set.IccExtend_val (zero_le_one' ℝ) F.curry t) x

Premises used: Real, ContinuousMap.Homotopy.curry, Set.IccExtend_val, zero_le_one', ContinuousMap.congr_fun, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : t ∈ I
⊢ Eq (α := C(X, Y)) ((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y))
    ((F.curry : (a : (↑I : Type)) → C(X, Y)) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ht) : C(X, Y))

Tactic:
Set.IccExtend_of_mem (zero_le_one' ℝ) F.curry ht

Premises used: Real, Set.Mem, ContinuousMap.Homotopy.curry, Set.IccExtend_of_mem, zero_le_one', Set.IccExtend, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ (F.extend : (a : ℝ) → C(X, Y)) 0 = f₀

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ (F.extend : (a : ℝ) → C(X, Y)) 1 = f₁

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : t ∈ I
x : X
⊢ Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y)
    ((F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ht, x) : Y)

Tactic:
simp [ht]
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F G : f₀.Homotopy f₁
h : F = G
x : (↑I : Type) × X
⊢ Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) x : Y) ((G : (a : (↑I : Type) × X) → Y) x : Y)

Tactic:
ContinuousMap.congr_fun (congr_arg _ h) x

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

Tactic:
F.toContinuousMap.congr_arg h

Premises used: ContinuousMap.congr_arg, ContinuousMap.Homotopy.toContinuousMap
-- 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)
F : f₀.Homotopy f₁
⊢ ∀ (x : X), Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (σ (0, x).1, (0, x).2) : Y) ((f₁ : (a : X) → Y) x : Y)

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)
F : f₀.Homotopy f₁
⊢ ∀ (x : X), Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (σ (1, x).1, (1, x).2) : Y) ((f₀ : (a : X) → Y) x : Y)

Tactic:
norm_num
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
h :
  ∀ (x : (↑I : Type) × X),
    Eq.{v + 1} (α := Y) ((F.symm.symm : (a : (↑I : Type) × X) → Y) x : Y) ((F : (a : (↑I : Type) × X) → Y) x : Y)
⊢ F.symm.symm = F

Tactic:
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)
F : f₀.Homotopy f₁
x : (↑I : Type) × X
⊢ Eq.{v + 1} (α := Y) ((F.symm.symm : (a : (↑I : Type) × X) → Y) x : Y) ((F : (a : (↑I : Type) × X) → Y) x : Y)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
⊢ Function.Bijective (α := f₀.Homotopy f₁) symm

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

Premises used: Iff.mpr, ContinuousMap.Homotopy.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'
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
⊢ Continuous (Y := ℝ) fun (x : (↑I : Type) × X) ↦ (↑x.1 : ℝ)

Tactic:
fun_prop
-- 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₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
⊢ Continuous (Y := (↑I : Type) × X) fun (x : (↑I : Type) × X) ↦ (Set.projIcc 0 1 extend._proof_1 (2 * (↑x.1 : ℝ)), x.2)

Tactic:
fun_prop
-- 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₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
⊢ Continuous (Y := (↑I : Type) × X) fun (x : (↑I : Type) × X) ↦
    (Set.projIcc 0 1 extend._proof_1 (2 * (↑x.1 : ℝ) - 1), x.2)

Tactic:
fun_prop
-- 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₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : (↑I : Type) × X
hx : (↑x.1 : ℝ) = 1 / 2
⊢ Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ)) : C(X, Y)) : (a : X) → Y) x.2 : Y)
    ((((G.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ) - 1) : C(X, Y)) : (a : X) → Y) x.2 : Y)

Tactic:
norm_num [hx]
-- 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₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : X
⊢ Eq.{v + 1} (α := Y)
    (if (↑(0, x).1 : ℝ) ≤ 1 / 2 then
        (((F.extend : (a : ℝ) → C(X, Y)) (HMul.hMul (α := ℝ) 2 (↑(0, x).1 : ℝ)) : C(X, Y)) : (a : X) → Y) (0, x).2
      else
        (((G.extend : (a : ℝ) → C(X, Y)) (HMul.hMul (α := ℝ) 2 (↑(0, x).1 : ℝ) - 1) : C(X, Y)) : (a : X) → Y) (0, x).2 :
      Y)
    ((f₀ : (a : X) → Y) x : Y)

Tactic:
norm_num
-- 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₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : X
⊢ Eq.{v + 1} (α := Y)
    (if (↑(1, x).1 : ℝ) ≤ 1 / 2 then
        (((F.extend : (a : ℝ) → C(X, Y)) (HMul.hMul (α := ℝ) 2 (↑(1, x).1 : ℝ)) : C(X, Y)) : (a : X) → Y) (1, x).2
      else
        (((G.extend : (a : ℝ) → C(X, Y)) (HMul.hMul (α := ℝ) 2 (↑(1, x).1 : ℝ) - 1) : C(X, Y)) : (a : X) → Y) (1, x).2 :
      Y)
    ((f₂ : (a : X) → Y) x : Y)

Tactic:
norm_num
-- 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₂
x : (↑I : Type) × X
pos :
  ∀ (h : (↑x.1 : ℝ) ≤ 1 / 2),
    Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ)) : C(X, Y)) : (a : X) → Y) x.2 : Y)
      ((F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ)) ⋯, x.2) : Y)
neg :
  ∀ (h : ¬(↑x.1 : ℝ) ≤ 1 / 2),
    Eq.{v + 1} (α := Y) ((((G.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ) - 1) : C(X, Y)) : (a : X) → Y) x.2 : Y)
      ((G : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ) - 1) ⋯, x.2) : Y)
⊢ Eq.{v + 1} (α := Y)
    (if (↑x.1 : ℝ) ≤ 1 / 2 then (((F.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ)) : C(X, Y)) : (a : X) → Y) x.2
      else (((G.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ) - 1) : C(X, Y)) : (a : X) → Y) x.2 :
      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:
split_ifs
-- 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₂
x : (↑I : Type) × X
h : (↑x.1 : ℝ) ≤ 1 / 2
pos :
  Eq.{v + 1} (α := Y)
    ((((F.curry : (a : (↑(Set.Icc 0 1) : Type)) → C(X, Y))
              (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x) (2 * (↑x.1 : ℝ)) ⋯) :
            C(X, Y)) :
          (a : X) → Y)
        x.2 :
      Y)
    ((F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ)) ⋯, x.2) : Y)
pos₁ : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (2 * (↑x.1 : ℝ))
⊢ Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ)) : C(X, Y)) : (a : X) → Y) x.2 : Y)
    ((F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ)) ⋯, x.2) : Y)

Tactic:
rw [extend, ContinuousMap.coe_IccExtend, Set.IccExtend_of_mem]

Premises used: Set.IccExtend_of_mem, ContinuousMap.Homotopy.extend, ContinuousMap.coe_IccExtend
-- 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₂
x : (↑I : Type) × X
h : ¬(↑x.1 : ℝ) ≤ 1 / 2
neg :
  Eq.{v + 1} (α := Y)
    ((((G.curry : (a : (↑(Set.Icc 0 1) : Type)) → C(X, Y))
              (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x) (2 * (↑x.1 : ℝ) - 1) ⋯) :
            C(X, Y)) :
          (a : X) → Y)
        x.2 :
      Y)
    ((G : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ) - 1) ⋯, x.2) : Y)
neg₁ : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (2 * (↑x.1 : ℝ) - 1)
⊢ Eq.{v + 1} (α := Y) ((((G.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ) - 1) : C(X, Y)) : (a : X) → Y) x.2 : Y)
    ((G : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ) - 1) ⋯, x.2) : Y)

Tactic:
rw [extend, ContinuousMap.coe_IccExtend, Set.IccExtend_of_mem]

Premises used: Set.IccExtend_of_mem, ContinuousMap.Homotopy.extend, ContinuousMap.coe_IccExtend
-- 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₂
h :
  ∀ (t : (↑I : Type)) (snd : X),
    Eq.{v + 1} (α := Y) (((F.trans G).symm : (a : (↑I : Type) × X) → Y) (t, snd) : Y)
      ((G.symm.trans F.symm : (a : (↑I : Type) × X) → Y) (t, snd) : Y)
⊢ (F.trans G).symm = G.symm.trans F.symm

Tactic:
ext ⟨t, _⟩
-- 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 :
  Eq.{v + 1} (α := Y)
    (if h : (↑(σ (t, snd).1, (t, snd).2).1 : ℝ) ≤ 1 / 2 then
      (F : (a : (↑I : Type) × X) → Y)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ (t, snd).1, (t, snd).2).1 : ℝ)) ⋯,
          (σ (t, snd).1, (t, snd).2).2)
    else
      (G : (a : (↑I : Type) × X) → Y)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ (t, snd).1, (t, snd).2).1 : ℝ) - 1) ⋯,
          (σ (t, snd).1, (t, snd).2).2))
    (if h : (↑(t, snd).1 : ℝ) ≤ 1 / 2 then
      (G.symm : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(t, snd).1 : ℝ)) ⋯, (t, snd).2)
    else
      (F.symm : (a : (↑I : Type) × X) → Y)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(t, snd).1 : ℝ) - 1) ⋯, (t, snd).2))
⊢ Eq.{v + 1} (α := Y) (((F.trans G).symm : (a : (↑I : Type) × X) → Y) (t, snd) : Y)
    ((G.symm.trans F.symm : (a : (↑I : Type) × X) → Y) (t, snd) : Y)

Tactic:
rw [trans_apply, symm_apply, trans_apply]

Premises used: ContinuousMap.Homotopy.symm_apply, ContinuousMap.Homotopy.trans_apply
-- 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 :
  Eq.{v + 1} (α := Y)
    (if h : 1 - (↑t : ℝ) ≤ 1 / 2 then
      (F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ))) ⋯, snd)
    else (G : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ)) - 1) ⋯, snd))
    (if h : (↑t : ℝ) ≤ 1 / 2 then
      (G : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯), snd)
    else (F : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯), snd))
⊢ Eq.{v + 1} (α := Y)
    (if h : (↑(σ (t, snd).1, (t, snd).2).1 : ℝ) ≤ 1 / 2 then
      (F : (a : (↑I : Type) × X) → Y)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ (t, snd).1, (t, snd).2).1 : ℝ)) ⋯,
          (σ (t, snd).1, (t, snd).2).2)
    else
      (G : (a : (↑I : Type) × X) → Y)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ (t, snd).1, (t, snd).2).1 : ℝ) - 1) ⋯,
          (σ (t, snd).1, (t, snd).2).2))
    (if h : (↑(t, snd).1 : ℝ) ≤ 1 / 2 then
      (G.symm : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(t, snd).1 : ℝ)) ⋯, (t, snd).2)
    else
      (F.symm : (a : (↑I : Type) × X) → Y)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(t, snd).1 : ℝ) - 1) ⋯, (t, snd).2))

Tactic:
simp only [coe_symm_eq, symm_apply]

Premises used: ContinuousMap.Homotopy.symm_apply, unitInterval.coe_symm_eq
-- 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
pos :
  ∀ (h₁ : 1 - (↑t : ℝ) ≤ 1 / 2) (h₂ : (↑t : ℝ) ≤ 1 / 2),
    Eq.{v + 1} (α := Y)
      ((F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ))) ⋯, snd) : Y)
      ((G : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯), snd) : Y)
neg :
  ∀ (h₁ : 1 - (↑t : ℝ) ≤ 1 / 2) (h₂ : ¬(↑t : ℝ) ≤ 1 / 2),
    Eq.{v + 1} (α := Y)
      ((F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ))) ⋯, snd) : Y)
      ((F : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯), snd) : Y)
pos₁ :
  ∀ (h₁ : ¬1 - (↑t : ℝ) ≤ 1 / 2) (h₂ : (↑t : ℝ) ≤ 1 / 2),
    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)
neg₁ :
  ∀ (h₁ : ¬1 - (↑t : ℝ) ≤ 1 / 2) (h₂ : ¬(↑t : ℝ) ≤ 1 / 2),
    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)
⊢ Eq.{v + 1} (α := Y)
    (if h : 1 - (↑t : ℝ) ≤ 1 / 2 then
      (F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ))) ⋯, snd)
    else (G : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ)) - 1) ⋯, snd))
    (if h : (↑t : ℝ) ≤ 1 / 2 then
      (G : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯), snd)
    else (F : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯), snd))

Tactic:
split_ifs with h₁ h₂ h₂
-- 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 : (↑t : ℝ) < 1 / 2 → 2 / 2 = 1
linarith₁ : (↑t : ℝ) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (↑t : ℝ) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : (↑t : ℝ) < 1 / 2 → 2 / 2 = 1
linarith₄ : (↑t : ℝ) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : (↑t : ℝ) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : (↑t : ℝ) < 1 / 2 → 2 / 2 = 1
linarith₇ : (↑t : ℝ) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : (↑t : ℝ) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₉ :
  (↑t : ℝ) < 1 / 2 →
    HMul.hMul (α := ℝ) 2 1 - 2 * (↑t : ℝ) - HMul.hMul (α := ℝ) 1 1 + (2 * (↑t : ℝ) - HMul.hMul (α := ℝ) 1 1) = 0
linarith₁₀ : 1 / 2 < (↑t : ℝ) → 2 / 2 = 1
linarith₁₁ : 1 / 2 < (↑t : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ : 1 / 2 < (↑t : ℝ) → GT.gt (α := ℝ) 2 0
linarith₁₃ : 1 / 2 < (↑t : ℝ) → 2 / 2 = 1
linarith₁₄ : 1 / 2 < (↑t : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₅ : 1 / 2 < (↑t : ℝ) → GT.gt (α := ℝ) 2 0
linarith₁₆ : 1 / 2 < (↑t : ℝ) → 2 / 2 = 1
linarith₁₇ : 1 / 2 < (↑t : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₈ : 1 / 2 < (↑t : ℝ) → GT.gt (α := ℝ) 2 0
linarith₁₉ : 1 / 2 < (↑t : ℝ) → 2 * (↑t : ℝ) - HMul.hMul (α := ℝ) 1 1 + (HMul.hMul (α := ℝ) 1 1 - 2 * (↑t : ℝ)) = 0
⊢ (↑t : ℝ) = 1 / 2

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
⊢ (↑t : ℝ) = 1 / 2

Tactic:
have ht : (t : ℝ) = 1 / 2 := by 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
ht : (↑t : ℝ) = 1 / 2
⊢ Eq.{v + 1} (α := Y)
    ((F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ))) ⋯, snd) : Y)
    ((G : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯), snd) : Y)

Tactic:
norm_num [ht]
-- 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 :
  Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ))) ⋯ =
    σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)
⊢ Eq.{v + 1} (α := Y)
    ((F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ))) ⋯, snd) : Y)
    ((F : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯), 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
neg :
  (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ))) ⋯) : ℝ) =
    (↑(σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)) : ℝ)
⊢ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ))) ⋯ =
    σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext