case pos
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : i₁ = i₂
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁

case neg
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
by_cases h : i₁ = i₂
no goals
case pos
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : i₁ = i₂
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
simp [h]
case neg
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
hc : ↑(card {i₁, i₂}) ≠ 0
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
case neg
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
have hc : (card ({i₁, i₂} : Finset ι) : k) ≠ 0 := by
  rw [card_insert_of_not_mem (not_mem_singleton.2 h), card_singleton]
  norm_num
  exact nonzero_of_invertible _
case neg
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
hc : ↑(card {i₁, i₂}) ≠ 0
⊢ (↑(weightedVSubOfPoint {i₁, i₂} p (p i₁)) fun i => centroidWeights k {i₁, i₂} i) +ᵥ p i₁ =
    2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
case neg
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
hc : ↑(card {i₁, i₂}) ≠ 0
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
rw [centroid_def,
  affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _
    (sum_centroidWeights_eq_one_of_cast_card_ne_zero _ hc) (p i₁)]
no goals
case neg
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
hc : ↑(card {i₁, i₂}) ≠ 0
⊢ (↑(weightedVSubOfPoint {i₁, i₂} p (p i₁)) fun i => centroidWeights k {i₁, i₂} i) +ᵥ p i₁ =
    2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
simp [h, one_add_one_eq_two]
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ ↑(1 + 1) ≠ 0
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ ↑(card {i₁, i₂}) ≠ 0
rw [card_insert_of_not_mem (not_mem_singleton.2 h), card_singleton]
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ ¬2 = 0
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ ↑(1 + 1) ≠ 0
norm_num
no goals
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.484128
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ ¬2 = 0
exact nonzero_of_invertible _