awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
f : P₁ →ᴬ[k] P₂
g : P₁ →ᴬ[k] P₃
p : P₁
⊢ Eq (α := P₂ × P₃) ((f.prod g : (a : P₁) → P₂ × P₃) p : P₂ × P₃)
    (((f : (a : P₁) → P₂) p, (g : (a : P₁) → P₃) p) : P₂ × P₃)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst_9 : AddCommGroup W₂
inst_10 : Module R W₂
inst_11 : TopologicalSpace Q₂
inst_12 : AddTorsor W₂ Q₂
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
P₄ : Type u_14
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
V₄ : Type u_18
inst_13 : Ring k
inst_14 : AddCommGroup V₁
inst_15 : Module k V₁
inst_16 : AddTorsor V₁ P₁
inst_17 : TopologicalSpace P₁
inst_18 : AddCommGroup V₂
inst_19 : Module k V₂
inst_20 : AddTorsor V₂ P₂
inst_21 : TopologicalSpace P₂
inst_22 : AddCommGroup V₃
inst_23 : Module k V₃
inst_24 : AddTorsor V₃ P₃
inst_25 : TopologicalSpace P₃
inst_26 : AddCommGroup V₄
inst_27 : Module k V₄
inst_28 : AddTorsor V₄ P₄
inst_29 : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₃ →ᴬ[k] P₄
dsimp : Continuous (Y := P₂ × P₄) fun (a : P₁ × P₃) ↦ ((f : (a : P₁) → P₂) a.1, (g : (a : P₃) → P₄) a.2)
⊢ Continuous (Y := P₂ × P₄) fun (a : P₁ × P₃) ↦ ((↑f : P₁ →ᵃ[k] P₂).prodMap (↑g : P₃ →ᵃ[k] P₄)).toFun a

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst_9 : AddCommGroup W₂
inst_10 : Module R W₂
inst_11 : TopologicalSpace Q₂
inst_12 : AddTorsor W₂ Q₂
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
P₄ : Type u_14
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
V₄ : Type u_18
inst_13 : Ring k
inst_14 : AddCommGroup V₁
inst_15 : Module k V₁
inst_16 : AddTorsor V₁ P₁
inst_17 : TopologicalSpace P₁
inst_18 : AddCommGroup V₂
inst_19 : Module k V₂
inst_20 : AddTorsor V₂ P₂
inst_21 : TopologicalSpace P₂
inst_22 : AddCommGroup V₃
inst_23 : Module k V₃
inst_24 : AddTorsor V₃ P₃
inst_25 : TopologicalSpace P₃
inst_26 : AddCommGroup V₄
inst_27 : Module k V₄
inst_28 : AddTorsor V₄ P₄
inst_29 : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₃ →ᴬ[k] P₄
⊢ Continuous (Y := P₂ × P₄) fun (a : P₁ × P₃) ↦ ((f : (a : P₁) → P₂) a.1, (g : (a : P₃) → P₄) a.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
P₄ : Type u_14
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
V₄ : Type u_18
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₃ →ᴬ[k] P₄
⊢ Eq (α := (a : P₁ × P₃) → P₂ × P₄) (⇑(f.prodMap g) : (a : P₁ × P₃) → P₂ × P₄)
    (Prod.map (⇑f : (a : P₁) → P₂) (⇑g : (a : P₃) → P₄))

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
P₄ : Type u_14
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
V₄ : Type u_18
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₃ →ᴬ[k] P₄
x : P₁ × P₃
⊢ Eq (α := P₂ × P₄) ((f.prodMap g : (a : P₁ × P₃) → P₂ × P₄) x : P₂ × P₄)
    (((f : (a : P₁) → P₂) x.1, (g : (a : P₃) → P₄) x.2) : P₂ × P₄)

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : TopologicalSpace V₁
inst_14 : IsTopologicalAddTorsor P₁
inst_15 : TopologicalSpace V₂
inst_16 : IsTopologicalAddTorsor P₂
inst_17 : TopologicalSpace V₃
inst_18 : IsTopologicalAddTorsor P₃
f : P₁ →ᴬ[k] P₂
g : P₁ →ᴬ[k] P₃
⊢ Eq (α := V₁ →L[k] V₂ × V₃) (f.prod g).contLinear (ContinuousLinearMap.prod f.contLinear g.contLinear)

Tactic:
rfl

Premises used: ContinuousAffineMap.contLinear, Function.prod, ContinuousLinearMap.prod, LinearMap.prod, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
P₄ : Type u_14
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
V₄ : Type u_18
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
inst_17 : TopologicalSpace V₁
inst_18 : IsTopologicalAddTorsor P₁
inst_19 : TopologicalSpace V₂
inst_20 : IsTopologicalAddTorsor P₂
inst_21 : TopologicalSpace V₃
inst_22 : IsTopologicalAddTorsor P₃
inst_23 : TopologicalSpace V₄
inst_24 : IsTopologicalAddTorsor P₄
f : P₁ →ᴬ[k] P₂
g : P₃ →ᴬ[k] P₄
⊢ Eq (α := V₁ × V₃ →L[k] V₂ × V₄) (f.prodMap g).contLinear (ContinuousLinearMap.prodMap f.contLinear g.contLinear)

Tactic:
rfl

Premises used: ContinuousAffineMap.contLinear, ContinuousLinearMap.prodMap, Function.prod, ContinuousLinearMap.prod, LinearMap.prod, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
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
f : V →L[R] W
⊢ ∀ (p v : V),
    (f : (a : V) → W) (v +ᵥ p) =
      HVAdd.hVAdd (α := W) (β := W) (((↑f : V →ₗ[R] W) : (a : V) → W) v : W) ((f : (a : V) → W) p : W)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
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
f : V →L[R] W
⊢ Eq (α := (a : V) → W) (⇑f.toContinuousAffineMap : (a : V) → W) (⇑f : (a : V) → W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
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
f : V →L[R] W
⊢ Eq.{u_3 + 1} (α := W) ((f.toContinuousAffineMap : (a : V) → W) 0 : W) (0 : W)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
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 →L[R] W
⊢ f.toContinuousAffineMap.contLinear = f

Tactic:
rfl

Premises used: ContinuousAffineMap.contLinear, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
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
rcases :
  ∀ (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)
⊢ (⇑f : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.contLinear : (a : V) → W) : (a : V) → W)
      (Function.const V ((f : (a : V) → W) 0) : V → W)

Tactic:
rcases f with ⟨f, h⟩
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
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)
rw₆ 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
⊢ (⇑{ 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)

Tactic:
rw [ContinuousAffineMap.coe_mk_contLinear_eq_linear, ContinuousAffineMap.coe_mk, f.decomp,
    Pi.add_apply, LinearMap.map_zero, zero_add, ← Function.const_def]

Premises used: ContinuousAffineMap.coe_mk, ContinuousAffineMap.coe_mk_contLinear_eq_linear, LinearMap.map_zero, zero_add, Pi.add_apply, Function.const_def, AffineMap.decomp
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
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
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)
⊢ (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

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
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
h₆ : Eq.{u_5 + 1} (α := Q) ((f : (a : V) → Q) (HVAdd.hVAdd (β := V) x 0) : Q) ((f : (a : V) → Q) x : Q)
h₇ : Eq.{u_5 + 1} (α := Q) ((f : (a : V) → Q) (x + 0) : 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)

Tactic:
simp_rw [vadd_apply, f.contLinear.coe_toContinuousAffineMap, coe_const, Function.const_apply,
      ← f.map_vadd, vadd_eq_add, add_zero]

Premises used: Function.const_apply, ContinuousAffineMap.contLinear, ContinuousAffineMap.map_vadd, ContinuousAffineMap.coe_const, vadd_eq_add, add_zero, ContinuousLinearMap.coe_toContinuousAffineMap, ContinuousAffineMap.vadd_apply
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
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
⊢ IsTopologicalAddGroup W

Tactic:
haveI := IsTopologicalAddTorsor.to_isTopologicalAddGroup W Q
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
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
this : IsTopologicalAddGroup W
v : Q
f : V →L[R] W
fst :
  ((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W)))
        ((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
          (v, f))).1 =
    (v, f).1
snd :
  ∀ (x : V),
    Eq.{u_4 + 1} (α := W)
      ((((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W)))
                ((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
                  (v, f))).2 :
            (a : V) → W)
          x :
        W)
      (((v, f).2 : (a : V) → W) x : W)
⊢ (fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W)))
      ((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1)) (v, f)) =
    (v, f)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
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
this : IsTopologicalAddGroup W
v : Q
f : V →L[R] W
⊢ ((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W)))
        ((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
          (v, f))).1 =
    (v, f).1

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
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
this : IsTopologicalAddGroup W
v : Q
f : V →L[R] W
x : V
⊢ Eq.{u_4 + 1} (α := W)
    ((((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W)))
              ((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
                (v, f))).2 :
          (a : V) → W)
        x :
      W)
    (((v, f).2 : (a : V) → W) x : W)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace W
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace Q
inst_10 : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
⊢ Eq.{u_5 + 1} (α := Q) (((decompEquiv R V Q : (a : V →ᴬ[R] Q) → Q × (V →L[R] W)) f).1 : Q) ((f : (a : V) → Q) 0 : Q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace W
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace Q
inst_10 : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
⊢ Eq (α := V →L[R] W) ((decompEquiv R V Q : (a : V →ᴬ[R] Q) → Q × (V →L[R] W)) f).2 f.contLinear

Tactic:
rfl

Premises used: ContinuousAffineMap.contLinear, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace W
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace Q
inst_10 : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
x : V
⊢ (((Equiv.symm (decompEquiv R V Q) : (a : Q × (V →L[R] W)) → V →ᴬ[R] Q) p : V →ᴬ[R] Q) : (a : V) → Q) x =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) ((p.2 : (a : V) → W) x : W) p.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace W
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace Q
inst_10 : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
⊢ IsTopologicalAddGroup W

Tactic:
haveI := IsTopologicalAddTorsor.to_isTopologicalAddGroup W Q
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace W
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace Q
inst_10 : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
this : IsTopologicalAddGroup W
h :
  ∀ (x : V),
    Eq.{u_4 + 1} (α := W)
      ((contLinear.{u_1, u_3, u_4, u_3, u_5} (P := V) (Q := Q)
              ((Equiv.symm (decompEquiv R V Q) : (a : Q × (V →L[R] W)) → V →ᴬ[R] Q) p) :
            (a : V) → W)
          x :
        W)
      ((p.2 : (a : V) → W) x : W)
⊢ contLinear.{u_1, u_3, u_4, u_3, u_5} (P := V) (Q := Q)
      ((Equiv.symm (decompEquiv R V Q) : (a : Q × (V →L[R] W)) → V →ᴬ[R] Q) p) =
    p.2

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace W
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace Q
inst_10 : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
this : IsTopologicalAddGroup W
x : V
⊢ Eq.{u_4 + 1} (α := W)
    ((contLinear.{u_1, u_3, u_4, u_3, u_5} (P := V) (Q := Q)
            ((Equiv.symm (decompEquiv R V Q) : (a : Q × (V →L[R] W)) → V →ᴬ[R] Q) p) :
          (a : V) → W)
        x :
      W)
    ((p.2 : (a : V) → W) x : W)

Tactic:
simp [decompEquiv]

Premises used: ContinuousAffineMap.decompEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
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 : IsTopologicalAddGroup W
f : V →ᴬ[R] W
⊢ Eq.{u_4 + 1} (α := W) (((decompLinearEquiv R S V W : (a : V →ᴬ[R] W) → W × (V →L[R] W)) f).1 : W)
    ((f : (a : V) → W) 0 : W)

Tactic:
rfl

Premises used: rfl