awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun (j' : ι) ↦ if j' = i then x else 1 - x
⊢ s.sum w = 1

Tactic:
simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]

Premises used: Finset.filter_false_of_mem, Finset.filter_true_of_mem, Finset.filter_insert, Finset.sum_ite
-- 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 : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun (j' : ι) ↦ if j' = i then x else 1 - x
⊢ s.sum w = 1

Tactic:
have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]
-- 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 : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun (j' : ι) ↦ if j' = i then x else 1 - x
hw : s.sum w = 1
h : (b.coord i : (a : P) → k) ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) = x
⊢ ∃ (a : P), (b.coord i : (a : P) → k) a = x

Tactic:
use s.affineCombination k b w

Premises used: Finset.affineCombination, DFunLike.coe
-- 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 : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun (j' : ι) ↦ if j' = i then x else 1 - x
hw : s.sum w = 1
⊢ (b.coord i : (a : P) → k) ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) = x

Tactic:
simp [w, b.coord_apply_combination_of_mem hi hw]

Premises used: AffineBasis.coord_apply_combination_of_mem
-- 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 : Nontrivial ι
i : ι
intro : ∀ (x : k), ∃ (a : P), (b.coord i : (a : P) → k) a = x
intro₁ : ∀ (x : k) (j : ι) (hij : j ≠ i), ∃ (a : P), (b.coord i : (a : P) → k) a = x
intro₂ : ∀ (x : k) (j : ι) (hij : j ≠ i), ∃ (a : P), (b.coord i : (a : P) → k) a = x
intro₃ intro₄ :
  ∀ (x : k) (j : ι) (hij : j ≠ i),
    let s : Finset ι := {i, j};
    ∀ (hi : i ∈ s), ∃ (a : P), (b.coord i : (a : P) → k) a = x
intro₅ :
  ∀ (x : k) (j : ι) (hij : j ≠ i),
    let s : Finset ι := {i, j};
    ∀ (hi : i ∈ s),
      let w : ι → k := fun (j' : ι) ↦ if j' = i then x else 1 - x;
      ∀ (hw : s.sum w = 1), ∃ (a : P), (b.coord i : (a : P) → k) a = x
h :
  ∀ (x : k) (j : ι) (hij : j ≠ i),
    let s : Finset ι := {i, j};
    ∀ (hi : i ∈ s),
      let w : ι → k := fun (j' : ι) ↦ if j' = i then x else 1 - x;
      ∀ (hw : s.sum w = 1),
        (b.coord i : (a : P) → k) ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) = x
⊢ Function.Surjective.{u_7 + 1, u_5 + 1} (α := P) (β := k) (⇑(b.coord i) : (a : P) → k)

Tactic:
classical
    intro x
    obtain ⟨j, hij⟩ := exists_ne i
    let s : Finset ι := {i, j}
    have hi : i ∈ s := by simp [s]
    let w : ι → k := fun j' => if j' = i then x else 1 - x
    have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]
    use s.affineCombination k b w
    simp [w, b.coord_apply_combination_of_mem hi hw]

Premises used: exists_ne
-- 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 : ι ≃ ι'
v w : V
h :
  ∀ (x : ι),
    -((b.basisOf x).sumCoords : (a : V) → k) (v + w) =
      HAdd.hAdd (α := ι → k) (β := ι → k) (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) v)
        (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) w) x
⊢ (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) (v + w)) =
    HAdd.hAdd (α := ι → k) (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) v) fun (i : ι) ↦
      -((b.basisOf i).sumCoords : (a : V) → k) w

Tactic:
ext
-- 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 : ι ≃ ι'
v w : V
x : ι
⊢ -((b.basisOf x).sumCoords : (a : V) → k) (v + w) =
    HAdd.hAdd (α := ι → k) (β := ι → k) (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) v)
      (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) w) x

Tactic:
simp only [map_add, Pi.add_apply, neg_add]

Premises used: neg_add, map_add, Pi.add_apply
-- 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 : ι ≃ ι'
t : k
v : V
h :
  ∀ (x : ι),
    -((b.basisOf x).sumCoords : (a : V) → k) (t • v) =
      HSMul.hSMul (α := k) (β := ι → k) ((RingHom.id k : (a : k) → k) t : k)
        (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) v) x
⊢ (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) (t • v)) =
    HSMul.hSMul (α := k) (β := ι → k) ((RingHom.id k : (a : k) → k) t : k) fun (i : ι) ↦
      -((b.basisOf i).sumCoords : (a : V) → k) v

Tactic:
ext
-- 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 : ι ≃ ι'
t : k
v : V
x : ι
⊢ -((b.basisOf x).sumCoords : (a : V) → k) (t • v) =
    HSMul.hSMul (α := k) (β := ι → k) ((RingHom.id k : (a : k) → k) t : k)
      (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) v) x

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 : ι ≃ ι'
p : P
v : V
h :
  ∀ (x : ι),
    (b.coord x : (a : P) → k) (v +ᵥ p) =
      HVAdd.hVAdd (α := ι → k) (β := ι → k)
        (({ toFun := fun (v : V) (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) v, map_add' := ⋯, map_smul' := ⋯ :
                V →ₗ[k] ι → k } :
              (a : V) → ι → k)
            v :
          ι → k)
        (fun (i : ι) ↦ (b.coord i : (a : P) → k) p) x
⊢ (fun (i : ι) ↦ (b.coord i : (a : P) → k) (v +ᵥ p)) =
    HVAdd.hVAdd (α := ι → k) (β := ι → k)
      (({ toFun := fun (v : V) (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) v, map_add' := ⋯, map_smul' := ⋯ :
              V →ₗ[k] ι → k } :
            (a : V) → ι → k)
          v :
        ι → k)
      fun (i : ι) ↦ (b.coord i : (a : P) → k) p

Tactic:
ext
-- 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 : ι ≃ ι'
p : P
v : V
x : ι
⊢ (b.coord x : (a : P) → k) (v +ᵥ p) =
    HVAdd.hVAdd (α := ι → k) (β := ι → k)
      (({ toFun := fun (v : V) (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) v, map_add' := ⋯, map_smul' := ⋯ :
              V →ₗ[k] ι → k } :
            (a : V) → ι → k)
          v :
        ι → k)
      (fun (i : ι) ↦ (b.coord i : (a : P) → k) p) x

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
q : P
i : ι
⊢ Eq.{u_5 + 1} (α := k) ((b.coords : (a : P) → ι → k) q i : k) ((b.coord i : (a : P) → k) q : k)

Tactic:
rfl

Premises used: 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_1 : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
x : V
b : AffineBasis ι k P
rw :
  Eq.{u_7 + 1} (α := AffineSubspace k P)
    (affineSpan k (range fun (i : ι) ↦ HVAdd.hVAdd (β := P) x ((b : (a : ι) → P) i : P))) ⊤
rw₁ :
  Eq (α := AffineSubspace k P)
    (affineSpan k (HVAdd.hVAdd (β := Set P) x (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))) ⊤
rw₂ : HVAdd.hVAdd (β := AffineSubspace k P) x (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) = ⊤
rw₃ : HVAdd.hVAdd (β := AffineSubspace k P) x ⊤ = ⊤
rw₄ rw₅ : Eq.{u_7 + 1} (α := AffineSubspace k P) ⊤ ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k (range (HVAdd.hVAdd (β := (a : ι) → P) x (⇑b : (a : ι) → P)))) ⊤

Tactic:
rw [Pi.vadd_def, ← vadd_set_range, ← AffineSubspace.pointwise_vadd_span, b.tot,
        AffineSubspace.pointwise_vadd_top]

Premises used: AffineBasis.tot, Set.vadd_set_range, Pi.vadd_def, AffineSubspace.pointwise_vadd_top, AffineSubspace.pointwise_vadd_span
-- 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
v : V
b : AffineBasis ι k P
⊢ (⇑(v +ᵥ b) : (a : ι) → P) = HVAdd.hVAdd (β := (a : ι) → P) v (⇑b : (a : ι) → 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
v : V
b : AffineBasis ι k P
h :
  ∀ (x : ι) (i : { j : ι // j ≠ x }),
    Eq.{u_6 + 1} (α := V) (((v +ᵥ b).basisOf x : (a : { j : ι // j ≠ x }) → V) i : V)
      ((b.basisOf x : (a : { j : ι // j ≠ x }) → V) i : V)
⊢ (v +ᵥ b).basisOf = b.basisOf

Tactic:
ext
-- 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
v : V
b : AffineBasis ι k P
x : ι
i : { j : ι // j ≠ x }
⊢ Eq.{u_6 + 1} (α := V) (((v +ᵥ b).basisOf x : (a : { j : ι // j ≠ x }) → V) i : V)
    ((b.basisOf x : (a : { j : ι // j ≠ x }) → V) 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
i : ι
v : V
b : AffineBasis ι k P
h :
  ∀ (p : P),
    Eq.{u_5 + 1} (α := k) (((v +ᵥ b).coord i : (a : P) → k) p : k)
      (((b.coord i).comp (↑(AffineEquiv.symm (AffineEquiv.constVAdd k P v)) : P →ᵃ[k] P) : (a : P) → k) p : k)
⊢ (v +ᵥ b).coord i = (b.coord i).comp (↑(AffineEquiv.symm (AffineEquiv.constVAdd k P v)) : P →ᵃ[k] P)

Tactic:
ext p
-- 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
i : ι
v : V
b : AffineBasis ι k P
p : P
h :
  Eq.{u_5 + 1} (α := k)
    (Finsupp.sum (M := k)
      (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k)
        (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)))
      fun (x : { j : ι // ¬j = i }) ↦ id)
    (Finsupp.sum (M := k) (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) ((-v +ᵥ p) -ᵥ (b : (a : ι) → P) i))
      fun (x : { j : ι // ¬j = i }) ↦ id)
⊢ Eq.{u_5 + 1} (α := k) (((v +ᵥ b).coord i : (a : P) → k) p : k)
    (((b.coord i).comp (↑(AffineEquiv.symm (AffineEquiv.constVAdd k P v)) : P →ᵃ[k] P) : (a : P) → k) p : k)

Tactic:
simp only [coord, ne_eq, basisOf_vadd, coe_vadd, Pi.vadd_apply, Basis.coe_sumCoords,
    AffineMap.coe_mk, AffineEquiv.constVAdd_symm, AffineMap.coe_comp, AffineEquiv.coe_toAffineMap,
    Function.comp_apply, AffineEquiv.constVAdd_apply, sub_right_inj]

Premises used: AffineMap.coe_comp, AffineEquiv.constVAdd_apply, sub_right_inj, AffineBasis.coe_vadd, AffineMap.coe_mk, AffineBasis.coord, ne_eq, AffineEquiv.coe_toAffineMap, AffineEquiv.constVAdd_symm, Function.comp_apply, AffineBasis.basisOf_vadd, Pi.vadd_apply, 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
i : ι
v : V
b : AffineBasis ι k P
p : P
h :
  Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) ((-v +ᵥ p) -ᵥ (b : (a : ι) → P) i) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
⊢ Eq.{u_5 + 1} (α := k)
    (Finsupp.sum (M := k)
      (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k)
        (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)))
      fun (x : { j : ι // ¬j = i }) ↦ id)
    (Finsupp.sum (M := k) (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) ((-v +ᵥ p) -ᵥ (b : (a : ι) → P) i))
      fun (x : { j : ι // ¬j = i }) ↦ id)

Tactic:
congr! 1
-- 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
i : ι
v : V
b : AffineBasis ι k P
p : P
h :
  Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (-v + (p -ᵥ (b : (a : ι) → P) i)) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
h₁ :
  Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ (b : (a : ι) → P) i - v) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
h₂ h₃ :
  Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ (b : (a : ι) → P) i - v) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ (b : (a : ι) → P) i - v) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
⊢ Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) ((-v +ᵥ p) -ᵥ (b : (a : ι) → P) i) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)

Tactic:
rw [vadd_vsub_assoc, neg_add_eq_sub, vsub_vadd_eq_vsub_sub]

Premises used: vadd_vsub_assoc, neg_add_eq_sub, vsub_vadd_eq_vsub_sub
-- 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_1 : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst_4 : Group G
inst_5 : Group G'
inst_6 : DistribMulAction G V
inst_7 : DistribMulAction G' V
inst_8 : SMulCommClass G k V
inst_9 : SMulCommClass G' k V
a : G
b : AffineBasis ι k V
rw :
  Eq (α := AffineSubspace k V) (affineSpan k (range fun (i : ι) ↦ HSMul.hSMul (β := V) a ((b : (a : ι) → V) i : V))) ⊤
rw₁ :
  Eq (α := AffineSubspace k V)
    (affineSpan k (HSMul.hSMul (β := Set V) a (range.{u_6, u_1 + 1} (ι := ι) (⇑b : (a : ι) → V)))) ⊤
rw₂ : HSMul.hSMul (β := AffineSubspace k V) a (affineSpan k (range.{u_6, u_1 + 1} (ι := ι) (⇑b : (a : ι) → V))) = ⊤
rw₃ : HSMul.hSMul (β := AffineSubspace k V) a ⊤ = ⊤
rw₄ rw₅ : Eq.{u_6 + 1} (α := AffineSubspace k V) ⊤ ⊤
⊢ Eq (α := AffineSubspace k V) (affineSpan k (range (HSMul.hSMul (β := (a : ι) → V) a (⇑b : (a : ι) → V)))) ⊤

Tactic:
rw [Pi.smul_def, ← smul_set_range, ← AffineSubspace.smul_span, b.tot,
          AffineSubspace.smul_top (Group.isUnit a)]

Premises used: AffineBasis.tot, Group.isUnit, AffineSubspace.smul_top, Set.smul_set_range, Pi.smul_def, AffineSubspace.smul_span
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst : AddCommGroup V
inst_1 : Ring k
inst_2 : Module k V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
a : G
b : AffineBasis ι k V
⊢ (⇑(a • b) : (a : ι) → V) = HSMul.hSMul (β := (a : ι) → V) a (⇑b : (a : ι) → V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst : AddCommGroup V
inst_1 : Ring k
inst_2 : Module k V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
a₁ :
  ∀ (j : { j : ι // j ≠ i }),
    Eq.{u_6 + 1} (α := V) (((a • b).basisOf i : (a : { j : ι // j ≠ i }) → V) j : V)
      ((a • b.basisOf i : (a : { j : ι // j ≠ i }) → V) j : V)
⊢ (a • b).basisOf i = a • b.basisOf i

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst : AddCommGroup V
inst_1 : Ring k
inst_2 : Module k V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
j : { j : ι // j ≠ i }
⊢ Eq.{u_6 + 1} (α := V) (((a • b).basisOf i : (a : { j : ι // j ≠ i }) → V) j : V)
    ((a • b.basisOf i : (a : { j : ι // j ≠ i }) → V) j : V)

Tactic:
simp [smul_sub]

Premises used: smul_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
k : Type u_5
V : Type u_6
inst : AddCommGroup V
inst_1 : Ring k
inst_2 : Module k V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
a : G
b : AffineBasis ι k V
e : ι ≃ ι'
⊢ (a • b).reindex e = a • b.reindex e

Tactic:
rfl

Premises used: AffineBasis.reindex, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst : AddCommGroup V
inst_1 : Ring k
inst_2 : Module k V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
h :
  ∀ (v : V),
    Eq.{u_5 + 1} (α := k) (((a • b).coord i : (a : V) → k) v : k)
      (((b.coord i).comp
              (LinearMap.toAffineMap (↑(LinearEquiv.symm (DistribMulAction.toLinearEquiv k V a)) : V →ₗ[k] V)) :
            (a : V) → k)
          v :
        k)
⊢ (a • b).coord i =
    (b.coord i).comp (LinearMap.toAffineMap (↑(LinearEquiv.symm (DistribMulAction.toLinearEquiv k V a)) : V →ₗ[k] V))

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst : AddCommGroup V
inst_1 : Ring k
inst_2 : Module k V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
v : V
⊢ Eq.{u_5 + 1} (α := k) (((a • b).coord i : (a : V) → k) v : k)
    (((b.coord i).comp
            (LinearMap.toAffineMap (↑(LinearEquiv.symm (DistribMulAction.toLinearEquiv k V a)) : V →ₗ[k] V)) :
          (a : V) → k)
        v :
      k)

Tactic:
simp [map_sub, coord]

Premises used: map_sub, 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 : DivisionRing k
inst_3 : Module k V
inst_4 : CharZero k
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
rw :
  Eq.{u_5 + 1} (α := k)
    ((b.coord i : (a : P) → k)
        ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Finset.centroidWeights k s) : P) :
      k)
    ((↑s.card : k)⁻¹ : k)
rw₁ : Finset.centroidWeights k s i = (↑s.card : k)⁻¹
rw₂ : Eq.{u_5 + 1} (α := k) (Function.const ι (↑s.card : k)⁻¹ i) (↑s.card : k)⁻¹
rw₃ rw₄ : Eq.{u_5 + 1} (α := k) (↑s.card : k)⁻¹ (↑s.card : k)⁻¹
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) (Finset.centroid k s (⇑b : (a : ι) → P)) : k) ((↑s.card : k)⁻¹ : k)

Tactic:
rw [Finset.centroid,
    b.coord_apply_combination_of_mem hi (s.sum_centroidWeights_eq_one_of_nonempty _ ⟨i, hi⟩),
    Finset.centroidWeights, Function.const_apply]

Premises used: Function.const_apply, Finset.sum_centroidWeights_eq_one_of_nonempty, Exists.intro, Finset.centroid, Finset.centroidWeights, AffineBasis.coord_apply_combination_of_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
t : Set P
ht : Eq (α := AffineSubspace k P) (affineSpan k t) ⊤
obtain :
  ∀ (s : Set P) (hst : s ⊆ t) (h_tot : Eq (α := AffineSubspace k P) (affineSpan k s) (affineSpan k t))
    (h_ind :
      AffineIndependent.{u_5, u_6, u_7, u_7} k (P := P) (ι := { x : P // x ∈ s })
        (Subtype.val (p := fun (x : P) ↦ x ∈ s))),
    ∃ s ⊆ t,
      ∃ (b : AffineBasis (↑s : Type u_7) k P),
        Eq (α := (a : (↑s : Type u_7)) → P) (⇑b : (a : (↑s : Type u_7)) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
⊢ ∃ s ⊆ t,
    ∃ (b : AffineBasis (↑s : Type u_7) k P),
      Eq (α := (a : (↑s : Type u_7)) → P) (⇑b : (a : (↑s : Type u_7)) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ s))

Tactic:
obtain ⟨s, hst, h_tot, h_ind⟩ := exists_affineIndependent k V t

Premises used: exists_affineIndependent
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
t : Set P
ht : Eq (α := AffineSubspace k P) (affineSpan k t) ⊤
s : Set P
hst : s ⊆ t
h_tot : Eq (α := AffineSubspace k P) (affineSpan k s) (affineSpan k t)
h_ind :
  AffineIndependent.{u_5, u_6, u_7, u_7} k (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
⊢ ∃ s ⊆ t,
    ∃ (b : AffineBasis (↑s : Type u_7) k P),
      Eq (α := (a : (↑s : Type u_7)) → P) (⇑b : (a : (↑s : Type u_7)) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ s))

Tactic:
⟨s, hst, ⟨(↑), h_ind, ?_⟩, rfl⟩

Premises used: AffineBasis.mk, And.intro, Exists.intro, Subtype.val, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
t : Set P
ht : Eq (α := AffineSubspace k P) (affineSpan k t) ⊤
s : Set P
hst : s ⊆ t
h_tot : Eq (α := AffineSubspace k P) (affineSpan k s) (affineSpan k t)
h_ind :
  AffineIndependent.{u_5, u_6, u_7, u_7} k (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
refine :
  Eq.{u_7 + 1} (α := AffineSubspace k P)
    (affineSpan k (range (ι := (↑s : Type u_7)) (Subtype.val (p := fun (x : P) ↦ x ∈ s)))) ⊤
⊢ ∃ s ⊆ t,
    ∃ (b : AffineBasis (↑s : Type u_7) k P),
      Eq (α := (a : (↑s : Type u_7)) → P) (⇑b : (a : (↑s : Type u_7)) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ s))

Tactic:
refine ⟨s, hst, ⟨(↑), h_ind, ?_⟩, rfl⟩