awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h : (↑(σ t) : ℝ) ≤ 1 / 2
h₁ : ¬(↑t : ℝ) ≤ 1 / 2
⊢ Eq (α := X) ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ)) ⋯) : X)
    ((γ : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)) : X)
have neg : ∀ (h_1 : 1 - (↑t : ℝ) ≤ 1 / 2) (h₁ : ¬(↑t : ℝ) ≤ 1 / 2),
  Eq (α := X) ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ)) sorry) : X)
    ((γ : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry)) : X)
Tactic: rw [coe_symm_eq] at h
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h : ¬(↑(σ t) : ℝ) ≤ 1 / 2
h₂ : (↑t : ℝ) ≤ 1 / 2
⊢ Eq (α := X) ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ) - 1) ⋯) : X)
    ((γ' : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)) : X)
have pos : ∀ (h_1 : ¬1 - (↑t : ℝ) ≤ 1 / 2) (h₂ : (↑t : ℝ) ≤ 1 / 2),
  Eq (α := X) ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ) - 1) sorry) : X)
    ((γ' : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry)) : X)
Tactic: rw [coe_symm_eq] at h
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h : ¬(↑(σ t) : ℝ) ≤ 1 / 2
h₂ : ¬(↑t : ℝ) ≤ 1 / 2
⊢ Eq (α := X) ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ) - 1) ⋯) : X)
    ((γ : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)) : X)
have neg : ∀ (h_1 : ¬1 - (↑t : ℝ) ≤ 1 / 2) (h₂ : ¬(↑t : ℝ) ≤ 1 / 2),
  Eq (α := X) ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ) - 1) sorry) : X)
    ((γ : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry)) : X)
Tactic: rw [coe_symm_eq] at h
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : (↑(σ t) : ℝ) ≤ 1 / 2
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.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : (↑(σ t) : ℝ) ≤ 1 / 2
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.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : (↑(σ t) : ℝ) ≤ 1 / 2
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.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : (↑(σ t) : ℝ) ≤ 1 / 2
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 → 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.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : (↑(σ t) : ℝ) ≤ 1 / 2
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 → 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.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : (↑(σ t) : ℝ) ≤ 1 / 2
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 → 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.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : (↑(σ t) : ℝ) ≤ 1 / 2
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 → 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.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : (↑(σ t) : ℝ) ≤ 1 / 2
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 → 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 / 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.Path (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : (↑(σ t) : ℝ) ≤ 1 / 2
h : 1 - (↑t : ℝ) ≤ 1 / 2
h₁ : (↑t : ℝ) ≤ 1 / 2
⊢ Eq (α := X) ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ)) ⋯) : X)
    ((γ' : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)) : X)
have ht : (↑t : ℝ) = 1 / 2
Tactic: have ht : (t : ℝ) = 1 / 2 := by linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : (↑(σ t) : ℝ) ≤ 1 / 2
h : 1 - (↑t : ℝ) ≤ 1 / 2
h₁ : ¬(↑t : ℝ) ≤ 1 / 2
⊢ Eq (α := X) ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ)) ⋯) : X)
    ((γ : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)) : X)
have neg : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ)) sorry) : ℝ) =
  (↑(σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry)) : ℝ)
Tactic: refine congr_arg _ (Subtype.ext ?_)
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : ¬(↑(σ t) : ℝ) ≤ 1 / 2
h : ¬1 - (↑t : ℝ) ≤ 1 / 2
h₂ : (↑t : ℝ) ≤ 1 / 2
⊢ Eq (α := X) ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ) - 1) ⋯) : X)
    ((γ' : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)) : X)
have pos : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ) - 1) sorry) : ℝ) =
  (↑(σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry)) : ℝ)
Tactic: refine congr_arg _ (Subtype.ext ?_)
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : ¬(↑(σ t) : ℝ) ≤ 1 / 2
h : ¬1 - (↑t : ℝ) ≤ 1 / 2
h₂ : ¬(↑t : ℝ) ≤ 1 / 2
⊢ Eq (α := X) ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ) - 1) ⋯) : X)
    ((γ : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)) : X)
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : ¬(↑(σ t) : ℝ) ≤ 1 / 2
h : ¬1 - (↑t : ℝ) ≤ 1 / 2
h₂ : ¬(↑t : ℝ) ≤ 1 / 2
⊢ False
have linarith : 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : ¬(↑(σ t) : ℝ) ≤ 1 / 2
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.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : ¬(↑(σ t) : ℝ) ≤ 1 / 2
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.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h_1 : ¬(↑(σ t) : ℝ) ≤ 1 / 2
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₆ : 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.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
have inl : t ≤ 0 → Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
Tactic: obtain _ | ht₀ := le_total t 0
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
inl : t ≤ 0 → Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
have inr : ∀ (ht₀ : 0 ≤ t), Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
Tactic: obtain _ | ht₀ := le_total t 0
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h : t ≤ 0
⊢ t ≤ 0
have linarith : 0 < t → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h : t ≤ 0
linarith : 0 < t → 2 / 2 = 1
⊢ t ≤ 0
have linarith₁ : 0 < t → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h : t ≤ 0
linarith : 0 < t → 2 / 2 = 1
linarith₁ : 0 < t → HMul.hMul (α := ℝ) 1 2 = 2
⊢ t ≤ 0
have linarith₂ : 0 < t → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h : t ≤ 0
linarith : 0 < t → 2 / 2 = 1
linarith₁ : 0 < t → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 0 < t → GT.gt (α := ℝ) 2 0
⊢ t ≤ 0
have linarith₃ : 0 < t → t - 0 + (0 - t) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h : t ≤ 0
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
have inl : x = (γ₁.extend : (a : ℝ) → X) (2 * t)
Tactic: rw [extend_of_le_zero _ (by linarith)]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h : t ≤ 0
⊢ 2 * t ≤ 0
have linarith : 0 < 2 * t → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h : t ≤ 0
linarith : 0 < 2 * t → 2 / 2 = 1
⊢ 2 * t ≤ 0
have linarith₁ : 0 < 2 * t → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h : t ≤ 0
linarith : 0 < 2 * t → 2 / 2 = 1
linarith₁ : 0 < 2 * t → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 2 * t ≤ 0
have linarith₂ : 0 < 2 * t → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h : t ≤ 0
linarith : 0 < 2 * t → 2 / 2 = 1
linarith₁ : 0 < 2 * t → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 0 < 2 * t → GT.gt (α := ℝ) 2 0
⊢ 2 * t ≤ 0
have linarith₃ : 0 < 2 * t → 2 * (t - 0) + (0 - 2 * t) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h : t ≤ 0
⊢ x = (γ₁.extend : (a : ℝ) → X) (2 * t)
have inl : x = x
Tactic: rw [extend_of_le_zero _ (by linarith)]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h : t ≤ 0
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
have inl : x = (γ₁.extend : (a : ℝ) → X) (2 * t)
Tactic: repeat rw [extend_of_le_zero _ (by linarith)]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
⊢ t ≤ 1
have linarith : 1 < t → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
linarith : 1 < t → 2 / 2 = 1
⊢ t ≤ 1
have linarith₁ : 1 < t → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
linarith : 1 < t → 2 / 2 = 1
linarith₁ : 1 < t → HMul.hMul (α := ℝ) 1 2 = 2
⊢ t ≤ 1
have linarith₂ : 1 < t → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
linarith : 1 < t → 2 / 2 = 1
linarith₁ : 1 < t → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < t → GT.gt (α := ℝ) 2 0
⊢ t ≤ 1
have linarith₃ : 1 < t → -1 + (2 * t - HMul.hMul (α := ℝ) 1 1) + 2 * (1 - t) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
have inr : Eq (α := X) ((γ₁.trans γ₂ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t sorry) : X)
  ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
Tactic: rwa [extend_apply _ ⟨ht₀, by linarith⟩, trans_apply, dif_pos, extend_apply]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
inr :
  Eq (α := X) ((γ₁.trans γ₂ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : X)
    ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
have inr₁ : Eq (α := X)
  (if h : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t sorry) : ℝ) ≤ 1 / 2 then
      (γ₁ : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t sorry) : ℝ)) sorry)
    else
      (γ₂ : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t sorry) : ℝ) - 1) sorry) :
    X)
  ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
Tactic: rwa [extend_apply _ ⟨ht₀, by linarith⟩, trans_apply, dif_pos, extend_apply]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
inr :
  Eq (α := X) ((γ₁.trans γ₂ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : X)
    ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
inr₁ :
  Eq (α := X)
    (if h : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ) ≤ 1 / 2 then
        (γ₁ : (a : (↑I : Type)) → X)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ)) ⋯)
      else
        (γ₂ : (a : (↑I : Type)) → X)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ) - 1) ⋯) :
      X)
    ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
have inr₂ : Eq (α := X)
  ((γ₁ : (a : (↑I : Type)) → X)
      (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t sorry) : ℝ)) sorry) :
    X)
  ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
Tactic: rwa [extend_apply _ ⟨ht₀, by linarith⟩, trans_apply, dif_pos, extend_apply]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
inr :
  Eq (α := X) ((γ₁.trans γ₂ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : X)
    ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
inr₁ :
  Eq (α := X)
    (if h : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ) ≤ 1 / 2 then
        (γ₁ : (a : (↑I : Type)) → X)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ)) ⋯)
      else
        (γ₂ : (a : (↑I : Type)) → X)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ) - 1) ⋯) :
      X)
    ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
inr₂ :
  Eq (α := X)
    ((γ₁ : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ)) ⋯) :
      X)
    ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
have inr₃ : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t sorry) : ℝ) ≤ 1 / 2
Tactic: rwa [extend_apply _ ⟨ht₀, by linarith⟩, trans_apply, dif_pos, extend_apply]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
inr :
  Eq (α := X) ((γ₁.trans γ₂ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : X)
    ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
inr₁ :
  Eq (α := X)
    (if h : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ) ≤ 1 / 2 then
        (γ₁ : (a : (↑I : Type)) → X)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ)) ⋯)
      else
        (γ₂ : (a : (↑I : Type)) → X)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ) - 1) ⋯) :
      X)
    ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
inr₂ :
  Eq (α := X)
    ((γ₁ : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ)) ⋯) :
      X)
    ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
inr₃ : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ) ≤ 1 / 2
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
have inr₄ : Eq (α := X)
  ((γ₁ : (a : (↑I : Type)) → X)
      (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t sorry) : ℝ)) sorry) :
    X)
  ((γ₁ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * t) sorry) : X)
Tactic: rwa [extend_apply _ ⟨ht₀, by linarith⟩, trans_apply, dif_pos, extend_apply]