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₂
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
⊢ 2 * (1 - (↑t : ℝ)) = 1 - (2 * (↑t : ℝ) - 1)
have linarith₇ : 1 - (2 * (↑t : ℝ) - 1) < 2 * (1 - (↑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 : 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
⊢ 2 * (1 - (↑t : ℝ)) = 1 - (2 * (↑t : ℝ) - 1)
have linarith₈ : 1 - (2 * (↑t : ℝ) - 1) < 2 * (1 - (↑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 : 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
⊢ 2 * (1 - (↑t : ℝ)) = 1 - (2 * (↑t : ℝ) - 1)
have linarith₉ : 1 - (2 * (↑t : ℝ) - 1) < 2 * (1 - (↑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 : 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
⊢ 2 * (1 - (↑t : ℝ)) = 1 - (2 * (↑t : ℝ) - 1)
have linarith₁₃ : 1 - (2 * (↑t : ℝ) - 1) < 2 * (1 - (↑t : ℝ)) → 1 - (2 * (↑t : ℝ) - 1) - 2 * (1 - (↑t : ℝ)) = 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
⊢ 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)
have pos : Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ)) - 1) sorry =
  σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) 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 : ℝ)) - 1) ⋯ =
    σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)
have pos : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 - (↑t : ℝ)) - 1) sorry) : ℝ) =
  (↑(σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) 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 = 1 - 2 * (↑t : ℝ)
have linarith : 2 * (1 - (↑t : ℝ)) - 1 < 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 : 2 * (1 - (↑t : ℝ)) - 1 < 1 - 2 * (↑t : ℝ) → 2 / 2 = 1
⊢ 2 * (1 - (↑t : ℝ)) - 1 = 1 - 2 * (↑t : ℝ)
have linarith₁ : 2 * (1 - (↑t : ℝ)) - 1 < 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 : 2 * (1 - (↑t : ℝ)) - 1 < 1 - 2 * (↑t : ℝ) → 2 / 2 = 1
linarith₁ : 2 * (1 - (↑t : ℝ)) - 1 < 1 - 2 * (↑t : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 2 * (1 - (↑t : ℝ)) - 1 = 1 - 2 * (↑t : ℝ)
have linarith₂ : 2 * (1 - (↑t : ℝ)) - 1 < 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 : 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
⊢ 2 * (1 - (↑t : ℝ)) - 1 = 1 - 2 * (↑t : ℝ)
have linarith₆ : 2 * (1 - (↑t : ℝ)) - 1 < 1 - 2 * (↑t : ℝ) → 2 * (1 - (↑t : ℝ)) - 1 - (1 - 2 * (↑t : ℝ)) = 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 < 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
⊢ 2 * (1 - (↑t : ℝ)) - 1 = 1 - 2 * (↑t : ℝ)
have linarith₇ : 1 - 2 * (↑t : ℝ) < 2 * (1 - (↑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 < 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
⊢ 2 * (1 - (↑t : ℝ)) - 1 = 1 - 2 * (↑t : ℝ)
have linarith₈ : 1 - 2 * (↑t : ℝ) < 2 * (1 - (↑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 < 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
⊢ 2 * (1 - (↑t : ℝ)) - 1 = 1 - 2 * (↑t : ℝ)
have linarith₉ : 1 - 2 * (↑t : ℝ) < 2 * (1 - (↑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 < 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
⊢ 2 * (1 - (↑t : ℝ)) - 1 = 1 - 2 * (↑t : ℝ)
have linarith₁₃ : 1 - 2 * (↑t : ℝ) < 2 * (1 - (↑t : ℝ)) - 1 → 1 - 2 * (↑t : ℝ) - (2 * (1 - (↑t : ℝ)) - 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
⊢ 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)
have neg : False
Tactic: exfalso
-- 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
⊢ False
have linarith : 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 / 2 = 1
⊢ False
have linarith₁ : 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 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
⊢ False
have linarith₂ : 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 / 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
⊢ False
have linarith₆ : HMul.hMul (α := ℝ) 1 1 - (HMul.hMul (α := ℝ) 2 1 - 2 * (↑t : ℝ)) + (HMul.hMul (α := ℝ) 1 1 - 2 * (↑t : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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)
⊢ P { toFun := fun (x : X) ↦ (F.toHomotopy (P := P).trans (G.toHomotopy (P := P))).toFun (t, x), continuous_toFun := ⋯ }
have 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 := sorry }
Tactic: simp only [Homotopy.trans]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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)
⊢ 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 := ⋯ }
have 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 := sorry }
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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 := ⋯ }
⊢ 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 := ⋯ }
have 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 := sorry }
Tactic: split_ifs
-- 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₁ : 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)
have rw : Eq.{v + 1} (α := Y) ((f₀ : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)
Tactic: rw [F.eq_fst t hx, ← F.eq_fst 1 hx, F.apply_one]
-- 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₁ : 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)
⊢ Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (t, x) : Y) ((f₁ : (a : X) → Y) x : Y)
have rw₁ : Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (1, x) : Y) ((f₁ : (a : X) → Y) x : Y)
Tactic: rw [F.eq_fst t hx, ← F.eq_fst 1 hx, F.apply_one]
-- 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₁ : 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)
⊢ Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (t, x) : Y) ((f₁ : (a : X) → Y) x : Y)
have rw₂ : Eq.{v + 1} (α := Y) ((f₁ : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)
Tactic: rw [F.eq_fst t hx, ← F.eq_fst 1 hx, F.apply_one]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : (↑I : Type)
x : X
hx : x ∈ S
⊢ Eq.{v + 1} (α := Y)
    (({
            toFun := fun (x : X) ↦
              (F.toHomotopy (P := fun (f : C(X, Y)) ↦
                        ∀ x ∈ S, Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)).trans
                    (G.toHomotopy (P := fun (f : C(X, Y)) ↦
                      ∀ x ∈ S, Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)))).toFun
                (t, x),
            continuous_toFun := ⋯ : C(X, Y) } :
          (a : X) → Y)
        x :
      Y)
    ((f₀ : (a : X) → Y) x : Y)
have simp : Eq.{v + 1} (α := Y)
  (({
          toFun := fun (x : X) ↦
            if (↑t : ℝ) ≤ 1 / 2 then
              (((F.toHomotopy (P := fun (f : C(X, Y)) ↦
                            ∀ x ∈ S, Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)).extend :
                        (a : ℝ) → C(X, Y))
                      (2 * (↑t : ℝ)) :
                    C(X, Y)) :
                  (a : X) → Y)
                x
            else
              (((G.toHomotopy (P := fun (f : C(X, Y)) ↦
                            ∀ x ∈ S, Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)).extend :
                        (a : ℝ) → C(X, Y))
                      (2 * (↑t : ℝ) - 1) :
                    C(X, Y)) :
                  (a : X) → Y)
                x,
          continuous_toFun := sorry : C(X, Y) } :
        (a : X) → Y)
      x :
    Y)
  ((f₀ : (a : X) → Y) x : Y)
Tactic: simp only [Homotopy.trans]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
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)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : (↑I : Type)
x : X
hx : x ∈ S
⊢ Eq.{v + 1} (α := Y)
    (({
            toFun := fun (x : X) ↦
              if (↑t : ℝ) ≤ 1 / 2 then
                (((F.toHomotopy (P := fun (f : C(X, Y)) ↦
                              ∀ x ∈ S,
                                Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)).extend :
                          (a : ℝ) → C(X, Y))
                        (2 * (↑t : ℝ)) :
                      C(X, Y)) :
                    (a : X) → Y)
                  x
              else
                (((G.toHomotopy (P := fun (f : C(X, Y)) ↦
                              ∀ x ∈ S,
                                Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)).extend :
                          (a : ℝ) → C(X, Y))
                        (2 * (↑t : ℝ) - 1) :
                      C(X, Y)) :
                    (a : X) → Y)
                  x,
            continuous_toFun := ⋯ : C(X, Y) } :
          (a : X) → Y)
        x :
      Y)
    ((f₀ : (a : X) → Y) x : Y)
have pos : ∀ (h : (↑t : ℝ) ≤ 1 / 2),
  Eq.{v + 1} (α := Y)
    (({
            toFun := fun (x : X) ↦
              (((F.toHomotopy (P := fun (f : C(X, Y)) ↦
                            ∀ x ∈ S, Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)).extend :
                        (a : ℝ) → C(X, Y))
                      (2 * (↑t : ℝ)) :
                    C(X, Y)) :
                  (a : X) → Y)
                x,
            continuous_toFun := sorry : C(X, Y) } :
          (a : X) → Y)
        x :
      Y)
    ((f₀ : (a : X) → Y) x : Y)
Tactic: split_ifs