awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  Membership.mem (α := P) (γ := AffineSubspace k P)
    (affineSpan k
      (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i₁ 1) : P)
        (singleton (α := P)
          ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i₂ i₃ c) : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)
refine_2 :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (1 - c) : SignType)
    ((SignType.sign : (a : k) → SignType) c : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (affineCombinationLineMapWeights i₂ i₃ c i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (affineCombinationLineMapWeights i₂ i₃ c i₃) : SignType)

Tactic:
rw [Finset.affineCombinationLineMapWeights_apply_left h₂₃,
      Finset.affineCombinationLineMapWeights_apply_right h₂₃]

Premises used: Finset.affineCombinationLineMapWeights_apply_left, Finset.affineCombinationLineMapWeights_apply_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  Membership.mem (α := P) (γ := AffineSubspace k P)
    (affineSpan k
      (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i₁ 1) : P)
        (singleton (α := P)
          ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i₂ i₃ c) : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (1 - c) : SignType)
    ((SignType.sign : (a : k) → SignType) c : SignType)

Tactic:
simp_all only [sub_pos, sign_pos]

Premises used: sub_pos, sign_pos
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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
q : ι' → P
i : ι'
j : ι
⊢ b.toMatrix q i j = (b.coord j : (a : P) → k) (q i)

Tactic:
rfl

Premises used: AffineBasis.toMatrix, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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
inst_4 : DecidableEq ι
a : ∀ (i j : ι), b.toMatrix (⇑b : (a : ι) → P) i j = 1 i j
⊢ Eq (α := Matrix ι ι k) (b.toMatrix (⇑b : (a : ι) → P)) 1

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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
inst_4 : DecidableEq ι
i j : ι
a : Eq.{u₂ + 1} (α := k) ((b.coord j : (a : P) → k) ((b : (a : ι) → P) i : P) : k) (1 i j : k)
a₁ : Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0) (1 i j)
a₂ : Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0 : k) (Pi.single (M := fun (x : ι) ↦ k) i 1 j : k)
a₃ a₄ : Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0) (if j = i then 1 else 0)
⊢ b.toMatrix (⇑b : (a : ι) → P) i j = 1 i j

Tactic:
rw [toMatrix_apply, coord_apply, Matrix.one_eq_pi_single, Pi.single_apply]

Premises used: AffineBasis.coord_apply, Pi.single_apply, Matrix.one_eq_pi_single, AffineBasis.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 ι
q : ι' → P
i : ι'
⊢ Eq.{u₂ + 1} (α := k) (∑ j : ι, b.toMatrix q i j) 1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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
intro : ∀ (val : Fintype ι'), AffineIndependent k p
⊢ AffineIndependent k p

Tactic:
cases nonempty_fintype ι'

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 ι'
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
⊢ AffineIndependent k p

Tactic:
rw [affineIndependent_iff_eq_of_fintype_affineCombination_eq]

Premises used: affineIndependent_iff_eq_of_fintype_affineCombination_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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)
h : ∀ (j : ι), (w₁ ᵥ* b.toMatrix p) j = (w₂ ᵥ* b.toMatrix p) j
⊢ w₁ ᵥ* b.toMatrix p = w₂ ᵥ* b.toMatrix p

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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) (∑ 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))
⊢ (w₁ ᵥ* b.toMatrix p) j = (w₂ ᵥ* b.toMatrix p) j

Tactic:
change (∑ i, w₁ i • b.coord j (p i)) = ∑ i, w₂ i • b.coord j (p i)

Premises used: Finset.univ, AffineBasis.coord, HSMul.hSMul, DFunLike.coe, Finset.sum
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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)
h₅ 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))

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]

Premises used: Finset.univ, Finset.affineCombination_eq_linear_combination, AffineBasis.coord, Finset.map_affineCombination, Function.comp_def, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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

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]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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
⊢ 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'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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' :
  Eq (α := ι' → k) ((fun (w : ι → k) ↦ w ᵥ* A) (w₁ ᵥ* b.toMatrix p)) ((fun (w : ι → k) ↦ w ᵥ* A) (w₂ ᵥ* b.toMatrix p))
⊢ w₁ = w₂

Tactic:
simpa only [Matrix.vecMul_vecMul, hA, Matrix.vecMul_one] using hweq'

Premises used: Matrix.vecMul_vecMul, Matrix.vecMul_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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
intro : ∀ (val : Fintype ι), Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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)
rw : range.{u₄, u₁ + 1} (ι := ι) (⇑b : (a : ι) → P) ⊆ (↑(affineSpan k (range p)) : Set P)
⊢ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤

Tactic:
rw [eq_top_iff, ← b.tot, affineSpan_le]

Premises used: AffineBasis.tot, eq_top_iff, affineSpan_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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)
i : ι
⊢ Membership.mem (α := P) (↑(affineSpan k (range p)) : Set P) ((b : (a : ι) → P) i : P)

Tactic:
this i
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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)
i : ι
⊢ Membership.mem (α := P) (↑(affineSpan k (range p)) : Set P) ((b : (a : ι) → P) i : P)

Tactic:
exact this i
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 ι
intro : ∀ (i : ι), Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (range p)) ((b : (a : ι) → P) i : P)
⊢ Eq (α := AffineSubspace k P) (affineSpan k (range 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
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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) (∑ j : ι', A i j * ∑ l : ι, b.toMatrix p j l)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 * ∑ l : ι, b.toMatrix p j l) (∑ j : ι', ∑ l : ι, A i j * b.toMatrix p j l)

Tactic:
simp_rw [Finset.mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : ι
rw 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)
⊢ 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:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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) (∑ l : ι, ∑ j : ι', A i j * b.toMatrix p j l) (∑ l : ι, (A * b.toMatrix p) i l)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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) (∑ l : ι, (A * b.toMatrix p) i l) 1

Tactic:
simp [hA, Matrix.one_apply]

Premises used: Matrix.one_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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)
A₄ : Eq.{u₂ + 1} (α := k) (∑ l : ι, (A * b.toMatrix p) i l) 1
⊢ Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 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]

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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

Tactic:
have hAi : ∑ j, A i j = 1 := by
    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]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
apply :
  ∀ (i_1 : ι),
    Eq.{u₂ + 1} (α := k) ((b.coord i_1 : (a : P) → k) ((b : (a : ι) → P) i : P) : k)
      ((b.coord i_1 : (a : P) → k) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P) : k)
⊢ Eq.{u₄ + 1} (α := P) ((b : (a : ι) → P) i : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P)

Tactic:
apply b.ext_elem

Premises used: AffineBasis.ext_elem
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
j : ι
rw :
  Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0)
    (∑ i_1 : ι', HSMul.hSMul (β := k) (A i i_1) (((⇑(b.coord j) : (a : P) → k) ∘ p) i_1))
⊢ Eq.{u₂ + 1} (α := k) ((b.coord j : (a : P) → k) ((b : (a : ι) → P) i : P) : k)
    ((b.coord j : (a : P) → k) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P) : k)

Tactic:
rw [b.coord_apply, Finset.univ.map_affineCombination _ _ hAi,
      Finset.univ.affineCombination_eq_linear_combination _ _ hAi]

Premises used: Finset.univ, AffineBasis.coord_apply, Finset.affineCombination_eq_linear_combination, Finset.map_affineCombination
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
j : ι
change : (if j = i then 1 else 0) = (A * b.toMatrix p) i j
⊢ Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0)
    (∑ i_1 : ι', HSMul.hSMul (β := k) (A i i_1) (((⇑(b.coord j) : (a : P) → k) ∘ p) i_1))

Tactic:
change _ = (A * b.toMatrix p) i j

Premises used: HMul.hMul, AffineBasis.toMatrix