awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
p : P
ht : (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw :
  (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P) =
    s.touchpoint signs i
rw₁ :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
⊢ p = s.touchpoint signs i
have rw₂ : Eq.{u_2 + 1} (α := P)
  (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
          (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
        (s.exsphere signs).center) :
    P)
  (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
          (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
        (s.excenter signs)) :
    P)
Tactic: rw [ht.eq_orthogonalProjection, touchpoint, orthogonalProjectionSpan, excenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
p : P
ht : (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw :
  (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P) =
    s.touchpoint signs i
rw₁ :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
rw₂ :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
⊢ p = s.touchpoint signs i
have rw₃ : Eq.{u_2 + 1} (α := P)
  (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
          (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
        (s.exsphere signs).center) :
    P)
  (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
          (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
        (s.exsphere signs).center) :
    P)
Tactic: rw [ht.eq_orthogonalProjection, touchpoint, orthogonalProjectionSpan, excenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
p : P
⊢ (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points)) ↔ p = s.touchpoint signs i
have refine : p = s.touchpoint signs i → (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points))
Tactic: refine ⟨eq_touchpoint_of_isTangentAt_exsphere, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
hf : Fact (Module.finrank ℝ V = n)
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
    ((s.exsphere signs).orthRadius (s.touchpoint signs i))
have refine : Module.finrank.{0, u_1} ℝ ↥(AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite i).points))) + 1 =
  Module.finrank ℝ V
Tactic: refine (h.isTangentAt_touchpoint i).eq_orthRadius_of_finrank_add_one_eq (h.exradius_pos.ne') ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
hf : Fact (Module.finrank ℝ V = n)
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ Module.finrank.{0, u_1} ℝ ↥(AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite i).points))) + 1 =
    Module.finrank ℝ V
have rw : n - 1 + 1 = n
Tactic: rw [direction_affineSpan, (s.faceOpposite i).independent.finrank_vectorSpan_add_one,
    Fintype.card_fin, hf.out]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
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
hf : Fact (Module.finrank ℝ V = n)
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ n - 1 + 1 = n
have this : n ≠ 0
Tactic: have := NeZero.ne n
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
signs : Finset (Fin (n + 1))
⊢ (∃ (r : ℝ), ∀ (i : Fin (n + 1)), (s.signedInfDist i : (a : P) → ℝ) p = (if i ∈ signs then -1 else 1) * r) ↔
    s.ExcenterExists signs ∧ p = s.excenter signs
have refine_1 : (∃ (r : ℝ), ∀ (i : Fin (n + 1)), (s.signedInfDist i : (a : P) → ℝ) p = (if i ∈ signs then -1 else 1) * r) →
  s.ExcenterExists signs ∧ p = s.excenter signs
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
signs : Finset (Fin (n + 1))
refine_1 :
  (∃ (r : ℝ), ∀ (i : Fin (n + 1)), (s.signedInfDist i : (a : P) → ℝ) p = (if i ∈ signs then -1 else 1) * r) →
    s.ExcenterExists signs ∧ p = s.excenter signs
⊢ (∃ (r : ℝ), ∀ (i : Fin (n + 1)), (s.signedInfDist i : (a : P) → ℝ) p = (if i ∈ signs then -1 else 1) * r) ↔
    s.ExcenterExists signs ∧ p = s.excenter signs
have refine_2 : s.ExcenterExists signs ∧ p = s.excenter signs →
  ∃ (r : ℝ), ∀ (i : Fin (n + 1)), (s.signedInfDist i : (a : P) → ℝ) p = (if i ∈ signs then -1 else 1) * r
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
signs : Finset (Fin (n + 1))
r : ℝ
h : ∀ (i : Fin (n + 1)), (s.signedInfDist i : (a : P) → ℝ) p = (if i ∈ signs then -1 else 1) * r
⊢ s.ExcenterExists signs ∧ p = s.excenter signs
have refine_1 : ∀ (w : Fin (n + 1) → ℝ) (h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1)
  (hp :
    Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P))
  (h :
    ∀ (i : Fin (n + 1)),
      (s.signedInfDist i : (a : P) → ℝ)
          ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
        (if i ∈ signs then -1 else 1) * r),
  s.ExcenterExists signs ∧
    (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.excenter signs
Tactic: obtain ⟨w, h1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp
Cleared hypotheses: p, hp, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
⊢ w i * ‖s.points i -ᵥ s.altitudeFoot i‖ = (if i ∈ signs then -1 else 1) * r
have rw : (s.signedInfDist i : (a : P) → ℝ)
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
  (if i ∈ signs then -1 else 1) * r
Tactic: rw [altitudeFoot, ← s.signedInfDist_affineCombination i h1]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
⊢ s.ExcenterExists signs ∧
    (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.excenter signs
have h' : ∀ (i : Fin (n + 1)), w i * ‖s.points i -ᵥ s.altitudeFoot i‖ = (if i ∈ signs then -1 else 1) * r
Tactic: have h' : ∀ i, w i * ‖s.points i -ᵥ s.altitudeFoot i‖ = (if i ∈ signs then -1 else 1) * r := by
      intro i
      rw [altitudeFoot, ← s.signedInfDist_affineCombination i h1]
      exact h i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
h' : ∀ (i : Fin (n + 1)), w i * ‖s.points i -ᵥ s.altitudeFoot i‖ = (if i ∈ signs then -1 else 1) * r
⊢ s.ExcenterExists signs ∧
    (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.excenter signs
have h'₁ : ∀ (i : Fin (n + 1)), w i * dist (s.points i) (s.altitudeFoot i) = (if i ∈ signs then -1 else 1) * r
Tactic: simp_rw [← dist_eq_norm_vsub] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
h' : ∀ (i : Fin (n + 1)), w i * dist (s.points i) (s.altitudeFoot i) = (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
⊢ w i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
have h'₁ : w i * dist (s.points i) (s.altitudeFoot i) = (if i ∈ signs then -1 else 1) * r
Tactic: replace h' := h' i
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
h' : w i * dist (s.points i) (s.altitudeFoot i) = (if i ∈ signs then -1 else 1) * r
⊢ w i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
have h'₁ : w i = (if i ∈ signs then -1 else 1) * r / s.height i
Tactic: rw [← height, ← eq_div_iff (s.height_pos i).ne'] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
h' : w i = (if i ∈ signs then -1 else 1) * r / s.height i
⊢ w i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
have rw : (if i ∈ signs then -1 else 1) * r / s.height i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
Tactic: rw [h', mul_comm, div_eq_mul_inv, mul_assoc, height, altitudeFoot, orthogonalProjectionSpan]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
h' : w i = (if i ∈ signs then -1 else 1) * r / s.height i
rw : (if i ∈ signs then -1 else 1) * r / s.height i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
⊢ w i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
have rw₁ : (r * if i ∈ signs then -1 else 1) / s.height i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
Tactic: rw [h', mul_comm, div_eq_mul_inv, mul_assoc, height, altitudeFoot, orthogonalProjectionSpan]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
h' : w i = (if i ∈ signs then -1 else 1) * r / s.height i
rw : (if i ∈ signs then -1 else 1) * r / s.height i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
rw₁ : (r * if i ∈ signs then -1 else 1) / s.height i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
⊢ w i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
have rw₂ : (r * if i ∈ signs then -1 else 1) * (s.height i)⁻¹ = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
Tactic: rw [h', mul_comm, div_eq_mul_inv, mul_assoc, height, altitudeFoot, orthogonalProjectionSpan]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
h' : w i = (if i ∈ signs then -1 else 1) * r / s.height i
rw : (if i ∈ signs then -1 else 1) * r / s.height i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
rw₁ : (r * if i ∈ signs then -1 else 1) / s.height i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
rw₂ : (r * if i ∈ signs then -1 else 1) * (s.height i)⁻¹ = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
⊢ w i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
have rw₃ : r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹) = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
Tactic: rw [h', mul_comm, div_eq_mul_inv, mul_assoc, height, altitudeFoot, orthogonalProjectionSpan]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
h' : w i = (if i ∈ signs then -1 else 1) * r / s.height i
rw : (if i ∈ signs then -1 else 1) * r / s.height i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
rw₁ : (r * if i ∈ signs then -1 else 1) / s.height i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
rw₂ : (r * if i ∈ signs then -1 else 1) * (s.height i)⁻¹ = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
rw₃ : r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹) = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
⊢ w i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
have rw₄ : r * ((if i ∈ signs then -1 else 1) * (dist (s.points i) (s.altitudeFoot i))⁻¹) =
  r * ((if i ∈ signs then -1 else 1) * (dist (s.points i) (s.altitudeFoot i))⁻¹)
Tactic: rw [h', mul_comm, div_eq_mul_inv, mul_assoc, height, altitudeFoot, orthogonalProjectionSpan]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
h' : w i = (if i ∈ signs then -1 else 1) * r / s.height i
rw : (if i ∈ signs then -1 else 1) * r / s.height i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
rw₁ : (r * if i ∈ signs then -1 else 1) / s.height i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
rw₂ : (r * if i ∈ signs then -1 else 1) * (s.height i)⁻¹ = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
rw₃ : r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹) = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
rw₄ :
  r * ((if i ∈ signs then -1 else 1) * (dist (s.points i) (s.altitudeFoot i))⁻¹) =
    r * ((if i ∈ signs then -1 else 1) * (dist (s.points i) (s.altitudeFoot i))⁻¹)
⊢ w i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
have rw₅ : r *
    ((if i ∈ signs then -1 else 1) *
      (dist (s.points i)
          (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                (s.points i)) :
            P))⁻¹) =
  r *
    ((if i ∈ signs then -1 else 1) *
      (dist (s.points i)
          (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                (s.points i)) :
            P))⁻¹)
Tactic: rw [h', mul_comm, div_eq_mul_inv, mul_assoc, height, altitudeFoot, orthogonalProjectionSpan]