awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
W : Type u_3
Q : Type u_4
inst : NormedAddCommGroup W
inst_1 : MetricSpace Q
inst_2 : NormedAddTorsor W Q
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 W
p₁ p₂ : Q
h : p₁ ≠ p₂
c₁ c₂ : 𝕜
rw : dist c₁ c₂ ≤ (↑(nndist p₁ p₂)⁻¹ : ℝ) * (dist c₁ c₂ * dist p₁ p₂)
rw₁ : dist c₁ c₂ ≤ (↑(nndist p₁ p₂) : ℝ)⁻¹ * (dist c₁ c₂ * dist p₁ p₂)
rw₂ : dist c₁ c₂ ≤ (dist p₁ p₂)⁻¹ * (dist c₁ c₂ * dist p₁ p₂)
rw₃ : dist c₁ c₂ ≤ dist c₁ c₂ * ((dist p₁ p₂)⁻¹ * dist p₁ p₂)
rw₄ : dist c₁ c₂ ≤ dist c₁ c₂ * 1
rw₅ rw₆ : dist c₁ c₂ ≤ dist c₁ c₂
⊢ dist c₁ c₂ ≤
    (↑(nndist p₁ p₂)⁻¹ : ℝ) *
      dist.{u_4} (α := Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₁ : Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₂ : Q)

Tactic:
rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm,
      inv_mul_cancel₀ (dist_ne_zero.2 h), mul_one]

Premises used: Iff.mpr, dist_ne_zero, dist_nndist, mul_left_comm, NNReal.coe_inv, mul_one, inv_mul_cancel₀, dist_lineMap_lineMap
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
p₁ p₂ p₃ p₄ : V
⊢ dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2

Tactic:
simpa using dist_midpoint_midpoint_le' (𝕜 := ℝ) p₁ p₂ p₃ p₄

Premises used: dist_midpoint_midpoint_le'
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
p₁ p₂ p₃ p₄ : V
⊢ nndist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (nndist p₁ p₃ + nndist p₂ p₄) / 2

Tactic:
dist_midpoint_midpoint_le _ _ _ _

Premises used: dist_midpoint_midpoint_le, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
V : Type u_1
P : Type u_2
W : Type u_3
Q : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
inst_3 : NormedAddCommGroup W
inst_4 : MetricSpace Q
inst_5 : NormedAddTorsor W Q
inst_6 : NormedSpace ℝ V
inst_7 : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : P := Classical.arbitrary P
⊢ Eq.{u_3 + 1} (α := W)
    (Function.comp.{u_1 + 1, u_4 + 1, u_3 + 1} (α := V)
      (⇑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) : (a : Q) → W)
      (f ∘ (⇑(AffineEquiv.vaddConst ℝ c) : (a : V) → P)) 0)
    0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
V : Type u_1
P : Type u_2
W : Type u_3
Q : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
inst_3 : NormedAddCommGroup W
inst_4 : MetricSpace Q
inst_5 : NormedAddTorsor W Q
inst_6 : NormedSpace ℝ V
inst_7 : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : P := Classical.arbitrary P
x y : V
⊢ Eq (α := W)
    (((⇑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) : (a : Q) → W) ∘
        f ∘ (⇑(AffineEquiv.vaddConst ℝ c) : (a : V) → P))
      (midpoint ℝ x y))
    (midpoint ℝ
      (((⇑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) : (a : Q) → W) ∘
          f ∘ (⇑(AffineEquiv.vaddConst ℝ c) : (a : V) → P))
        x)
      (((⇑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) : (a : Q) → W) ∘
          f ∘ (⇑(AffineEquiv.vaddConst ℝ c) : (a : V) → P))
        y))

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
V : Type u_1
P : Type u_2
W : Type u_3
Q : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
inst_3 : NormedAddCommGroup W
inst_4 : MetricSpace Q
inst_5 : NormedAddTorsor W Q
inst_6 : NormedSpace ℝ V
inst_7 : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : P := Classical.arbitrary P
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(AddMonoidHom.ofMapMidpoint ℝ ℝ
          ((⇑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) : (a : Q) → W) ∘
            f ∘ (⇑(AffineEquiv.vaddConst ℝ c) : (a : V) → P))
          ⋯ ⋯) :
      (a : V) → W)

Tactic:
apply_rules [Continuous.vadd, Continuous.vsub, continuous_const, hfc.comp, continuous_id]

Premises used: Continuous.comp, continuous_const, Continuous.vsub, continuous_id, Continuous.vadd
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
V : Type u_1
P : Type u_2
W : Type u_3
Q : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
inst_3 : NormedAddCommGroup W
inst_4 : MetricSpace Q
inst_5 : NormedAddTorsor W Q
inst_6 : NormedSpace ℝ V
inst_7 : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : P := Classical.arbitrary P
p : P
⊢ f p =
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := W)
      (((↑(AddMonoidHom.toRealLinearMap
                  (AddMonoidHom.ofMapMidpoint ℝ ℝ
                    ((⇑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) : (a : Q) → W) ∘
                      f ∘ (⇑(AffineEquiv.vaddConst ℝ c) : (a : V) → P))
                    ⋯ ⋯)
                  ⋯) :
              V →ₗ[ℝ] W) :
            (a : V) → W)
          (p -ᵥ c) :
        W)
      (f c)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
P : Type u_3
inst_4 : PseudoMetricSpace P
inst_5 : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
x : E
⊢ HSMul.hSMul (β := P → E) k⁻¹ (fun (x : P) ↦ x -ᵥ c) ((fun (x : E) ↦ k • x +ᵥ c) x) = x

Tactic:
simp [inv_smul_smul₀ hk]

Premises used: inv_smul_smul₀
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
P : Type u_3
inst_4 : PseudoMetricSpace P
inst_5 : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
p : P
⊢ (fun (x : E) ↦ k • x +ᵥ c) (HSMul.hSMul (β := P → E) k⁻¹ (fun (x : P) ↦ x -ᵥ c) p) = p

Tactic:
simp [smul_inv_smul₀ hk]

Premises used: smul_inv_smul₀
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
P : Type u_3
inst_4 : PseudoMetricSpace P
inst_5 : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
x y : E
rw : edist (k • x) (k • y) = (↑‖k‖₊ : ENNReal) * edist x y
⊢ edist (k • x +ᵥ c) (k • y +ᵥ c) = (↑‖k‖₊ : ENNReal) * edist x y

Tactic:
rw [show edist (k • x +ᵥ c) (k • y +ᵥ c) = _ from (IsometryEquiv.vaddConst c).isometry ..]

Premises used: IsometryEquiv.vaddConst, HSMul.hSMul, IsometryEquiv.isometry
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
P : Type u_3
inst_4 : PseudoMetricSpace P
inst_5 : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
x y : E
⊢ edist (k • x) (k • y) = (↑‖k‖₊ : ENNReal) * edist x y

Tactic:
edist_smul₀ ..

Premises used: edist_smul₀
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
P : Type u_3
inst_4 : PseudoMetricSpace P
inst_5 : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
x y : E
⊢ edist (k • x) (k • y) = (↑‖k‖₊ : ENNReal) * edist x y

Tactic:
exact edist_smul₀ ..

Premises used: edist_smul₀
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
P : Type u_3
inst_4 : PseudoMetricSpace P
inst_5 : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
x y : E
h : dist x y ≠ 0
⊢ dist.{u_3} (α := P) ((smulTorsor c hk : (a : E) → P) x : P) ((smulTorsor c hk : (a : E) → P) y : P) =
    (↑‖k‖₊ : ℝ) * dist x y

Tactic:
simp [dist_eq_norm, ← smul_sub, norm_smul]

Premises used: dist_eq_norm, norm_smul, smul_sub
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
P : Type u_3
inst_4 : PseudoMetricSpace P
inst_5 : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
⊢ Eq.{u_2 + 1} (α := Set E) ((⇑(smulTorsor c hk) : (a : E) → P) ⁻¹' Metric.ball c ‖k‖) (Metric.ball 0 1)

Tactic:
aesop (add simp norm_smul)

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
P : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor E P
inst_6 : Nontrivial ι
b : AffineBasis ι 𝕜 P
i : ι
⊢ IsOpenMap.{u_4, u_2} (X := P) (Y := 𝕜) (⇑(b.coord i) : (a : P) → 𝕜)

Tactic:
AffineMap.isOpenMap_linear_iff.mp <|
    (b.coord i).linear.isOpenMap_of_finiteDimensional <|
      (b.coord i).linear_surjective_iff.mpr (b.surjective_coord i)

Premises used: Iff.mpr, AffineBasis.coord, AffineMap.linear_surjective_iff, AffineMap.isOpenMap_linear_iff, AffineBasis.surjective_coord, AffineMap.linear, Iff.mp, LinearMap.isOpenMap_of_finiteDimensional
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
P : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor E P
inst_6 : FiniteDimensional 𝕜 E
b : AffineBasis ι 𝕜 P
i : ι
⊢ Continuous.{u_4, u_2} (X := P) (Y := 𝕜) (⇑(b.coord i) : (a : P) → 𝕜)

Tactic:
(b.coord i).continuous_of_finiteDimensional

Premises used: AffineBasis.coord, AffineMap.continuous_of_finiteDimensional
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
inl :
  Subsingleton ι →
    Eq.{u_2 + 1} (α := Set E)
      (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
      {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}
inr :
  Nontrivial ι →
    Eq.{u_2 + 1} (α := Set E)
      (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
      {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}
⊢ Eq.{u_2 + 1} (α := Set E)
    (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}

Tactic:
cases subsingleton_or_nontrivial ι

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h : Subsingleton ι
⊢ Eq.{u_2 + 1} (α := Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)) univ

Tactic:
have : range b = univ :=
      AffineSubspace.eq_univ_of_subsingleton_span_eq_top (subsingleton_range _) b.tot
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h : Subsingleton ι
this : Eq.{u_2 + 1} (α := Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)) univ
⊢ Eq.{u_2 + 1} (α := Set E)
    (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h : Nontrivial ι
⊢ FiniteDimensional ℝ E

Tactic:
haveI : FiniteDimensional ℝ E := b.finiteDimensional
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h : Nontrivial ι
this : FiniteDimensional ℝ E
rw :
  Eq.{u_2 + 1} (α := Set E) (⋂ (i : ι), {x : E | LE.le (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)})
    (⋂ (i : ι), preimage (β := ℝ) (⇑(b.coord i) : (a : E) → ℝ) (Ici 0))
⊢ Eq.{u_2 + 1} (α := Set E)
    ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)) : Set E)
    (⋂ (i : ι), preimage (β := ℝ) (⇑(b.coord i) : (a : E) → ℝ) (Ici 0) : Set E)

Tactic:
rw [b.convexHull_eq_nonneg_coord, setOf_forall]

Premises used: AffineBasis.convexHull_eq_nonneg_coord, Set.setOf_forall
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ Eq.{u_2 + 1} (α := Set E) (⋂ (i : ι), {x : E | LE.le (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)})
    (⋂ (i : ι), preimage (β := ℝ) (⇑(b.coord i) : (a : E) → ℝ) (Ici 0))

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ Eq.{u_2 + 1} (α := Set E)
    ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)) : Set E)
    (⋂ (i : ι), preimage (β := ℝ) (⇑(b.coord i) : (a : E) → ℝ) (Ici 0) : Set E)

Tactic:
have : convexHull ℝ (range b) = ⋂ i, b.coord i ⁻¹' Ici 0 := by
      rw [b.convexHull_eq_nonneg_coord, setOf_forall]; rfl
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h : Nontrivial ι
this_1 : FiniteDimensional ℝ E
this :
  Eq.{u_2 + 1} (α := Set E)
    ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)) : Set E)
    (⋂ (i : ι), preimage (β := ℝ) (⇑(b.coord i) : (a : E) → ℝ) (Ici 0) : Set E)
inr :
  ∀ (x : E),
    Membership.mem (γ := Set E)
        (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) x ↔
      Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)} x
⊢ Eq.{u_2 + 1} (α := Set E)
    (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h : Nontrivial ι
this_1 : FiniteDimensional ℝ E
this :
  Eq.{u_2 + 1} (α := Set E)
    ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)) : Set E)
    (⋂ (i : ι), preimage (β := ℝ) (⇑(b.coord i) : (a : E) → ℝ) (Ici 0) : Set E)
x : E
⊢ Membership.mem (γ := Set E)
      (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) x ↔
    Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)} x

Tactic:
simp only [this, interior_iInter_of_finite, ←
      IsOpenMap.preimage_interior_eq_interior_preimage (isOpenMap_barycentric_coord b _)
        (continuous_barycentric_coord b _),
      interior_Ici, mem_iInter, mem_setOf_eq, mem_Ioi, mem_preimage]

Premises used: interior_Ici, Set.mem_Ioi, IsOpenMap.preimage_interior_eq_interior_preimage, Set.mem_setOf_eq, Set.mem_iInter, continuous_barycentric_coord, isOpenMap_barycentric_coord, Set.mem_preimage, interior_iInter_of_finite
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
hne : s.Nonempty
h : AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
obtain :
  ∀ (q : P) (hq : q ∈ s),
    ∃ (t : Set P),
      s ⊆ t ∧
        t ⊆ u ∧
          AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ t })
              (Subtype.val (p := fun (x : P) ↦ x ∈ t)) ∧
            Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤
⊢ ∃ (t : Set P),
    s ⊆ t ∧
      t ⊆ u ∧
        AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ t })
            (Subtype.val (p := fun (x : P) ↦ x ∈ t)) ∧
          Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤

Tactic:
obtain ⟨q, hq⟩ := hne
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
q : P
hq : q ∈ s
obtain :
  ∀ (ε : ℝ) (ε0 : 0 < ε) (hεu : Metric.closedBall q ε ⊆ u),
    ∃ (t : Set P),
      s ⊆ t ∧
        t ⊆ u ∧
          AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ t })
              (Subtype.val (p := fun (x : P) ↦ x ∈ t)) ∧
            Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤
⊢ ∃ (t : Set P),
    s ⊆ t ∧
      t ⊆ u ∧
        AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ t })
            (Subtype.val (p := fun (x : P) ↦ x ∈ t)) ∧
          Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤

Tactic:
obtain ⟨ε, ε0, hεu⟩ := Metric.nhds_basis_closedBall.mem_iff.1 (hu.mem_nhds <| hsu hq)

Premises used: Filter.HasBasis.mem_iff, IsOpen.mem_nhds, Iff.mp, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
obtain :
  ∀ (t : Set P) (ht₁ : s ⊆ t) (ht₂ : AffineIndependent ℝ (P := P) fun (p : (↑t : Type u_2)) ↦ (↑p : P))
    (ht₃ : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤),
    ∃ (t : Set P),
      s ⊆ t ∧
        t ⊆ u ∧
          AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ t })
              (Subtype.val (p := fun (x : P) ↦ x ∈ t)) ∧
            Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤
⊢ ∃ (t : Set P),
    s ⊆ t ∧
      t ⊆ u ∧
        AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ t })
            (Subtype.val (p := fun (x : P) ↦ x ∈ t)) ∧
          Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤

Tactic:
obtain ⟨t, ht₁, ht₂, ht₃⟩ := exists_subset_affineIndependent_affineSpan_eq_top h

Premises used: exists_subset_affineIndependent_affineSpan_eq_top
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ (P := P) fun (p : (↑t : Type u_2)) ↦ (↑p : P)
ht₃ : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤
f : P → P := fun (y : P) ↦ (lineMap q y : (a : ℝ) → P) (ε / dist y q)
⊢ ∀ (y : P), f y ∈ u

Tactic:
fun y => hεu ?_
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ (P := P) fun (p : (↑t : Type u_2)) ↦ (↑p : P)
ht₃ : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤
f : P → P := fun (y : P) ↦ (lineMap q y : (a : ℝ) → P) (ε / dist y q)
refine : ∀ (y : P), f y ∈ Metric.closedBall q ε
⊢ ∀ (y : P), f y ∈ u

Tactic:
refine fun y => hεu ?_
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ (P := P) fun (p : (↑t : Type u_2)) ↦ (↑p : P)
ht₃ : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤
f : P → P := fun (y : P) ↦ (lineMap q y : (a : ℝ) → P) (ε / dist y q)
y : P
simp : Membership.mem (α := P) (Metric.closedBall q ε) ((lineMap q y : (a : ℝ) → P) (ε / dist y q) : P)
⊢ f y ∈ Metric.closedBall q ε

Tactic:
simp only [f]
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ (P := P) fun (p : (↑t : Type u_2)) ↦ (↑p : P)
ht₃ : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤
f : P → P := fun (y : P) ↦ (lineMap q y : (a : ℝ) → P) (ε / dist y q)
y : P
rw : ‖y -ᵥ q‖ / ‖y -ᵥ q‖ * ε ≤ ε
⊢ Membership.mem (α := P) (Metric.closedBall q ε) ((lineMap q y : (a : ℝ) → P) (ε / dist y q) : P)

Tactic:
rw [Metric.mem_closedBall, lineMap_apply, dist_vadd_left, norm_smul, Real.norm_eq_abs,
      dist_eq_norm_vsub V y q, abs_div, abs_of_pos ε0, abs_of_nonneg (norm_nonneg _), div_mul_comm]

Premises used: norm_smul, abs_div, dist_vadd_left, AffineMap.lineMap_apply, div_mul_comm, abs_of_nonneg, dist_eq_norm_vsub, Metric.mem_closedBall, abs_of_pos, norm_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ (P := P) fun (p : (↑t : Type u_2)) ↦ (↑p : P)
ht₃ : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤
f : P → P := fun (y : P) ↦ (lineMap q y : (a : ℝ) → P) (ε / dist y q)
y : P
⊢ ‖y -ᵥ q‖ / ‖y -ᵥ q‖ * ε ≤ ε

Tactic:
mul_le_of_le_one_left ε0.le (div_self_le_one _)

Premises used: LT.lt.le, div_self_le_one, mul_le_of_le_one_left