awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w₂ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w₂ j) : SignType)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
rw :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - w₁ i) + w₁ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
rw₁ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - w₁ i) + w₁ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - w₁ j) + w₁ j) : SignType)
rw₂ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0) + 0) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - w₁ j) + w₁ j) : SignType)
rw₃ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0) + 0) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0) + 0) : SignType)
rw₄ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0)) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0) + 0) : SignType)
rw₅ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0)) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0)) : SignType)
rw₆ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * w₂ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0)) : SignType)
rw₇ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * w₂ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * w₂ j) : SignType)
rw₈ :
  HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : k) → SignType) r : SignType)
      ((SignType.sign : (a : k) → SignType) (w₂ i) : SignType) =
    (SignType.sign : (a : k) → SignType) (r * w₂ j)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
have rw₉ : HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : k) → SignType) r : SignType)
    ((SignType.sign : (a : k) → SignType) (w₂ i) : SignType) =
  HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : k) → SignType) r : SignType)
    ((SignType.sign : (a : k) → SignType) (w₂ j) : SignType)
Tactic: rw [hr i hi, hr j hj, hi0, hj0, add_zero, add_zero, sub_zero, sub_zero, sign_mul, sign_mul, hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w₂ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w₂ j) : SignType)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
rw :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - w₁ i) + w₁ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
rw₁ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - w₁ i) + w₁ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - w₁ j) + w₁ j) : SignType)
rw₂ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0) + 0) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - w₁ j) + w₁ j) : SignType)
rw₃ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0) + 0) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0) + 0) : SignType)
rw₄ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0)) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0) + 0) : SignType)
rw₅ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0)) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0)) : SignType)
rw₆ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * w₂ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0)) : SignType)
rw₇ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * w₂ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * w₂ j) : SignType)
rw₈ :
  HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : k) → SignType) r : SignType)
      ((SignType.sign : (a : k) → SignType) (w₂ i) : SignType) =
    (SignType.sign : (a : k) → SignType) (r * w₂ j)
rw₉ :
  HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : k) → SignType) r : SignType)
      ((SignType.sign : (a : k) → SignType) (w₂ i) : SignType) =
    HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : k) → SignType) r : SignType)
      ((SignType.sign : (a : k) → SignType) (w₂ j) : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
have rw₁₀ : HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : k) → SignType) r : SignType)
    ((SignType.sign : (a : k) → SignType) (w₂ j) : SignType) =
  HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : k) → SignType) r : SignType)
    ((SignType.sign : (a : k) → SignType) (w₂ j) : SignType)
Tactic: rw [hr i hi, hr j hj, hi0, hj0, add_zero, add_zero, sub_zero, sub_zero, sign_mul, sign_mul, hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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 i₁) (singleton (α := P) ((AffineMap.lineMap (p i₂) (p i₃) : (a : k) → P) c : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)
have 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)
Tactic: rw [← s.affineCombination_piSingle k p h₁, ←
      s.affineCombination_affineCombinationLineMapWeights p h₂ h₃ c] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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) (w i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)
have refine_1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, Pi.single (M := fun (a : ι) ↦ k) i₁ 1 i) 1
Tactic: refine
      sign_eq_of_affineCombination_mem_affineSpan_pair h hw ?_
        (s.sum_affineCombinationLineMapWeights h₂ h₃ c) hs h₂ h₃
        (Pi.single_eq_of_ne h₁₂.symm _)
        (Pi.single_eq_of_ne h₁₃.symm _) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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_1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, Pi.single (M := fun (a : ι) ↦ k) i₁ 1 i) 1
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)
have refine_2 : 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: refine
      sign_eq_of_affineCombination_mem_affineSpan_pair h hw ?_
        (s.sum_affineCombinationLineMapWeights h₂ h₃ c) hs h₂ h₃
        (Pi.single_eq_of_ne h₁₂.symm _)
        (Pi.single_eq_of_ne h₁₃.symm _) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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.{u_1 + 1} (α := k) (∑ i ∈ s, Pi.single (M := fun (a : ι) ↦ k) i₁ 1 i) 1
have refine_1 : Eq.{u_1 + 1} (α := k) (if i₁ ∈ s then 1 else 0) 1
Tactic: rw [Finset.sum_pi_single', if_pos h₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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_1 : Eq.{u_1 + 1} (α := k) (if i₁ ∈ s then 1 else 0) 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, Pi.single (M := fun (a : ι) ↦ k) i₁ 1 i) 1
have refine_1₁ : Eq.{u_1 + 1} (α := k) 1 1
Tactic: rw [Finset.sum_pi_single', if_pos h₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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) (affineCombinationLineMapWeights i₂ i₃ c i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (affineCombinationLineMapWeights i₂ i₃ c i₃) : SignType)
have refine_2 : Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (1 - c) : SignType)
  ((SignType.sign : (a : k) → SignType) c : SignType)
Tactic: rw [Finset.affineCombinationLineMapWeights_apply_left h₂₃,
      Finset.affineCombinationLineMapWeights_apply_right h₂₃]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 i₁) (singleton (α := P) ((AffineMap.lineMap (p i₂) (p i₃) : (a : k) → P) c : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)
have rw : ∀
  (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) ((AffineMap.lineMap (p i₂) (p i₃) : (a : k) → P) c : P))))
      ((affineCombination k s p : (a : ι → k) → P) w : P)),
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)
Tactic: classical
    rw [← s.affineCombination_piSingle k p h₁, ←
      s.affineCombination_affineCombinationLineMapWeights p h₂ h₃ c] at hs
    refine
      sign_eq_of_affineCombination_mem_affineSpan_pair h hw ?_
        (s.sum_affineCombinationLineMapWeights h₂ h₃ c) hs h₂ h₃
        (Pi.single_eq_of_ne h₁₂.symm _)
        (Pi.single_eq_of_ne h₁₃.symm _) ?_
    · rw [Finset.sum_pi_single', if_pos h₁]
    rw [Finset.affineCombinationLineMapWeights_apply_left h₂₃,
      Finset.affineCombinationLineMapWeights_apply_right h₂₃]
    simp_all only [sub_pos, sign_pos]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 i₁) (singleton (α := P) ((AffineMap.lineMap (p i₂) (p i₃) : (a : k) → P) c : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)
rw :
  ∀
    (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) ((AffineMap.lineMap (p i₂) (p i₃) : (a : k) → P) c : P))))
        ((affineCombination k s p : (a : ι → k) → P) w : P)),
    Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i₂) : SignType)
      ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)
have rw₁ : ∀
  (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) (w i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)
Tactic: classical
    rw [← s.affineCombination_piSingle k p h₁, ←
      s.affineCombination_affineCombinationLineMapWeights p h₂ h₃ c] at hs
    refine
      sign_eq_of_affineCombination_mem_affineSpan_pair h hw ?_
        (s.sum_affineCombinationLineMapWeights h₂ h₃ c) hs h₂ h₃
        (Pi.single_eq_of_ne h₁₂.symm _)
        (Pi.single_eq_of_ne h₁₃.symm _) ?_
    · rw [Finset.sum_pi_single', if_pos h₁]
    rw [Finset.affineCombinationLineMapWeights_apply_left h₂₃,
      Finset.affineCombinationLineMapWeights_apply_right h₂₃]
    simp_all only [sub_pos, sign_pos]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 i₁) (singleton (α := P) ((AffineMap.lineMap (p i₂) (p i₃) : (a : k) → P) c : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)
rw :
  ∀
    (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) ((AffineMap.lineMap (p i₂) (p i₃) : (a : k) → P) c : P))))
        ((affineCombination k s p : (a : ι → k) → P) w : P)),
    Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i₂) : SignType)
      ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)
rw₁ rw₂ rw₃ :
  ∀
    (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) (w i₂) : SignType)
      ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)
have refine_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.{u_1 + 1} (α := k) (∑ i ∈ s, Pi.single (M := fun (a : ι) ↦ k) i₁ 1 i) 1
Tactic: classical
    rw [← s.affineCombination_piSingle k p h₁, ←
      s.affineCombination_affineCombinationLineMapWeights p h₂ h₃ c] at hs
    refine
      sign_eq_of_affineCombination_mem_affineSpan_pair h hw ?_
        (s.sum_affineCombinationLineMapWeights h₂ h₃ c) hs h₂ h₃
        (Pi.single_eq_of_ne h₁₂.symm _)
        (Pi.single_eq_of_ne h₁₃.symm _) ?_
    · rw [Finset.sum_pi_single', if_pos h₁]
    rw [Finset.affineCombinationLineMapWeights_apply_left h₂₃,
      Finset.affineCombinationLineMapWeights_apply_right h₂₃]
    simp_all only [sub_pos, sign_pos]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : DecidableEq ι
⊢ Eq (α := Matrix ι ι k) (b.toMatrix (⇑b : (a : ι) → P)) 1
have a : ∀ (i j : ι), b.toMatrix (⇑b : (a : ι) → P) i j = 1 i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : DecidableEq ι
i j : ι
⊢ b.toMatrix (⇑b : (a : ι) → P) i j = 1 i j
have a : Eq.{u₂ + 1} (α := k) ((b.coord j : (a : P) → k) ((b : (a : ι) → P) i : P) : k) (1 i j : k)
Tactic: rw [toMatrix_apply, coord_apply, Matrix.one_eq_pi_single, Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
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)
⊢ b.toMatrix (⇑b : (a : ι) → P) i j = 1 i j
have a₁ : Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0) (1 i j)
Tactic: rw [toMatrix_apply, coord_apply, Matrix.one_eq_pi_single, Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
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)
⊢ b.toMatrix (⇑b : (a : ι) → P) i j = 1 i j
have a₂ : Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0 : k) (Pi.single (M := fun (x : ι) ↦ k) i 1 j : k)
Tactic: rw [toMatrix_apply, coord_apply, Matrix.one_eq_pi_single, Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
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)
⊢ b.toMatrix (⇑b : (a : ι) → P) i j = 1 i j
have a₃ : Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0) (if j = i then 1 else 0)
Tactic: rw [toMatrix_apply, coord_apply, Matrix.one_eq_pi_single, Pi.single_apply]