awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
⊢ f = const R P q ↔ (↑f : P →ᵃ[R] Q) = AffineMap.const R P q

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

Premises used: Iff.intro
-- 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
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
refine_1 : ∀ (h : f = const R P q), (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
refine_2 : ∀ (h : (↑f : P →ᵃ[R] Q) = AffineMap.const R P q), f = const R P q
⊢ f = const R P q ↔ (↑f : P →ᵃ[R] Q) = AffineMap.const R P q

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- 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
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
h : f = const R P q
refine_1 :
  ∀ (p : P),
    Eq.{u_5 + 1} (α := Q) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p : Q) ((AffineMap.const R P q : (a : P) → Q) p : Q)
⊢ (↑f : P →ᵃ[R] Q) = AffineMap.const R P q

Tactic:
ext
-- 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
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
h : (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
refine_2 : ∀ (x : P), Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
⊢ f = const R P q

Tactic:
ext
-- 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
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
h : f = const R P q
p : P
refine_1 :
  Eq.{u_5 + 1} (α := Q) (((↑(const R P q) : P →ᵃ[R] Q) : (a : P) → Q) p : Q)
    ((AffineMap.const R P q : (a : P) → Q) p : Q)
⊢ Eq.{u_5 + 1} (α := Q) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p : Q) ((AffineMap.const R P q : (a : P) → Q) p : Q)

Tactic:
rw [h]
-- 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
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
h : f = const R P q
p : P
⊢ Eq.{u_5 + 1} (α := Q) (((↑(const R P q) : P →ᵃ[R] Q) : (a : P) → Q) p : Q)
    ((AffineMap.const R P q : (a : P) → Q) p : Q)

Tactic:
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
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
h : (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
x : P
refine_2 : Eq.{u_5 + 1} (α := Q) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
refine_2₁ : Eq.{u_5 + 1} (α := Q) ((AffineMap.const R P q : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
refine_2₂ : q = (const R P q : (a : P) → Q) x
refine_2₃ : q = Function.const P q x
refine_2₄ refine_2₅ : q = q
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)

Tactic:
rw [← coe_toAffineMap, h, AffineMap.const_apply, coe_const, Function.const_apply]

Premises used: Function.const_apply, ContinuousAffineMap.coe_toAffineMap, AffineMap.const_apply, ContinuousAffineMap.coe_const
-- 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
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
⊢ ∀ (q : Q), f = const R P q ↔ (↑f : P →ᵃ[R] Q) = AffineMap.const R P q

Tactic:
have h₂ : ∀ q : Q, f = const R P q ↔ (f : P →ᵃ[R] Q) = AffineMap.const R P q := by
    intro q
    refine ⟨fun h => ?_, fun h => ?_⟩ <;> ext
    · rw [h]; rfl
    · rw [← coe_toAffineMap, h, AffineMap.const_apply, coe_const, Function.const_apply]
-- 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
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
h₂ : ∀ (q : Q), f = const R P q ↔ (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
simp_rw : (↑f : P →ᵃ[R] Q).linear = 0 ↔ ∃ (q : Q), (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
⊢ Eq (α := V →L[R] W) f.contLinear 0 ↔ ∃ (q : Q), f = const R P q

Tactic:
simp_rw [h₁, h₂]
-- 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
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
h₂ : ∀ (q : Q), f = const R P q ↔ (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
⊢ (↑f : P →ᵃ[R] Q).linear = 0 ↔ ∃ (q : Q), (↑f : P →ᵃ[R] Q) = AffineMap.const R P q

Tactic:
(f : P →ᵃ[R] Q).linear_eq_zero_iff_exists_const

Premises used: AffineMap.linear_eq_zero_iff_exists_const, ContinuousAffineMap.toAffineMap
-- 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
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
h₂ : ∀ (q : Q), f = const R P q ↔ (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
⊢ (↑f : P →ᵃ[R] Q).linear = 0 ↔ ∃ (q : Q), (↑f : P →ᵃ[R] Q) = AffineMap.const R P q

Tactic:
exact (f : P →ᵃ[R] Q).linear_eq_zero_iff_exists_const

Premises used: AffineMap.linear_eq_zero_iff_exists_const, ContinuousAffineMap.toAffineMap
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
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 W
⊢ Eq (α := (a : P) → W) (⇑0 : (a : P) → W) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
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 W
x : P
⊢ Eq.{u_3 + 1} (α := W) ((0 : (a : P) → W) x : W) (0 : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
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
S : Type u_10
inst_7 : TopologicalSpace W
inst_8 : Monoid S
inst_9 : DistribMulAction S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
t : S
f : P →ᴬ[R] W
⊢ (⇑(t • f) : (a : P) → W) = HSMul.hSMul (β := (a : P) → W) t (⇑f : (a : P) → W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
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
S : Type u_10
inst_7 : TopologicalSpace W
inst_8 : Monoid S
inst_9 : DistribMulAction S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
t : S
f : P →ᴬ[R] W
x : P
⊢ (t • f : (a : P) → W) x = HSMul.hSMul (β := W) t ((f : (a : P) → W) x : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
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
S : Type u_10
inst_7 : TopologicalSpace W
inst_8 : Monoid S
inst_9 : DistribMulAction S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : TopologicalSpace V
inst_13 : IsTopologicalAddTorsor P
inst_14 : IsTopologicalAddGroup W
t : S
f : P →ᴬ[R] W
⊢ (t • f).contLinear = HSMul.hSMul (β := V →L[R] W) t f.contLinear

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
P : Type u_4
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 W
inst_8 : IsTopologicalAddGroup W
f g : P →ᴬ[R] W
⊢ (⇑(f + g) : (a : P) → W) = HAdd.hAdd (α := (a : P) → W) (⇑f : (a : P) → W) (⇑g : (a : P) → W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
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 W
inst_8 : IsTopologicalAddGroup W
f g : P →ᴬ[R] W
x : P
⊢ (f + g : (a : P) → W) x = HAdd.hAdd (α := W) (β := W) ((f : (a : P) → W) x : W) ((g : (a : P) → W) x : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
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 W
inst_8 : IsTopologicalAddGroup W
f g : P →ᴬ[R] W
⊢ (⇑(f - g) : (a : P) → W) = HSub.hSub (α := (a : P) → W) (⇑f : (a : P) → W) (⇑g : (a : P) → W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
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 W
inst_8 : IsTopologicalAddGroup W
f g : P →ᴬ[R] W
x : P
⊢ (f - g : (a : P) → W) x = HSub.hSub (α := W) (β := W) ((f : (a : P) → W) x : W) ((g : (a : P) → W) x : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
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 W
inst_8 : IsTopologicalAddGroup W
f : P →ᴬ[R] W
⊢ Eq (α := (a : P) → W) (⇑(-f) : (a : P) → W) (-(⇑f : (a : P) → W))

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
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 W
inst_8 : IsTopologicalAddGroup W
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
⊢ Eq (α := V →L[R] W) (contLinear.{u_1, u_2, u_3, u_4, u_3} (P := P) (Q := W) 0) 0

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
P : Type u_4
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 W
inst_8 : IsTopologicalAddGroup W
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
f g : P →ᴬ[R] W
⊢ (f + g).contLinear = HAdd.hAdd (α := V →L[R] W) f.contLinear g.contLinear

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
P : Type u_4
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 W
inst_8 : IsTopologicalAddGroup W
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
f g : P →ᴬ[R] W
⊢ (f - g).contLinear = HSub.hSub (α := V →L[R] W) f.contLinear g.contLinear

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
P : Type u_4
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 W
inst_8 : IsTopologicalAddGroup W
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
f : P →ᴬ[R] W
⊢ Eq (α := V →L[R] W) (-f).contLinear (-f.contLinear)

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
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
inst_9 : TopologicalSpace W
inst_10 : IsTopologicalAddGroup W
inst_11 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] W
g : P →ᴬ[R] Q
p : P
⊢ (f +ᵥ g : (a : P) → Q) p =
    HVAdd.hVAdd.{u_3, u_5, u_5} (α := W) (β := Q) ((f : (a : P) → W) p : W) ((g : (a : P) → Q) p : Q)

Tactic:
rfl

Premises used: 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
inst_9 : TopologicalSpace W
inst_10 : IsTopologicalAddGroup W
inst_11 : IsTopologicalAddTorsor Q
f g : P →ᴬ[R] Q
p : P
⊢ (f -ᵥ g : (a : P) → W) p = VSub.vsub.{u_3, u_5} (P := Q) ((f : (a : P) → Q) p : Q) ((g : (a : P) → Q) p : Q)

Tactic:
rfl

Premises used: 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
inst_9 : TopologicalSpace W
inst_10 : IsTopologicalAddGroup W
inst_11 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] W
g : P →ᴬ[R] Q
⊢ (↑(f +ᵥ g) : P →ᵃ[R] Q) = (↑f : P →ᵃ[R] W) +ᵥ (↑g : P →ᵃ[R] Q)

Tactic:
rfl

Premises used: 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
inst_9 : TopologicalSpace W
inst_10 : IsTopologicalAddGroup W
inst_11 : IsTopologicalAddTorsor Q
f g : P →ᴬ[R] Q
⊢ (↑(f -ᵥ g) : P →ᵃ[R] W) = (↑f : P →ᵃ[R] Q) -ᵥ (↑g : P →ᵃ[R] Q)

Tactic:
rfl

Premises used: 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
inst_9 : TopologicalSpace W
inst_10 : IsTopologicalAddGroup W
inst_11 : IsTopologicalAddTorsor Q
inst_12 : ContinuousConstSMul R W
inst_13 : SMulCommClass R R W
f g : P →ᴬ[R] Q
c : R
p : P
⊢ Eq.{u_5 + 1} (α := Q) ((((AffineMap.lineMap f g : (a : R) → P →ᴬ[R] Q) c : P →ᴬ[R] Q) : (a : P) → Q) p : Q)
    (((AffineMap.lineMap ((f : (a : P) → Q) p) ((g : (a : P) → Q) p) : R →ᵃ[R] Q) : (a : R) → Q) c : Q)

Tactic:
simp [AffineMap.lineMap_apply]

Premises used: AffineMap.lineMap_apply
-- 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
inst_9 : TopologicalSpace W
inst_10 : IsTopologicalAddGroup W
inst_11 : IsTopologicalAddTorsor Q
inst_12 : TopologicalSpace V
inst_13 : IsTopologicalAddTorsor P
f : P →ᴬ[R] W
g : P →ᴬ[R] Q
⊢ (f +ᵥ g).contLinear = HAdd.hAdd (α := V →L[R] W) f.contLinear g.contLinear

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
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
inst_9 : TopologicalSpace W
inst_10 : IsTopologicalAddGroup W
inst_11 : IsTopologicalAddTorsor Q
inst_12 : TopologicalSpace V
inst_13 : IsTopologicalAddTorsor P
f g : P →ᴬ[R] Q
⊢ (f -ᵥ g).contLinear = HSub.hSub (α := V →L[R] W) f.contLinear g.contLinear

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
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₁) ↦ ((f : (a : P₁) → P₂) a, (g : (a : P₁) → P₃) a)
⊢ Continuous (Y := P₂ × P₃) fun (a : P₁) ↦ ((↑f : P₁ →ᵃ[k] P₂).prod (↑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₁) ↦ ((f : (a : P₁) → P₂) a, (g : (a : P₁) → P₃) a)

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
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₃
⊢ Eq (α := (a : P₁) → P₂ × P₃) (⇑(f.prod g) : (a : P₁) → P₂ × P₃)
    (Function.prod (α := fun (a : P₁) ↦ P₂) (β := fun (a : P₁) ↦ P₃) (⇑f : (a : P₁) → P₂) (⇑g : (a : P₁) → P₃))

Tactic:
rfl

Premises used: Function.prod, rfl