awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((hmulE : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (hmulE : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
⊢ Continuous G

Tactic:
have hG : Continuous G := by fun_prop
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((hmulE : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (hmulE : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
x : X
y : Y
⊢ { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (0, x, y) =
    (comp
          {
            toFun := fun (p : (X × Y) × X × Y) ↦
              ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
            continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
          (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (@e _ inst _, @e _ inst_1 _))) :
        (a : X × Y) → X × Y)
      (x, y)

Tactic:
Prod.ext (HSpace.hmulE.1.2 x) (HSpace.hmulE.1.2 y)

Premises used: Prod.ext, ContinuousMap.HomotopyWith.toHomotopy, HSpace.hmulE, ContinuousMap.Homotopy.map_zero_left
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((hmulE : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (hmulE : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
x : X
y : Y
⊢ { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (0, x, y) =
    (comp
          {
            toFun := fun (p : (X × Y) × X × Y) ↦
              ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
            continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
          (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (@e _ inst _, @e _ inst_1 _))) :
        (a : X × Y) → X × Y)
      (x, y)

Tactic:
exact Prod.ext (HSpace.hmulE.1.2 x) (HSpace.hmulE.1.2 y)

Premises used: Prod.ext
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((hmulE : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (hmulE : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
x : X
y : Y
⊢ { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (1, x, y) =
    (ContinuousMap.id (X × Y) : (a : X × Y) → X × Y) (x, y)

Tactic:
Prod.ext (HSpace.hmulE.1.3 x) (HSpace.hmulE.1.3 y)

Premises used: Prod.ext, ContinuousMap.HomotopyWith.toHomotopy, ContinuousMap.Homotopy.map_one_left, HSpace.hmulE
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((hmulE : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (hmulE : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
x : X
y : Y
⊢ { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (1, x, y) =
    (ContinuousMap.id (X × Y) : (a : X × Y) → X × Y) (x, y)

Tactic:
exact Prod.ext (HSpace.hmulE.1.3 x) (HSpace.hmulE.1.3 y)

Premises used: Prod.ext
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((hmulE : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (hmulE : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
t : (↑I : Type)
x : X
y : Y
h : Membership.mem (γ := Set (X × Y)) {(@e _ inst _, @e _ inst_1 _)} (x, y)
⊢ x = @e _ inst _ ∧ y = @e _ inst_1 _

Tactic:
replace h := Prod.mk_inj.mp h
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((hmulE : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (hmulE : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
t : (↑I : Type)
x : X
y : Y
h : x = @e _ inst _ ∧ y = @e _ inst_1 _
⊢ Eq (α := X × Y)
    (({
            toFun := fun (x : X × Y) ↦
              (Homotopy.toContinuousMap (f₀ :=
                    comp
                      {
                        toFun := fun (p : (X × Y) × X × Y) ↦
                          ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
                        continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
                      (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (@e _ inst _, @e _ inst_1 _))))
                    (f₁ := ContinuousMap.id (X × Y))
                    { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ :
                      Homotopy
                        (comp
                          {
                            toFun := fun (p : (X × Y) × X × Y) ↦
                              ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
                            continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
                          (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (@e _ inst _, @e _ inst_1 _))))
                        (ContinuousMap.id (X × Y)) }).toFun
                (t, x),
            continuous_toFun := ⋯ : C(X × Y, X × Y) } :
          (a : X × Y) → X × Y)
        (x, y) :
      X × Y)
    ((comp
            {
              toFun := fun (p : (X × Y) × X × Y) ↦
                ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
              continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
            (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (@e _ inst _, @e _ inst_1 _))) :
          (a : X × Y) → X × Y)
        (x, y) :
      X × Y)

Tactic:
Prod.ext (HSpace.hmulE.2 t x h.1) (HSpace.hmulE.2 t y h.2)

Premises used: ContinuousMap.HomotopyWith.prop', And.right, And.left, Prod.ext, HSpace.hmulE
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((hmulE : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (hmulE : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
t : (↑I : Type)
x : X
y : Y
h : x = @e _ inst _ ∧ y = @e _ inst_1 _
⊢ Eq (α := X × Y)
    (({
            toFun := fun (x : X × Y) ↦
              (Homotopy.toContinuousMap (f₀ :=
                    comp
                      {
                        toFun := fun (p : (X × Y) × X × Y) ↦
                          ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
                        continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
                      (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (@e _ inst _, @e _ inst_1 _))))
                    (f₁ := ContinuousMap.id (X × Y))
                    { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ :
                      Homotopy
                        (comp
                          {
                            toFun := fun (p : (X × Y) × X × Y) ↦
                              ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
                            continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
                          (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (@e _ inst _, @e _ inst_1 _))))
                        (ContinuousMap.id (X × Y)) }).toFun
                (t, x),
            continuous_toFun := ⋯ : C(X × Y, X × Y) } :
          (a : X × Y) → X × Y)
        (x, y) :
      X × Y)
    ((comp
            {
              toFun := fun (p : (X × Y) × X × Y) ↦
                ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
              continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
            (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (@e _ inst _, @e _ inst_1 _))) :
          (a : X × Y) → X × Y)
        (x, y) :
      X × Y)

Tactic:
exact Prod.ext (HSpace.hmulE.2 t x h.1) (HSpace.hmulE.2 t y h.2)

Premises used: Prod.ext
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
M : Type u
inst : MulOneClass M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
h :
  ∀ (a : M),
    Eq (α := M)
      ((comp { toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ : C(M × M, M) }
              (prodMk (const M 1) (ContinuousMap.id M)) :
            (a : M) → M)
          a :
        M)
      ((ContinuousMap.id M : (a : M) → M) a : M)
⊢ Eq (α := C(M, M))
    (comp { toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ : C(M × M, M) }
      (prodMk (const M 1) (ContinuousMap.id M)))
    (ContinuousMap.id M)

Tactic:
ext1
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
M : Type u
inst : MulOneClass M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
a : M
⊢ Eq (α := M)
    ((comp { toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ : C(M × M, M) }
            (prodMk (const M 1) (ContinuousMap.id M)) :
          (a : M) → M)
        a :
      M)
    ((ContinuousMap.id M : (a : M) → M) a : M)

Tactic:
apply one_mul

Premises used: one_mul
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
M : Type u
inst : MulOneClass M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
h :
  ∀ (a : M),
    Eq (α := M)
      ((comp { toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ : C(M × M, M) }
              (prodMk (ContinuousMap.id M) (const M 1)) :
            (a : M) → M)
          a :
        M)
      ((ContinuousMap.id M : (a : M) → M) a : M)
⊢ Eq (α := C(M, M))
    (comp { toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ : C(M × M, M) }
      (prodMk (ContinuousMap.id M) (const M 1)))
    (ContinuousMap.id M)

Tactic:
ext1
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
M : Type u
inst : MulOneClass M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
a : M
⊢ Eq (α := M)
    ((comp { toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ : C(M × M, M) }
            (prodMk (ContinuousMap.id M) (const M 1)) :
          (a : M) → M)
        a :
      M)
    ((ContinuousMap.id M : (a : M) → M) a : M)

Tactic:
apply mul_one

Premises used: mul_one
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
G : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
⊢ Eq.{u + 1} (α := G) 1 (@HSpace.e _ inst _)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
G G' : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace G'
inst_4 : Group G'
inst_5 : IsTopologicalGroup G'
⊢ Eq (α := HSpace (G × G')) (hSpace (G × G'))
    {
      hmul :=
        {
          toFun := fun (p : (G × G') × G × G') ↦
            ((HSpace.hmul : (a : G × G) → G) (p.1.1, p.2.1), (HSpace.hmul : (a : G' × G') → G') (p.1.2, p.2.2)),
          continuous_toFun := ⋯ },
      e := (@HSpace.e _ inst _, @HSpace.e _ inst_3 _), hmul_e_e := ⋯,
      eHmul :=
        HomotopyWith.mk (P := fun (f : C(G × G', G × G')) ↦
          ∀ (x : G × G'),
            Membership.mem (γ := Set (G × G')) {(@HSpace.e _ inst _, @HSpace.e _ inst_3 _)} x →
              Eq (α := G × G') ((f : (a : G × G') → G × G') x : G × G')
                ((comp
                        {
                          toFun := fun (p : (G × G') × G × G') ↦
                            ((HSpace.hmul : (a : G × G) → G) (p.1.1, p.2.1),
                              (HSpace.hmul : (a : G' × G') → G') (p.1.2, p.2.2)),
                          continuous_toFun := ⋯ : C((G × G') × G × G', G × G') }
                        (prodMk (const (G × G') (@HSpace.e _ inst _, @HSpace.e _ inst_3 _))
                          (ContinuousMap.id (G × G'))) :
                      (a : G × G') → G × G')
                    x :
                  G × G'))
          {
            toFun := fun (p : (↑I : Type) × G × G') ↦
              ((HSpace.eHmul : (a : (↑I : Type) × G) → G) (p.1, p.2.1),
                (HSpace.eHmul : (a : (↑I : Type) × G') → G') (p.1, p.2.2)),
            continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ }
          ⋯,
      hmulE :=
        HomotopyWith.mk (P := fun (f : C(G × G', G × G')) ↦
          ∀ (x : G × G'),
            Membership.mem (γ := Set (G × G')) {(@HSpace.e _ inst _, @HSpace.e _ inst_3 _)} x →
              Eq (α := G × G') ((f : (a : G × G') → G × G') x : G × G')
                ((comp
                        {
                          toFun := fun (p : (G × G') × G × G') ↦
                            ((HSpace.hmul : (a : G × G) → G) (p.1.1, p.2.1),
                              (HSpace.hmul : (a : G' × G') → G') (p.1.2, p.2.2)),
                          continuous_toFun := ⋯ : C((G × G') × G × G', G × G') }
                        (prodMk (ContinuousMap.id (G × G'))
                          (const (G × G') (@HSpace.e _ inst _, @HSpace.e _ inst_3 _))) :
                      (a : G × G') → G × G')
                    x :
                  G × G'))
          {
            toFun := fun (p : (↑I : Type) × G × G') ↦
              ((HSpace.hmulE : (a : (↑I : Type) × G) → G) (p.1, p.2.1),
                (HSpace.hmulE : (a : (↑I : Type) × G') → G') (p.1, p.2.2)),
            continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ }
          ⋯ }

Tactic:
rfl
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
⊢ Continuous (Y := ℝ) fun (p : (↑I : Type) × (↑I : Type)) ↦ 2 * (↑p.1 : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
⊢ Continuous (Y := ℝ) fun (p : (↑I : Type) × (↑I : Type)) ↦ 1 + (↑p.2 : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
θ : (↑I : Type)
⊢ HMul.hMul (α := ℝ) 2 (↑(0, θ).1 : ℝ) / (1 + (↑(0, θ).2 : ℝ)) ≤ 0

Tactic:
simp only [coe_zero, mul_zero, zero_div, le_refl]

Premises used: le_refl, Set.Icc.coe_zero, zero_div, MulZeroClass.mul_zero
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
θ : (↑I : Type)
dsimp : 1 * (1 + (↑θ : ℝ)) ≤ HMul.hMul (α := ℝ) 2 (↑1 : ℝ)
⊢ 1 * (1 + (↑(1, θ).2 : ℝ)) ≤ HMul.hMul (α := ℝ) 2 (↑(1, θ).1 : ℝ)

Tactic:
dsimp only
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
θ : (↑I : Type)
rw : (↑θ : ℝ) + 1 ≤ HAdd.hAdd (α := ℝ) 1 1
⊢ 1 * (1 + (↑θ : ℝ)) ≤ HMul.hMul (α := ℝ) 2 (↑1 : ℝ)

Tactic:
rw [coe_one, one_mul, mul_one, add_comm, ← one_add_one_eq_two]

Premises used: one_add_one_eq_two, add_comm, Set.Icc.coe_one, mul_one, one_mul
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
θ : (↑I : Type)
simp : (↑θ : ℝ) ≤ 1
⊢ (↑θ : ℝ) + 1 ≤ HAdd.hAdd (α := ℝ) 1 1

Tactic:
simp only [add_le_add_iff_right]

Premises used: add_le_add_iff_right
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
θ : (↑I : Type)
⊢ (↑θ : ℝ) ≤ 1

Tactic:
le_one _

Premises used: unitInterval.le_one
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
θ : (↑I : Type)
⊢ (↑θ : ℝ) ≤ 1

Tactic:
exact le_one _

Premises used: unitInterval.le_one
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
t : (↑I : Type)
simp : (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1
⊢ (↑(qRight (t, 0)) : ℝ) = if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1

Tactic:
simp only [qRight, coe_zero, add_zero, div_one]

Premises used: Set.Icc.coe_zero, unitInterval.qRight, add_zero, div_one
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
t : (↑I : Type)
pos : (↑t : ℝ) ≤ 1 / 2 → (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = 2 * (↑t : ℝ)
neg : ¬(↑t : ℝ) ≤ 1 / 2 → (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = 1
⊢ (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1

Tactic:
split_ifs
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
rw : (↑t : ℝ) ∈ Set.Icc 0 (1 / 2)
⊢ (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = 2 * (↑t : ℝ)

Tactic:
rw [Set.projIcc_of_mem _ ((mul_pos_mem_iff zero_lt_two).2 _)]

Premises used: Iff.mpr, Set.projIcc_of_mem, unitInterval.mul_pos_mem_iff, zero_lt_two
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
⊢ (↑t : ℝ) ∈ Set.Icc 0 (1 / 2)

Tactic:
⟨t.2.1, ?_⟩

Premises used: Set.Mem, setOf, Set.Icc, And.left, And.intro, Subtype.property
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
refine : (↑t : ℝ) ≤ 1 / 2
⊢ (↑t : ℝ) ∈ Set.Icc 0 (1 / 2)

Tactic:
refine ⟨t.2.1, ?_⟩
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
⊢ (↑t : ℝ) ≤ 1 / 2

Tactic:
tauto
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
neg : 1 ≤ 2 * (↑t : ℝ)
rw : LT.lt (α := ℝ) 0 1
⊢ (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = 1

Tactic:
rw [(Set.projIcc_eq_right _).2]

Premises used: Iff.mpr, Set.projIcc_eq_right
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 2 * (↑t : ℝ) < 1 → 2 / 2 = 1
linarith₁ : 2 * (↑t : ℝ) < 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * (↑t : ℝ) < 1 → GT.gt (α := ℝ) 2 0
linarith₃ : 2 * (↑t : ℝ) < 1 → HMul.hMul (α := ℝ) 1 1 - 2 * (↑t : ℝ) + (2 * (↑t : ℝ) - 1) = 0
⊢ 1 ≤ 2 * (↑t : ℝ)

Tactic:
linarith
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ LT.lt (α := ℝ) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ LT.lt (α := ℝ) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
t : (↑I : Type)
⊢ Set.projIcc 0 1 qRight._proof_1 (2 * (↑(t, 1).1 : ℝ) / HAdd.hAdd (α := ℝ) 1 (↑(t, 1).2 : ℝ)) =
    Set.projIcc 0 1 ⋯ (↑t : ℝ)

Tactic:
norm_num
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
θ : (↑I : Type)
γ : Path x y
⊢ Continuous.{0, u} (Y := X) fun (t : (↑I : Type)) ↦ (γ : (a : (↑I : Type)) → X) (qRight (t, θ))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
θ : (↑I : Type)
γ : Path x y
rw : (γ : (a : (↑I : Type)) → X) 0 = x
rw₁ rw₂ : x = x
⊢ (γ : (a : (↑I : Type)) → X) (qRight (0, θ)) = x

Tactic:
rw [qRight_zero_left, γ.source]

Premises used: unitInterval.qRight_zero_left, Path.source
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
θ : (↑I : Type)
γ : Path x y
rw : (γ : (a : (↑I : Type)) → X) 1 = y
rw₁ rw₂ : y = y
⊢ (γ : (a : (↑I : Type)) → X) (qRight (1, θ)) = y

Tactic:
rw [qRight_one_left, γ.target]

Premises used: unitInterval.qRight_one_left, Path.target
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
⊢ Continuous (Y := Path x y) fun (p : (↑I : Type) × Path x y) ↦ delayReflRight p.1 p.2

Tactic:
continuous_uncurry_iff.mp <|
    (continuous_snd.comp continuous_fst).eval <|
      continuous_qRight.comp <| continuous_snd.prodMk <| continuous_fst.comp continuous_fst

Premises used: Continuous.comp, continuous_snd, continuous_fst, unitInterval.continuous_qRight, Path.continuous_uncurry_iff, Iff.mp, Continuous.eval, Continuous.prodMk
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
a :
  ∀ (t : (↑I : Type)),
    Eq (α := X) ((delayReflRight 0 γ : (a : (↑I : Type)) → X) t : X) ((γ.trans (refl y) : (a : (↑I : Type)) → X) t : X)
⊢ delayReflRight 0 γ = γ.trans (refl y)

Tactic:
ext t
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
a :
  Eq (α := X) ((γ : (a : (↑I : Type)) → X) (qRight (t, 0)) : X)
    (if h : (↑t : ℝ) ≤ 1 / 2 then (γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)
      else y :
      X)
⊢ Eq (α := X) ((delayReflRight 0 γ : (a : (↑I : Type)) → X) t : X) ((γ.trans (refl y) : (a : (↑I : Type)) → X) t : X)

Tactic:
simp only [delayReflRight, trans_apply, Path.coe_mk_mk,
    refl_apply]

Premises used: Path.refl_apply, Path.delayReflRight, Path.trans_apply, Path.coe_mk_mk
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
pos :
  ∀ (h : (↑t : ℝ) ≤ 1 / 2),
    Eq (α := X) ((γ : (a : (↑I : Type)) → X) (qRight (t, 0)) : X)
      ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : X)
neg : ∀ (h : ¬(↑t : ℝ) ≤ 1 / 2), (γ : (a : (↑I : Type)) → X) (qRight (t, 0)) = y
⊢ Eq (α := X) ((γ : (a : (↑I : Type)) → X) (qRight (t, 0)) : X)
    (if h : (↑t : ℝ) ≤ 1 / 2 then (γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)
      else y :
      X)

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
rw : ((γ : (a : (↑I : Type)) → X) 1 : X)
| y

Tactic:
rw [← γ.target]

Premises used: Path.target
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
neg : Eq (α := X) ((γ : (a : (↑I : Type)) → X) (qRight (t, 0)) : X) ((γ : (a : (↑I : Type)) → X) 1 : X)
⊢ (γ : (a : (↑I : Type)) → X) (qRight (t, 0)) = y

Tactic:
conv_rhs => rw [← γ.target]

Premises used: Path.target
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
neg : Eq (α := X) ((γ : (a : (↑I : Type)) → X) (qRight (t, 0)) : X) ((γ : (a : (↑I : Type)) → X) 1 : X)
⊢ (γ : (a : (↑I : Type)) → X) (qRight (t, 0)) = y

Tactic:
on_goal 1 => conv_rhs => rw [← γ.target]

Premises used: Path.target
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
neg : qRight (t, 0) = 1
⊢ Eq (α := X) ((γ : (a : (↑I : Type)) → X) (qRight (t, 0)) : X) ((γ : (a : (↑I : Type)) → X) 1 : X)

Tactic:
apply congr_arg γ

Premises used: congr_arg, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
neg : (↑(qRight (t, 0)) : ℝ) = (↑1 : ℝ)
⊢ qRight (t, 0) = 1

Tactic:
ext1
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
neg : (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) = (↑1 : ℝ)
⊢ (↑(qRight (t, 0)) : ℝ) = (↑1 : ℝ)

Tactic:
rw [qRight_zero_right]

Premises used: unitInterval.qRight_zero_right
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
pos : qRight (t, 0) = Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯
⊢ Eq (α := X) ((γ : (a : (↑I : Type)) → X) (qRight (t, 0)) : X)
    ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : X)

Tactic:
apply congr_arg γ

Premises used: congr_arg, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
pos : (↑(qRight (t, 0)) : ℝ) = (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : ℝ)
⊢ qRight (t, 0) = Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯

Tactic:
ext1
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
pos : (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) = (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : ℝ)
⊢ (↑(qRight (t, 0)) : ℝ) = (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : ℝ)

Tactic:
rw [qRight_zero_right]

Premises used: unitInterval.qRight_zero_right