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
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:
classical 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
-- 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
⊢ Eq.{u_5 + 1} (α := k)
    ((b.coord i : (a : P) → k) ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) : k) (0 : k)

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

Premises used: AffineBasis.coord_apply, Finset.affineCombination_eq_linear_combination, if_false, mul_boole, Finset.map_affineCombination, Function.comp_apply, smul_eq_mul, DFunLike.coe, Finset.sum_ite_eq
-- 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
⊢ Eq.{u_5 + 1} (α := k)
    ((b.coord i : (a : P) → k) ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) : k) (0 : k)

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

Premises used: AffineBasis.coord_apply, Finset.affineCombination_eq_linear_combination, if_false, mul_boole, Finset.map_affineCombination, Function.comp_apply, smul_eq_mul, 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 : Fintype ι
q : P
rw : Membership.mem (γ := AffineSubspace k P) ⊤ q
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) q

Tactic:
rw [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
inst_4 : Fintype ι
q : P
⊢ Membership.mem (γ := AffineSubspace k P) ⊤ q

Tactic:
AffineSubspace.mem_top k V q

Premises used: AffineSubspace.mem_top
-- 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 : Fintype ι
q : P
⊢ Membership.mem (γ := AffineSubspace k P) ⊤ q

Tactic:
exact AffineSubspace.mem_top k V q

Premises used: AffineSubspace.mem_top
-- 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 : Fintype ι
q : P
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) q

Tactic:
have hq : q ∈ affineSpan k (range b) := by
    rw [b.tot]
    exact AffineSubspace.mem_top k V q
-- 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 : Fintype ι
q : P
hq : Membership.mem (γ := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) q
obtain :
  ∀ (w : ι → k) (hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1)
    (hq :
      Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
        (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
        ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)),
    Eq.{u_5 + 1} (α := k)
      (∑ i : ι,
        (b.coord i : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P))
      1
⊢ Eq.{u_5 + 1} (α := k) (∑ i : ι, (b.coord i : (a : P) → k) q) 1

Tactic:
obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq

Premises used: eq_affineCombination_of_mem_affineSpan_of_fintype, 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
inst_4 : Fintype ι
w : ι → k
hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1
hq :
  Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
⊢ Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1

Tactic:
hw
-- 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 : Fintype ι
w : ι → k
hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1
hq :
  Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
h :
  ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x →
      (b.coord x : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) =
        w x
⊢ Eq.{u_5 + 1} (α := k)
    (∑ i : ι,
      (b.coord i : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P))
    1

Tactic:
convert! hw
-- 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 : Fintype ι
w : ι → k
hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1
hq :
  Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
x : ι
h : Membership.mem (γ := Finset ι) Finset.univ x
⊢ (b.coord x : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) = w x

Tactic:
b.coord_apply_combination_of_mem (Finset.mem_univ _) hw

Premises used: Finset.mem_univ, 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 : Fintype ι
w : ι → k
hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1
hq :
  Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
x : ι
h : Membership.mem (γ := Finset ι) Finset.univ x
⊢ (b.coord x : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) = w x

Tactic:
exact b.coord_apply_combination_of_mem (Finset.mem_univ _) hw

Premises used: Finset.mem_univ, 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 : Fintype ι
q : P
hq : Membership.mem (γ := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) q
obtain :
  ∀ (w : ι → k) (hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1)
    (hq :
      Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
        (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
        ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)),
    Eq.{u_7 + 1} (α := P)
      ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
          (b.coord i : (a : P) → k)
            ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) :
        P)
      ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
⊢ ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
      (b.coord i : (a : P) → k) q) =
    q

Tactic:
obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq

Premises used: eq_affineCombination_of_mem_affineSpan_of_fintype, 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
inst_4 : Fintype ι
w : ι → k
hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1
hq :
  Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
h :
  (fun (i : ι) ↦
      (b.coord i : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)) =
    w
⊢ Eq.{u_7 + 1} (α := P)
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
        (b.coord i : (a : P) → k)
          ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) :
      P)
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)

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 : AffineBasis ι k P
inst_4 : Fintype ι
w : ι → k
hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1
hq :
  Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
h :
  ∀ (i : ι),
    (b.coord i : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) =
      w i
⊢ (fun (i : ι) ↦
      (b.coord i : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)) =
    w

Tactic:
ext i
-- 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 : Fintype ι
w : ι → k
hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1
hq :
  Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
i : ι
⊢ (b.coord i : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) = w i

Tactic:
b.coord_apply_combination_of_mem (Finset.mem_univ i) hw

Premises used: Finset.mem_univ, 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 : Fintype ι
w : ι → k
hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1
hq :
  Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
i : ι
⊢ (b.coord i : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) = w i

Tactic:
exact b.coord_apply_combination_of_mem (Finset.mem_univ i) hw

Premises used: Finset.mem_univ, AffineBasis.coord_apply_combination_of_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
inst : AddCommGroup V
inst_1 : Ring k
inst_2 : Module k V
inst_3 : Fintype ι
b : AffineBasis ι k V
v : V
⊢ ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → V) : (a : ι → k) → V) fun (i : ι) ↦
      (b.coord i : (a : V) → k) v) =
    v

Tactic:
have hb := b.affineCombination_coord_eq_self v
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
inst : AddCommGroup V
inst_1 : Ring k
inst_2 : Module k V
inst_3 : Fintype ι
b : AffineBasis ι k V
v : V
hb :
  ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → V) : (a : ι → k) → V) fun (i : ι) ↦
      (b.coord i : (a : V) → k) v) =
    v
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (hb :
      ∑ i : ι,
          HSMul.hSMul.{u_5, u_6, u_6} (α := k) (β := V) ((b.coord i : (a : V) → k) v : k) ((b : (a : ι) → V) i : V) =
        v),
    ∑ i : ι, HSMul.hSMul.{u_5, u_6, u_6} (α := k) (β := V) ((b.coord i : (a : V) → k) v : k) ((b : (a : ι) → V) i : V) =
      v
⊢ ∑ i : ι, HSMul.hSMul.{u_5, u_6, u_6} (α := k) (β := V) ((b.coord i : (a : V) → k) v : k) ((b : (a : ι) → V) i : V) = v

Tactic:
rwa [Finset.univ.affineCombination_eq_linear_combination _ _ (b.sum_coord_apply_eq_one v)] at hb

Premises used: Finset.univ, Finset.affineCombination_eq_linear_combination, AffineBasis.sum_coord_apply_eq_one
-- 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 : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q₁ : k) ((b.coord i : (a : P) → k) q₂ : k)
intro : ∀ (val : Fintype ι), q₁ = q₂
⊢ q₁ = q₂

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- 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 : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q₁ : k) ((b.coord i : (a : P) → k) q₂ : k)
val : Fintype ι
intro :
  Eq.{u_7 + 1} (α := P)
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
        (b.coord i : (a : P) → k) q₁ :
      P)
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
        (b.coord i : (a : P) → k) q₂ :
      P)
⊢ q₁ = q₂

Tactic:
rw [← b.affineCombination_coord_eq_self q₁, ← b.affineCombination_coord_eq_self q₂]

Premises used: AffineBasis.affineCombination_coord_eq_self
-- 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 : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q₁ : k) ((b.coord i : (a : P) → k) q₂ : k)
val : Fintype ι
⊢ Eq.{u_7 + 1} (α := P)
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
        (b.coord i : (a : P) → k) q₁ :
      P)
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
        (b.coord i : (a : P) → k) q₂ :
      P)

Tactic:
simp only [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 : Subsingleton ι
i : ι
h : ∀ (q : P), Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 q : k)
⊢ Eq (α := (a : P) → k) (⇑(b.coord i) : (a : P) → k) 1

Tactic:
ext q
-- 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 : Subsingleton ι
i : ι
q : P
rw : Set.Subsingleton.{u_7} (α := P) (image.{u_1, u_7} (α := ι) (⇑b : (a : ι) → P) univ)
⊢ Set.Subsingleton.{u_7} (α := 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
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 : Subsingleton ι
i : ι
q : P
hs : Set.Subsingleton.{u_1} (α := ι) univ
⊢ Set.Subsingleton.{u_7} (α := P) (image.{u_1, u_7} (α := ι) (⇑b : (a : ι) → P) univ)

Tactic:
apply Subsingleton.image

Premises used: Set.Subsingleton.image
-- 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 : Subsingleton ι
i : ι
q : P
⊢ Set.Subsingleton.{u_1} (α := ι) univ

Tactic:
apply subsingleton_of_subsingleton

Premises used: Set.subsingleton_of_subsingleton
-- 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 : Subsingleton ι
i : ι
q : P
⊢ Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))

Tactic:
have hp : (range b).Subsingleton := by
    rw [← image_univ]
    apply Subsingleton.image
    apply subsingleton_of_subsingleton
-- 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 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
⊢ Subsingleton P

Tactic:
haveI := AffineSubspace.subsingleton_of_subsingleton_span_eq_top hp b.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
inst_4 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
this : Subsingleton P
s : Finset ι := {i}
⊢ i ∈ s

Tactic:
simp [s]
-- 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 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
this : Subsingleton P
s : Finset ι := {i}
⊢ i ∈ s

Tactic:
have hi : i ∈ s := by simp [s]
-- 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 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
⊢ Eq.{u_5 + 1} (α := k) (s.sum (Function.const ι 1)) 1

Tactic:
simp [s]
-- 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 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
⊢ Eq.{u_5 + 1} (α := k) (s.sum (Function.const ι 1)) 1

Tactic:
have hw : s.sum (Function.const ι (1 : k)) = 1 := by simp [s]
-- 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 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : Eq.{u_5 + 1} (α := k) (s.sum (Function.const ι 1)) 1
⊢ q = (Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Function.const ι 1)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- 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 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : Eq.{u_5 + 1} (α := k) (s.sum (Function.const ι 1)) 1
⊢ q = (Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Function.const ι 1)

Tactic:
have hq : q = s.affineCombination k b (Function.const ι (1 : k)) := by
    simp [eq_iff_true_of_subsingleton]
-- 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 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : Eq.{u_5 + 1} (α := k) (s.sum (Function.const ι 1)) 1
hq : q = (Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Function.const ι 1)
h : Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 : k)
h₁ :
  Eq.{u_5 + 1} (α := k)
    ((b.coord i : (a : P) → k)
        ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Function.const ι 1) : P) :
      k)
    (1 : k)
h₂ : Eq.{u_5 + 1} (α := k) (Function.const ι 1 i) 1
h₃ h₄ : Eq.{u_5 + 1} (α := k) 1 1
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 q : k)

Tactic:
rw [Pi.one_apply, hq, b.coord_apply_combination_of_mem hi hw, Function.const_apply]

Premises used: Function.const_apply, Pi.one_apply, 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 : ι
x : k
obtain : ∀ (j : ι) (hij : j ≠ i), ∃ (a : P), (b.coord i : (a : P) → k) a = x
⊢ ∃ (a : P), (b.coord i : (a : P) → k) a = x

Tactic:
obtain ⟨j, hij⟩ := exists_ne i

Premises used: exists_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 : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
⊢ i ∈ s

Tactic:
simp [s]
-- 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}
⊢ i ∈ s

Tactic:
have hi : i ∈ s := by simp [s]