awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hw : MDiffAt f w
pos :
  Eq (α := TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((ContinuousLinearMap.comp (M₂ :=
            TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y ⋯ (↑w : ℝ)))
            (mfderiv% f (projIcc x y ⋯ (↑w : ℝ))) (mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) (↑w : ℝ)) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
        1 :
      TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
pos₁ : MDiffAt f (projIcc x y ⋯ (↑w : ℝ))
pos₂ : MDiffAt[Icc x y] (projIcc x y ⋯) (↑w : ℝ)
⊢ Eq (α := TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) I (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
        1 :
      TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
have pos₃ : UniqueMDiffWithinAt 𝓘(ℝ, ℝ) (Icc x y) (↑w : ℝ)
Tactic: rw [mfderiv_comp_mfderivWithin (I' := 𝓡∂ 1)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hw : MDiffAt f w
⊢ w = projIcc x y ⋯ (↑w : ℝ)
have rw : w = Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) sorry
Tactic: rw [projIcc_of_mem]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hw : MDiffAt f w
rw : w = Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) ⋯
⊢ w = projIcc x y ⋯ (↑w : ℝ)
have hx : (↑w : ℝ) ∈ Icc x y
Tactic: rw [projIcc_of_mem]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hw : MDiffAt f w
⊢ Eq (α := TangentSpace I (f (projIcc x y ⋯ (↑w : ℝ))))
    ((mfderiv% f (projIcc x y ⋯ (↑w : ℝ)) :
          (a : TangentSpace (𝓡∂ 1) (projIcc x y ⋯ (↑w : ℝ))) → TangentSpace I (f (projIcc x y ⋯ (↑w : ℝ))))
        ((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
            (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace (𝓡∂ 1) (projIcc x y ⋯ (↑w : ℝ)))
          1) :
      TangentSpace I (f (projIcc x y ⋯ (↑w : ℝ))))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
have this : w = projIcc x y sorry (↑w : ℝ)
Tactic: have : w = projIcc x y h.out.le (w : ℝ) := by rw [projIcc_of_mem]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hw : MDiffAt f w
this : w = projIcc x y ⋯ (↑w : ℝ)
⊢ Eq (α := TangentSpace I (f (projIcc x y ⋯ (↑w : ℝ))))
    ((mfderiv% f (projIcc x y ⋯ (↑w : ℝ)) :
          (a : TangentSpace (𝓡∂ 1) (projIcc x y ⋯ (↑w : ℝ))) → TangentSpace I (f (projIcc x y ⋯ (↑w : ℝ))))
        ((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
            (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace (𝓡∂ 1) (projIcc x y ⋯ (↑w : ℝ)))
          1) :
      TangentSpace I (f (projIcc x y ⋯ (↑w : ℝ))))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
have pos : Eq (α := TangentSpace I (f (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) sorry)))
  ((mfderiv% f (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) sorry) :
        (a : TangentSpace (𝓡∂ 1) ⟨(↑w : ℝ), sorry⟩) → TangentSpace I (f ⟨(↑w : ℝ), sorry⟩))
      (((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y sorry) (Icc x y) (↑w : ℝ) :
            TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ) →L[ℝ]
              TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1)
                (projIcc x y sorry (↑w : ℝ))) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace (𝓡∂ 1) ⟨(↑w : ℝ), sorry⟩)
        1) :
    TangentSpace I (f (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) sorry)))
  ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
Tactic: rw [projIcc_of_mem _ w.2]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hw : MDiffAt f w
this : w = projIcc x y ⋯ (↑w : ℝ)
⊢ Eq (α := TangentSpace I (f (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) ⋯)))
    ((mfderiv% f (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) ⋯) :
          (a : TangentSpace (𝓡∂ 1) ⟨(↑w : ℝ), ⋯⟩) → TangentSpace I (f ⟨(↑w : ℝ), ⋯⟩))
        (((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
              TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ) →L[ℝ]
                TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1)
                  (projIcc x y ⋯ (↑w : ℝ))) :
            (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace (𝓡∂ 1) ⟨(↑w : ℝ), ⋯⟩)
          1) :
      TangentSpace I (f (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) ⋯)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
have pos : Eq (α :=
  TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1)
    (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) sorry))
  (((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y sorry) (Icc x y) (↑w : ℝ) :
        TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ) →L[ℝ]
          TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y sorry (↑w : ℝ))) :
      (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace (𝓡∂ 1) ⟨(↑w : ℝ), sorry⟩)
    1)
  1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (↑z : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (Icc x y)
          (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val ∘ projIcc x y ⋯) (↑z : ℝ)))
      1)
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
      1)
have e_a : Eq (α :=
  TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ) →L[ℝ]
    TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y sorry) (↑z : ℝ)))
  (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y sorry) (Icc x y) (↑z : ℝ))
  (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
⊢ Eq (α :=
    TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ) →L[ℝ]
      TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (↑z : ℝ)))
    (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (Icc x y)
      (↑z : ℝ))
    (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ))
have apply : ∀ x_1 ∈ Icc x y, (Subtype.val (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y) ∘ projIcc x y sorry) x_1 = id x_1
Tactic: apply mfderivWithin_congr_of_mem _ z.2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
    ((mfderiv% (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)) z :
        (a : TangentSpace (𝓡∂ 1) z) → TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
      1)
    1
have A : Eq (α := TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y sorry) (↑z : ℝ)))
  ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y sorry) (Icc x y)
        (↑z : ℝ) :
      (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val ∘ projIcc x y sorry) (↑z : ℝ)))
    1)
  ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
      (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
    1)
Tactic: have A : mfderiv[Icc x y] (Subtype.val ∘ (projIcc x y h.out.le)) z 1
      = mfderiv[Icc x y] (@id ℝ) z 1 := by
    congr 1
    apply mfderivWithin_congr_of_mem _ z.2
    intro z hz
    simp [projIcc_of_mem h.out.le hz]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
A :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (↑z : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (Icc x y)
          (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val ∘ projIcc x y ⋯) (↑z : ℝ)))
      1)
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
      1)
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
    ((mfderiv% (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)) z :
        (a : TangentSpace (𝓡∂ 1) z) → TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
      1)
    1
have rw : Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
  ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
      (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
    1)
  1
Tactic: rw [← mfderivWithin_comp_projIcc_one, A]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
A :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (↑z : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (Icc x y)
          (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val ∘ projIcc x y ⋯) (↑z : ℝ)))
      1)
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
      1)
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
      1)
    1
have simp : Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
  ((fderivWithin ℝ id (Icc x y) (↑z : ℝ) : (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) 1) 1
Tactic: simp only [id_eq, mfderivWithin_eq_fderivWithin]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
A :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (↑z : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (Icc x y)
          (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val ∘ projIcc x y ⋯) (↑z : ℝ)))
      1)
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
      1)
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
    ((fderivWithin ℝ id (Icc x y) (↑z : ℝ) : (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) 1) 1
have rw : Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
  ((ContinuousLinearMap.id ℝ ℝ : (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) 1) 1
Tactic: rw [fderivWithin_id (uniqueDiffOn_Icc h.out _ z.2)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
inst : NeZero n
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | 0 ≤ x.ofLp 0} x
x_1 : EuclideanSpace ℝ (Fin n)
hy : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | 0 ≤ x.ofLp 0} x_1
x_2 x_3 : ℝ
h : 0 ≤ x_2
h_1 : 0 ≤ x_3
h_2 : x_2 + x_3 = 1
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | 0 ≤ x.ofLp 0}
    (x_2 • x + x_3 • x_1)
have dsimp : 0 ≤ x_2 * x.ofLp 0 + x_3 * x_1.ofLp 0
Tactic: dsimp at hx hy ⊢
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x.ofLp i} x
x_1 : EuclideanSpace ℝ (Fin n)
hy :
  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x.ofLp i} x_1
x_2 x_3 : ℝ
h : 0 ≤ x_2
h_1 : 0 ≤ x_3
h_2 : x_2 + x_3 = 1
i : Fin n
⊢ 0 ≤ (x_2 • x + x_3 • x_1).ofLp i
have dsimp : 0 ≤ x_2 * x.ofLp i + x_3 * x_1.ofLp i
Tactic: dsimp at hx hy ⊢
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : ∀ (i : Fin n), 0 ≤ x.ofLp i
x_1 : EuclideanSpace ℝ (Fin n)
hy : ∀ (i : Fin n), 0 ≤ x_1.ofLp i
x_2 x_3 : ℝ
h : 0 ≤ x_2
h_1 : 0 ≤ x_3
h_2 : x_2 + x_3 = 1
i : Fin n
⊢ 0 ≤ x_2 * x.ofLp i + x_3 * x_1.ofLp i
have hx₁ : 0 ≤ x.ofLp i
Tactic: specialize hx i
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
n : ℕ
x x_1 : EuclideanSpace ℝ (Fin n)
hy : ∀ (i : Fin n), 0 ≤ x_1.ofLp i
x_2 x_3 : ℝ
h : 0 ≤ x_2
h_1 : 0 ≤ x_3
h_2 : x_2 + x_3 = 1
i : Fin n
hx : 0 ≤ x.ofLp i
⊢ 0 ≤ x_2 * x.ofLp i + x_3 * x_1.ofLp i
have hy₁ : 0 ≤ x_1.ofLp i
Tactic: specialize hy i
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (interior {y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | a < y.ofLp i}
have change : interior (f ⁻¹' Ici a) = f ⁻¹' Ioi a
Tactic: change interior (f ⁻¹' Ici a) = f ⁻¹' Ioi a
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
⊢ interior (f ⁻¹' Ici a) = f ⁻¹' Ioi a
have hf₂ : Continuous (Y := ℝ) fun (f : PiLp p fun (x : Fin n) ↦ ℝ) ↦ f.ofLp i
Tactic: rw [← (PiLp.isOpenMap_apply p _ i).preimage_interior_eq_interior_preimage, interior_Ici]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (closure {y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i}
have change : closure (f ⁻¹' Ici a) = f ⁻¹' Ici a
Tactic: change closure (f ⁻¹' Ici a) = f ⁻¹' Ici a
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
⊢ closure (f ⁻¹' Ici a) = f ⁻¹' Ici a
have hfc : Continuous (Y := ℝ) fun (f : PiLp p fun (x : Fin n) ↦ ℝ) ↦ f.ofLp i
Tactic: rw [← (PiLp.isOpenMap_apply p _ i).preimage_closure_eq_closure_preimage, closure_Ici]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (closure {y : PiLp p fun (x : Fin n) ↦ ℝ | a < y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i}
have change : closure (f ⁻¹' Ioi a) = f ⁻¹' Ici a
Tactic: change closure (f ⁻¹' Ioi a) = f ⁻¹' Ici a
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
⊢ closure (f ⁻¹' Ioi a) = f ⁻¹' Ici a
have hfc : Continuous (Y := ℝ) fun (f : PiLp p fun (x : Fin n) ↦ ℝ) ↦ f.ofLp i
Tactic: rw [← (PiLp.isOpenMap_apply p _ i).preimage_closure_eq_closure_preimage, closure_Ioi]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (frontier {y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | a = y.ofLp i}
have rw : Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ))
  ({y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i} \ {y : PiLp p fun (x : Fin n) ↦ ℝ | a < y.ofLp i})
  {y : PiLp p fun (x : Fin n) ↦ ℝ | a = y.ofLp i}
Tactic: rw [frontier, closure_halfSpace, interior_halfSpace]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ))
    ({y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i} \ {y : PiLp p fun (x : Fin n) ↦ ℝ | a < y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | a = y.ofLp i}
have h : ∀ (y : PiLp p fun (x : Fin n) ↦ ℝ),
  Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ))
      ({y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i} \ {y : PiLp p fun (x : Fin n) ↦ ℝ | a < y.ofLp i}) y ↔
    Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | a = y.ofLp i} y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
have h : ∀ (x : PiLp p fun (x : Fin n) ↦ ℝ),
  Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
      x ↔
    Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (⋂ (i : Fin n), f i ⁻¹' Ici a) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
x : PiLp p fun (x : Fin n) ↦ ℝ
⊢ Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
      x ↔
    Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (⋂ (i : Fin n), f i ⁻¹' Ici a) x
have h : (∀ (i : Fin n), a ≤ x.ofLp i) ↔ ∀ (i : Fin n), a ≤ f i x
Tactic: simp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (interior {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
have h : Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
  (⋂ (i : Fin n), f i ⁻¹' Ici a)
Tactic: have h : { y : PiLp p (fun _ : Fin n ↦ ℝ) | ∀ i : Fin n, a ≤ y i } = ⋂ i, (f i) ⁻¹' Ici a := by
    ext; simp; rfl
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ioi a)
have h₁ : ∀ (x : PiLp p fun (x : Fin n) ↦ ℝ),
  Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
      x ↔
    Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (⋂ (i : Fin n), f i ⁻¹' Ioi a) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
x : PiLp p fun (x : Fin n) ↦ ℝ
⊢ Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
      x ↔
    Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (⋂ (i : Fin n), f i ⁻¹' Ioi a) x
have h₁ : (∀ (i : Fin n), a < x.ofLp i) ↔ ∀ (i : Fin n), a < f i x
Tactic: simp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (interior {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
have h' : Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
  (⋂ (i : Fin n), f i ⁻¹' Ioi a)
Tactic: have h' : { y : PiLp p (fun _ : Fin n ↦ ℝ) | ∀ i : Fin n, a < y i } = ⋂ i, (f i) ⁻¹' Ioi a := by
    ext; simp; rfl
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
h' :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ioi a)
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (interior {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
have rw : Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (⋂ (i : Fin n), interior (f i ⁻¹' Ici a)) (⋂ (i : Fin n), f i ⁻¹' Ioi a)
Tactic: rw [h, h', interior_iInter_of_finite]