awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
⊢ 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)
have e_linear₁ : g (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (g p)
Tactic: rw [← f_add, h, ← g_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
⊢ 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)
have e_linear₂ : g (v +ᵥ p) = g (v +ᵥ p)
Tactic: rw [← f_add, h, ← g_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
| VSub.vsub.{u_4, u_5} (P := P2) ((f : (a : P1) → P2) p1 : P2) ((f : (a : P1) → P2) p2 : P2)
have rw : ((f.linear : (a : V1) → V2) (p1 -ᵥ p2) : V2)
Tactic: rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ (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)
have 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)
Tactic: conv_rhs => rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
⊢ (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)
have conv_rhs₁ : Eq.{u_4 + 1} (α := V2) ((f.linear : (a : V1) → V2) (p1 -ᵥ p2) : V2) ((f.linear : (a : V1) → V2) (p1 -ᵥ p2) : V2)
Tactic: conv_rhs => rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
⊢ f = g
have h : ∀ (q : P1), Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) q : P2) ((g : (a : P1) → P2) q : P2)
Tactic: ext q
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
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
⊢ Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) q : P2) ((g : (a : P1) → P2) q : P2)
have hgl : (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
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
⊢ Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) q : P2) ((g : (a : P1) → P2) q : P2)
have 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)
Tactic: have := f.map_vadd' q (q -ᵥ p)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
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)
⊢ Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) q : P2) ((g : (a : P1) → P2) q : P2)
have 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)
Tactic: rw [h₁, hgl, toFun_eq_coe, map_vadd, linearMap_vsub, h₂] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ P1
have inhabit : (inhabited_h : Inhabited P1) → P1
Tactic: inhabit P1
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) default : P2) ((g : (a : P1) → P2) default : P2)
have rw : Eq.{u_5 + 1} (α := P2) ((g : (a : P1) → P2) default : P2) ((g : (a : P1) → P2) default : P2)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
have refine_1 : ∀ (h : f.linear = 0), ∃ (q : P2), f = const k P1 q
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ f.linear = 0 ↔ ∃ (q : P2), f = const k P1 q
have refine_2 : ∀ (h : ∃ (q : P2), f = const k P1 q), f.linear = 0
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ ∃ (q : P2), f = const k P1 q
have h₁ : f = const k P1 ((f : (a : P1) → P2) (Classical.arbitrary P1))
Tactic: use f (Classical.arbitrary P1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ f = const k P1 ((f : (a : P1) → P2) (Classical.arbitrary P1))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ 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)
have h₁ : Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) p : P2)
  (Function.const P1 ((f : (a : P1) → P2) (Classical.arbitrary P1)) p : P2)
Tactic: rw [coe_const, Function.const_apply, ← @vsub_eq_zero_iff_eq V2, ← f.linearMap_vsub, h,
      LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
⊢ 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)
have h₂ : Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) p : P2) ((f : (a : P1) → P2) (Classical.arbitrary P1) : P2)
Tactic: rw [coe_const, Function.const_apply, ← @vsub_eq_zero_iff_eq V2, ← f.linearMap_vsub, h,
      LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
⊢ 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)
have h₃ : VSub.vsub.{u_4, u_5} (P := P2) ((f : (a : P1) → P2) p : P2) ((f : (a : P1) → P2) (Classical.arbitrary P1) : P2) = 0
Tactic: rw [coe_const, Function.const_apply, ← @vsub_eq_zero_iff_eq V2, ← f.linearMap_vsub, h,
      LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ 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)
have h₄ : Eq.{u_4 + 1} (α := V2) ((f.linear : (a : V1) → V2) (p -ᵥ Classical.arbitrary P1) : V2) (0 : V2)
Tactic: rw [coe_const, Function.const_apply, ← @vsub_eq_zero_iff_eq V2, ← f.linearMap_vsub, h,
      LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
⊢ 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)
have h₅ : Eq.{u_4 + 1} (α := V2) ((0 : (a : V1) → V2) (p -ᵥ Classical.arbitrary P1) : V2) (0 : V2)
Tactic: rw [coe_const, Function.const_apply, ← @vsub_eq_zero_iff_eq V2, ← f.linearMap_vsub, h,
      LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
⊢ 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)
have h₆ : Eq.{u_4 + 1} (α := V2) 0 0
Tactic: rw [coe_const, Function.const_apply, ← @vsub_eq_zero_iff_eq V2, ← f.linearMap_vsub, h,
      LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ f.linear = 0
have refine_2 : ∀ (q : P2), Eq (α := V1 →ₗ[k] V2) (linear (const k P1 q)) 0
Tactic: rcases h with ⟨q, rfl⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ f (v +ᵥ p') = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2) (f p')
have 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')
Tactic: rw [h, h p', vadd_vsub_assoc, f'.map_add, vadd_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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')
⊢ f (v +ᵥ p') = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2) (f p')
have 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))
Tactic: rw [h, h p', vadd_vsub_assoc, f'.map_add, vadd_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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))
⊢ f (v +ᵥ p') = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2) (f p')
have 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))
Tactic: rw [h, h p', vadd_vsub_assoc, f'.map_add, vadd_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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))
⊢ f (v +ᵥ p') = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2) (f p')
have 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))
Tactic: rw [h, h p', vadd_vsub_assoc, f'.map_add, vadd_vadd]