awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
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
inst_4 : FiniteDimensional ℝ V
s : Set P
p : P
t : (i : V) → Set ℝ
ht : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), Membership.mem (γ := Filter ℝ) atTop (t i)
u : (i : V) → Set V
hu : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), u i ∈ 𝓝 i
smul_subset_s :
  ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), t i • u i ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, Membership.mem (γ := Set V) (Metric.sphere 0 1) x
h₂ : Subset.{u_1} (α := Set V) (Metric.sphere 0 1) (⋃ x ∈ cover, u x)
x : P
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x) ‖x -ᵥ p‖
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
x'_mem : Membership.mem (γ := Set V) (Metric.sphere 0 1) x'
y : V
y_mem : y ∈ cover
hy : x' ∈ u y
⊢ x ∈ s
have rw : ‖x -ᵥ p‖ • x' +ᵥ p ∈ s
Tactic: rw [← vsub_vadd x p, ← show ‖x -ᵥ p‖ • x' = x -ᵥ p from smul_inv_smul₀ hx.1.ne' (x -ᵥ p)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
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
inst_4 : FiniteDimensional ℝ V
s : Set P
⊢ Bornology.IsBounded s ↔ asymptoticCone ℝ s ⊆ {0}
have refine : ∀ (h : asymptoticCone ℝ s ⊆ {0}), Bornology.IsBounded s
Tactic: refine ⟨asymptoticCone_subset_singleton_of_bounded, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
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
inst_4 : FiniteDimensional ℝ V
s : Set P
h : asymptoticCone ℝ s ⊆ {0}
⊢ Bornology.IsBounded s
have simp_rw : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), sᶜ ∈ asymptoticNhds ℝ P i
Tactic: simp_rw [isBounded_def, cobounded_eq_iSup_sphere_asymptoticNhds, mem_iSup]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
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
inst_4 : FiniteDimensional ℝ V
s : Set P
h : asymptoticCone ℝ s ⊆ {0}
v : V
hv : Membership.mem (γ := Set V) (Metric.sphere 0 1) v
⊢ sᶜ ∈ asymptoticNhds ℝ P v
have by_contra : ∀ (h' : sᶜ ∉ asymptoticNhds ℝ P v), False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
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
inst_4 : FiniteDimensional ℝ V
s : Set P
⊢ ¬Bornology.IsBounded s ↔ ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
have rw : (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) ↔ ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
Tactic: rw [isBounded_iff_asymptoticCone_subset_singleton, Set.subset_singleton_iff, not_forall]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
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
inst_4 : FiniteDimensional ℝ V
s : Set P
⊢ (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) ↔ ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
have mp : (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
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
inst_4 : FiniteDimensional ℝ V
s : Set P
mp : (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
⊢ (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) ↔ ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
have mpr : (∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s) → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
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
inst_4 : FiniteDimensional ℝ V
s : Set P
mp : (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr : (∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s) → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
⊢ (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) ↔ ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
have mp₁ : ∀ (w : V), ¬(w ∈ asymptoticCone ℝ s → w = 0) → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
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
inst_4 : FiniteDimensional ℝ V
s : Set P
mp : (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr : (∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s) → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
mp₁ mp₂ mp₃ : ∀ (w : V), ¬(w ∈ asymptoticCone ℝ s → w = 0) → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
⊢ (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) ↔ ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
have mpr₁ : ∀ (w : V), w ≠ 0 → w ∈ asymptoticCone ℝ s → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
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
inst_4 : FiniteDimensional ℝ V
s : Set P
mp : (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr : (∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s) → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
mp₁ mp₂ mp₃ : ∀ (w : V), ¬(w ∈ asymptoticCone ℝ s → w = 0) → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr₁ mpr₂ mpr₃ : ∀ (w : V), w ≠ 0 → w ∈ asymptoticCone ℝ s → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
⊢ (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) ↔ ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
have mp₄ : ∀ w ∈ asymptoticCone ℝ s, ¬w = 0 → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
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
inst_4 : FiniteDimensional ℝ V
s : Set P
mp : (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr : (∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s) → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
mp₁ mp₂ mp₃ : ∀ (w : V), ¬(w ∈ asymptoticCone ℝ s → w = 0) → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr₁ mpr₂ mpr₃ : ∀ (w : V), w ≠ 0 → w ∈ asymptoticCone ℝ s → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
mp₄ mp₅ mp₆ : ∀ w ∈ asymptoticCone ℝ s, ¬w = 0 → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr₄ mpr₅ mpr₆ : ∀ (w : V), w ≠ 0 → w ∈ asymptoticCone ℝ s → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
mp₇ mp₈ mp₉ : ∀ w ∈ asymptoticCone ℝ s, ¬w = 0 → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr₇ mpr₈ mpr₉ : ∀ (w : V), w ≠ 0 → w ∈ asymptoticCone ℝ s → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
mp₁₀ mp₁₁ : ∀ w ∈ asymptoticCone ℝ s, ¬w = 0 → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr₁₀ mpr₁₁ : ∀ (w : V), w ≠ 0 → w ∈ asymptoticCone ℝ s → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
⊢ (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) ↔ ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
have mpr₁₂ : ∀ (w : V), w ≠ 0 → w ∈ asymptoticCone ℝ s → ¬(w ∈ asymptoticCone ℝ s → w = 0)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
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
inst_4 : FiniteDimensional ℝ V
s : Set P
mp : (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr : (∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s) → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
mp₁ mp₂ mp₃ : ∀ (w : V), ¬(w ∈ asymptoticCone ℝ s → w = 0) → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr₁ mpr₂ mpr₃ : ∀ (w : V), w ≠ 0 → w ∈ asymptoticCone ℝ s → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
mp₄ mp₅ mp₆ : ∀ w ∈ asymptoticCone ℝ s, ¬w = 0 → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr₄ mpr₅ mpr₆ : ∀ (w : V), w ≠ 0 → w ∈ asymptoticCone ℝ s → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
mp₇ mp₈ mp₉ : ∀ w ∈ asymptoticCone ℝ s, ¬w = 0 → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr₇ mpr₈ mpr₉ : ∀ (w : V), w ≠ 0 → w ∈ asymptoticCone ℝ s → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
mp₁₀ mp₁₁ : ∀ w ∈ asymptoticCone ℝ s, ¬w = 0 → ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
mpr₁₀ mpr₁₁ : ∀ (w : V), w ≠ 0 → w ∈ asymptoticCone ℝ s → ∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)
mpr₁₂ : ∀ (w : V), w ≠ 0 → w ∈ asymptoticCone ℝ s → ¬(w ∈ asymptoticCone ℝ s → w = 0)
⊢ (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) ↔ ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
have mpr₁₃ : (w : V) → w ≠ 0 → w ∈ asymptoticCone ℝ s → V
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points (i + 1), t.points (i + 2)}) (p i)
hp' : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points i, p i}) p'
⊢ Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i)) (∏ i : Fin 3, dist (p i) (t.points (i + 2)))
have hp₁ : ∀ (i : Fin 3), ∃ (r : 𝕜), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) r = p i
Tactic: simp_rw [mem_affineSpan_pair_iff_exists_lineMap_eq] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp' : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points i, p i}) p'
hp : ∀ (i : Fin 3), ∃ (r : 𝕜), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) r = p i
⊢ Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i)) (∏ i : Fin 3, dist (p i) (t.points (i + 2)))
have choose : ∀ (r : (i : Fin 3) → 𝕜)
  (hr : ∀ (i : Fin 3), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) (r i) = p i),
  Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i)) (∏ i : Fin 3, dist (p i) (t.points (i + 2)))
Tactic: choose r hr using hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp' : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points i, p i}) p'
r : (i : Fin 3) → 𝕜
hr : ∀ (i : Fin 3), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) (r i) = p i
⊢ Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i)) (∏ i : Fin 3, dist (p i) (t.points (i + 2)))
have hp'₁ : ∀ (i : Fin 3),
  Membership.mem (γ := AffineSubspace 𝕜 P)
    (affineSpan 𝕜
      (insert (t.points i)
        (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) (r i) : P))))
    p'
Tactic: simp_rw [← hr] at hp'
Cleared hypotheses: hp'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
r : (i : Fin 3) → 𝕜
hr : ∀ (i : Fin 3), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) (r i) = p i
hp' :
  ∀ (i : Fin 3),
    Membership.mem (γ := AffineSubspace 𝕜 P)
      (affineSpan 𝕜
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) (r i) : P))))
      p'
⊢ Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i)) (∏ i : Fin 3, dist (p i) (t.points (i + 2)))
have simp_rw : Eq (α := ℝ)
  (∏ x : Fin (2 + 1),
    dist (t.points (x + 1)) ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)))
  (∏ x : Fin 3, dist ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)) (t.points (x + 2)))
Tactic: simp_rw [← hr, dist_lineMap_right, dist_left_lineMap, Finset.prod_mul_distrib, ← norm_prod,
    prod_eq_prod_one_sub_of_mem_line_point_lineMap hp']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
r : (i : Fin 3) → 𝕜
hr : ∀ (i : Fin 3), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) (r i) = p i
hp' :
  ∀ (i : Fin 3),
    Membership.mem (γ := AffineSubspace 𝕜 P)
      (affineSpan 𝕜
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) (r i) : P))))
      p'
simp_rw :
  Eq (α := ℝ)
    (∏ x : Fin (2 + 1),
      dist (t.points (x + 1)) ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)))
    (∏ x : Fin 3,
      dist ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)) (t.points (x + 2)))
⊢ Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i)) (∏ i : Fin 3, dist (p i) (t.points (i + 2)))
have simp_rw₁ : Eq (α := ℝ)
  (∏ x : Fin (2 + 1),
    dist (t.points (x + 1)) ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)))
  (∏ x : Fin 3, ‖1 - r x‖ * dist (t.points (x + 1)) (t.points (x + 2)))
Tactic: simp_rw [← hr, dist_lineMap_right, dist_left_lineMap, Finset.prod_mul_distrib, ← norm_prod,
    prod_eq_prod_one_sub_of_mem_line_point_lineMap hp']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
r : (i : Fin 3) → 𝕜
hr : ∀ (i : Fin 3), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) (r i) = p i
hp' :
  ∀ (i : Fin 3),
    Membership.mem (γ := AffineSubspace 𝕜 P)
      (affineSpan 𝕜
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) (r i) : P))))
      p'
simp_rw :
  Eq (α := ℝ)
    (∏ x : Fin (2 + 1),
      dist (t.points (x + 1)) ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)))
    (∏ x : Fin 3,
      dist ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)) (t.points (x + 2)))
simp_rw₁ :
  Eq (α := ℝ)
    (∏ x : Fin (2 + 1),
      dist (t.points (x + 1)) ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)))
    (∏ x : Fin 3, ‖1 - r x‖ * dist (t.points (x + 1)) (t.points (x + 2)))
⊢ Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i)) (∏ i : Fin 3, dist (p i) (t.points (i + 2)))
have simp_rw₂ : Eq (α := ℝ) (∏ x : Fin (2 + 1), ‖r x‖ * dist (t.points (x + 1)) (t.points (x + 2)))
  (∏ x : Fin 3, ‖1 - r x‖ * dist (t.points (x + 1)) (t.points (x + 2)))
Tactic: simp_rw [← hr, dist_lineMap_right, dist_left_lineMap, Finset.prod_mul_distrib, ← norm_prod,
    prod_eq_prod_one_sub_of_mem_line_point_lineMap hp']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
r : (i : Fin 3) → 𝕜
hr : ∀ (i : Fin 3), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) (r i) = p i
hp' :
  ∀ (i : Fin 3),
    Membership.mem (γ := AffineSubspace 𝕜 P)
      (affineSpan 𝕜
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) (r i) : P))))
      p'
simp_rw :
  Eq (α := ℝ)
    (∏ x : Fin (2 + 1),
      dist (t.points (x + 1)) ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)))
    (∏ x : Fin 3,
      dist ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)) (t.points (x + 2)))
simp_rw₁ :
  Eq (α := ℝ)
    (∏ x : Fin (2 + 1),
      dist (t.points (x + 1)) ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)))
    (∏ x : Fin 3, ‖1 - r x‖ * dist (t.points (x + 1)) (t.points (x + 2)))
simp_rw₂ :
  Eq (α := ℝ) (∏ x : Fin (2 + 1), ‖r x‖ * dist (t.points (x + 1)) (t.points (x + 2)))
    (∏ x : Fin 3, ‖1 - r x‖ * dist (t.points (x + 1)) (t.points (x + 2)))
⊢ Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i)) (∏ i : Fin 3, dist (p i) (t.points (i + 2)))
have simp_rw₃ : HMul.hMul (α := ℝ) (∏ x : Fin (2 + 1), ‖r x‖) (∏ x : Fin (2 + 1), dist (t.points (x + 1)) (t.points (x + 2))) =
  HMul.hMul (α := ℝ) (∏ x : Fin 3, ‖1 - r x‖) (∏ x : Fin 3, dist (t.points (x + 1)) (t.points (x + 2)))
Tactic: simp_rw [← hr, dist_lineMap_right, dist_left_lineMap, Finset.prod_mul_distrib, ← norm_prod,
    prod_eq_prod_one_sub_of_mem_line_point_lineMap hp']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
r : (i : Fin 3) → 𝕜
hr : ∀ (i : Fin 3), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) (r i) = p i
hp' :
  ∀ (i : Fin 3),
    Membership.mem (γ := AffineSubspace 𝕜 P)
      (affineSpan 𝕜
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : 𝕜) → P) (r i) : P))))
      p'
simp_rw :
  Eq (α := ℝ)
    (∏ x : Fin (2 + 1),
      dist (t.points (x + 1)) ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)))
    (∏ x : Fin 3,
      dist ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)) (t.points (x + 2)))
simp_rw₁ :
  Eq (α := ℝ)
    (∏ x : Fin (2 + 1),
      dist (t.points (x + 1)) ((AffineMap.lineMap (t.points (x + 1)) (t.points (x + 2)) : (a : 𝕜) → P) (r x)))
    (∏ x : Fin 3, ‖1 - r x‖ * dist (t.points (x + 1)) (t.points (x + 2)))
simp_rw₂ :
  Eq (α := ℝ) (∏ x : Fin (2 + 1), ‖r x‖ * dist (t.points (x + 1)) (t.points (x + 2)))
    (∏ x : Fin 3, ‖1 - r x‖ * dist (t.points (x + 1)) (t.points (x + 2)))
simp_rw₃ :
  HMul.hMul (α := ℝ) (∏ x : Fin (2 + 1), ‖r x‖) (∏ x : Fin (2 + 1), dist (t.points (x + 1)) (t.points (x + 2))) =
    HMul.hMul (α := ℝ) (∏ x : Fin 3, ‖1 - r x‖) (∏ x : Fin 3, dist (t.points (x + 1)) (t.points (x + 2)))
⊢ Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i)) (∏ i : Fin 3, dist (p i) (t.points (i + 2)))
have simp_rw₄ : norm.{u_1} (E := 𝕜) (∏ b : Fin (2 + 1), r b) * ∏ x : Fin (2 + 1), dist (t.points (x + 1)) (t.points (x + 2)) =
  norm.{u_1} (E := 𝕜) (∏ b : Fin 3, (1 - r b)) * ∏ x : Fin 3, dist (t.points (x + 1)) (t.points (x + 2))
Tactic: simp_rw [← hr, dist_lineMap_right, dist_left_lineMap, Finset.prod_mul_distrib, ← norm_prod,
    prod_eq_prod_one_sub_of_mem_line_point_lineMap hp']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2)
hp : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points (i + 1), t.points (i + 2)}) (p i)
hp' : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points i, p i}) p'
⊢ Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i) / dist (p i) (t.points (i + 2))) 1
have aux : ∀ (i : Fin 3), dist (p i) (t.points (i + 2)) ≠ 0
Tactic: have aux (i) : dist (p i) (t.points (i + 2)) ≠ 0 := by simpa using hp0 i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2)
hp : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points (i + 1), t.points (i + 2)}) (p i)
hp' : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points i, p i}) p'
aux : ∀ (i : Fin 3), dist (p i) (t.points (i + 2)) ≠ 0
⊢ Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i) / dist (p i) (t.points (i + 2))) 1
have key : Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i)) (∏ i : Fin 3, dist (p i) (t.points (i + 2)))
Tactic: have key := prod_dist_eq_prod_dist_of_mem_line_of_mem_line hp hp'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2)
hp : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points (i + 1), t.points (i + 2)}) (p i)
hp' : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points i, p i}) p'
aux : ∀ (i : Fin 3), dist (p i) (t.points (i + 2)) ≠ 0
key : Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i)) (∏ i : Fin 3, dist (p i) (t.points (i + 2)))
⊢ Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i) / dist (p i) (t.points (i + 2))) 1
have rw : ∀
  (key :
    dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1)) (p 0) *
          dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 1)) (p 1) *
        dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1)) (p 2) =
      ∏ i : Fin 3, dist (p i) (t.points (i + 2))),
  dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1)) (p 0) /
          dist (p 0) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 2)) *
        (dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 1)) (p 1) /
          dist (p 1) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 2))) *
      (dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1)) (p 2) /
        dist (p 2) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 2))) =
    1
Tactic: rw [Fin.prod_univ_three] at key ⊢
Cleared hypotheses: key