awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ 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)
have 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 : ℝ)) sorry) :
          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 : ℝ)) sorry, x.2) : Y)
Tactic: rw [extend, ContinuousMap.coe_IccExtend, Set.IccExtend_of_mem]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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)
⊢ 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)
have pos₁ : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (2 * (↑x.1 : ℝ))
Tactic: rw [extend, ContinuousMap.coe_IccExtend, Set.IccExtend_of_mem]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ 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)
have 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) sorry) :
          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) sorry, x.2) : Y)
Tactic: rw [extend, ContinuousMap.coe_IccExtend, Set.IccExtend_of_mem]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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)
⊢ 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)
have neg₁ : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (2 * (↑x.1 : ℝ) - 1)
Tactic: rw [extend, ContinuousMap.coe_IccExtend, Set.IccExtend_of_mem]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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₂
⊢ (F.trans G).symm = G.symm.trans F.symm
have 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)
Tactic: ext ⟨t, _⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ 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)
have 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 : ℝ)) sorry, (σ (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) sorry,
        (σ (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 : ℝ)) sorry, (t, snd).2)
  else
    (F.symm : (a : (↑I : Type) × X) → Y)
      (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(t, snd).1 : ℝ) - 1) sorry, (t, snd).2))
Tactic: rw [trans_apply, symm_apply, trans_apply]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ 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))
have 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 : ℝ))) sorry, snd)
  else (G : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ)) - 1) sorry, snd))
  (if h : (↑t : ℝ) ≤ 1 / 2 then
    (G : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry), snd)
  else (F : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry), snd))
Tactic: simp only [coe_symm_eq, symm_apply]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ 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))
have 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 : ℝ))) sorry, snd) : Y)
    ((G : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry), snd) : Y)
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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)
⊢ 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))
have 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 : ℝ))) sorry, snd) : Y)
    ((F : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry), snd) : Y)
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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)
⊢ 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))
have 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) sorry, snd) : Y)
    ((G : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry), snd) : Y)
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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)
⊢ 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))
have 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) sorry, snd) : Y)
    ((F : (a : (↑I : Type) × X) → Y) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry), snd) : Y)
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
have linarith : (↑t : ℝ) < 1 / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ (↑t : ℝ) = 1 / 2
have linarith₁ : (↑t : ℝ) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ (↑t : ℝ) = 1 / 2
have linarith₂ : (↑t : ℝ) < 1 / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ (↑t : ℝ) = 1 / 2
have linarith₉ : (↑t : ℝ) < 1 / 2 →
  HMul.hMul (α := ℝ) 2 1 - 2 * (↑t : ℝ) - HMul.hMul (α := ℝ) 1 1 + (2 * (↑t : ℝ) - HMul.hMul (α := ℝ) 1 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ (↑t : ℝ) = 1 / 2
have linarith₁₀ : 1 / 2 < (↑t : ℝ) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ (↑t : ℝ) = 1 / 2
have linarith₁₁ : 1 / 2 < (↑t : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ (↑t : ℝ) = 1 / 2
have linarith₁₂ : 1 / 2 < (↑t : ℝ) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ (↑t : ℝ) = 1 / 2
have linarith₁₉ : 1 / 2 < (↑t : ℝ) → 2 * (↑t : ℝ) - HMul.hMul (α := ℝ) 1 1 + (HMul.hMul (α := ℝ) 1 1 - 2 * (↑t : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (hypothesis)
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
⊢ 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)
have ht : (↑t : ℝ) = 1 / 2
Tactic: have ht : (t : ℝ) = 1 / 2 := by linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ 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)
have neg : Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ))) sorry =
  σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ))) ⋯ =
    σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)
have neg : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ))) sorry) : ℝ) =
  (↑(σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry)) : ℝ)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ 2 * (1 - (↑t : ℝ)) = 1 - (2 * (↑t : ℝ) - 1)
have linarith : 2 * (1 - (↑t : ℝ)) < 1 - (2 * (↑t : ℝ) - 1) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ 2 * (1 - (↑t : ℝ)) = 1 - (2 * (↑t : ℝ) - 1)
have linarith₁ : 2 * (1 - (↑t : ℝ)) < 1 - (2 * (↑t : ℝ) - 1) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ 2 * (1 - (↑t : ℝ)) = 1 - (2 * (↑t : ℝ) - 1)
have linarith₂ : 2 * (1 - (↑t : ℝ)) < 1 - (2 * (↑t : ℝ) - 1) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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
⊢ 2 * (1 - (↑t : ℝ)) = 1 - (2 * (↑t : ℝ) - 1)
have linarith₆ : 2 * (1 - (↑t : ℝ)) < 1 - (2 * (↑t : ℝ) - 1) → 2 * (1 - (↑t : ℝ)) - (1 - (2 * (↑t : ℝ) - 1)) = 0
Tactic: linarith