awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
pos :
  ∀ (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 : ℝ)) ⋯)) : X)
neg :
  ∀ (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)
pos₁ :
  ∀ (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)
neg₁ :
  ∀ (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)
⊢ Eq.{u_1 + 1} (α := X)
    (if h : (↑(σ t) : ℝ) ≤ 1 / 2 then
      (γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ)) ⋯)
    else (γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ) - 1) ⋯))
    (if h : (↑t : ℝ) ≤ 1 / 2 then
      (γ' : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯))
    else (γ : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)))

Tactic:
split_ifs with h h₁ h₂
-- Module: Mathlib.Topology.Path
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
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) : ℝ)) ⋯) : X)
      ((γ' : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)) : X)
⊢ 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)

Tactic:
rw [coe_symm_eq] at h

Premises used: unitInterval.coe_symm_eq
-- Module: Mathlib.Topology.Path
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
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) : ℝ)) ⋯) : X)
      ((γ : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)) : X)
⊢ 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)

Tactic:
rw [coe_symm_eq] at h

Premises used: unitInterval.coe_symm_eq
-- Module: Mathlib.Topology.Path
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
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) ⋯) : X)
      ((γ' : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)) : X)
⊢ 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)

Tactic:
rw [coe_symm_eq] at h

Premises used: unitInterval.coe_symm_eq
-- Module: Mathlib.Topology.Path
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
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) ⋯) : X)
      ((γ : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)) : X)
⊢ 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)

Tactic:
rw [coe_symm_eq] at h

Premises used: unitInterval.coe_symm_eq
-- Module: Mathlib.Topology.Path
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
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.Path
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

Tactic:
have ht : (t : ℝ) = 1 / 2 := by linarith
-- Module: Mathlib.Topology.Path
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
ht : (↑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)

Tactic:
norm_num [ht]
-- Module: Mathlib.Topology.Path
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)

Tactic:
congr_arg _ (Subtype.ext ?_)

Premises used: congr_arg, Subtype.ext
-- Module: Mathlib.Topology.Path
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
neg :
  (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ)) ⋯) : ℝ) =
    (↑(σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)) : ℝ)
⊢ 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)

Tactic:
refine congr_arg _ (Subtype.ext ?_)

Premises used: congr_arg, Subtype.ext
-- Module: Mathlib.Topology.Path
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
⊢ (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ)) ⋯) : ℝ) =
    (↑(σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)) : ℝ)

Tactic:
norm_num [sub_sub_eq_add_sub, mul_sub]

Premises used: mul_sub, sub_sub_eq_add_sub
-- Module: Mathlib.Topology.Path
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)

Tactic:
congr_arg _ (Subtype.ext ?_)

Premises used: congr_arg, Subtype.ext
-- Module: Mathlib.Topology.Path
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
pos :
  (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ) - 1) ⋯) : ℝ) =
    (↑(σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)) : ℝ)
⊢ 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)

Tactic:
refine congr_arg _ (Subtype.ext ?_)

Premises used: congr_arg, Subtype.ext
-- Module: Mathlib.Topology.Path
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
⊢ 2 * (1 - (↑t : ℝ)) - 1 = 1 - 2 * (↑t : ℝ)

Tactic:
ring
-- Module: Mathlib.Topology.Path
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
neg : False
⊢ 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)

Tactic:
exfalso
-- Module: Mathlib.Topology.Path
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
linarith₉ :
  HMul.hMul (α := ℝ) 1 1 - (HMul.hMul (α := ℝ) 2 1 - 2 * (↑t : ℝ)) + (HMul.hMul (α := ℝ) 1 1 - 2 * (↑t : ℝ)) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Topology.Path
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)
inr : ∀ (ht₀ : 0 ≤ t), 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)

Tactic:
obtain _ | ht₀ := le_total t 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Topology.Path
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
linarith₃ : 0 < t → t - 0 + (0 - t) = 0
⊢ t ≤ 0

Tactic:
linarith
-- Module: Mathlib.Topology.Path
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
inl : x = (γ₁.extend : (a : ℝ) → X) (2 * t)
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)

Tactic:
rw [extend_of_le_zero _ (by linarith)]

Premises used: Path.extend_of_le_zero
-- Module: Mathlib.Topology.Path
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
linarith₃ : 0 < 2 * t → 2 * (t - 0) + (0 - 2 * t) = 0
linarith₄ : 0 < 2 * t → GT.gt (α := ℝ) 2 0
⊢ 2 * t ≤ 0

Tactic:
linarith
-- Module: Mathlib.Topology.Path
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
inl inl₁ : x = x
⊢ x = (γ₁.extend : (a : ℝ) → X) (2 * t)

Tactic:
rw [extend_of_le_zero _ (by linarith)]

Premises used: Path.extend_of_le_zero
-- Module: Mathlib.Topology.Path
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
inl inl₁ inl₂ : x = (γ₁.extend : (a : ℝ) → X) (2 * t)
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)

Tactic:
repeat rw [extend_of_le_zero _ (by linarith)]

Premises used: Path.extend_of_le_zero
-- Module: Mathlib.Topology.Path
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
linarith₃ : 1 < t → -1 + (2 * t - HMul.hMul (α := ℝ) 1 1) + 2 * (1 - t) = 0
linarith₄ : 1 < t → GT.gt (α := ℝ) 2 0
⊢ t ≤ 1

Tactic:
linarith
-- Module: Mathlib.Topology.Path
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
inr₄ :
  Eq (α := X)
    ((γ₁ : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ)) ⋯) :
      X)
    ((γ₁ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * t) ⋯) : X)
inr₅ : Membership.mem (γ := Set ℝ) (Icc 0 1) (2 * t)
inr₆ : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ) ≤ 1 / 2
inr₇ :
  Eq (α := X)
    ((γ₁ : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ)) ⋯) :
      X)
    ((γ₁ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * t) ⋯) : X)
inr₈ : Membership.mem (γ := Set ℝ) (Icc 0 1) (2 * t)
inr₉ inr₁₀ 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)

Tactic:
rwa [extend_apply _ ⟨ht₀, by linarith⟩, trans_apply, dif_pos, extend_apply]

Premises used: Path.extend_apply, dif_pos, Path.trans_apply, And.intro
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
rw : (((γ₁.trans γ₂).extend : (a : ℝ) → X) (1 - (1 - t)) : X)
| (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X)

Tactic:
rw [← sub_sub_cancel 1 t]

Premises used: sub_sub_cancel, OfNat.ofNat
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
conv_lhs :
  Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) (1 - (1 - t)) : X) ((γ₂.extend : (a : ℝ) → X) (2 * t - 1) : X)
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₂.extend : (a : ℝ) → X) (2 * t - 1) : X)

Tactic:
conv_lhs => rw [← sub_sub_cancel 1 t]

Premises used: sub_sub_cancel, OfNat.ofNat
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
linarith : 1 / 2 < 1 - t → 2 / 2 = 1
linarith₁ : 1 / 2 < 1 - t → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 < 1 - t → GT.gt (α := ℝ) 2 0
linarith₃ : 1 / 2 < 1 - t → 2 / 2 = 1
linarith₄ : 1 / 2 < 1 - t → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 / 2 < 1 - t → GT.gt (α := ℝ) 2 0
linarith₆ :
  1 / 2 < 1 - t → HMul.hMul (α := ℝ) 1 1 - 2 * t + (HMul.hMul (α := ℝ) 1 1 - (HMul.hMul (α := ℝ) 2 1 - 2 * t)) = 0
⊢ 1 - t ≤ 1 / 2

Tactic:
linarith
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
rw : Eq (α := X) ((γ₂.extend : (a : ℝ) → X) (1 - 2 * (1 - t)) : X) ((γ₂.extend : (a : ℝ) → X) (2 * t - 1) : X)
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) (1 - (1 - t)) : X) ((γ₂.extend : (a : ℝ) → X) (2 * t - 1) : X)

Tactic:
rw [← extend_symm_apply, trans_symm, extend_trans_of_le_half _ _ (by linarith), extend_symm_apply]

Premises used: Path.extend_symm_apply, Path.extend_trans_of_le_half, Path.trans_symm
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
h : 1 - 2 * (1 - t) = 2 * t - 1
⊢ Eq (α := X) ((γ₂.extend : (a : ℝ) → X) (1 - 2 * (1 - t)) : X) ((γ₂.extend : (a : ℝ) → X) (2 * t - 1) : X)

Tactic:
congr 1
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
linarith : 1 - 2 * (1 - t) < 2 * t - 1 → 2 / 2 = 1
linarith₁ : 1 - 2 * (1 - t) < 2 * t - 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - 2 * (1 - t) < 2 * t - 1 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - 2 * (1 - t) < 2 * t - 1 → 1 - 2 * (1 - t) - (2 * t - 1) = 0
linarith₄ : 2 * t - 1 < 1 - 2 * (1 - t) → 2 / 2 = 1
linarith₅ : 2 * t - 1 < 1 - 2 * (1 - t) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 2 * t - 1 < 1 - 2 * (1 - t) → GT.gt (α := ℝ) 2 0
linarith₇ : 2 * t - 1 < 1 - 2 * (1 - t) → 2 * t - 1 - (1 - 2 * (1 - t)) = 0
⊢ 1 - 2 * (1 - t) = 2 * t - 1

Tactic:
linarith
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a : X
a₁ :
  ∀ (x : (↑I : Type)),
    Eq (α := X) ((trans (refl a) (refl a) : (a : (↑I : Type)) → X) x : X) ((refl a : (a : (↑I : Type)) → X) x : X)
⊢ Eq (α := Path a a) (trans (refl a) (refl a)) (refl a)

Tactic:
ext
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a : X
x : (↑I : Type)
⊢ Eq (α := X) ((trans (refl a) (refl a) : (a : (↑I : Type)) → X) x : X) ((refl a : (a : (↑I : Type)) → X) x : X)

Tactic:
simp [Path.trans]

Premises used: Path.trans
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
rw :
  Eq (α := Set X)
    ((⇑γ₁.extend : (a : ℝ) → X) '' HMul.hMul (α := ℝ) 2 '' Iic (1 / 2) ∪
      image (α := ℝ) (⇑γ₂.extend : (a : ℝ) → X) ((fun (x : ℝ) ↦ x - 1) '' HMul.hMul (α := ℝ) 2 '' Ici (1 / 2)))
    (range (ι := (↑I : Type)) (⇑γ₁ : (a : (↑I : Type)) → X) ∪ range (ι := (↑I : Type)) (⇑γ₂ : (a : (↑I : Type)) → X))
⊢ Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ₁.trans γ₂) : (a : (↑I : Type)) → X))
    (range (ι := (↑I : Type)) (⇑γ₁ : (a : (↑I : Type)) → X) ∪ range (ι := (↑I : Type)) (⇑γ₂ : (a : (↑I : Type)) → X))

Tactic:
rw [← extend_range, ← image_univ, ← Iic_union_Ici (a := 1 / 2), image_union,
    EqOn.image_eq fun t ht ↦ extend_trans_of_le_half _ _ (mem_Iic.1 ht),
    EqOn.image_eq fun t ht ↦ extend_trans_of_half_le _ _ (mem_Ici.1 ht),
    ← image_image γ₁.extend, ← image_image (γ₂.extend <| · - 1), ← image_image γ₂.extend]

Premises used: Set.image_image, Set.image_univ, Path.extend_trans_of_le_half, HSub.hSub, Path.extend_range, Path.extend, Set.Iic_union_Ici, Set.EqOn.image_eq, Set.mem_Ici, Iff.mp, Set.mem_Iic, OfNat.ofNat, DFunLike.coe, Path.extend_trans_of_half_le, Set.image_union
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ Eq (α := Set X)
    ((⇑γ₁.extend : (a : ℝ) → X) '' HMul.hMul (α := ℝ) 2 '' Iic (1 / 2) ∪
      image (α := ℝ) (⇑γ₂.extend : (a : ℝ) → X) ((fun (x : ℝ) ↦ x - 1) '' HMul.hMul (α := ℝ) 2 '' Ici (1 / 2)))
    (range (ι := (↑I : Type)) (⇑γ₁ : (a : (↑I : Type)) → X) ∪ range (ι := (↑I : Type)) (⇑γ₂ : (a : (↑I : Type)) → X))

Tactic:
norm_num [image_mul_left_Ici, image_mul_left_Iic,
    image_extend_of_subset, Icc_subset_Iic_self, Icc_subset_Ici_self]

Premises used: Set.Icc_subset_Iic_self, Path.image_extend_of_subset, Set.image_mul_left_Iic, Set.Icc_subset_Ici_self, Set.image_mul_left_Ici
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
γ_1 γ : Path x y
f : X → Y
h : ContinuousOn f (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
⊢ Function.comp (α := (↑I : Type)) f (⇑γ : (a : (↑I : Type)) → X) 0 = f x

Tactic:
simp
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
γ_1 γ : Path x y
f : X → Y
h : ContinuousOn f (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
⊢ Function.comp (α := (↑I : Type)) f (⇑γ : (a : (↑I : Type)) → X) 1 = f y

Tactic:
simp
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
γ : Path x y
f : X → Y
h : Continuous[inst, inst_1] f
h₁ : ∀ (t : (↑I : Type)), (γ.map h : (a : (↑I : Type)) → Y) t = (f ∘ (⇑γ : (a : (↑I : Type)) → X)) t
⊢ Eq (α := (a : (↑I : Type)) → Y) (⇑(γ.map h) : (a : (↑I : Type)) → Y) (f ∘ (⇑γ : (a : (↑I : Type)) → X))

Tactic:
ext t
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
γ : Path x y
f : X → Y
h : Continuous[inst, inst_1] f
t : (↑I : Type)
⊢ (γ.map h : (a : (↑I : Type)) → Y) t = (f ∘ (⇑γ : (a : (↑I : Type)) → X)) t

Tactic:
rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
γ : Path x y
f : X → Y
h : Continuous[inst, inst_1] f
⊢ (γ.map h).symm = γ.symm.map h

Tactic:
rfl

Premises used: Path.map, Path.map', rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous[inst, inst_1] f
a :
  ∀ (t : (↑I : Type)),
    Eq (α := Y) (((γ.trans γ').map h : (a : (↑I : Type)) → Y) t : Y)
      (((γ.map h).trans (γ'.map h) : (a : (↑I : Type)) → Y) t : Y)
⊢ (γ.trans γ').map h = (γ.map h).trans (γ'.map h)

Tactic:
ext t