awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Fintype ι
inst_5 : Finite ι'
inst_6 : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
⊢ AffineIndependent k p
have intro : ∀ (val : Fintype ι'), AffineIndependent k p
Tactic: cases nonempty_fintype ι'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Fintype ι
inst_5 : Finite ι'
inst_6 : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val : Fintype ι'
⊢ AffineIndependent k p
have intro : ∀ (w1 w2 : ι' → k),
  Eq.{u₂ + 1} (α := k) (∑ i : ι', w1 i) 1 →
    Eq.{u₂ + 1} (α := k) (∑ i : ι', w2 i) 1 →
      Eq.{u₄ + 1} (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w1 : P)
          ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w2 : P) →
        w1 = w2
Tactic: rw [affineIndependent_iff_eq_of_fintype_affineCombination_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Fintype ι
inst_5 : Finite ι'
inst_6 : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₁ i) 1
hw₂ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₂ i) 1
hweq :
  Eq.{u₄ + 1} (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P)
⊢ w₁ ᵥ* b.toMatrix p = w₂ ᵥ* b.toMatrix p
have h : ∀ (j : ι), (w₁ ᵥ* b.toMatrix p) j = (w₂ ᵥ* b.toMatrix p) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Fintype ι
inst_5 : Finite ι'
inst_6 : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₁ i) 1
hw₂ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₂ i) 1
hweq :
  Eq.{u₄ + 1} (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P)
j : ι
⊢ (w₁ ᵥ* b.toMatrix p) j = (w₂ ᵥ* b.toMatrix p) j
have h : Eq.{u₂ + 1} (α := k) (∑ i : ι', HSMul.hSMul (β := k) (w₁ i) ((b.coord j : (a : P) → k) (p i) : k))
  (∑ i : ι', HSMul.hSMul (β := k) (w₂ i) ((b.coord j : (a : P) → k) (p i) : k))
Tactic: change (∑ i, w₁ i • b.coord j (p i)) = ∑ i, w₂ i • b.coord j (p i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Fintype ι
inst_5 : Finite ι'
inst_6 : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₁ i) 1
hw₂ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₂ i) 1
hweq :
  Eq.{u₄ + 1} (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P)
j : ι
⊢ Eq.{u₂ + 1} (α := k) (∑ i : ι', HSMul.hSMul (β := k) (w₁ i) ((b.coord j : (a : P) → k) (p i) : k))
    (∑ i : ι', HSMul.hSMul (β := k) (w₂ i) ((b.coord j : (a : P) → k) (p i) : k))
have h : Eq.{u₂ + 1} (α := k)
  ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₁ : k)
  (∑ i : ι', HSMul.hSMul (β := k) (w₂ i) ((b.coord j : (a : P) → k) (p i) : k) : k)
Tactic: rw [← Finset.univ.affineCombination_eq_linear_combination _ _ hw₁,
      ← Finset.univ.affineCombination_eq_linear_combination _ _ hw₂,
      ← Function.comp_def (b.coord j) p, ← Finset.univ.map_affineCombination p w₁ hw₁,
      ← Finset.univ.map_affineCombination p w₂ hw₂, hweq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Fintype ι
inst_5 : Finite ι'
inst_6 : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₁ i) 1
hw₂ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₂ i) 1
hweq :
  Eq.{u₄ + 1} (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P)
j : ι
h :
  Eq.{u₂ + 1} (α := k)
    ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₁ : k)
    (∑ i : ι', HSMul.hSMul (β := k) (w₂ i) ((b.coord j : (a : P) → k) (p i) : k) : k)
⊢ Eq.{u₂ + 1} (α := k) (∑ i : ι', HSMul.hSMul (β := k) (w₁ i) ((b.coord j : (a : P) → k) (p i) : k))
    (∑ i : ι', HSMul.hSMul (β := k) (w₂ i) ((b.coord j : (a : P) → k) (p i) : k))
have h₁ : Eq.{u₂ + 1} (α := k)
  ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₁ : k)
  ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₂ : k)
Tactic: rw [← Finset.univ.affineCombination_eq_linear_combination _ _ hw₁,
      ← Finset.univ.affineCombination_eq_linear_combination _ _ hw₂,
      ← Function.comp_def (b.coord j) p, ← Finset.univ.map_affineCombination p w₁ hw₁,
      ← Finset.univ.map_affineCombination p w₂ hw₂, hweq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Fintype ι
inst_5 : Finite ι'
inst_6 : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₁ i) 1
hw₂ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₂ i) 1
hweq :
  Eq.{u₄ + 1} (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P)
j : ι
h :
  Eq.{u₂ + 1} (α := k)
    ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₁ : k)
    (∑ i : ι', HSMul.hSMul (β := k) (w₂ i) ((b.coord j : (a : P) → k) (p i) : k) : k)
h₁ :
  Eq.{u₂ + 1} (α := k)
    ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₁ : k)
    ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₂ : k)
⊢ Eq.{u₂ + 1} (α := k) (∑ i : ι', HSMul.hSMul (β := k) (w₁ i) ((b.coord j : (a : P) → k) (p i) : k))
    (∑ i : ι', HSMul.hSMul (β := k) (w₂ i) ((b.coord j : (a : P) → k) (p i) : k))
have h₂ : Eq.{u₂ + 1} (α := k)
  ((Finset.affineCombination k Finset.univ ((⇑(b.coord j) : (a : P) → k) ∘ p) : (a : ι' → k) → k) w₁ : k)
  ((Finset.affineCombination k Finset.univ ((⇑(b.coord j) : (a : P) → k) ∘ p) : (a : ι' → k) → k) w₂ : k)
Tactic: rw [← Finset.univ.affineCombination_eq_linear_combination _ _ hw₁,
      ← Finset.univ.affineCombination_eq_linear_combination _ _ hw₂,
      ← Function.comp_def (b.coord j) p, ← Finset.univ.map_affineCombination p w₁ hw₁,
      ← Finset.univ.map_affineCombination p w₂ hw₂, hweq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Fintype ι
inst_5 : Finite ι'
inst_6 : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₁ i) 1
hw₂ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₂ i) 1
hweq :
  Eq.{u₄ + 1} (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P)
j : ι
h :
  Eq.{u₂ + 1} (α := k)
    ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₁ : k)
    (∑ i : ι', HSMul.hSMul (β := k) (w₂ i) ((b.coord j : (a : P) → k) (p i) : k) : k)
h₁ :
  Eq.{u₂ + 1} (α := k)
    ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₁ : k)
    ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₂ : k)
h₂ :
  Eq.{u₂ + 1} (α := k)
    ((Finset.affineCombination k Finset.univ ((⇑(b.coord j) : (a : P) → k) ∘ p) : (a : ι' → k) → k) w₁ : k)
    ((Finset.affineCombination k Finset.univ ((⇑(b.coord j) : (a : P) → k) ∘ p) : (a : ι' → k) → k) w₂ : k)
⊢ Eq.{u₂ + 1} (α := k) (∑ i : ι', HSMul.hSMul (β := k) (w₁ i) ((b.coord j : (a : P) → k) (p i) : k))
    (∑ i : ι', HSMul.hSMul (β := k) (w₂ i) ((b.coord j : (a : P) → k) (p i) : k))
have h₃ : Eq.{u₂ + 1} (α := k)
  ((b.coord j : (a : P) → k) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P) : k)
  ((Finset.affineCombination k Finset.univ ((⇑(b.coord j) : (a : P) → k) ∘ p) : (a : ι' → k) → k) w₂ : k)
Tactic: rw [← Finset.univ.affineCombination_eq_linear_combination _ _ hw₁,
      ← Finset.univ.affineCombination_eq_linear_combination _ _ hw₂,
      ← Function.comp_def (b.coord j) p, ← Finset.univ.map_affineCombination p w₁ hw₁,
      ← Finset.univ.map_affineCombination p w₂ hw₂, hweq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Fintype ι
inst_5 : Finite ι'
inst_6 : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₁ i) 1
hw₂ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₂ i) 1
hweq :
  Eq.{u₄ + 1} (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P)
j : ι
h :
  Eq.{u₂ + 1} (α := k)
    ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₁ : k)
    (∑ i : ι', HSMul.hSMul (β := k) (w₂ i) ((b.coord j : (a : P) → k) (p i) : k) : k)
h₁ :
  Eq.{u₂ + 1} (α := k)
    ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₁ : k)
    ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₂ : k)
h₂ :
  Eq.{u₂ + 1} (α := k)
    ((Finset.affineCombination k Finset.univ ((⇑(b.coord j) : (a : P) → k) ∘ p) : (a : ι' → k) → k) w₁ : k)
    ((Finset.affineCombination k Finset.univ ((⇑(b.coord j) : (a : P) → k) ∘ p) : (a : ι' → k) → k) w₂ : k)
h₃ :
  Eq.{u₂ + 1} (α := k)
    ((b.coord j : (a : P) → k) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P) : k)
    ((Finset.affineCombination k Finset.univ ((⇑(b.coord j) : (a : P) → k) ∘ p) : (a : ι' → k) → k) w₂ : k)
⊢ Eq.{u₂ + 1} (α := k) (∑ i : ι', HSMul.hSMul (β := k) (w₁ i) ((b.coord j : (a : P) → k) (p i) : k))
    (∑ i : ι', HSMul.hSMul (β := k) (w₂ i) ((b.coord j : (a : P) → k) (p i) : k))
have h₄ : Eq.{u₂ + 1} (α := k)
  ((b.coord j : (a : P) → k) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P) : k)
  ((b.coord j : (a : P) → k) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P) : k)
Tactic: rw [← Finset.univ.affineCombination_eq_linear_combination _ _ hw₁,
      ← Finset.univ.affineCombination_eq_linear_combination _ _ hw₂,
      ← Function.comp_def (b.coord j) p, ← Finset.univ.map_affineCombination p w₁ hw₁,
      ← Finset.univ.map_affineCombination p w₂ hw₂, hweq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Fintype ι
inst_5 : Finite ι'
inst_6 : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₁ i) 1
hw₂ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₂ i) 1
hweq :
  Eq.{u₄ + 1} (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P)
j : ι
h :
  Eq.{u₂ + 1} (α := k)
    ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₁ : k)
    (∑ i : ι', HSMul.hSMul (β := k) (w₂ i) ((b.coord j : (a : P) → k) (p i) : k) : k)
h₁ :
  Eq.{u₂ + 1} (α := k)
    ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₁ : k)
    ((Finset.affineCombination k Finset.univ fun (i : ι') ↦ (b.coord j : (a : P) → k) (p i) : (a : ι' → k) → k) w₂ : k)
h₂ :
  Eq.{u₂ + 1} (α := k)
    ((Finset.affineCombination k Finset.univ ((⇑(b.coord j) : (a : P) → k) ∘ p) : (a : ι' → k) → k) w₁ : k)
    ((Finset.affineCombination k Finset.univ ((⇑(b.coord j) : (a : P) → k) ∘ p) : (a : ι' → k) → k) w₂ : k)
h₃ :
  Eq.{u₂ + 1} (α := k)
    ((b.coord j : (a : P) → k) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P) : k)
    ((Finset.affineCombination k Finset.univ ((⇑(b.coord j) : (a : P) → k) ∘ p) : (a : ι' → k) → k) w₂ : k)
h₄ :
  Eq.{u₂ + 1} (α := k)
    ((b.coord j : (a : P) → k) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P) : k)
    ((b.coord j : (a : P) → k) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P) : k)
⊢ Eq.{u₂ + 1} (α := k) (∑ i : ι', HSMul.hSMul (β := k) (w₁ i) ((b.coord j : (a : P) → k) (p i) : k))
    (∑ i : ι', HSMul.hSMul (β := k) (w₂ i) ((b.coord j : (a : P) → k) (p i) : k))
have h₅ : Eq.{u₂ + 1} (α := k)
  ((b.coord j : (a : P) → k) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P) : k)
  ((b.coord j : (a : P) → k) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P) : k)
Tactic: rw [← Finset.univ.affineCombination_eq_linear_combination _ _ hw₁,
      ← Finset.univ.affineCombination_eq_linear_combination _ _ hw₂,
      ← Function.comp_def (b.coord j) p, ← Finset.univ.map_affineCombination p w₁ hw₁,
      ← Finset.univ.map_affineCombination p w₂ hw₂, hweq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (hypothesis)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Fintype ι
inst_5 : Finite ι'
inst_6 : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₁ i) 1
hw₂ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₂ i) 1
hweq :
  Eq.{u₄ + 1} (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P)
⊢ w₁ = w₂
have hweq' : w₁ ᵥ* b.toMatrix p = w₂ ᵥ* b.toMatrix p
Tactic: have hweq' : w₁ ᵥ* b.toMatrix p = w₂ ᵥ* b.toMatrix p := by
    ext j
    change (∑ i, w₁ i • b.coord j (p i)) = ∑ i, w₂ i • b.coord j (p i)
    rw [← Finset.univ.affineCombination_eq_linear_combination _ _ hw₁,
      ← Finset.univ.affineCombination_eq_linear_combination _ _ hw₂,
      ← Function.comp_def (b.coord j) p, ← Finset.univ.map_affineCombination p w₁ hw₁,
      ← Finset.univ.map_affineCombination p w₂ hw₂, hweq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (hypothesis)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Fintype ι
inst_5 : Finite ι'
inst_6 : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₁ i) 1
hw₂ : Eq.{u₂ + 1} (α := k) (∑ i : ι', w₂ i) 1
hweq :
  Eq.{u₄ + 1} (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₁ : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) w₂ : P)
hweq' : w₁ ᵥ* b.toMatrix p = w₂ ᵥ* b.toMatrix p
⊢ w₁ = w₂
have hweq'₁ : Eq (α := ι' → k) ((fun (w : ι → k) ↦ w ᵥ* A) (w₁ ᵥ* b.toMatrix p)) ((fun (w : ι → k) ↦ w ᵥ* A) (w₂ ᵥ* b.toMatrix p))
Tactic: replace hweq' := congr_arg (fun w => w ᵥ* A) hweq'
Cleared hypotheses: hweq'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
⊢ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
have intro : ∀ (val : Fintype ι), Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
this : ∀ (i : ι), Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (range p)) ((b : (a : ι) → P) i : P)
⊢ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
have rw : range.{u₄, u₁ + 1} (ι := ι) (⇑b : (a : ι) → P) ⊆ (↑(affineSpan k (range p)) : Set P)
Tactic: rw [eq_top_iff, ← b.tot, affineSpan_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
⊢ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
have intro : ∀ (i : ι), Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (range p)) ((b : (a : ι) → P) i : P)
Tactic: suffices ∀ i, b i ∈ affineSpan k (range p) by
    rw [eq_top_iff, ← b.tot, affineSpan_le]
    rintro q ⟨i, rfl⟩
    exact this i
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
⊢ Eq.{u₂ + 1} (α := k) (∑ j : ι', ∑ l : ι, A i j * b.toMatrix p j l) (∑ l : ι, ∑ j : ι', A i j * b.toMatrix p j l)
have rw : Eq.{u₂ + 1} (α := k) (∑ y : ι, ∑ x : ι', A i x * b.toMatrix p x y) (∑ l : ι, ∑ j : ι', A i j * b.toMatrix p j l)
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
⊢ Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
have A₁ : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) (∑ j : ι', A i j * ∑ l : ι, b.toMatrix p j l)
Tactic: calc
      ∑ j, A i j = ∑ j, A i j * ∑ l, b.toMatrix p j l := by simp
      _ = ∑ j, ∑ l, A i j * b.toMatrix p j l := by simp_rw [Finset.mul_sum]
      _ = ∑ l, ∑ j, A i j * b.toMatrix p j l := by rw [Finset.sum_comm]
      _ = ∑ l, (A * b.toMatrix p) i l := rfl
      _ = 1 := by simp [hA, Matrix.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
A₁ : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) (∑ j : ι', A i j * ∑ l : ι, b.toMatrix p j l)
⊢ Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
have A₂ : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j * ∑ l : ι, b.toMatrix p j l) (∑ j : ι', ∑ l : ι, A i j * b.toMatrix p j l)
Tactic: calc
      ∑ j, A i j = ∑ j, A i j * ∑ l, b.toMatrix p j l := by simp
      _ = ∑ j, ∑ l, A i j * b.toMatrix p j l := by simp_rw [Finset.mul_sum]
      _ = ∑ l, ∑ j, A i j * b.toMatrix p j l := by rw [Finset.sum_comm]
      _ = ∑ l, (A * b.toMatrix p) i l := rfl
      _ = 1 := by simp [hA, Matrix.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
A₁ : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) (∑ j : ι', A i j * ∑ l : ι, b.toMatrix p j l)
A₂ : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j * ∑ l : ι, b.toMatrix p j l) (∑ j : ι', ∑ l : ι, A i j * b.toMatrix p j l)
⊢ Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
have A₃ : Eq.{u₂ + 1} (α := k) (∑ j : ι', ∑ l : ι, A i j * b.toMatrix p j l) (∑ l : ι, ∑ j : ι', A i j * b.toMatrix p j l)
Tactic: calc
      ∑ j, A i j = ∑ j, A i j * ∑ l, b.toMatrix p j l := by simp
      _ = ∑ j, ∑ l, A i j * b.toMatrix p j l := by simp_rw [Finset.mul_sum]
      _ = ∑ l, ∑ j, A i j * b.toMatrix p j l := by rw [Finset.sum_comm]
      _ = ∑ l, (A * b.toMatrix p) i l := rfl
      _ = 1 := by simp [hA, Matrix.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
A₁ : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) (∑ j : ι', A i j * ∑ l : ι, b.toMatrix p j l)
A₂ : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j * ∑ l : ι, b.toMatrix p j l) (∑ j : ι', ∑ l : ι, A i j * b.toMatrix p j l)
A₃ : Eq.{u₂ + 1} (α := k) (∑ j : ι', ∑ l : ι, A i j * b.toMatrix p j l) (∑ l : ι, ∑ j : ι', A i j * b.toMatrix p j l)
⊢ Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
have A₄ : Eq.{u₂ + 1} (α := k) (∑ l : ι, (A * b.toMatrix p) i l) 1
Tactic: calc
      ∑ j, A i j = ∑ j, A i j * ∑ l, b.toMatrix p j l := by simp
      _ = ∑ j, ∑ l, A i j * b.toMatrix p j l := by simp_rw [Finset.mul_sum]
      _ = ∑ l, ∑ j, A i j * b.toMatrix p j l := by rw [Finset.sum_comm]
      _ = ∑ l, (A * b.toMatrix p) i l := rfl
      _ = 1 := by simp [hA, Matrix.one_apply]