awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
M' : Type u_4
inst_7 : AddCommMonoid M'
inst_8 : Module R M'
s : Set M'
q : M' →ₗ[R] M
h :
  ∀ (x : N),
    Membership.mem (γ := PointedCone R N) (dual p ((⇑q : (a : M') → M) '' s)) x ↔
      Membership.mem (γ := PointedCone R N) (dual (p ∘ₗ q) s) x
⊢ Eq (α := PointedCone R N) (dual p ((⇑q : (a : M') → M) '' s)) (dual (p ∘ₗ q) s)

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
M' : Type u_4
inst_7 : AddCommMonoid M'
inst_8 : Module R M'
s : Set M'
q : M' →ₗ[R] M
x : N
⊢ Membership.mem (γ := PointedCone R N) (dual p ((⇑q : (a : M') → M) '' s)) x ↔
    Membership.mem (γ := PointedCone R N) (dual (p ∘ₗ q) s) x

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
⊢ Eq (α := PointedCone R N) (dual p s) (dual LinearMap.id ((⇑p : (a : M) → N →ₗ[R] R) '' s))

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R M
⊢ Eq (α := PointedCone R N) (dual p (↑C : Set M)) (dual LinearMap.id (↑(map p C) : Set (N →ₗ[R] R)))

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
h :
  ∀ (x : N),
    Membership.mem (γ := PointedCone R N) (dual p s) x ↔
      Membership.mem (γ := PointedCone R N) (comap p.flip (dual (Module.Dual.eval R M) s)) x
⊢ Eq (α := PointedCone R N) (dual p s) (comap p.flip (dual (Module.Dual.eval R M) s))

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
⊢ Membership.mem (γ := PointedCone R N) (dual p s) x ↔
    Membership.mem (γ := PointedCone R N) (comap p.flip (dual (Module.Dual.eval R M) s)) x

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
hp : Injective (α := N) (β := M →ₗ[R] R) (⇑p.flip : (a : N) → M →ₗ[R] R)
⊢ LE.le (α := PointedCone R N) 0 (dual p univ)

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
hp : Injective (α := N) (β := M →ₗ[R] R) (⇑p.flip : (a : N) → M →ₗ[R] R)
refine :
  ∀ (y : N) (hy : Membership.mem (γ := Submodule.{u_1, u_3} { c : R // 0 ≤ c } N) (dual p univ) y),
    Eq (α := M →ₗ[R] R) ((p.flip : (a : N) → M →ₗ[R] R) y : M →ₗ[R] R) (0 : M →ₗ[R] R)
⊢ Eq (α := PointedCone R N) (dual p univ) 0

Tactic:
refine le_antisymm (fun y hy ↦ (map_eq_zero_iff p.flip hp).1 ?_) (by simp)

Premises used: le_antisymm
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
hp : Injective (α := N) (β := M →ₗ[R] R) (⇑p.flip : (a : N) → M →ₗ[R] R)
y : N
hy : Membership.mem (γ := Submodule.{u_1, u_3} { c : R // 0 ≤ c } N) (dual p univ) y
h :
  ∀ (x : M),
    Eq.{u_1 + 1} (α := R) ((((p.flip : (a : N) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
      ((0 : (a : M) → R) x : R)
⊢ Eq (α := M →ₗ[R] R) ((p.flip : (a : N) → M →ₗ[R] R) y : M →ₗ[R] R) (0 : M →ₗ[R] R)

Tactic:
ext x
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
hp : Injective (α := N) (β := M →ₗ[R] R) (⇑p.flip : (a : N) → M →ₗ[R] R)
y : N
hy : Membership.mem (γ := Submodule.{u_1, u_3} { c : R // 0 ≤ c } N) (dual p univ) y
x : M
⊢ LE.le.{u_1} (α := R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R) (0 : R)

Tactic:
simpa using hy <| mem_univ (-x)

Premises used: Set.mem_univ, Neg.neg
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
hp : Injective (α := N) (β := M →ₗ[R] R) (⇑p.flip : (a : N) → M →ₗ[R] R)
y : N
hy : Membership.mem (γ := Submodule.{u_1, u_3} { c : R // 0 ≤ c } N) (dual p univ) y
x : M
⊢ Eq.{u_1 + 1} (α := R) ((((p.flip : (a : N) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) ((0 : (a : M) → R) x : R)

Tactic:
exact (hy <| mem_univ x).antisymm' <| by simpa using hy <| mem_univ (-x)

Premises used: LE.le.antisymm', Set.mem_univ
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
h :
  ∀ (x : N), Membership.mem (γ := PointedCone R N) (dual p (-s)) x ↔ Membership.mem (γ := PointedCone R N) (-dual p s) x
⊢ Eq (α := PointedCone R N) (dual p (-s)) (-dual p s)

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
⊢ Membership.mem (γ := PointedCone R N) (dual p (-s)) x ↔ Membership.mem (γ := PointedCone R N) (-dual p s) x

Tactic:
simp
-- 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
i : Fin (n + 1)
⊢ s.altitude i = mk' (s.points i) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ affineSpan ℝ (Set.range s.points)

Tactic:
rfl

Premises used: Affine.Simplex.altitude, 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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
h :
  ∀ (i : Fin (m + 1)) (x : P),
    x ∈ (s.reindex e).altitude i ↔ x ∈ (s.altitude ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
⊢ (s.reindex e).altitude = s.altitude ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))

Tactic:
ext i
-- 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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
i : Fin (m + 1)
x : P
h :
  Membership.mem (γ := AffineSubspace ℝ P)
      (mk' ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i)
          (direction
              (affineSpan ℝ
                (s.points '' (Set.image (α := Fin (m + 1)) (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)) {i})ᶜ)))ᗮ ⊓
        affineSpan ℝ (Set.range (s.reindex e).points))
      x ↔
    x ∈ (s.altitude ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
⊢ x ∈ (s.reindex e).altitude i ↔ x ∈ (s.altitude ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i

Tactic:
simp_rw [altitude, reindex_points, Set.image_comp, Equiv.image_compl]

Premises used: Equiv.image_compl, Affine.Simplex.altitude, Affine.Simplex.reindex_points, Set.image_comp
-- 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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
i : Fin (m + 1)
x : P
⊢ Membership.mem (γ := AffineSubspace ℝ P)
      (mk' ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i)
          (direction
              (affineSpan ℝ
                (s.points '' (Set.image (α := Fin (m + 1)) (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)) {i})ᶜ)))ᗮ ⊓
        affineSpan ℝ (Set.range (s.reindex e).points))
      x ↔
    x ∈ (s.altitude ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i

Tactic:
simp [altitude]

Premises used: Affine.Simplex.altitude
-- 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
i : Fin (n + 1)
⊢ s.points i ∈ s.altitude i

Tactic:
(mem_inf_iff _ _ _).2 ⟨self_mem_mk' _ _, mem_affineSpan ℝ (Set.mem_range_self _)⟩

Premises used: Set.mem_range_self, Iff.mpr, AffineSubspace.self_mem_mk', Real, Set.Mem, mem_affineSpan, And.intro, AffineSubspace.mem_inf_iff
-- 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
i : Fin (n + 1)
rw :
  Eq (α := Submodule ℝ V)
    (direction (mk' (s.points i) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₁ :
  Eq (α := Submodule ℝ V)
    (direction (mk' (s.points i) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ) ⊓
      direction (affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₂ :
  Eq (α := Submodule ℝ V)
    ((direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ direction (affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₃ :
  Eq (α := Submodule ℝ V) ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ direction (affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₄ rw₅ :
  Eq (α := Submodule ℝ V) ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
⊢ (s.altitude i).direction = (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
rw [altitude_def,
    direction_inf_of_mem (self_mem_mk' (s.points i) _) (mem_affineSpan ℝ (Set.mem_range_self _)),
    direction_mk', direction_affineSpan, direction_affineSpan]

Premises used: Set.mem_range_self, AffineSubspace.self_mem_mk', direction_affineSpan, AffineSubspace.direction_inf_of_mem, Affine.Simplex.points, Real, mem_affineSpan, AffineSubspace.direction_mk', Affine.Simplex.altitude_def
-- 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
i : Fin (n + 1)
rw : vectorSpan ℝ (s.points '' {i}ᶜ) ⟂ (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
⊢ vectorSpan ℝ (s.points '' {i}ᶜ) ⟂ (s.altitude i).direction

Tactic:
rw [direction_altitude]

Premises used: Affine.Simplex.direction_altitude
-- 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
i : Fin (n + 1)
⊢ vectorSpan ℝ (s.points '' {i}ᶜ) ⟂ (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
(Submodule.isOrtho_orthogonal_right _).mono_right inf_le_left

Premises used: Submodule.isOrtho_orthogonal_right, Submodule.IsOrtho.mono_right, inf_le_left
-- 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
i : Fin (n + 1)
⊢ vectorSpan ℝ (s.points '' {i}ᶜ) ⟂ (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
exact (Submodule.isOrtho_orthogonal_right _).mono_right inf_le_left

Premises used: Submodule.isOrtho_orthogonal_right, Submodule.IsOrtho.mono_right, inf_le_left
-- 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ (s.map f.toAffineMap ⋯).altitude i = AffineSubspace.map f.toAffineMap (s.altitude i)

Tactic:
(eq_iff_direction_eq_of_mem (p := f (s.points i)) ?_ ?_).mpr ?_

Premises used: Iff.mpr, AffineSubspace.eq_iff_direction_eq_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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
refine_1 : Membership.mem (α := P₂) ((s.map f.toAffineMap ⋯).altitude i) ((f : (a : P) → P₂) (s.points i) : P₂)
refine_2 :
  Membership.mem (α := P₂) (AffineSubspace.map f.toAffineMap (s.altitude i)) ((f : (a : P) → P₂) (s.points i) : P₂)
refine_3 : ((s.map f.toAffineMap ⋯).altitude i).direction = (AffineSubspace.map f.toAffineMap (s.altitude i)).direction
⊢ (s.map f.toAffineMap ⋯).altitude i = AffineSubspace.map f.toAffineMap (s.altitude i)

Tactic:
refine (eq_iff_direction_eq_of_mem (p := f (s.points i)) ?_ ?_).mpr ?_

Premises used: Iff.mpr, AffineSubspace.eq_iff_direction_eq_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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ Membership.mem (α := P₂) ((s.map f.toAffineMap ⋯).altitude i) ((f : (a : P) → P₂) (s.points i) : P₂)

Tactic:
(s.map f.toAffineMap f.injective).mem_altitude i

Premises used: Set.Mem, Affine.Simplex.map, AffineIsometry.toAffineMap, Affine.Simplex.mem_altitude, AffineIsometry.injective
-- 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ Membership.mem (α := P₂) ((s.map f.toAffineMap ⋯).altitude i) ((f : (a : P) → P₂) (s.points i) : P₂)

Tactic:
exact (s.map f.toAffineMap f.injective).mem_altitude i

Premises used: Affine.Simplex.map, AffineIsometry.toAffineMap, Affine.Simplex.mem_altitude, AffineIsometry.injective
-- 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ Membership.mem (α := P₂) (AffineSubspace.map f.toAffineMap (s.altitude i)) ((f : (a : P) → P₂) (s.points i) : P₂)

Tactic:
mem_map_of_mem f.toAffineMap (s.mem_altitude i)

Premises used: Set.Mem, AffineIsometry.toAffineMap, Affine.Simplex.mem_altitude, AffineSubspace.mem_map_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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ Membership.mem (α := P₂) (AffineSubspace.map f.toAffineMap (s.altitude i)) ((f : (a : P) → P₂) (s.points i) : P₂)

Tactic:
exact mem_map_of_mem f.toAffineMap (s.mem_altitude i)

Premises used: AffineIsometry.toAffineMap, Affine.Simplex.mem_altitude, AffineSubspace.mem_map_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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := V) (β := V₂) (⇑f.linear : (a : V) → V₂)

Tactic:
have hf : Function.Injective f.linear := f.linearIsometry.injective
-- 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
rw : s.altitude i = AffineSubspace.map S.subtype (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i)
⊢ AffineSubspace.map S.subtype (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i) = s.altitude i

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ ((s.restrict S hS).map (AffineIsometry.toAffineMap (subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S)) ⋯).altitude i =
    AffineSubspace.map (AffineIsometry.toAffineMap (subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S))
      (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i)

Tactic:
(s.restrict S hS).altitude_map S.subtypeₐᵢ i

Premises used: Affine.Simplex.altitude_map, AffineSubspace.subtypeₐᵢ
-- 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ s.altitude i = AffineSubspace.map S.subtype (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i)

Tactic:
convert! (s.restrict S hS).altitude_map S.subtypeₐᵢ i
-- 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ Nonempty.{u_2 + 1} ↥S

Tactic:
haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
this : Nonempty.{u_2 + 1} ↥S
rw :
  Eq.{u_2 + 1} (α := AffineSubspace ℝ ↥S) (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i : AffineSubspace ℝ ↥S)
    (comap S.subtype (AffineSubspace.map S.subtype (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i)) :
      AffineSubspace ℝ ↥S)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := AffineSubspace ℝ ↥S) (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i : AffineSubspace ℝ ↥S)
    (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i : AffineSubspace ℝ ↥S)
⊢ Eq.{u_2 + 1} (α := AffineSubspace ℝ ↥S) (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i : AffineSubspace ℝ ↥S)
    (comap S.subtype (s.altitude i) : AffineSubspace ℝ ↥S)

Tactic:
rw [← s.map_altitude_restrict S hS, comap_map_eq_of_injective S.subtype_injective]

Premises used: Affine.Simplex.map_altitude_restrict, AffineSubspace.subtype_injective, AffineSubspace.comap_map_eq_of_injective
-- 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
rw : FiniteDimensional.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
⊢ FiniteDimensional.{0, u_1} ℝ ↥(s.altitude i).direction

Tactic:
rw [direction_altitude]

Premises used: Affine.Simplex.direction_altitude
-- 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ FiniteDimensional.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))

Tactic:
infer_instance
-- 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 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
rw : finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = 1
⊢ finrank.{0, u_1} ℝ ↥(s.altitude i).direction = 1

Tactic:
rw [direction_altitude]

Premises used: Affine.Simplex.direction_altitude
-- 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 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))

Tactic:
have h := Submodule.finrank_add_inf_finrank_orthogonal
    (vectorSpan_mono ℝ (Set.image_subset_range s.points {i}ᶜ))
-- 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 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
h :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
⊢ n ≠ 0

Tactic:
have := NeZero.ne n