awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst_13 : Ring R
inst_14 : AddCommGroup W
inst_15 : Module k W
inst_16 : Module R W
inst_17 : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x x_1 : P₁ →ᵃ[k] W
h :
  ∀ (p : P₂),
    Eq.{u_11 + 1} (α := W) ((Equiv.toFun (e.arrowCongrEquiv (refl k W)) (x + x_1) : (a : P₂) → W) p : W)
      ((Equiv.toFun (e.arrowCongrEquiv (refl k W)) x + Equiv.toFun (e.arrowCongrEquiv (refl k W)) x_1 : (a : P₂) → W)
          p :
        W)
⊢ Equiv.toFun (e.arrowCongrEquiv (refl k W)) (x + x_1) =
    Equiv.toFun (e.arrowCongrEquiv (refl k W)) x + Equiv.toFun (e.arrowCongrEquiv (refl k W)) x_1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst_13 : Ring R
inst_14 : AddCommGroup W
inst_15 : Module k W
inst_16 : Module R W
inst_17 : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x x_1 : P₁ →ᵃ[k] W
p : P₂
⊢ Eq.{u_11 + 1} (α := W) ((Equiv.toFun (e.arrowCongrEquiv (refl k W)) (x + x_1) : (a : P₂) → W) p : W)
    ((Equiv.toFun (e.arrowCongrEquiv (refl k W)) x + Equiv.toFun (e.arrowCongrEquiv (refl k W)) x_1 : (a : P₂) → W) p :
      W)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst_13 : Ring R
inst_14 : AddCommGroup W
inst_15 : Module k W
inst_16 : Module R W
inst_17 : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x : R
x_1 : P₁ →ᵃ[k] W
h :
  ∀ (p : P₂),
    Eq.{u_11 + 1} (α := W) ((Equiv.toFun (e.arrowCongrEquiv (refl k W)) (x • x_1) : (a : P₂) → W) p : W)
      ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (Equiv.toFun (e.arrowCongrEquiv (refl k W)) x_1) :
            (a : P₂) → W)
          p :
        W)
⊢ Equiv.toFun (e.arrowCongrEquiv (refl k W)) (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (Equiv.toFun (e.arrowCongrEquiv (refl k W)) x_1)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst_13 : Ring R
inst_14 : AddCommGroup W
inst_15 : Module k W
inst_16 : Module R W
inst_17 : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x : R
x_1 : P₁ →ᵃ[k] W
p : P₂
⊢ Eq.{u_11 + 1} (α := W) ((Equiv.toFun (e.arrowCongrEquiv (refl k W)) (x • x_1) : (a : P₂) → W) p : W)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (Equiv.toFun (e.arrowCongrEquiv (refl k W)) x_1) :
          (a : P₂) → W)
        p :
      W)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
R : Type u_10
W : Type u_11
inst_7 : Ring R
inst_8 : AddCommGroup W
inst_9 : Module k W
inst_10 : Module R W
inst_11 : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
f : P₁ →ᵃ[k] W
x : P₂
⊢ Eq.{u_11 + 1} (α := W) ((((congrLeftₗ R W e : (a : P₁ →ᵃ[k] W) → P₂ →ᵃ[k] W) f : P₂ →ᵃ[k] W) : (a : P₂) → W) x : W)
    ((f : (a : P₁) → W) ((e.symm : (a : P₂) → P₁) x : P₁) : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
R : Type u_10
W : Type u_11
inst_7 : Ring R
inst_8 : AddCommGroup W
inst_9 : Module k W
inst_10 : Module R W
inst_11 : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
f : P₂ →ᵃ[k] W
x : P₁
⊢ Eq.{u_11 + 1} (α := W)
    ((((LinearEquiv.symm (congrLeftₗ R W e) : (a : P₂ →ᵃ[k] W) → P₁ →ᵃ[k] W) f : P₁ →ᵃ[k] W) : (a : P₁) → W) x : W)
    ((f : (a : P₂) → W) ((e : (a : P₁) → P₂) x : P₂) : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst_13 : Ring R
inst_14 : AddCommGroup W
inst_15 : Module k W
inst_16 : Module R W
inst_17 : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
Q : Type u_12
inst_18 : AffineSpace W Q
x : P₁ →ᵃ[k] Q
x_1 : P₁ →ᵃ[k] W
h :
  ∀ (p : P₂),
    Eq.{u_12 + 1} (α := Q)
      ((((e.arrowCongrEquiv (refl k Q) : (a : P₁ →ᵃ[k] Q) → P₂ →ᵃ[k] Q) (x_1 +ᵥ x) : P₂ →ᵃ[k] Q) : (a : P₂) → Q) p : Q)
      ((HVAdd.hVAdd (α := P₂ →ᵃ[k] W) (β := P₂ →ᵃ[k] Q)
              ((congrLeftₗ R W e : (a : P₁ →ᵃ[k] W) → P₂ →ᵃ[k] W) x_1 : P₂ →ᵃ[k] W)
              ((e.arrowCongrEquiv (refl k Q) : (a : P₁ →ᵃ[k] Q) → P₂ →ᵃ[k] Q) x : P₂ →ᵃ[k] Q) :
            (a : P₂) → Q)
          p :
        Q)
⊢ (e.arrowCongrEquiv (refl k Q) : (a : P₁ →ᵃ[k] Q) → P₂ →ᵃ[k] Q) (x_1 +ᵥ x) =
    HVAdd.hVAdd (α := P₂ →ᵃ[k] W) (β := P₂ →ᵃ[k] Q)
      ((congrLeftₗ R W e : (a : P₁ →ᵃ[k] W) → P₂ →ᵃ[k] W) x_1 : P₂ →ᵃ[k] W)
      ((e.arrowCongrEquiv (refl k Q) : (a : P₁ →ᵃ[k] Q) → P₂ →ᵃ[k] Q) x : P₂ →ᵃ[k] Q)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst_13 : Ring R
inst_14 : AddCommGroup W
inst_15 : Module k W
inst_16 : Module R W
inst_17 : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
Q : Type u_12
inst_18 : AffineSpace W Q
x : P₁ →ᵃ[k] Q
x_1 : P₁ →ᵃ[k] W
p : P₂
⊢ Eq.{u_12 + 1} (α := Q)
    ((((e.arrowCongrEquiv (refl k Q) : (a : P₁ →ᵃ[k] Q) → P₂ →ᵃ[k] Q) (x_1 +ᵥ x) : P₂ →ᵃ[k] Q) : (a : P₂) → Q) p : Q)
    ((HVAdd.hVAdd (α := P₂ →ᵃ[k] W) (β := P₂ →ᵃ[k] Q)
            ((congrLeftₗ R W e : (a : P₁ →ᵃ[k] W) → P₂ →ᵃ[k] W) x_1 : P₂ →ᵃ[k] W)
            ((e.arrowCongrEquiv (refl k Q) : (a : P₁ →ᵃ[k] Q) → P₂ →ᵃ[k] Q) x : P₂ →ᵃ[k] Q) :
          (a : P₂) → Q)
        p :
      Q)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
R : Type u_10
W : Type u_11
inst_7 : Ring R
inst_8 : AddCommGroup W
inst_9 : Module k W
inst_10 : Module R W
inst_11 : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
Q : Type u_12
inst_12 : AffineSpace W Q
f : P₁ →ᵃ[k] Q
x : P₂
⊢ Eq.{u_12 + 1} (α := Q) ((((congrLeft R e Q : (a : P₁ →ᵃ[k] Q) → P₂ →ᵃ[k] Q) f : P₂ →ᵃ[k] Q) : (a : P₂) → Q) x : Q)
    ((f : (a : P₁) → Q) ((e.symm : (a : P₂) → P₁) x : P₁) : Q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AffineSpace V₁ P₁
inst_6 : AffineSpace V₂ P₂
R : Type u_10
W : Type u_11
inst_7 : Ring R
inst_8 : AddCommGroup W
inst_9 : Module k W
inst_10 : Module R W
inst_11 : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
Q : Type u_12
inst_12 : AffineSpace W Q
f : P₂ →ᵃ[k] Q
x : P₁
⊢ Eq.{u_12 + 1} (α := Q)
    ((((symm (congrLeft R e Q) : (a : P₂ →ᵃ[k] Q) → P₁ →ᵃ[k] Q) f : P₁ →ᵃ[k] Q) : (a : P₁) → Q) x : Q)
    ((f : (a : P₂) → Q) ((e : (a : P₁) → P₂) x : P₂) : Q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
v v' : V₁
p : P₁
c : k
⊢ HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) ((lineMap v v' : (a : k) → V₁) c : V₁) p =
    (lineMap (v +ᵥ p) (v' +ᵥ p) : (a : k) → P₁) c

Tactic:
(vaddConst k p).apply_lineMap v v' c

Premises used: AffineEquiv.apply_lineMap, AffineEquiv.vaddConst
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
p₁ p₂ p₃ : P₁
c : k
⊢ (lineMap p₁ p₂ : (a : k) → P₁) c -ᵥ p₃ = (lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₃) : (a : k) → V₁) c

Tactic:
(vaddConst k p₃).symm.apply_lineMap p₁ p₂ c

Premises used: AffineEquiv.apply_lineMap, AffineEquiv.vaddConst, AffineEquiv.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
p₁ p₂ p₃ : P₁
c : k
⊢ p₁ -ᵥ (lineMap p₂ p₃ : (a : k) → P₁) c = (lineMap (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) : (a : k) → V₁) c

Tactic:
(constVSub k p₁).apply_lineMap p₂ p₃ c

Premises used: AffineEquiv.apply_lineMap, AffineEquiv.constVSub
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
v : V₁
p₁ p₂ : P₁
c : k
⊢ HVAdd.hVAdd (β := P₁) v ((lineMap p₁ p₂ : (a : k) → P₁) c : P₁) = (lineMap (v +ᵥ p₁) (v +ᵥ p₂) : (a : k) → P₁) c

Tactic:
(constVAdd k P₁ v).apply_lineMap p₁ p₂ c

Premises used: AffineEquiv.apply_lineMap, AffineEquiv.constVAdd
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
P₁ : Type u_2
V₁ : Type u_6
inst : AddCommGroup V₁
inst_1 : AffineSpace V₁ P₁
R' : Type u_10
inst_2 : CommRing R'
inst_3 : Module R' V₁
c p : P₁
⊢ Eq (α := P₁) ((homothety c (-1) : (a : P₁) → P₁) p : P₁) ((pointReflection R' c : (a : P₁) → P₁) p : P₁)

Tactic:
simp [homothety_apply, Equiv.pointReflection_apply]

Premises used: AffineMap.homothety_apply, Equiv.pointReflection_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
x x_1 : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add :
  ∀ (p : P1) (v : V1), f (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f_linear : (a : V1) → V2) v : V2) (f p)
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add :
  ∀ (p : P1) (v : V1), g (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (g p)
h : f = g
obtain :
  ∀ (p : P1),
    { toFun := f, linear := f_linear, map_vadd' := f_add : P1 →ᵃ[k] P2 } =
      { toFun := g, linear := g_linear, map_vadd' := g_add }
⊢ { toFun := f, linear := f_linear, map_vadd' := f_add : P1 →ᵃ[k] P2 } =
    { toFun := g, linear := g_linear, map_vadd' := g_add }

Tactic:
obtain ⟨p⟩ := (AddTorsor.nonempty : Nonempty P1)

Premises used: AddTorsor.nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
x x_1 : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add :
  ∀ (p : P1) (v : V1), f (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f_linear : (a : V1) → V2) v : V2) (f p)
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add :
  ∀ (p : P1) (v : V1), g (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (g p)
h : f = g
p : P1
e_linear : ∀ (v : V1), Eq.{u_4 + 1} (α := V2) ((f_linear : (a : V1) → V2) v : V2) ((g_linear : (a : V1) → V2) v : V2)
⊢ { toFun := f, linear := f_linear, map_vadd' := f_add : P1 →ᵃ[k] P2 } =
    { toFun := g, linear := g_linear, map_vadd' := g_add }

Tactic:
congr with v
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
x x_1 : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add :
  ∀ (p : P1) (v : V1), f (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f_linear : (a : V1) → V2) v : V2) (f p)
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add :
  ∀ (p : P1) (v : V1), g (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (g p)
h : f = g
p : P1
v : V1
e_linear :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f_linear : (a : V1) → V2) v : V2) (f p) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (f p)
⊢ Eq.{u_4 + 1} (α := V2) ((f_linear : (a : V1) → V2) v : V2) ((g_linear : (a : V1) → V2) v : V2)

Tactic:
apply vadd_right_cancel (f p)

Premises used: vadd_right_cancel
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
x x_1 : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add :
  ∀ (p : P1) (v : V1), f (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f_linear : (a : V1) → V2) v : V2) (f p)
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add :
  ∀ (p : P1) (v : V1), g (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (g p)
h : f = g
p : P1
v : V1
e_linear : f (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (f p)
e_linear₁ : g (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (g p)
e_linear₂ e_linear₃ : g (v +ᵥ p) = g (v +ᵥ p)
⊢ HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f_linear : (a : V1) → V2) v : V2) (f p) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (f p)

Tactic:
rw [← f_add, h, ← g_add]
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddCommGroup V₂
inst_4 : Module k V₂
f : V₁ →ₗ[k] V₂
⊢ Eq (α := (a : V₁) → V₂) (⇑f.toAffineMap : (a : V₁) → V₂) (⇑f : (a : V₁) → V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddCommGroup V₂
inst_4 : Module k V₂
f : V₁ →ₗ[k] V₂
⊢ f.toAffineMap.linear = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
f : P1 → P2
linear : V1 →ₗ[k] V2
add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((linear : (a : V1) → V2) v : V2) (f p)
⊢ (⇑{ toFun := f, linear := linear, map_vadd' := add : P1 →ᵃ[k] P2 } : (a : P1) → P2) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
⊢ f.toFun = (⇑f : (a : P1) → P2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ (f : (a : P1) → P2) (v +ᵥ p) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) (β := P2) ((f.linear : (a : V1) → V2) v : V2) ((f : (a : P1) → P2) p : P2)

Tactic:
f.map_vadd' p v

Premises used: AffineMap.map_vadd'
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
p1 p2 : P1
rw : ((f.linear : (a : V1) → V2) (p1 -ᵥ p2) : V2)
| VSub.vsub.{u_4, u_5} (P := P2) ((f : (a : P1) → P2) p1 : P2) ((f : (a : P1) → P2) p2 : P2)

Tactic:
rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]

Premises used: AffineMap.map_vadd, vsub_vadd, vadd_vsub
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
p1 p2 : P1
conv_rhs :
  (f.linear : (a : V1) → V2) (p1 -ᵥ p2) =
    VSub.vsub.{u_4, u_5} (P := P2) ((f : (a : P1) → P2) p1 : P2) ((f : (a : P1) → P2) p2 : P2)
conv_rhs₁ :
  Eq.{u_4 + 1} (α := V2) ((f.linear : (a : V1) → V2) (p1 -ᵥ p2) : V2) ((f.linear : (a : V1) → V2) (p1 -ᵥ p2) : V2)
⊢ (f.linear : (a : V1) → V2) (p1 -ᵥ p2) =
    VSub.vsub.{u_4, u_5} (P := P2) ((f : (a : P1) → P2) p1 : P2) ((f : (a : P1) → P2) p2 : P2)

Tactic:
conv_rhs => rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]

Premises used: AffineMap.map_vadd, vsub_vadd, vadd_vsub
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
f g : P1 →ᵃ[k] P2
h : ∀ (p : P1), Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) p : P2) ((g : (a : P1) → P2) p : P2)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
⊢ Function.Injective (α := P1 →ᵃ[k] P2) (β := P1 → P2) (DFunLike.coe (β := fun (x : P1) ↦ P2))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
x y : P1
h : x = y
⊢ Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) x : P2) ((f : (a : P1) → P2) y : P2)

Tactic:
congr_arg _ h

Premises used: congr_arg
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
f g : P1 →ᵃ[k] P2
h : f = g
x : P1
⊢ Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) x : P2) ((g : (a : P1) → P2) x : P2)

Tactic:
h ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
f g : P1 →ᵃ[k] P2
h₁ : f.linear = g.linear
p : P1
h₂ : Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) p : P2) ((g : (a : P1) → P2) p : P2)
h : ∀ (q : P1), Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) q : P2) ((g : (a : P1) → P2) q : P2)
⊢ f = g

Tactic:
ext q
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
f g : P1 →ᵃ[k] P2
h₁ : f.linear = g.linear
p : P1
h₂ : Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) p : P2) ((g : (a : P1) → P2) p : P2)
q : P1
⊢ (g.linear : (a : V1) → V2) (q -ᵥ p) = g.toFun ((q -ᵥ p) +ᵥ q) -ᵥ g.toFun q

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
f g : P1 →ᵃ[k] P2
h₁ : f.linear = g.linear
p : P1
h₂ : Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) p : P2) ((g : (a : P1) → P2) p : P2)
q : P1
⊢ (g.linear : (a : V1) → V2) (q -ᵥ p) = g.toFun ((q -ᵥ p) +ᵥ q) -ᵥ g.toFun q

Tactic:
have hgl : g.linear (q -ᵥ p) = toFun g ((q -ᵥ p) +ᵥ q) -ᵥ toFun g q := by simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
f g : P1 →ᵃ[k] P2
h₁ : f.linear = g.linear
p : P1
h₂ : Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) p : P2) ((g : (a : P1) → P2) p : P2)
q : P1
hgl : (g.linear : (a : V1) → V2) (q -ᵥ p) = g.toFun ((q -ᵥ p) +ᵥ q) -ᵥ g.toFun q
⊢ f.toFun ((q -ᵥ p) +ᵥ q) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f.linear : (a : V1) → V2) (q -ᵥ p) : V2) (f.toFun q)

Tactic:
have := f.map_vadd' q (q -ᵥ p)