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 : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
inst_4 : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
f : ι → P := update (β := fun (a : ι) ↦ P) p i p₀
hf : f = update (β := fun (a : ι) ↦ P) p i p₀
⊢ Eq (α := (x : (↑{x : ι | x ≠ i} : Type u_4)) → P) (fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ p (↑x : ι))
    fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)
have h : ∀ (x : (↑{x : ι | x ≠ i} : Type u_4)), p (↑x : ι) = f (↑x : ι)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
inst_4 : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
f : ι → P := update (β := fun (a : ι) ↦ P) p i p₀
hf : f = update (β := fun (a : ι) ↦ P) p i p₀
⊢ AffineIndependent k f
have h₁ : Eq (α := (x : (↑{x : ι | x ≠ i} : Type u_4)) → P) (fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ p (↑x : ι))
  fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)
Tactic: have h₁ : (fun x : {x | x ≠ i} ↦ p x) = fun x : {x | x ≠ i} ↦ f x := by ext x; aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
inst_4 : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
f : ι → P := update (β := fun (a : ι) ↦ P) p i p₀
hf : f = update (β := fun (a : ι) ↦ P) p i p₀
h₁ :
  Eq (α := (x : (↑{x : ι | x ≠ i} : Type u_4)) → P) (fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ p (↑x : ι))
    fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)
⊢ AffineIndependent k f
have h₂ : p '' {x : ι | x ≠ i} = f '' {x : ι | x ≠ i}
Tactic: have h₂ : p '' {x | x ≠ i} = f '' {x | x ≠ i} := Set.image_congr <| by simpa using congr_fun h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
inst_4 : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
f : ι → P := update (β := fun (a : ι) ↦ P) p i p₀
hf : f = update (β := fun (a : ι) ↦ P) p i p₀
h₁ :
  Eq (α := (x : (↑{x : ι | x ≠ i} : Type u_4)) → P) (fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ p (↑x : ι))
    fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)
h₂ : p '' {x : ι | x ≠ i} = f '' {x : ι | x ≠ i}
⊢ AffineIndependent k f
have ha₁ : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)
Tactic: replace ha : AffineIndependent k fun x : {x | x ≠ i} ↦ f x := h₁ ▸ AffineIndependent.subtype ha _
Cleared hypotheses: ha
-- 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
hs :
  Membership.mem (α := P) (γ := AffineSubspace k P)
    (affineSpan k
      (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
        (singleton (α := P) ((affineCombination k s p : (a : ι → k) → P) w₂ : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)
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)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
have rw : ∀ (hs : ∃ (r : k), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i) {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)),
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
Tactic: rw [affineCombination_mem_affineSpan_pair h hw hw₁ hw₂] at hs
Cleared hypotheses: hs, i, j, hi, hj, hi0, hj0, 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
hs : ∃ (r : k), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
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)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
have rcases : ∀ (r : k) (hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i),
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
Tactic: rcases hs with ⟨r, hr⟩
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 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
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
have rw : Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - w₁ i) + w₁ i) : 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)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
have 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)
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)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
have 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)
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)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
have 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)
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)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
have rw₄ : Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0)) : SignType)
  ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0) + 0) : 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)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
have rw₅ : Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0)) : SignType)
  ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0)) : 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)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
have rw₆ : Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * w₂ i) : SignType)
  ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0)) : 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)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
have rw₇ : Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * w₂ i) : SignType)
  ((SignType.sign : (a : k) → SignType) (r * 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)
⊢ 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) =
  (SignType.sign : (a : k) → SignType) (r * w₂ j)
Tactic: rw [hr i hi, hr j hj, hi0, hj0, add_zero, add_zero, sub_zero, sub_zero, sign_mul, sign_mul, hij]