awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (hypothesis)
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)
⊢ 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)
have h₁ : x = @e _ inst _ ∧ y = @e _ inst_1 _
Tactic: replace h := Prod.mk_inj.mp h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
M : Type u
inst : MulOneClass M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul 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)
have h : ∀ (a : M),
  Eq (α := M)
    ((comp { toFun := Function.uncurry Mul.mul, continuous_toFun := sorry : 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: ext1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
M : Type u
inst : MulOneClass M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul 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)
have h : ∀ (a : M),
  Eq (α := M)
    ((comp { toFun := Function.uncurry Mul.mul, continuous_toFun := sorry : 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: ext1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
θ : (↑I : Type)
⊢ 1 * (1 + (↑(1, θ).2 : ℝ)) ≤ HMul.hMul (α := ℝ) 2 (↑(1, θ).1 : ℝ)
have dsimp : 1 * (1 + (↑θ : ℝ)) ≤ HMul.hMul (α := ℝ) 2 (↑1 : ℝ)
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
θ : (↑I : Type)
⊢ 1 * (1 + (↑θ : ℝ)) ≤ HMul.hMul (α := ℝ) 2 (↑1 : ℝ)
have rw : (↑θ : ℝ) + 1 ≤ HAdd.hAdd (α := ℝ) 1 1
Tactic: rw [coe_one, one_mul, mul_one, add_comm, ← one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
θ : (↑I : Type)
⊢ (↑θ : ℝ) + 1 ≤ HAdd.hAdd (α := ℝ) 1 1
have simp : (↑θ : ℝ) ≤ 1
Tactic: simp only [add_le_add_iff_right]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
t : (↑I : Type)
⊢ (↑(qRight (t, 0)) : ℝ) = if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1
have simp : (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1
Tactic: simp only [qRight, coe_zero, add_zero, div_one]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
t : (↑I : Type)
⊢ (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1
have pos : (↑t : ℝ) ≤ 1 / 2 → (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = 2 * (↑t : ℝ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
t : (↑I : Type)
pos : (↑t : ℝ) ≤ 1 / 2 → (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = 2 * (↑t : ℝ)
⊢ (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1
have neg : ¬(↑t : ℝ) ≤ 1 / 2 → (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
⊢ (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = 2 * (↑t : ℝ)
have rw : (↑t : ℝ) ∈ Set.Icc 0 (1 / 2)
Tactic: rw [Set.projIcc_of_mem _ ((mul_pos_mem_iff zero_lt_two).2 _)]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = 1
have neg : 1 ≤ 2 * (↑t : ℝ)
Tactic: rw [(Set.projIcc_eq_right _).2]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
neg : 1 ≤ 2 * (↑t : ℝ)
⊢ (↑(Set.projIcc 0 1 qRight._proof_1 (2 * (↑t : ℝ))) : ℝ) = 1
have rw : LT.lt (α := ℝ) 0 1
Tactic: rw [(Set.projIcc_eq_right _).2]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ 1 ≤ 2 * (↑t : ℝ)
have linarith : 2 * (↑t : ℝ) < 1 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 2 * (↑t : ℝ) < 1 → 2 / 2 = 1
⊢ 1 ≤ 2 * (↑t : ℝ)
have linarith₁ : 2 * (↑t : ℝ) < 1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 2 * (↑t : ℝ) < 1 → 2 / 2 = 1
linarith₁ : 2 * (↑t : ℝ) < 1 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 ≤ 2 * (↑t : ℝ)
have linarith₂ : 2 * (↑t : ℝ) < 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
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
⊢ 1 ≤ 2 * (↑t : ℝ)
have linarith₃ : 2 * (↑t : ℝ) < 1 → HMul.hMul (α := ℝ) 1 1 - 2 * (↑t : ℝ) + (2 * (↑t : ℝ) - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
θ : (↑I : Type)
γ : Path x y
⊢ (γ : (a : (↑I : Type)) → X) (qRight (0, θ)) = x
have rw : (γ : (a : (↑I : Type)) → X) 0 = x
Tactic: rw [qRight_zero_left, γ.source]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
θ : (↑I : Type)
γ : Path x y
rw : (γ : (a : (↑I : Type)) → X) 0 = x
⊢ (γ : (a : (↑I : Type)) → X) (qRight (0, θ)) = x
have rw₁ : x = x
Tactic: rw [qRight_zero_left, γ.source]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
θ : (↑I : Type)
γ : Path x y
⊢ (γ : (a : (↑I : Type)) → X) (qRight (1, θ)) = y
have rw : (γ : (a : (↑I : Type)) → X) 1 = y
Tactic: rw [qRight_one_left, γ.target]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
θ : (↑I : Type)
γ : Path x y
rw : (γ : (a : (↑I : Type)) → X) 1 = y
⊢ (γ : (a : (↑I : Type)) → X) (qRight (1, θ)) = y
have rw₁ : y = y
Tactic: rw [qRight_one_left, γ.target]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflRight 0 γ = γ.trans (refl y)
have a : ∀ (t : (↑I : Type)),
  Eq (α := X) ((delayReflRight 0 γ : (a : (↑I : Type)) → X) t : X) ((γ.trans (refl y) : (a : (↑I : Type)) → X) t : X)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
⊢ Eq (α := X) ((delayReflRight 0 γ : (a : (↑I : Type)) → X) t : X) ((γ.trans (refl y) : (a : (↑I : Type)) → X) t : X)
have 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 : ℝ)) sorry)
    else y :
    X)
Tactic: simp only [delayReflRight, trans_apply, Path.coe_mk_mk,
    refl_apply]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
⊢ 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)
have 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 : ℝ)) sorry) : X)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
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)
⊢ 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)
have neg : ∀ (h : ¬(↑t : ℝ) ≤ 1 / 2), (γ : (a : (↑I : Type)) → X) (qRight (t, 0)) = y
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
| y
have rw : ((γ : (a : (↑I : Type)) → X) 1 : X)
Tactic: rw [← γ.target]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ (γ : (a : (↑I : Type)) → X) (qRight (t, 0)) = y
have neg : Eq (α := X) ((γ : (a : (↑I : Type)) → X) (qRight (t, 0)) : X) ((γ : (a : (↑I : Type)) → X) 1 : X)
Tactic: conv_rhs => rw [← γ.target]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ (γ : (a : (↑I : Type)) → X) (qRight (t, 0)) = y
have neg : Eq (α := X) ((γ : (a : (↑I : Type)) → X) (qRight (t, 0)) : X) ((γ : (a : (↑I : Type)) → X) 1 : X)
Tactic: on_goal 1 => conv_rhs => rw [← γ.target]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ Eq (α := X) ((γ : (a : (↑I : Type)) → X) (qRight (t, 0)) : X) ((γ : (a : (↑I : Type)) → X) 1 : X)
have neg : qRight (t, 0) = 1
Tactic: apply congr_arg γ
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ qRight (t, 0) = 1
have neg : (↑(qRight (t, 0)) : ℝ) = (↑1 : ℝ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ (↑(qRight (t, 0)) : ℝ) = (↑1 : ℝ)
have neg : (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) = (↑1 : ℝ)
Tactic: rw [qRight_zero_right]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
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)
have pos : qRight (t, 0) = Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry
Tactic: apply congr_arg γ
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
⊢ qRight (t, 0) = Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯
have pos : (↑(qRight (t, 0)) : ℝ) = (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry) : ℝ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
⊢ (↑(qRight (t, 0)) : ℝ) = (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : ℝ)
have pos : (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) = (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry) : ℝ)
Tactic: rw [qRight_zero_right]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflRight 1 γ = γ
have a : ∀ (t : (↑I : Type)),
  Eq (α := X) ((delayReflRight 1 γ : (a : (↑I : Type)) → X) t : X) ((γ : (a : (↑I : Type)) → X) t : X)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
H : (t₀ = 0 ∨ t₀ = 1) ∨ Membership.mem (γ := Set ({ j : N // j ≠ i } → (↑I : Type))) (boundary { j : N // j ≠ i }) t
⊢ Membership.mem (α := N → (↑I : Type)) (boundary N)
    ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) : N → (↑I : Type))
have inl : ∀ (H : t₀ = 0 ∨ t₀ = 1),
  Membership.mem (α := N → (↑I : Type)) (boundary N)
    ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) : N → (↑I : Type))
Tactic: obtain H | ⟨j, H⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
H : (t₀ = 0 ∨ t₀ = 1) ∨ Membership.mem (γ := Set ({ j : N // j ≠ i } → (↑I : Type))) (boundary { j : N // j ≠ i }) t
inl :
  ∀ (H : t₀ = 0 ∨ t₀ = 1),
    Membership.mem (α := N → (↑I : Type)) (boundary N)
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) :
        N → (↑I : Type))
⊢ Membership.mem (α := N → (↑I : Type)) (boundary N)
    ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) : N → (↑I : Type))
have inr : ∀ (j : { j : N // j ≠ i }) (H : t j = 0 ∨ t j = 1),
  Membership.mem (α := N → (↑I : Type)) (boundary N)
    ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) : N → (↑I : Type))
Tactic: obtain H | ⟨j, H⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
H : t₀ = 0 ∨ t₀ = 1
⊢ Membership.mem (α := N → (↑I : Type)) (boundary N)
    ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) : N → (↑I : Type))
have h : Eq (α := (↑I : Type))
    ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) i) 0 ∨
  Eq (α := (↑I : Type))
    ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) i) 1
Tactic: use i
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
H : t₀ = 0 ∨ t₀ = 1
⊢ Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) i) 0 ∨
    Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) i) 1
have h : Eq (α := (↑I : Type)) (if h : i = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) i sorry)) 0 ∨
  Eq (α := (↑I : Type)) (if h : i = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) i sorry)) 1
Tactic: rwa [funSplitAt_symm_apply, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
H : t₀ = 0 ∨ t₀ = 1
h :
  Eq (α := (↑I : Type)) (if h : i = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) i ⋯)) 0 ∨
    Eq (α := (↑I : Type)) (if h : i = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) i ⋯)) 1
⊢ Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) i) 0 ∨
    Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) i) 1
have h₁ : (t₀, t).1 = 0 ∨ (t₀, t).1 = 1
Tactic: rwa [funSplitAt_symm_apply, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
j : { j : N // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ Membership.mem (α := N → (↑I : Type)) (boundary N)
    ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) : N → (↑I : Type))
have h : Eq (α := (↑I : Type))
    ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) (↑j : N)) 0 ∨
  Eq (α := (↑I : Type))
    ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) (↑j : N)) 1
Tactic: use j
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
j : { j : N // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) (↑j : N)) 0 ∨
    Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) (↑j : N)) 1
have h : Eq (α := (↑I : Type))
    (if h : (↑j : N) = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) sorry)) 0 ∨
  Eq (α := (↑I : Type))
    (if h : (↑j : N) = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) sorry)) 1
Tactic: rwa [funSplitAt_symm_apply, dif_neg j.prop, Subtype.coe_eta]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
j : { j : N // j ≠ i }
H : t j = 0 ∨ t j = 1
h :
  Eq (α := (↑I : Type))
      (if h : (↑j : N) = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) ⋯)) 0 ∨
    Eq (α := (↑I : Type))
      (if h : (↑j : N) = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) ⋯)) 1
⊢ Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) (↑j : N)) 0 ∨
    Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) (↑j : N)) 1
have h₁ : (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) sorry) = 0 ∨
  (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) sorry) = 1
Tactic: rwa [funSplitAt_symm_apply, dif_neg j.prop, Subtype.coe_eta]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
j : { j : N // j ≠ i }
H : t j = 0 ∨ t j = 1
h :
  Eq (α := (↑I : Type))
      (if h : (↑j : N) = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) ⋯)) 0 ∨
    Eq (α := (↑I : Type))
      (if h : (↑j : N) = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) ⋯)) 1
h₁ :
  (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) ⋯) = 0 ∨
    (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) ⋯) = 1
⊢ Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) (↑j : N)) 0 ∨
    Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) (↑j : N)) 1
have h₂ : (t₀, t).2 j = 0 ∨ (t₀, t).2 j = 1
Tactic: rwa [funSplitAt_symm_apply, dif_neg j.prop, Subtype.coe_eta]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
f : (↑(Ω^ N X x) : Type (max u_1 u_2))
g : (N → (↑I : Type)) → X
h : g = (⇑f : (a : N → (↑I : Type)) → X)
⊢ copy f g h = f
have H : ∀ (x_1 : N → (↑I : Type)),
  Eq.{u_2 + 1} (α := X) ((copy f g h : (a : N → (↑I : Type)) → X) x_1 : X) ((f : (a : N → (↑I : Type)) → X) x_1 : X)
Tactic: ext x