awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
j : ι
simp_rw : Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0) (1 i j)
simp_rw₁ : Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0) (if i = j then 1 else 0)
⊢ (if j = i then 1 else 0) = (A * b.toMatrix p) i j

Tactic:
simp_rw [hA, Matrix.one_apply, @eq_comm _ i j]

Premises used: Matrix.one_apply, eq_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
⊢ Eq.{u₄ + 1} (α := P) ((b : (a : ι) → P) i : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P)

Tactic:
have hbi : b i = Finset.univ.affineCombination k p (A i) := by
    apply b.ext_elem
    intro j
    rw [b.coord_apply, Finset.univ.map_affineCombination _ _ hAi,
      Finset.univ.affineCombination_eq_linear_combination _ _ hAi]
    change _ = (A * b.toMatrix p) i j
    simp_rw [hA, Matrix.one_apply, @eq_comm _ i j]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
hbi :
  Eq.{u₄ + 1} (α := P) ((b : (a : ι) → P) i : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P)
intro :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (range p))
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (range p)) ((b : (a : ι) → P) i : P)

Tactic:
rw [hbi]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
hbi :
  Eq.{u₄ + 1} (α := P) ((b : (a : ι) → P) i : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (range p))
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P)

Tactic:
affineCombination_mem_affineSpan hAi p

Premises used: affineCombination_mem_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
hbi :
  Eq.{u₄ + 1} (α := P) ((b : (a : ι) → P) i : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (range p))
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P)

Tactic:
exact affineCombination_mem_affineSpan hAi p

Premises used: affineCombination_mem_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
b₂ : AffineBasis ι k P
x : P
h :
  ∀ (j : ι),
    vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j =
      (b.coords : (a : P) → ι → k) x j
⊢ vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) = (b.coords : (a : P) → ι → k) x

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
h : vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j = (b.coord j : (a : P) → k) x
⊢ vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j =
    (b.coords : (a : P) → ι → k) x j

Tactic:
change _ = b.coord j x

Premises used: AffineBasis.coord, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
rw :
  ((b.coord j : (a : P) → k)
      ((Finset.affineCombination k Finset.univ (⇑b₂ : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
          (b₂.coord i : (a : P) → k) x :
        P) :
    k)
| ((b.coord j : (a : P) → k) x : k)

Tactic:
rw [← b₂.affineCombination_coord_eq_self x]

Premises used: AffineBasis.affineCombination_coord_eq_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
h :
  vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j =
    (b.coord j : (a : P) → k)
      ((Finset.affineCombination k Finset.univ (⇑b₂ : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
          (b₂.coord i : (a : P) → k) x :
        P)
⊢ vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j = (b.coord j : (a : P) → k) x

Tactic:
conv_rhs => rw [← b₂.affineCombination_coord_eq_self x]

Premises used: AffineBasis.affineCombination_coord_eq_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
h :
  vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j =
    (Finset.affineCombination k Finset.univ
          (Function.comp.{u₁ + 1, u₄ + 1, u₂ + 1} (β := P) (⇑(b.coord j) : (a : P) → k) (⇑b₂ : (a : ι) → P)) :
        (a : ι → k) → k)
      fun (i : ι) ↦ (b₂.coord i : (a : P) → k) x
⊢ vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j =
    (b.coord j : (a : P) → k)
      ((Finset.affineCombination k Finset.univ (⇑b₂ : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
          (b₂.coord i : (a : P) → k) x :
        P)

Tactic:
rw [Finset.map_affineCombination _ _ _ (b₂.sum_coord_apply_eq_one x)]

Premises used: Finset.map_affineCombination, AffineBasis.sum_coord_apply_eq_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j =
    (Finset.affineCombination k Finset.univ
          (Function.comp.{u₁ + 1, u₄ + 1, u₂ + 1} (β := P) (⇑(b.coord j) : (a : P) → k) (⇑b₂ : (a : ι) → P)) :
        (a : ι → k) → k)
      fun (i : ι) ↦ (b₂.coord i : (a : P) → k) x

Tactic:
simp [Matrix.vecMul, dotProduct, toMatrix_apply, coords]

Premises used: dotProduct, Matrix.vecMul, AffineBasis.toMatrix_apply, AffineBasis.coords
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
b₂ : AffineBasis ι k P
inst_5 : DecidableEq ι
a :
  ∀ (l m : ι),
    HMul.hMul (α := Matrix ι ι k) (β := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P)) (b₂.toMatrix (⇑b : (a : ι) → P))
        l m =
      1 l m
⊢ HMul.hMul (α := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P)) (b₂.toMatrix (⇑b : (a : ι) → P)) = 1

Tactic:
ext l m
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
b₂ : AffineBasis ι k P
inst_5 : DecidableEq ι
l m : ι
a : vecMul (m := ι) ((b.coords : (a : P) → ι → k) ((b₂ : (a : ι) → P) l : P)) (b₂.toMatrix (⇑b : (a : ι) → P)) m = 1 l m
⊢ HMul.hMul (α := Matrix ι ι k) (β := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P)) (b₂.toMatrix (⇑b : (a : ι) → P)) l
      m =
    1 l m

Tactic:
change (b.coords (b₂ l) ᵥ* b₂.toMatrix b) m = _

Premises used: Matrix.vecMul, AffineBasis.toMatrix, DFunLike.coe, AffineBasis.coords
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
b₂ : AffineBasis ι k P
inst_5 : DecidableEq ι
l m : ι
a : Eq.{u₂ + 1} (α := k) ((b₂.coords : (a : P) → ι → k) ((b₂ : (a : ι) → P) l : P) m : k) (1 l m : k)
a₁ : Eq.{u₂ + 1} (α := k) ((b₂.coord m : (a : P) → k) ((b₂ : (a : ι) → P) l : P) : k) (1 l m : k)
a₂ : b₂.toMatrix (⇑b₂ : (a : ι) → P) l m = 1 l m
a₃ a₄ : Eq.{u₂ + 1} (α := k) (1 l m) (1 l m)
⊢ vecMul (m := ι) ((b.coords : (a : P) → ι → k) ((b₂ : (a : ι) → P) l : P)) (b₂.toMatrix (⇑b : (a : ι) → P)) m = 1 l m

Tactic:
rw [toMatrix_vecMul_coords, coords_apply, ← toMatrix_apply, toMatrix_self]

Premises used: AffineBasis.toMatrix_apply, AffineBasis.toMatrix_vecMul_coords, AffineBasis.coords_apply, AffineBasis.toMatrix_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
b₂ : AffineBasis ι k P
inst_5 : DecidableEq ι
⊢ IsUnit (M := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P))

Tactic:
⟨{  val := b.toMatrix b₂
      inv := b₂.toMatrix b
      val_inv := b.toMatrix_mul_toMatrix b₂
      inv_val := b₂.toMatrix_mul_toMatrix b }, rfl⟩

Premises used: AffineBasis.toMatrix_mul_toMatrix, IsUnit, Units.mk, Exists.intro, AffineBasis.toMatrix, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
inst_5 : DecidableEq ι
inst_6 : Nontrivial k
p : ι → P
mp : IsUnit (b.toMatrix p) → AffineIndependent k p ∧ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
mpr : AffineIndependent k p ∧ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤ → IsUnit (b.toMatrix p)
⊢ IsUnit (b.toMatrix p) ↔ AffineIndependent k p ∧ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
inst_5 : DecidableEq ι
inst_6 : Nontrivial k
p : ι → P
A : Matrix ι ι k
hA : b.toMatrix p * A = 1
hA' : A * b.toMatrix p = 1
⊢ AffineIndependent k p ∧ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤

Tactic:
⟨b.affineIndependent_of_toMatrix_right_inv p hA,
      b.affineSpan_eq_top_of_toMatrix_left_inv p hA'⟩

Premises used: AffineBasis.affineIndependent_of_toMatrix_right_inv, AffineBasis.affineSpan_eq_top_of_toMatrix_left_inv, And.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
inst_5 : DecidableEq ι
inst_6 : Nontrivial k
p : ι → P
A : Matrix ι ι k
hA : b.toMatrix p * A = 1
hA' : A * b.toMatrix p = 1
⊢ AffineIndependent k p ∧ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤

Tactic:
exact ⟨b.affineIndependent_of_toMatrix_right_inv p hA,
      b.affineSpan_eq_top_of_toMatrix_left_inv p hA'⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
inst_5 : DecidableEq ι
inst_6 : Nontrivial k
p : ι → P
h_tot : AffineIndependent k p
h_ind : Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
b' : AffineBasis ι k P := { toFun := p, ind' := h_tot, tot' := h_ind }
mpr : IsUnit (M := Matrix ι ι k) (b.toMatrix (⇑b' : (a : ι) → P))
⊢ IsUnit (b.toMatrix p)

Tactic:
change IsUnit (b.toMatrix b')

Premises used: IsUnit, AffineBasis.toMatrix, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
inst_5 : DecidableEq ι
inst_6 : Nontrivial k
p : ι → P
h_tot : AffineIndependent k p
h_ind : Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
b' : AffineBasis ι k P := { toFun := p, ind' := h_tot, tot' := h_ind }
⊢ IsUnit (M := Matrix ι ι k) (b.toMatrix (⇑b' : (a : ι) → P))

Tactic:
b.isUnit_toMatrix b'

Premises used: AffineBasis.isUnit_toMatrix
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
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 : Fintype ι
inst_5 : DecidableEq ι
inst_6 : Nontrivial k
p : ι → P
h_tot : AffineIndependent k p
h_ind : Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
b' : AffineBasis ι k P := { toFun := p, ind' := h_tot, tot' := h_ind }
⊢ IsUnit (M := Matrix ι ι k) (b.toMatrix (⇑b' : (a : ι) → P))

Tactic:
exact b.isUnit_toMatrix b'

Premises used: AffineBasis.isUnit_toMatrix
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
⊢ IsUnit (M := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P))

Tactic:
have hu := b.isUnit_toMatrix b₂
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (M := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P))
⊢ IsUnit (det (b.toMatrix (⇑b₂ : (a : ι) → P)))

Tactic:
rw [Matrix.isUnit_iff_isUnit_det] at hu

Premises used: Matrix.isUnit_iff_isUnit_det
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (det (b.toMatrix (⇑b₂ : (a : ι) → P)))
rw :
  vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) ᵥ*
      (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ =
    (b₂.coords : (a : P) → ι → k) x
rw₁ :
  (b₂.coords : (a : P) → ι → k) x ᵥ*
      HMul.hMul (α := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P)) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ =
    (b₂.coords : (a : P) → ι → k) x
rw₂ : Eq (α := ι → k) (vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) 1) ((b₂.coords : (a : P) → ι → k) x)
rw₃ rw₄ : Eq (α := ι → k) ((b₂.coords : (a : P) → ι → k) x : ι → k) ((b₂.coords : (a : P) → ι → k) x : ι → k)
⊢ vecMul (m := ι) ((b.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ = (b₂.coords : (a : P) → ι → k) x

Tactic:
rw [← b.toMatrix_vecMul_coords b₂, Matrix.vecMul_vecMul, Matrix.mul_nonsing_inv _ hu,
    Matrix.vecMul_one]

Premises used: AffineBasis.toMatrix_vecMul_coords, Matrix.vecMul_vecMul, Matrix.mul_nonsing_inv, Matrix.vecMul_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.Matrix
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (det (b.toMatrix (⇑b₂ : (a : ι) → P)))
rw :
  det (b.toMatrix (⇑b₂ : (a : ι) → P)) •
      vecMul (m := ι) ((b.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ =
    (cramer (b.toMatrix (⇑b₂ : (a : ι) → P))ᵀ : (a : ι → k) → ι → k) ((b.coords : (a : P) → ι → k) x : ι → k)
rw₁ rw₂ :
  Eq (α := ι → k)
    ((cramer (b.toMatrix (⇑b₂ : (a : ι) → P))ᵀ : (a : ι → k) → ι → k) ((b.coords : (a : P) → ι → k) x : ι → k) : ι → k)
    ((cramer (b.toMatrix (⇑b₂ : (a : ι) → P))ᵀ : (a : ι → k) → ι → k) ((b.coords : (a : P) → ι → k) x : ι → k) : ι → k)
⊢ HSMul.hSMul (β := ι → k) (det (b.toMatrix (⇑b₂ : (a : ι) → P))) ((b₂.coords : (a : P) → ι → k) x : ι → k) =
    (cramer (b.toMatrix (⇑b₂ : (a : ι) → P))ᵀ : (a : ι → k) → ι → k) ((b.coords : (a : P) → ι → k) x : ι → k)

Tactic:
rw [← b.toMatrix_inv_vecMul_toMatrix, Matrix.det_smul_inv_vecMul_eq_cramer_transpose _ _ hu]

Premises used: AffineBasis.toMatrix_inv_vecMul_toMatrix, Matrix.det_smul_inv_vecMul_eq_cramer_transpose
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
f : P →ᵃ[R] P'
a b : P
⊢ Eq.{u_5 + 1} (α := P') ((f : (a : P) → P') (midpoint R a b) : P')
    (midpoint R ((f : (a : P) → P') a) ((f : (a : P) → P') b) : P')

Tactic:
f.apply_lineMap a b _

Premises used: AffineMap.apply_lineMap, midpoint
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
f : P ≃ᵃ[R] P'
a b : P
⊢ Eq.{u_5 + 1} (α := P') ((f : (a : P) → P') (midpoint R a b) : P')
    (midpoint R ((f : (a : P) → P') a) ((f : (a : P) → P') b) : P')

Tactic:
f.apply_lineMap a b _

Premises used: AffineEquiv.apply_lineMap, midpoint
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
rw :
  ((pointReflection R ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) :
          P ≃ᵃ[R] P) :
        (a : P) → P)
      x =
    y
rw₁ :
  HVAdd.hVAdd (β := P) ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) -ᵥ x)
      ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) : P) =
    y
rw₂ :
  ((HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
          x) -ᵥ
        x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
        x =
    y
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
        x =
    y
rw₄ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x)) +ᵥ
      x =
    y
rw₅ :
  HAdd.hAdd (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) •
        (y -ᵥ x) +ᵥ
      x =
    y
rw₆ : HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) • (y -ᵥ x) +ᵥ x = y
rw₇ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ x) +ᵥ x = y
rw₈ : (y -ᵥ x) +ᵥ x = y
rw₉ rw₁₀ : y = y
⊢ (pointReflection R (midpoint R x y) : (a : P) → P) x = y

Tactic:
rw [midpoint, pointReflection_apply, lineMap_apply, vadd_vsub, vadd_vadd, ← add_smul, ← two_mul,
    mul_invOf_self, one_smul, vsub_vadd]

Premises used: vadd_vadd, two_mul, mul_invOf_self, one_smul, AffineMap.lineMap_apply, AffineEquiv.pointReflection_apply, add_smul, vsub_vadd, vadd_vsub, midpoint
-- Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y : P
rw :
  ((pointReflection ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) :
          Perm P) :
        (a : P) → P)
      x =
    y
rw₁ :
  HVAdd.hVAdd (β := P) ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) -ᵥ x)
      ((lineMap x y : (a : R) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) : P) =
    y
rw₂ :
  ((HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
          x) -ᵥ
        x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
        x =
    y
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +ᵥ
        x =
    y
rw₄ :
  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (y -ᵥ x)) +ᵥ
      x =
    y
rw₅ :
  HAdd.hAdd (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) •
        (y -ᵥ x) +ᵥ
      x =
    y
rw₆ : HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) • (y -ᵥ x) +ᵥ x = y
rw₇ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ x) +ᵥ x = y
rw₈ : (y -ᵥ x) +ᵥ x = y
rw₉ rw₁₀ : y = y
⊢ (pointReflection (midpoint R x y) : (a : P) → P) x = y

Tactic:
rw [midpoint, pointReflection_apply, lineMap_apply, vadd_vsub, vadd_vadd, ← add_smul, ← two_mul,
    mul_invOf_self, one_smul, vsub_vadd]

Premises used: vadd_vadd, two_mul, mul_invOf_self, one_smul, AffineMap.lineMap_apply, add_smul, vsub_vadd, vadd_vsub, midpoint, Equiv.pointReflection_apply