awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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 : x ∈ dist p ⁻¹' (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x)
⊢ Membership.mem (γ := Set ℝ) (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x) ‖x -ᵥ p‖

Tactic:
rw [Set.mem_preimage, dist_eq_norm_vsub'] at hx

Premises used: dist_eq_norm_vsub', Set.mem_preimage
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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)
rw : ‖x'‖ = 1
rw₁ : ‖‖x -ᵥ p‖⁻¹‖ * ‖x -ᵥ p‖ = 1
rw₂ : ‖‖x -ᵥ p‖‖⁻¹ * ‖x -ᵥ p‖ = 1
rw₃ : ‖x -ᵥ p‖⁻¹ * ‖x -ᵥ p‖ = 1
rw₄ rw₅ : Eq (α := ℝ) 1 1
⊢ Membership.mem (γ := Set V) (Metric.sphere 0 1) x'

Tactic:
rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hx.1.ne']

Premises used: norm_smul, mem_sphere_zero_iff_norm, norm_norm, norm_inv, LT.lt.ne', inv_mul_cancel₀
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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)
⊢ Membership.mem (γ := Set V) (Metric.sphere 0 1) x'

Tactic:
have x'_mem : x' ∈ Metric.sphere 0 1 := by
    rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hx.1.ne']
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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'
have : ∀ (y : V) (y_mem : y ∈ cover) (hy : x' ∈ u y), x ∈ s
⊢ x ∈ s

Tactic:
have ⟨y, y_mem, hy⟩ := Set.mem_iUnion₂.mp (h₂ x'_mem)
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
rw : ‖x -ᵥ p‖ • x' +ᵥ p ∈ s
⊢ x ∈ s

Tactic:
rw [← vsub_vadd x p, ← show ‖x -ᵥ p‖ • x' = x -ᵥ p from smul_inv_smul₀ hx.1.ne' (x -ᵥ p)]

Premises used: smul_inv_smul₀, VSub.vsub, LT.lt.ne', vsub_vadd
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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 -ᵥ p‖ • x' +ᵥ p ∈ s

Tactic:
smul_subset_s y (h₁ y y_mem) <| Set.smul_mem_smul (Set.biInter_subset_of_mem y_mem hx.2) hy

Premises used: Set.Mem, Set.smul_mem_smul, setOf, Set.biInter_subset_of_mem, And.right, Set.preimage
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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 -ᵥ p‖ • x' +ᵥ p ∈ s

Tactic:
exact smul_subset_s y (h₁ y y_mem) <| Set.smul_mem_smul (Set.biInter_subset_of_mem y_mem hx.2) hy

Premises used: Set.smul_mem_smul, Set.biInter_subset_of_mem, And.right
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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}

Tactic:
⟨asymptoticCone_subset_singleton_of_bounded, fun h => ?_⟩

Premises used: Iff.intro, asymptoticCone_subset_singleton_of_bounded
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
refine : ∀ (h : asymptoticCone ℝ s ⊆ {0}), Bornology.IsBounded s
⊢ Bornology.IsBounded s ↔ asymptoticCone ℝ s ⊆ {0}

Tactic:
refine ⟨asymptoticCone_subset_singleton_of_bounded, fun h => ?_⟩
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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}
simp_rw : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), sᶜ ∈ asymptoticNhds ℝ P i
⊢ Bornology.IsBounded s

Tactic:
simp_rw [isBounded_def, cobounded_eq_iSup_sphere_asymptoticNhds, mem_iSup]

Premises used: AffineSpace.cobounded_eq_iSup_sphere_asymptoticNhds, Filter.mem_iSup, Bornology.isBounded_def
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
by_contra : ∀ (h' : sᶜ ∉ asymptoticNhds ℝ P v), False
⊢ sᶜ ∈ asymptoticNhds ℝ P v

Tactic:
by_contra h'
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
h' : sᶜ ∉ asymptoticNhds ℝ P v
⊢ False

Tactic:
Metric.ne_of_mem_sphere hv one_ne_zero (h h')

Premises used: Metric.ne_of_mem_sphere, one_ne_zero
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
h' : sᶜ ∉ asymptoticNhds ℝ P v
⊢ False

Tactic:
exact Metric.ne_of_mem_sphere hv one_ne_zero (h h')

Premises used: Metric.ne_of_mem_sphere, one_ne_zero
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
rw : (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) ↔ ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
⊢ ¬Bornology.IsBounded s ↔ ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s

Tactic:
rw [isBounded_iff_asymptoticCone_subset_singleton, Set.subset_singleton_iff, not_forall]

Premises used: Set.subset_singleton_iff, isBounded_iff_asymptoticCone_subset_singleton, Classical.not_forall
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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)
mpr₁₃ : (w : V) → w ≠ 0 → w ∈ asymptoticCone ℝ s → V
mpr₁₄ : ∀ (w : V), w ≠ 0 → w ∈ asymptoticCone ℝ s → ¬(w ∈ asymptoticCone ℝ s → w = 0)
mpr₁₅ : (w : V) → w ≠ 0 → w ∈ asymptoticCone ℝ s → V
⊢ (∃ (x : V), ¬(x ∈ asymptoticCone ℝ s → x = 0)) ↔ ∃ (v : V), v ≠ 0 ∧ v ∈ asymptoticCone ℝ s

Tactic:
tauto
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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'
⊢ ∀ (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

Premises used: mem_affineSpan_pair_iff_exists_lineMap_eq
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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
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)))
⊢ 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
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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
⊢ ∀ (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'
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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)))
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))
⊢ Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i)) (∏ i : Fin 3, dist (p i) (t.points (i + 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']

Premises used: Finset.prod_mul_distrib, Affine.Triangle.prod_eq_prod_one_sub_of_mem_line_point_lineMap, dist_lineMap_right, norm_prod, dist_left_lineMap
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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'
i : Fin 3
⊢ dist (p i) (t.points (i + 2)) ≠ 0

Tactic:
simpa using hp0 i
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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'
⊢ ∀ (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
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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)) (∏ 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'
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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)))
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
⊢ Eq (α := ℝ) (∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i) / dist (p i) (t.points (i + 2))) 1

Tactic:
rw [Fin.prod_univ_three] at key ⊢

Premises used: Fin.prod_univ_three
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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 :
  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 (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) =
    dist (p 0) (t.points (HAdd.hAdd (α := Fin 3) 0 2)) * dist (p 1) (t.points (HAdd.hAdd (α := Fin 3) 1 2)) *
      dist (p 2) (t.points (HAdd.hAdd (α := Fin 3) 2 2))

Tactic:
rw [Fin.prod_univ_three] at key

Premises used: Fin.prod_univ_three
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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 :
  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) =
    dist (p 0) (t.points (HAdd.hAdd (α := Fin 3) 0 2)) * dist (p 1) (t.points (HAdd.hAdd (α := Fin 3) 1 2)) *
      dist (p 2) (t.points (HAdd.hAdd (α := Fin 3) 2 2))
⊢ dist (p 0) (t.points (HAdd.hAdd (α := Fin 3) 0 2)) ≠ 0

Tactic:
have := aux 0