awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hki' : s.points k ∈ Set.range (s.faceOpposite i).points
hkj' : s.points k ∈ Set.range (s.faceOpposite j).points
hs : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))

Tactic:
convert! AffineSubspace.vectorSpan_union_of_mem_of_mem ℝ hki' hkj'

Premises used: Real, AffineSubspace.vectorSpan_union_of_mem_of_mem
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
⊢ Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))

Tactic:
have hs : vectorSpan ℝ (Set.range s.points) =
          vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔
            vectorSpan ℝ (Set.range (s.faceOpposite j).points) := by
        rcases hk with ⟨k, hki, hkj⟩
        have hki' : s.points k ∈ Set.range (s.faceOpposite i).points := by
          rw [range_faceOpposite_points]
          exact Set.mem_image_of_mem _ hki
        have hkj' : s.points k ∈ Set.range (s.faceOpposite j).points := by
          rw [range_faceOpposite_points]
          exact Set.mem_image_of_mem _ hkj
        have hs :
            Set.range s.points =
              Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points := by
          simp only [range_faceOpposite_points, ← Set.image_union]
          simp_rw [← Set.image_univ, ← Set.compl_inter]
          rw [Set.inter_singleton_eq_empty.mpr ?_, Set.compl_empty]
          simpa using hij.symm
        convert! AffineSubspace.vectorSpan_union_of_mem_of_mem ℝ hki' hkj'
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
a :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ
      (s.points j -ᵥ s.altitudeFoot j) ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ
      (s.points j -ᵥ s.altitudeFoot j)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (s.points j -ᵥ s.altitudeFoot j)

Tactic:
rw [hs, ← Submodule.inf_orthogonal, Submodule.mem_inf]

Premises used: Submodule.mem_inf, Submodule.inf_orthogonal
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ
      (s.points j -ᵥ s.altitudeFoot j) ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ
      (s.points j -ᵥ s.altitudeFoot j)

Tactic:
⟨?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
a :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ
    (s.points j -ᵥ s.altitudeFoot j)
a₁ :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ
    (s.points j -ᵥ s.altitudeFoot j)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ
      (s.points j -ᵥ s.altitudeFoot j) ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ
      (s.points j -ᵥ s.altitudeFoot j)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
a :
  Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range (s.faceOpposite i).points)))ᗮ
    (r • (s.points i -ᵥ s.altitudeFoot i))
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ
    (s.points j -ᵥ s.altitudeFoot j)

Tactic:
rw [h, ← direction_affineSpan]

Premises used: direction_affineSpan
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range (s.faceOpposite i).points)))ᗮ
    (r • (s.points i -ᵥ s.altitudeFoot i))

Tactic:
Submodule.smul_mem _ _ (vsub_orthogonalProjection_mem_direction_orthogonal _ _)

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, Set.Mem, setOf, Submodule.smul_mem
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range (s.faceOpposite i).points)))ᗮ
    (r • (s.points i -ᵥ s.altitudeFoot i))

Tactic:
exact Submodule.smul_mem _ _ (vsub_orthogonalProjection_mem_direction_orthogonal _ _)

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, Submodule.smul_mem
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
a :
  Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range (s.faceOpposite j).points)))ᗮ
    (s.points j -ᵥ s.altitudeFoot j)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ
    (s.points j -ᵥ s.altitudeFoot j)

Tactic:
rw [← direction_affineSpan]

Premises used: direction_affineSpan
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range (s.faceOpposite j).points)))ᗮ
    (s.points j -ᵥ s.altitudeFoot j)

Tactic:
vsub_orthogonalProjection_mem_direction_orthogonal _ _

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, Set.Mem, setOf, Affine.Simplex.altitudeFoot
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range (s.faceOpposite j).points)))ᗮ
    (s.points j -ᵥ s.altitudeFoot j)

Tactic:
exact vsub_orthogonalProjection_mem_direction_orthogonal _ _

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
inl : -(s.height i * s.height i) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫
inr : ∀ (hij : i ≠ j), -(s.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫
⊢ -(s.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i : Fin (n + 1)
inl : -(s.height i * s.height i) < HPow.hPow (β := ℕ) ‖s.points i -ᵥ s.altitudeFoot i‖ 2
⊢ -(s.height i * s.height i) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫

Tactic:
rw [real_inner_self_eq_norm_sq]

Premises used: real_inner_self_eq_norm_sq
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i : Fin (n + 1)
⊢ -(s.height i * s.height i) < HPow.hPow (β := ℕ) ‖s.points i -ᵥ s.altitudeFoot i‖ 2

Tactic:
lt_of_lt_of_le (b := 0) ?_ ?_

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i : Fin (n + 1)
inl : -(s.height i * s.height i) < 0
inl₁ : 0 ≤ HPow.hPow (β := ℕ) ‖s.points i -ᵥ s.altitudeFoot i‖ 2
⊢ -(s.height i * s.height i) < HPow.hPow (β := ℕ) ‖s.points i -ᵥ s.altitudeFoot i‖ 2

Tactic:
refine lt_of_lt_of_le (b := 0) ?_ ?_

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i : Fin (n + 1)
inl : 0 < s.height i * s.height i
⊢ -(s.height i * s.height i) < 0

Tactic:
rw [neg_lt_zero]

Premises used: neg_lt_zero
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i : Fin (n + 1)
⊢ 0 < s.height i * s.height i

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i : Fin (n + 1)
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖s.points i -ᵥ s.altitudeFoot i‖ 2

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
inr : -⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ < s.height i * s.height j
⊢ -(s.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫

Tactic:
rw [neg_lt]

Premises used: neg_lt
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ -⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ < s.height i * s.height j

Tactic:
lt_of_abs_lt ?_

Premises used: lt_of_abs_lt
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
inr : |(-⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫)| < s.height i * s.height j
⊢ -⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ < s.height i * s.height j

Tactic:
refine lt_of_abs_lt ?_

Premises used: lt_of_abs_lt
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
inr : |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < s.height i * s.height j
⊢ |(-⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫)| < s.height i * s.height j

Tactic:
rw [abs_neg]

Premises used: abs_neg
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < s.height i * s.height j

Tactic:
abs_inner_vsub_altitudeFoot_lt_mul s hij

Premises used: Affine.Simplex.abs_inner_vsub_altitudeFoot_lt_mul
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < s.height i * s.height j

Tactic:
exact abs_inner_vsub_altitudeFoot_lt_mul s hij

Premises used: Affine.Simplex.abs_inner_vsub_altitudeFoot_lt_mul
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ 0 < |s.height i * s.height j|

Tactic:
simp [height]

Premises used: Affine.Simplex.height
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
rw : |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < |s.height i * s.height j|
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)| < 1

Tactic:
rw [abs_div, div_lt_one (by simp [height])]

Premises used: abs_div, div_lt_one
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
nth_rw : |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < s.height i * s.height j
nth_rw₁ : 0 ≤ s.height i * s.height j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < |s.height i * s.height j|

Tactic:
nth_rw 2 [abs_eq_self.2]

Premises used: Iff.mpr, abs_eq_self
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < s.height i * s.height j

Tactic:
abs_inner_vsub_altitudeFoot_lt_mul _ hij

Premises used: Affine.Simplex.abs_inner_vsub_altitudeFoot_lt_mul
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < s.height i * s.height j

Tactic:
exact abs_inner_vsub_altitudeFoot_lt_mul _ hij

Premises used: Affine.Simplex.abs_inner_vsub_altitudeFoot_lt_mul
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
simp : 0 ≤ dist (s.points i) (s.altitudeFoot i) * dist (s.points j) (s.altitudeFoot j)
⊢ 0 ≤ s.height i * s.height j

Tactic:
simp only [height]

Premises used: Affine.Simplex.height
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ 0 ≤ dist (s.points i) (s.altitudeFoot i) * dist (s.points j) (s.altitudeFoot j)

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : n.AtLeastTwo
s : Simplex ℝ P n
i j : Fin (n + 1)
⊢ 0 < s.height i * s.height j

Tactic:
simp [height]

Premises used: Affine.Simplex.height
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : n.AtLeastTwo
s : Simplex ℝ P n
i j : Fin (n + 1)
rw : -(s.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫
⊢ -1 < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)

Tactic:
rw [neg_lt, neg_div', div_lt_one (by simp [height]), neg_lt]

Premises used: neg_div', div_lt_one, neg_lt
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : n.AtLeastTwo
s : Simplex ℝ P n
i j : Fin (n + 1)
⊢ -(s.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫

Tactic:
neg_mul_lt_inner_vsub_altitudeFoot _ _ _

Premises used: Affine.Simplex.neg_mul_lt_inner_vsub_altitudeFoot
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : n.AtLeastTwo
s : Simplex ℝ P n
i j : Fin (n + 1)
⊢ -(s.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫

Tactic:
exact neg_mul_lt_inner_vsub_altitudeFoot _ _ _

Premises used: Affine.Simplex.neg_mul_lt_inner_vsub_altitudeFoot
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_5
inst_5 : TopologicalSpace H
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_10
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
h : M ≃ₘ^n⟮I, I'⟯ M'
⊢ Continuous[inst_7, inst_9] (⇑h : (a : M) → M')

Tactic:
h.contMDiff_toFun.continuous

Premises used: ContMDiff.continuous, Diffeomorph.contMDiff_toFun
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_5
inst_5 : TopologicalSpace H
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_10
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
h : M ≃ₘ^n⟮I, I'⟯ M'
⊢ ContMDiff.{u_1, u_2, u_5, u_9, u_3, u_6, u_10} I (M := M) I' (M' := M') n (⇑h : (a : M) → M')

Tactic:
h.contMDiff_toFun

Premises used: Diffeomorph.contMDiff_toFun
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_5
inst_5 : TopologicalSpace H
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_10
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
h : M ≃ₘ^n⟮I, I'⟯ M'
x : M
⊢ ContMDiffAt.{u_1, u_2, u_5, u_9, u_3, u_6, u_10} I I' (M' := M') n (⇑h : (a : M) → M') x

Tactic:
h.contMDiff.contMDiffAt

Premises used: ContMDiff.contMDiffAt, Diffeomorph.contMDiff