awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_2
inst : Ring k
inst_1 : Fintype ι
w : ι → k
⊢ Membership.mem (γ := AffineSubspace k (ι → k)) (fintypeAffineCoords ι k) w ↔ Eq.{u_2 + 1} (α := k) (∑ i : ι, w i) 1

Tactic:
simp [fintypeAffineCoords, Fintype.linearCombination_apply]

Premises used: Fintype.linearCombination_apply, fintypeAffineCoords
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
h : AffineIndependent k p
⊢ InjOn (β := P) (⇑(Finset.affineCombination k Finset.univ p) : (a : ι → k) → P)
    (↑(fintypeAffineCoords ι k) : Set (ι → k))

Tactic:
fun w₁ hw₁ w₂ hw₂ he ↦ (affineIndependent_iff_eq_of_fintype_affineCombination_eq k p).1
    h w₁ w₂ (mem_fintypeAffineCoords_iff_sum.1 hw₁) (mem_fintypeAffineCoords_iff_sum.1 hw₂) he

Premises used: affineIndependent_iff_eq_of_fintype_affineCombination_eq, Iff.mp, mem_fintypeAffineCoords_iff_sum, Set.InjOn
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_2
inst : Ring k
w : ι →₀ k
⊢ Membership.mem (γ := AffineSubspace k (ι →₀ k)) (finsuppAffineCoords ι k) w ↔
    Eq.{u_2 + 1} (α := k) ((Finsupp.linearCombination k 1 : (a : ι →₀ k) → k) w : k) (1 : k)

Tactic:
simp [finsuppAffineCoords]

Premises used: finsuppAffineCoords
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
⊢ Eq (α := AffineSubspace k PUnit.{u_8 + 1}) (affineSpan k (range id)) ⊤

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
f g : AffineBasis ι k P
h : f.toFun = g.toFun
mk :
  ∀ (toFun : ι → P) (ind' : AffineIndependent k toFun)
    (tot' : Eq (α := AffineSubspace k P) (affineSpan k (range toFun)) ⊤)
    (h : { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P }.toFun = g.toFun),
    { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
g : AffineBasis ι k P
toFun : ι → P
ind' : AffineIndependent k toFun
tot' : Eq (α := AffineSubspace k P) (affineSpan k (range toFun)) ⊤
h : { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P }.toFun = g.toFun
mk :
  ∀ (toFun_1 : ι → P) (ind'_1 : AffineIndependent k toFun_1)
    (tot'_1 : Eq (α := AffineSubspace k P) (affineSpan k (range toFun_1)) ⊤)
    (h :
      { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P }.toFun =
        { toFun := toFun_1, ind' := ind'_1, tot' := tot'_1 : AffineBasis ι k P }.toFun),
    { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P } =
      { toFun := toFun_1, ind' := ind'_1, tot' := tot'_1 }
⊢ { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P } = g

Tactic:
cases g
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
toFun : ι → P
ind' : AffineIndependent k toFun
tot' : Eq (α := AffineSubspace k P) (affineSpan k (range toFun)) ⊤
toFun_1 : ι → P
ind'_1 : AffineIndependent k toFun_1
tot'_1 : Eq (α := AffineSubspace k P) (affineSpan k (range toFun_1)) ⊤
h :
  { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P }.toFun =
    { toFun := toFun_1, ind' := ind'_1, tot' := tot'_1 : AffineBasis ι k P }.toFun
⊢ { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P } =
    { toFun := toFun_1, ind' := ind'_1, tot' := tot'_1 }

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b₁ b₂ : AffineBasis ι k P
h : Eq (α := (a : ι) → P) (⇑b₁ : (a : ι) → P) (⇑b₂ : (a : ι) → P)
⊢ b₁ = b₂

Tactic:
DFunLike.coe_injective h

Premises used: DFunLike.coe_injective
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
⊢ AffineIndependent.{u_5, u_6, u_7, u_1} k (P := P) (ι := ι) (⇑b : (a : ι) → P)

Tactic:
b.ind'

Premises used: AffineBasis.ind'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
⊢ Eq.{u_7 + 1} (α := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) ⊤

Tactic:
b.tot'

Premises used: AffineBasis.tot'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
hι : IsEmpty ι
⊢ False

Tactic:
simpa only [@range_eq_empty _ _ hι, AffineSubspace.span_empty, bot_ne_top] using b.tot

Premises used: AffineBasis.tot, AffineSubspace.span_empty, bot_ne_top, Set.range_eq_empty
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e_1 e : ι ≃ ι'
rw : Eq.{u_7 + 1} (α := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) ⊤
⊢ Eq.{u_7 + 1} (α := AffineSubspace k P)
    (affineSpan k
      (range.{u_7, u_2 + 1} (ι := ι')
        (Function.comp.{u_2 + 1, u_1 + 1, u_7 + 1} (β := ι) (⇑b : (a : ι) → P) (⇑e.symm : (a : ι') → ι))))
    ⊤

Tactic:
rw [e.symm.surjective.range_comp]

Premises used: Function.Surjective.range_comp, Equiv.surjective, Equiv.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e_1 e : ι ≃ ι'
⊢ Eq.{u_7 + 1} (α := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) ⊤

Tactic:
b.3

Premises used: AffineBasis.tot'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e_1 e : ι ≃ ι'
⊢ Eq.{u_7 + 1} (α := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) ⊤

Tactic:
exact b.3

Premises used: AffineBasis.tot'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
⊢ Eq (α := (a : ι') → P) (⇑(b.reindex e) : (a : ι') → P)
    (Function.comp.{u_2 + 1, u_1 + 1, u_7 + 1} (β := ι) (⇑b : (a : ι) → P) (⇑e.symm : (a : ι') → ι))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
i' : ι'
⊢ Eq.{u_7 + 1} (α := P) ((b.reindex e : (a : ι') → P) i' : P) ((b : (a : ι) → P) ((e.symm : (a : ι') → ι) i' : ι) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
⊢ b.reindex (Equiv.refl ι) = b

Tactic:
ext rfl

Premises used: AffineBasis.ext, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
this :
  Eq (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
rw :
  LE.le (α := Submodule k V) ⊤
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
rw₁ :
  LE.le (α := Submodule k V) ⊤
    (AffineSubspace.direction.{u_5, u_6, u_7} (P := P)
      (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))))
rw₂ : LE.le (α := Submodule k V) ⊤ (AffineSubspace.direction.{u_5, u_6, u_7} (P := P) ⊤)
rw₃ rw₄ : LE.le.{u_6} (α := Submodule k V) ⊤ ⊤
⊢ LE.le.{u_6} (α := Submodule k V) ⊤
    (Submodule.span k
      (range fun (i_2 : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑i_2 : ι) : P) ((b : (a : ι) → P) i : P)))

Tactic:
rw [this, ← direction_affineSpan, b.tot, AffineSubspace.direction_top]

Premises used: direction_affineSpan, AffineBasis.tot, AffineSubspace.direction_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
k₁ :
  Eq (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
⊢ LE.le.{u_6} (α := Submodule k V) ⊤
    (Submodule.span k
      (range fun (i_2 : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑i_2 : ι) : P) ((b : (a : ι) → P) i : P)))

Tactic:
suffices
        Submodule.span k (range fun j : { x // x ≠ i } => b ↑j -ᵥ b i) = vectorSpan k (range b) by
        rw [this, ← direction_affineSpan, b.tot, AffineSubspace.direction_top]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
rw : vectorSpan.{u_5, u_6, u_7} k (P := P) (image.{u_1, u_7} (α := ι) (⇑b : (a : ι) → P) univ)
| vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
conv_rhs :
  Eq (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (image.{u_1, u_7} (α := ι) (⇑b : (a : ι) → P) univ))
⊢ Eq (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))

Tactic:
conv_rhs => rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
rw :
  Eq.{u_6 + 1} (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (Submodule.span k ((fun (x : P) ↦ x -ᵥ (b : (a : ι) → P) i) '' image (α := ι) (⇑b : (a : ι) → P) (univ \ {i})))
⊢ Eq (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (image.{u_1, u_7} (α := ι) (⇑b : (a : ι) → P) univ))

Tactic:
rw [vectorSpan_image_eq_span_vsub_set_right_ne k b (mem_univ i)]

Premises used: vectorSpan_image_eq_span_vsub_set_right_ne, Set.mem_univ, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
e_s :
  Eq.{u_6 + 1} (α := Set V)
    (range fun (j : { x : ι // x ≠ i }) ↦
      VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P))
    ((fun (x : P) ↦ x -ᵥ (b : (a : ι) → P) i) '' image (α := ι) (⇑b : (a : ι) → P) (univ \ {i}))
⊢ Eq.{u_6 + 1} (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (Submodule.span k ((fun (x : P) ↦ x -ᵥ (b : (a : ι) → P) i) '' image (α := ι) (⇑b : (a : ι) → P) (univ \ {i})))

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
e_s :
  ∀ (v : V),
    Membership.mem (γ := Set V)
        (range fun (j : { x : ι // x ≠ i }) ↦
          VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P))
        v ↔
      Membership.mem (γ := Set V)
        ((fun (x : P) ↦ x -ᵥ (b : (a : ι) → P) i) '' image (α := ι) (⇑b : (a : ι) → P) (univ \ {i})) v
⊢ Eq.{u_6 + 1} (α := Set V)
    (range fun (j : { x : ι // x ≠ i }) ↦
      VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P))
    ((fun (x : P) ↦ x -ᵥ (b : (a : ι) → P) i) '' image (α := ι) (⇑b : (a : ι) → P) (univ \ {i}))

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
v : V
⊢ Membership.mem (γ := Set V)
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P))
      v ↔
    Membership.mem (γ := Set V)
      ((fun (x : P) ↦ x -ᵥ (b : (a : ι) → P) i) '' image (α := ι) (⇑b : (a : ι) → P) (univ \ {i})) v

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
i : ι
j : { j : ι // j ≠ i }
⊢ (b.basisOf i : (a : { j : ι // j ≠ i }) → V) j =
    VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)

Tactic:
simp [basisOf]

Premises used: AffineBasis.basisOf
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
i : ι'
a :
  ∀ (j : { j : ι' // j ≠ i }),
    Eq.{u_6 + 1} (α := V) (((b.reindex e).basisOf i : (a : { j : ι' // j ≠ i }) → V) j : V)
      ((Basis.reindex (ι := { j : ι // j ≠ (e.symm : (a : ι') → ι) i }) (b.basisOf ((e.symm : (a : ι') → ι) i))
              (e.subtypeEquiv (p := fun (j : ι) ↦ j ≠ (e.symm : (a : ι') → ι) i) (q := fun (b : ι') ↦ b ≠ i) ⋯) :
            (a : { j : ι' // j ≠ i }) → V)
          j :
        V)
⊢ (b.reindex e).basisOf i =
    Basis.reindex (ι := { j : ι // j ≠ (e.symm : (a : ι') → ι) i }) (b.basisOf ((e.symm : (a : ι') → ι) i))
      (e.subtypeEquiv (p := fun (j : ι) ↦ j ≠ (e.symm : (a : ι') → ι) i) (q := fun (b : ι') ↦ b ≠ i) ⋯)

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
i : ι'
j : { j : ι' // j ≠ i }
⊢ Eq.{u_6 + 1} (α := V) (((b.reindex e).basisOf i : (a : { j : ι' // j ≠ i }) → V) j : V)
    ((Basis.reindex (ι := { j : ι // j ≠ (e.symm : (a : ι') → ι) i }) (b.basisOf ((e.symm : (a : ι') → ι) i))
            (e.subtypeEquiv (p := fun (j : ι) ↦ j ≠ (e.symm : (a : ι') → ι) i) (q := fun (b : ι') ↦ b ≠ i) ⋯) :
          (a : { j : ι' // j ≠ i }) → V)
        j :
      V)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
i : ι
⊢ (b.coord i).linear = -(b.basisOf i).sumCoords

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
i : ι'
h :
  ∀ (p : P),
    Eq.{u_5 + 1} (α := k) (((b.reindex e).coord i : (a : P) → k) p : k)
      ((b.coord ((e.symm : (a : ι') → ι) i) : (a : P) → k) p : k)
⊢ (b.reindex e).coord i = b.coord ((e.symm : (a : ι') → ι) i)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
i : ι'
p : P
⊢ Eq.{u_5 + 1} (α := k) (((b.reindex e).coord i : (a : P) → k) p : k)
    ((b.coord ((e.symm : (a : ι') → ι) i) : (a : P) → k) p : k)

Tactic:
simp [AffineBasis.coord]

Premises used: AffineBasis.coord
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
i : ι'
p : P
⊢ Eq.{u_5 + 1} (α := k) (((b.reindex e).coord i : (a : P) → k) p : k)
    ((b.coord ((e.symm : (a : ι') → ι) i) : (a : P) → k) p : k)

Tactic:
classical simp [AffineBasis.coord]

Premises used: AffineBasis.coord
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
i : ι
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) i : P) : k) (1 : k)

Tactic:
simp only [coord, Basis.coe_sumCoords, map_zero, sub_zero,
    AffineMap.coe_mk, Finsupp.sum_zero_index, vsub_self]

Premises used: sub_zero, AffineMap.coe_mk, AffineBasis.coord, map_zero, Finsupp.sum_zero_index, vsub_self, Module.Basis.coe_sumCoords
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
i j : ι
h : i ≠ j
rw :
  Eq.{u_5 + 1} (α := k)
    (({
            toFun := fun (q : P) ↦
              HSub.hSub (α := k) (β := k) (1 : k)
                (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k),
            linear := -(b.basisOf i).sumCoords, map_vadd' := ⋯ } :
          (a : P) → k)
        ((b : (a : ι) → P) j : P) :
      k)
    (0 : k)
rw₁ :
  HSub.hSub (α := k) (β := k) (1 : k)
      (((b.basisOf i).sumCoords : (a : V) → k)
          (VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) j : P) ((b : (a : ι) → P) i : P)) :
        k) =
    0
rw₂ :
  HSub.hSub (α := k) (β := k) (1 : k)
      (((b.basisOf i).sumCoords : (a : V) → k)
          (VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑(Subtype.mk (p := fun (x : ι) ↦ x ≠ i) j ⋯) : ι) : P)
            ((b : (a : ι) → P) i : P)) :
        k) =
    0
rw₃ :
  HSub.hSub (α := k) (β := k) (1 : k)
      (((b.basisOf i).sumCoords : (a : V) → k)
          ((b.basisOf i : (a : { j : ι // j ≠ i }) → V) (Subtype.mk (p := fun (x : ι) ↦ x ≠ i) j ⋯) : V) :
        k) =
    0
rw₄ : HSub.hSub (α := k) 1 1 = 0
rw₅ rw₆ : Eq.{u_5 + 1} (α := k) 0 0
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (0 : k)

Tactic:
rw [coord, AffineMap.coe_mk, ← Subtype.coe_mk (p := (· ≠ i)) j h.symm, ← b.basisOf_apply,
    Basis.sumCoords_self_apply, sub_self]

Premises used: Subtype.coe_mk, sub_self, AffineMap.coe_mk, AffineBasis.coord, Ne.symm, Module.Basis.sumCoords_self_apply, AffineBasis.basisOf_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
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 : ι
inl :
  ∀ (h : i = j),
    Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (if i = j then 1 else 0 : k)
inr :
  ∀ (h : i ≠ j),
    Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (if i = j then 1 else 0 : k)
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (if i = j then 1 else 0 : k)

Tactic:
rcases eq_or_ne i j with h | h

Premises used: eq_or_ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
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 : ι
h : i = j
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (if i = j then 1 else 0 : k)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
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 : ι
h : i ≠ j
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (if i = j then 1 else 0 : k)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
w : ι → k
hw : s.sum w = 1
⊢ (b.coord i : (a : P) → k) ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) = w i

Tactic:
simp only [coord_apply, hi, Finset.affineCombination_eq_linear_combination, if_true,
      mul_boole, hw, Function.comp_apply, smul_eq_mul, s.sum_ite_eq,
      s.map_affineCombination b w hw]

Premises used: if_true, AffineBasis.coord_apply, Finset.affineCombination_eq_linear_combination, mul_boole, Finset.map_affineCombination, Function.comp_apply, smul_eq_mul, DFunLike.coe, Finset.sum_ite_eq