-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem centroid_eq_iff [CharZero k] {n : ℕ} (s : Simplex k P n) {fs₁ fs₂ : Finset (Fin (n + 1))}
    {m₁ m₂ : ℕ} (h₁ : #fs₁ = m₁ + 1) (h₂ : #fs₂ = m₂ + 1) :
    fs₁.centroid k s.points = fs₂.centroid k s.points ↔ fs₁ = fs₂

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n✝ : ℕ
s : Simplex k P n✝
fs₁ fs₂ : Finset (Fin (n✝ + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h✝ :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n✝ + 1)
ha : (↑fs₁).indicator (const (Fin (n✝ + 1)) (↑(m₁ + 1))⁻¹) i = (↑fs₂).indicator (const (Fin (n✝ + 1)) (↑(m₂ + 1))⁻¹) i
n : ℕ
h : ↑n + 1 = 0
⊢ False

Tactic:
norm_cast at h

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
ha :
  ∀ (x : Fin (n + 1)),
    (↑fs₁).indicator (const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) x = (↑fs₂).indicator (const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) x
⊢ fs₁ = fs₂

Tactic:
ext i

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
ha :
  ∀ (x : Fin (n + 1)),
    (↑fs₁).indicator (const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) x = (↑fs₂).indicator (const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) x
i : Fin (n + 1)
⊢ i ∈ fs₁ ↔ i ∈ fs₂

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha : (↑fs₁).indicator (const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i = (↑fs₂).indicator (const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
key : ∀ (n : ℕ), ↑n + 1 ≠ 0
⊢ i ∈ fs₁ ↔ i ∈ fs₂

Tactic:
constructor <;> intro hi <;> by_contra hni

Result:
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha : (↑fs₁).indicator (const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i = (↑fs₂).indicator (const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
key : ∀ (n : ℕ), ↑n + 1 ≠ 0
hi : i ∈ fs₁
hni : i ∉ fs₂
⊢ False

case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha : (↑fs₁).indicator (const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i = (↑fs₂).indicator (const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
key : ∀ (n : ℕ), ↑n + 1 ≠ 0
hi : i ∈ fs₂
hni : i ∉ fs₁
⊢ False

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
ha : (↑univ).indicator (centroidWeightsIndicator k fs₁) = (↑univ).indicator (centroidWeightsIndicator k fs₂)
⊢ fs₁ = fs₂

Tactic:
simp_rw [Finset.coe_univ, Set.indicator_univ, funext_iff,
  Finset.centroidWeightsIndicator_def, Finset.centroidWeights, h₁, h₂] at ha

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
ha :
  ∀ (x : Fin (n + 1)),
    (↑fs₁).indicator (const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) x = (↑fs₂).indicator (const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) x
⊢ fs₁ = fs₂

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha : (↑fs₁).indicator (const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i = (↑fs₂).indicator (const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
⊢ i ∈ fs₁ ↔ i ∈ fs₂

Tactic:
have key : ∀ n : ℕ, (n : k) + 1 ≠ 0 := fun n h => by norm_cast at h

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha : (↑fs₁).indicator (const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i = (↑fs₂).indicator (const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
key : ∀ (n : ℕ), ↑n + 1 ≠ 0
⊢ i ∈ fs₁ ↔ i ∈ fs₂

Proof state:
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha : (↑fs₁).indicator (const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i = (↑fs₂).indicator (const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
key : ∀ (n : ℕ), ↑n + 1 ≠ 0
hi : i ∈ fs₂
hni : i ∉ fs₁
⊢ False

Tactic:
simpa [hni, hi, key] using ha.symm

Result:
no goals