awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : TopologicalSpace W
inst_7 : IsTopologicalAddGroup V
inst_8 : IsTopologicalAddGroup W
f : V →ᵃ[R] W
h : Continuous f.toFun
⊢ (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W)
      ((⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W }.contLinear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
have rw : (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
  HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
    (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
Tactic: rw [ContinuousAffineMap.coe_mk_contLinear_eq_linear, ContinuousAffineMap.coe_mk, f.decomp,
    Pi.add_apply, LinearMap.map_zero, zero_add, ← Function.const_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : TopologicalSpace W
inst_7 : IsTopologicalAddGroup V
inst_8 : IsTopologicalAddGroup W
f : V →ᵃ[R] W
h : Continuous f.toFun
rw :
  (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
⊢ (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W)
      ((⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W }.contLinear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
have rw₁ : (⇑f : (a : V) → W) =
  HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
    (Function.const V ((f : (a : V) → W) 0) : V → W)
Tactic: rw [ContinuousAffineMap.coe_mk_contLinear_eq_linear, ContinuousAffineMap.coe_mk, f.decomp,
    Pi.add_apply, LinearMap.map_zero, zero_add, ← Function.const_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : TopologicalSpace W
inst_7 : IsTopologicalAddGroup V
inst_8 : IsTopologicalAddGroup W
f : V →ᵃ[R] W
h : Continuous f.toFun
rw :
  (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
rw₁ :
  (⇑f : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
      (Function.const V ((f : (a : V) → W) 0) : V → W)
⊢ (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W)
      ((⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W }.contLinear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
have rw₂ : (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
  (⇑f.linear : (a : V) → W) +
    Function.const V
      (HAdd.hAdd (α := (a : V) → W) (β := V → W) (⇑f.linear : (a : V) → W) (fun (x : V) ↦ (f : (a : V) → W) 0) 0)
Tactic: rw [ContinuousAffineMap.coe_mk_contLinear_eq_linear, ContinuousAffineMap.coe_mk, f.decomp,
    Pi.add_apply, LinearMap.map_zero, zero_add, ← Function.const_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : TopologicalSpace W
inst_7 : IsTopologicalAddGroup V
inst_8 : IsTopologicalAddGroup W
f : V →ᵃ[R] W
h : Continuous f.toFun
rw :
  (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
rw₁ :
  (⇑f : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
      (Function.const V ((f : (a : V) → W) 0) : V → W)
rw₂ :
  (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
    (⇑f.linear : (a : V) → W) +
      Function.const V
        (HAdd.hAdd (α := (a : V) → W) (β := V → W) (⇑f.linear : (a : V) → W) (fun (x : V) ↦ (f : (a : V) → W) 0) 0)
⊢ (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W)
      ((⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W }.contLinear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
have rw₃ : (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
  (⇑f.linear : (a : V) → W) +
    Function.const V (HAdd.hAdd (α := W) (β := W) ((f.linear : (a : V) → W) 0 : W) ((f : (a : V) → W) 0 : W))
Tactic: rw [ContinuousAffineMap.coe_mk_contLinear_eq_linear, ContinuousAffineMap.coe_mk, f.decomp,
    Pi.add_apply, LinearMap.map_zero, zero_add, ← Function.const_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : TopologicalSpace W
inst_7 : IsTopologicalAddGroup V
inst_8 : IsTopologicalAddGroup W
f : V →ᵃ[R] W
h : Continuous f.toFun
rw :
  (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
rw₁ :
  (⇑f : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
      (Function.const V ((f : (a : V) → W) 0) : V → W)
rw₂ :
  (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
    (⇑f.linear : (a : V) → W) +
      Function.const V
        (HAdd.hAdd (α := (a : V) → W) (β := V → W) (⇑f.linear : (a : V) → W) (fun (x : V) ↦ (f : (a : V) → W) 0) 0)
rw₃ :
  (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
    (⇑f.linear : (a : V) → W) +
      Function.const V (HAdd.hAdd (α := W) (β := W) ((f.linear : (a : V) → W) 0 : W) ((f : (a : V) → W) 0 : W))
⊢ (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W)
      ((⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W }.contLinear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
have rw₄ : (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
  (⇑f.linear : (a : V) → W) + Function.const V (HAdd.hAdd (α := W) (β := W) (0 : W) ((f : (a : V) → W) 0 : W))
Tactic: rw [ContinuousAffineMap.coe_mk_contLinear_eq_linear, ContinuousAffineMap.coe_mk, f.decomp,
    Pi.add_apply, LinearMap.map_zero, zero_add, ← Function.const_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : TopologicalSpace W
inst_7 : IsTopologicalAddGroup V
inst_8 : IsTopologicalAddGroup W
f : V →ᵃ[R] W
h : Continuous f.toFun
rw :
  (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
rw₁ :
  (⇑f : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
      (Function.const V ((f : (a : V) → W) 0) : V → W)
rw₂ :
  (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
    (⇑f.linear : (a : V) → W) +
      Function.const V
        (HAdd.hAdd (α := (a : V) → W) (β := V → W) (⇑f.linear : (a : V) → W) (fun (x : V) ↦ (f : (a : V) → W) 0) 0)
rw₃ :
  (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
    (⇑f.linear : (a : V) → W) +
      Function.const V (HAdd.hAdd (α := W) (β := W) ((f.linear : (a : V) → W) 0 : W) ((f : (a : V) → W) 0 : W))
rw₄ :
  (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
    (⇑f.linear : (a : V) → W) + Function.const V (HAdd.hAdd (α := W) (β := W) (0 : W) ((f : (a : V) → W) 0 : W))
⊢ (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W)
      ((⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W }.contLinear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
have rw₅ : (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
  HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
    (Function.const V ((f : (a : V) → W) 0) : V → W)
Tactic: rw [ContinuousAffineMap.coe_mk_contLinear_eq_linear, ContinuousAffineMap.coe_mk, f.decomp,
    Pi.add_apply, LinearMap.map_zero, zero_add, ← Function.const_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : TopologicalSpace W
inst_7 : IsTopologicalAddGroup V
inst_8 : IsTopologicalAddGroup W
f : V →ᵃ[R] W
h : Continuous f.toFun
rw :
  (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
rw₁ :
  (⇑f : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
      (Function.const V ((f : (a : V) → W) 0) : V → W)
rw₂ :
  (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
    (⇑f.linear : (a : V) → W) +
      Function.const V
        (HAdd.hAdd (α := (a : V) → W) (β := V → W) (⇑f.linear : (a : V) → W) (fun (x : V) ↦ (f : (a : V) → W) 0) 0)
rw₃ :
  (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
    (⇑f.linear : (a : V) → W) +
      Function.const V (HAdd.hAdd (α := W) (β := W) ((f.linear : (a : V) → W) 0 : W) ((f : (a : V) → W) 0 : W))
rw₄ :
  (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
    (⇑f.linear : (a : V) → W) + Function.const V (HAdd.hAdd (α := W) (β := W) (0 : W) ((f : (a : V) → W) 0 : W))
rw₅ :
  (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.linear : (a : V) → W) : (a : V) → W)
      (Function.const V ((f : (a : V) → W) 0) : V → W)
⊢ (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W)
      ((⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W }.contLinear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
have rw₆ : (HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0) =
  HAdd.hAdd (α := (a : V) → W) (⇑f.linear : (a : V) → W) fun (x : V) ↦ (f : (a : V) → W) 0
Tactic: rw [ContinuousAffineMap.coe_mk_contLinear_eq_linear, ContinuousAffineMap.coe_mk, f.decomp,
    Pi.add_apply, LinearMap.map_zero, zero_add, ← Function.const_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddTorsor W Q
inst_13 : TopologicalSpace Q
inst_14 : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
⊢ (fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
      ((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W))) f) =
    f
have h : ∀ (x : V),
  Eq.{u_5 + 1} (α := Q)
    (((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
            ((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W))) f) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddTorsor W Q
inst_13 : TopologicalSpace Q
inst_14 : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
x : V
⊢ Eq.{u_5 + 1} (α := Q)
    (((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
            ((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W))) f) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
have h : Eq.{u_5 + 1} (α := Q)
  ((HVAdd.hVAdd (α := V →ᴬ[R] W) (β := V →ᴬ[R] Q) (ContinuousLinearMap.toContinuousAffineMap f.contLinear)
          (const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) :
        (a : V) → Q)
      x :
    Q)
  ((f : (a : V) → Q) x : Q)
Tactic: simp_rw [vadd_apply, f.contLinear.coe_toContinuousAffineMap, coe_const, Function.const_apply,
      ← f.map_vadd, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddTorsor W Q
inst_13 : TopologicalSpace Q
inst_14 : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
x : V
h h₁ :
  Eq.{u_5 + 1} (α := Q)
    ((HVAdd.hVAdd (α := V →ᴬ[R] W) (β := V →ᴬ[R] Q) (ContinuousLinearMap.toContinuousAffineMap f.contLinear)
            (const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
⊢ Eq.{u_5 + 1} (α := Q)
    (((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
            ((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W))) f) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
have h₂ : HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q)
    ((ContinuousLinearMap.toContinuousAffineMap f.contLinear : (a : V) → W) x : W)
    (((const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) : (a : V) → Q) x : Q) =
  (f : (a : V) → Q) x
Tactic: simp_rw [vadd_apply, f.contLinear.coe_toContinuousAffineMap, coe_const, Function.const_apply,
      ← f.map_vadd, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddTorsor W Q
inst_13 : TopologicalSpace Q
inst_14 : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
x : V
h h₁ :
  Eq.{u_5 + 1} (α := Q)
    ((HVAdd.hVAdd (α := V →ᴬ[R] W) (β := V →ᴬ[R] Q) (ContinuousLinearMap.toContinuousAffineMap f.contLinear)
            (const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
h₂ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q)
      ((ContinuousLinearMap.toContinuousAffineMap f.contLinear : (a : V) → W) x : W)
      (((const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) : (a : V) → Q) x : Q) =
    (f : (a : V) → Q) x
⊢ Eq.{u_5 + 1} (α := Q)
    (((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
            ((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W))) f) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
have h₃ : HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q) ((f.contLinear : (a : V) → W) x : W)
    (((const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) : (a : V) → Q) x : Q) =
  (f : (a : V) → Q) x
Tactic: simp_rw [vadd_apply, f.contLinear.coe_toContinuousAffineMap, coe_const, Function.const_apply,
      ← f.map_vadd, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddTorsor W Q
inst_13 : TopologicalSpace Q
inst_14 : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
x : V
h h₁ :
  Eq.{u_5 + 1} (α := Q)
    ((HVAdd.hVAdd (α := V →ᴬ[R] W) (β := V →ᴬ[R] Q) (ContinuousLinearMap.toContinuousAffineMap f.contLinear)
            (const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
h₂ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q)
      ((ContinuousLinearMap.toContinuousAffineMap f.contLinear : (a : V) → W) x : W)
      (((const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) : (a : V) → Q) x : Q) =
    (f : (a : V) → Q) x
h₃ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q) ((f.contLinear : (a : V) → W) x : W)
      (((const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) : (a : V) → Q) x : Q) =
    (f : (a : V) → Q) x
⊢ Eq.{u_5 + 1} (α := Q)
    (((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
            ((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W))) f) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
have h₄ : HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q) ((f.contLinear : (a : V) → W) x : W)
    (Function.const V ((f : (a : V) → Q) 0) x : Q) =
  (f : (a : V) → Q) x
Tactic: simp_rw [vadd_apply, f.contLinear.coe_toContinuousAffineMap, coe_const, Function.const_apply,
      ← f.map_vadd, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddTorsor W Q
inst_13 : TopologicalSpace Q
inst_14 : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
x : V
h h₁ :
  Eq.{u_5 + 1} (α := Q)
    ((HVAdd.hVAdd (α := V →ᴬ[R] W) (β := V →ᴬ[R] Q) (ContinuousLinearMap.toContinuousAffineMap f.contLinear)
            (const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
h₂ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q)
      ((ContinuousLinearMap.toContinuousAffineMap f.contLinear : (a : V) → W) x : W)
      (((const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) : (a : V) → Q) x : Q) =
    (f : (a : V) → Q) x
h₃ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q) ((f.contLinear : (a : V) → W) x : W)
      (((const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) : (a : V) → Q) x : Q) =
    (f : (a : V) → Q) x
h₄ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q) ((f.contLinear : (a : V) → W) x : W)
      (Function.const V ((f : (a : V) → Q) 0) x : Q) =
    (f : (a : V) → Q) x
⊢ Eq.{u_5 + 1} (α := Q)
    (((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
            ((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W))) f) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
have h₅ : HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q) ((f.contLinear : (a : V) → W) x : W) ((f : (a : V) → Q) 0 : Q) =
  (f : (a : V) → Q) x
Tactic: simp_rw [vadd_apply, f.contLinear.coe_toContinuousAffineMap, coe_const, Function.const_apply,
      ← f.map_vadd, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddTorsor W Q
inst_13 : TopologicalSpace Q
inst_14 : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
x : V
h h₁ :
  Eq.{u_5 + 1} (α := Q)
    ((HVAdd.hVAdd (α := V →ᴬ[R] W) (β := V →ᴬ[R] Q) (ContinuousLinearMap.toContinuousAffineMap f.contLinear)
            (const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
h₂ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q)
      ((ContinuousLinearMap.toContinuousAffineMap f.contLinear : (a : V) → W) x : W)
      (((const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) : (a : V) → Q) x : Q) =
    (f : (a : V) → Q) x
h₃ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q) ((f.contLinear : (a : V) → W) x : W)
      (((const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) : (a : V) → Q) x : Q) =
    (f : (a : V) → Q) x
h₄ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q) ((f.contLinear : (a : V) → W) x : W)
      (Function.const V ((f : (a : V) → Q) 0) x : Q) =
    (f : (a : V) → Q) x
h₅ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q) ((f.contLinear : (a : V) → W) x : W) ((f : (a : V) → Q) 0 : Q) =
    (f : (a : V) → Q) x
⊢ Eq.{u_5 + 1} (α := Q)
    (((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
            ((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W))) f) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
have h₆ : Eq.{u_5 + 1} (α := Q) ((f : (a : V) → Q) (HVAdd.hVAdd (β := V) x 0) : Q) ((f : (a : V) → Q) x : Q)
Tactic: simp_rw [vadd_apply, f.contLinear.coe_toContinuousAffineMap, coe_const, Function.const_apply,
      ← f.map_vadd, vadd_eq_add, add_zero]