awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this :
  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)
⊢ HVAdd.hVAdd (β := P2) (VSub.vsub.{u_4, u_5} (P := P2) ((f : (a : P1) → P2) q : P2) ((g : (a : P1) → P2) p : P2))
      ((f : (a : P1) → P2) q : P2) =
    HVAdd.hVAdd (β := P2) (g.toFun ((q -ᵥ p) +ᵥ q) -ᵥ g.toFun q) ((f : (a : P1) → P2) q : P2)

Tactic:
rw [h₁, hgl, toFun_eq_coe, map_vadd, linearMap_vsub, h₂] at this

Premises used: AffineMap.toFun_eq_coe, AffineMap.linearMap_vsub, 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 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
this :
  HVAdd.hVAdd (β := P2) (VSub.vsub.{u_4, u_5} (P := P2) ((f : (a : P1) → P2) q : P2) ((g : (a : P1) → P2) p : P2))
      ((f : (a : P1) → P2) q : P2) =
    HVAdd.hVAdd (β := P2) (g.toFun ((q -ᵥ p) +ᵥ q) -ᵥ g.toFun q) ((f : (a : P1) → P2) q : P2)
⊢ Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) q : P2) ((g : (a : P1) → P2) q : P2)

Tactic:
simpa
-- 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
inhabit : (inhabited_h : Inhabited P1) → P1
⊢ P1

Tactic:
inhabit P1
-- 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
inhabited_h : Inhabited P1
⊢ P1

Tactic:
exact default

Premises used: Inhabited.default
-- 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
rw rw₁ : Eq.{u_5 + 1} (α := P2) ((g : (a : P1) → P2) default : P2) ((g : (a : P1) → P2) default : P2)
⊢ Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) default : P2) ((g : (a : P1) → P2) default : P2)

Tactic:
rw [h]
-- 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
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst_7 : AddCommGroup V3
inst_8 : Module k V3
inst_9 : AffineSpace V3 P3
inst_10 : AddCommGroup V4
inst_11 : Module k V4
inst_12 : AffineSpace V4 P4
p : P2
x : P1
x_1 : V1
this : AddAction V2 P2 := inferInstance
⊢ Function.const P1 p (x_1 +ᵥ x) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((0 : (a : V1) → V2) x_1 : V2) (Function.const P1 p x)

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
p : P2
⊢ (⇑(const k P1 p) : (a : P1) → P2) = Function.const P1 p

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
p : P2
q : P1
⊢ (const k P1 p : (a : P1) → P2) q = p

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
p : P2
⊢ Eq (α := V1 →ₗ[k] V2) (linear (const k P1 p)) 0

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.linear = 0 ↔ ∃ (q : P2), f = const k P1 q

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- 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
refine_1 : ∀ (h : f.linear = 0), ∃ (q : P2), f = const k P1 q
refine_2 : ∀ (h : ∃ (q : P2), f = const k P1 q), f.linear = 0
⊢ f.linear = 0 ↔ ∃ (q : P2), f = const k P1 q

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- 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
h : f.linear = 0
h₁ : f = const k P1 ((f : (a : P1) → P2) (Classical.arbitrary P1))
⊢ ∃ (q : P2), f = const k P1 q

Tactic:
use f (Classical.arbitrary P1)

Premises used: Classical.arbitrary, DFunLike.coe
-- 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
h : f.linear = 0
h₁ :
  ∀ (p : P1),
    Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) p : P2)
      (((const k P1 ((f : (a : P1) → P2) (Classical.arbitrary P1)) : P1 →ᵃ[k] P2) : (a : P1) → P2) p : P2)
⊢ f = const k P1 ((f : (a : P1) → P2) (Classical.arbitrary P1))

Tactic:
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
f : P1 →ᵃ[k] P2
h : f.linear = 0
p : P1
h₁ :
  Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) p : P2)
    (Function.const P1 ((f : (a : P1) → P2) (Classical.arbitrary P1)) p : P2)
h₂ : Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) p : P2) ((f : (a : P1) → P2) (Classical.arbitrary P1) : P2)
h₃ : VSub.vsub.{u_4, u_5} (P := P2) ((f : (a : P1) → P2) p : P2) ((f : (a : P1) → P2) (Classical.arbitrary P1) : P2) = 0
h₄ : Eq.{u_4 + 1} (α := V2) ((f.linear : (a : V1) → V2) (p -ᵥ Classical.arbitrary P1) : V2) (0 : V2)
h₅ : Eq.{u_4 + 1} (α := V2) ((0 : (a : V1) → V2) (p -ᵥ Classical.arbitrary P1) : V2) (0 : V2)
h₆ h₇ : Eq.{u_4 + 1} (α := V2) 0 0
⊢ Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) p : P2)
    (((const k P1 ((f : (a : P1) → P2) (Classical.arbitrary P1)) : P1 →ᵃ[k] P2) : (a : P1) → P2) p : P2)

Tactic:
rw [coe_const, Function.const_apply, ← @vsub_eq_zero_iff_eq V2, ← f.linearMap_vsub, h,
      LinearMap.zero_apply]

Premises used: Function.const_apply, LinearMap.zero_apply, vsub_eq_zero_iff_eq, AffineMap.linearMap_vsub, AffineMap.coe_const
-- 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
h : ∃ (q : P2), f = const k P1 q
refine_2 : ∀ (q : P2), Eq (α := V1 →ₗ[k] V2) (linear (const k P1 q)) 0
⊢ f.linear = 0

Tactic:
rcases h with ⟨q, 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
q : P2
⊢ Eq (α := V1 →ₗ[k] V2) (linear (const k P1 q)) 0

Tactic:
const_linear k P1 q

Premises used: AffineMap.const_linear
-- 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
q : P2
⊢ Eq (α := V1 →ₗ[k] V2) (linear (const k P1 q)) 0

Tactic:
exact const_linear k P1 q

Premises used: AffineMap.const_linear
-- 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
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst_7 : AddCommGroup V3
inst_8 : Module k V3
inst_9 : AffineSpace V3 P3
inst_10 : AddCommGroup V4
inst_11 : Module k V4
inst_12 : AffineSpace V4 P4
⊢ Nonempty (P1 →ᵃ[k] P2)

Tactic:
(AddTorsor.nonempty : Nonempty P2).map <| const k P1

Premises used: AddTorsor.nonempty, AffineMap.const, Nonempty.map
-- 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
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst_7 : AddCommGroup V3
inst_8 : Module k V3
inst_9 : AffineSpace V3 P3
inst_10 : AddCommGroup V4
inst_11 : Module k V4
inst_12 : AffineSpace V4 P4
f : P1 → P2
f' : V1 →ₗ[k] V2
p : P1
h : ∀ (p' : P1), f p' = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) (f p)
p' : P1
v : V1
rw :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) ((v +ᵥ p') -ᵥ p) : V2) (f p) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2) (f p')
rw₁ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) ((v +ᵥ p') -ᵥ p) : V2) (f p) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2)
      (HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) (f p))
rw₂ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) (v + (p' -ᵥ p)) : V2) (f p) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2)
      (HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) (f p))
rw₃ :
  HAdd.hAdd (α := V2) (β := V2) ((f' : (a : V1) → V2) v : V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) +ᵥ f p =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2)
      (HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) (f p))
rw₄ rw₅ :
  HAdd.hAdd (α := V2) (β := V2) ((f' : (a : V1) → V2) v : V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) +ᵥ f p =
    HAdd.hAdd (α := V2) (β := V2) ((f' : (a : V1) → V2) v : V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) +ᵥ f p
⊢ f (v +ᵥ p') = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2) (f p')

Tactic:
rw [h, h p', vadd_vsub_assoc, f'.map_add, vadd_vadd]

Premises used: LinearMap.map_add, vadd_vsub_assoc, vadd_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 → P2
f' : V1 →ₗ[k] V2
p : P1
h : ∀ (p' : P1), f p' = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) (f p)
⊢ (⇑(mk' f f' p h) : (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 → P2
f' : V1 →ₗ[k] V2
p : P1
h : ∀ (p' : P1), f p' = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) (f p)
⊢ (mk' f f' p h).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
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst_7 : AddCommGroup V3
inst_8 : Module k V3
inst_9 : AffineSpace V3 P3
inst_10 : AddCommGroup V4
inst_11 : Module k V4
inst_12 : AffineSpace V4 P4
R : Type u_10
inst_13 : Monoid R
inst_14 : DistribMulAction R V2
inst_15 : SMulCommClass k R V2
c : R
f : P1 →ᵃ[k] V2
p : P1
v : V1
⊢ HSMul.hSMul (β := (a : P1) → V2) c (⇑f : (a : P1) → V2) (v +ᵥ p) =
    HVAdd.hVAdd (α := V2) ((c • f.linear : (a : V1) → V2) v : V2)
      (HSMul.hSMul (β := (a : P1) → V2) c (⇑f : (a : P1) → V2) p)

Tactic:
simp [smul_add]

Premises used: smul_add
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
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
R : Type u_10
inst_6 : Monoid R
inst_7 : DistribMulAction R V2
inst_8 : SMulCommClass k R V2
c : R
f : P1 →ᵃ[k] V2
⊢ (⇑(c • f) : (a : P1) → V2) = HSMul.hSMul (β := (a : P1) → V2) c (⇑f : (a : P1) → V2)

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
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
R : Type u_10
inst_6 : Monoid R
inst_7 : DistribMulAction R V2
inst_8 : SMulCommClass k R V2
t : R
f : P1 →ᵃ[k] V2
⊢ (t • f).linear = t • f.linear

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
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst_7 : AddCommGroup V3
inst_8 : Module k V3
inst_9 : AffineSpace V3 P3
inst_10 : AddCommGroup V4
inst_11 : Module k V4
inst_12 : AffineSpace V4 P4
f g : P1 →ᵃ[k] V2
p : P1
v : V1
⊢ HAdd.hAdd (α := (a : P1) → V2) (β := (a : P1) → V2) (⇑f : (a : P1) → V2) (⇑g : (a : P1) → V2) (v +ᵥ p) =
    HVAdd.hVAdd (α := V2) ((f.linear + g.linear : (a : V1) → V2) v : V2)
      (HAdd.hAdd (α := (a : P1) → V2) (β := (a : P1) → V2) (⇑f : (a : P1) → V2) (⇑g : (a : P1) → V2) p)

Tactic:
simp [add_add_add_comm]

Premises used: add_add_add_comm
-- 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
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst_7 : AddCommGroup V3
inst_8 : Module k V3
inst_9 : AffineSpace V3 P3
inst_10 : AddCommGroup V4
inst_11 : Module k V4
inst_12 : AffineSpace V4 P4
f g : P1 →ᵃ[k] V2
p : P1
v : V1
⊢ HSub.hSub (α := (a : P1) → V2) (β := (a : P1) → V2) (⇑f : (a : P1) → V2) (⇑g : (a : P1) → V2) (v +ᵥ p) =
    HVAdd.hVAdd (α := V2) ((f.linear - g.linear : (a : V1) → V2) v : V2)
      (HSub.hSub (α := (a : P1) → V2) (β := (a : P1) → V2) (⇑f : (a : P1) → V2) (⇑g : (a : P1) → V2) p)

Tactic:
simp [sub_add_sub_comm]

Premises used: sub_add_sub_comm
-- 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
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst_7 : AddCommGroup V3
inst_8 : Module k V3
inst_9 : AffineSpace V3 P3
inst_10 : AddCommGroup V4
inst_11 : Module k V4
inst_12 : AffineSpace V4 P4
f : P1 →ᵃ[k] V2
p : P1
v : V1
⊢ (-(⇑f : (a : P1) → V2)) (v +ᵥ p) =
    HVAdd.hVAdd (α := V2) (β := V2) ((-f.linear : (a : V1) → V2) v : V2) ((-(⇑f : (a : P1) → V2)) p : V2)

Tactic:
simp [add_comm, map_vadd f]

Premises used: AffineMap.map_vadd, add_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
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
⊢ Eq (α := (a : P1) → V2) (⇑0 : (a : P1) → V2) 0

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
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
f g : P1 →ᵃ[k] V2
⊢ (⇑(f + g) : (a : P1) → V2) = HAdd.hAdd (α := (a : P1) → V2) (⇑f : (a : P1) → V2) (⇑g : (a : P1) → V2)

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
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
f : P1 →ᵃ[k] V2
⊢ Eq (α := (a : P1) → V2) (⇑(-f) : (a : P1) → V2) (-(⇑f : (a : P1) → V2))

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
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
f g : P1 →ᵃ[k] V2
⊢ (⇑(f - g) : (a : P1) → V2) = HSub.hSub (α := (a : P1) → V2) (⇑f : (a : P1) → V2) (⇑g : (a : P1) → V2)

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
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
⊢ Eq (α := V1 →ₗ[k] V2) (linear.{u_1, u_2, u_3, u_4, u_4} (P1 := P1) (P2 := V2) 0) 0

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
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
f g : P1 →ᵃ[k] V2
⊢ (f + g).linear = f.linear + g.linear

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
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
f g : P1 →ᵃ[k] V2
⊢ (f - g).linear = f.linear - g.linear

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
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
f : P1 →ᵃ[k] V2
⊢ (-f).linear = -f.linear

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
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst_7 : AddCommGroup V3
inst_8 : Module k V3
inst_9 : AffineSpace V3 P3
inst_10 : AddCommGroup V4
inst_11 : Module k V4
inst_12 : AffineSpace V4 P4
f : P1 →ᵃ[k] V2
g : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ (fun (p : P1) ↦
        HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) (β := P2) ((f : (a : P1) → V2) p : V2) ((g : (a : P1) → P2) p : P2))
      (v +ᵥ p) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) (β := P2) ((f.linear + g.linear : (a : V1) → V2) v : V2)
      ((fun (p : P1) ↦
          HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) (β := P2) ((f : (a : P1) → V2) p : V2) ((g : (a : P1) → P2) p : P2))
        p)

Tactic:
simp [vadd_vadd, add_right_comm]

Premises used: vadd_vadd, add_right_comm
-- 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
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst_7 : AddCommGroup V3
inst_8 : Module k V3
inst_9 : AffineSpace V3 P3
inst_10 : AddCommGroup V4
inst_11 : Module k V4
inst_12 : AffineSpace V4 P4
f g : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ (fun (p : P1) ↦ VSub.vsub.{u_4, u_5} (P := P2) ((f : (a : P1) → P2) p : P2) ((g : (a : P1) → P2) p : P2)) (v +ᵥ p) =
    HVAdd.hVAdd (α := V2) (β := V2) ((f.linear - g.linear : (a : V1) → V2) v : V2)
      ((fun (p : P1) ↦ VSub.vsub.{u_4, u_5} (P := P2) ((f : (a : P1) → P2) p : P2) ((g : (a : P1) → P2) p : P2)) p)

Tactic:
simp [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, sub_add_eq_add_sub]

Premises used: vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, sub_add_eq_add_sub
-- 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] V2
g : P1 →ᵃ[k] P2
p : P1
⊢ (f +ᵥ g : (a : P1) → P2) p =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) (β := P2) ((f : (a : P1) → V2) p : V2) ((g : (a : P1) → P2) p : 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] V2
g : P1 →ᵃ[k] P2
⊢ (f +ᵥ g).linear = f.linear + g.linear

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 g : P1 →ᵃ[k] P2
p : P1
⊢ (f -ᵥ g : (a : P1) → V2) p = VSub.vsub.{u_4, u_5} (P := P2) ((f : (a : P1) → P2) p : P2) ((g : (a : P1) → P2) p : 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 g : P1 →ᵃ[k] P2
⊢ (f -ᵥ g).linear = f.linear - g.linear

Tactic:
rfl

Premises used: rfl