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
f : P →ᵃ[R] Q
h : Continuous f.toFun
⊢ (↑{ toAffineMap := f, cont := h : P →ᴬ[R] Q } : P →ᵃ[R] Q) = f

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
f : P →ᵃ[R] Q
h : Continuous f.toFun
⊢ (↑{ toAffineMap := f, cont := h : P →ᴬ[R] Q } : C(P, Q)) =
    { toFun := (⇑f : (a : P) → Q), continuous_toFun := h : C(P, Q) }

Tactic:
rfl

Premises used: toContinuousMap, 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
f : P →ᵃ[R] Q
h : Continuous f.toFun
⊢ Eq (α := (a : P) → Q) (⇑{ toAffineMap := f, cont := h : P →ᴬ[R] Q } : (a : P) → Q) (⇑f : (a : 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
f : P →ᴬ[R] Q
h : Continuous (↑f : P →ᵃ[R] Q).toFun
h₁ :
  ∀ (x : P),
    Eq.{u_5 + 1} (α := Q) (({ toAffineMap := (↑f : P →ᵃ[R] Q), cont := h : P →ᴬ[R] Q } : (a : P) → Q) x : Q)
      ((f : (a : P) → Q) x : Q)
⊢ { toAffineMap := (↑f : P →ᵃ[R] Q), cont := h : P →ᴬ[R] Q } = f

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
f : P →ᴬ[R] Q
h : Continuous (↑f : P →ᵃ[R] Q).toFun
x : P
⊢ Eq.{u_5 + 1} (α := Q) (({ toAffineMap := (↑f : P →ᵃ[R] Q), cont := h : P →ᴬ[R] Q } : (a : P) → Q) x : Q)
    ((f : (a : P) → Q) x : 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
f : P →ᴬ[R] Q
⊢ Continuous.{u_4, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)

Tactic:
f.2

Premises used: ContinuousAffineMap.cont
-- 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
q : Q
⊢ (⇑(const R P q) : (a : P) → Q) = Function.const 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
⊢ Nonempty Q

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
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
⊢ Eq.{u_4 + 1} (α := (a : P) → P) (⇑(id R P) : (a : P) → P) _root_.id

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
W₂ : Type u_6
Q₂ : Type u_7
inst_9 : AddCommGroup W₂
inst_10 : Module R W₂
inst_11 : TopologicalSpace Q₂
inst_12 : AddTorsor W₂ Q₂
f : Q →ᴬ[R] Q₂
g : P →ᴬ[R] Q
⊢ Eq (α := (a : P) → Q₂) (⇑(f.comp g) : (a : P) → Q₂)
    (Function.comp.{u_4 + 1, u_5 + 1, u_7 + 1} (β := Q) (⇑f : (a : Q) → Q₂) (⇑g : (a : 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
W₂ : Type u_6
Q₂ : Type u_7
inst_9 : AddCommGroup W₂
inst_10 : Module R W₂
inst_11 : TopologicalSpace Q₂
inst_12 : AddTorsor W₂ Q₂
f : Q →ᴬ[R] Q₂
g : P →ᴬ[R] Q
p : P
⊢ Eq.{u_7 + 1} (α := Q₂) ((f.comp g : (a : P) → Q₂) p : Q₂) ((f : (a : Q) → Q₂) ((g : (a : P) → Q) p : Q) : 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
f : P →ᴬ[R] Q
⊢ f.comp (id R P) = f

Tactic:
ext fun _ => rfl

Premises used: ContinuousAffineMap.ext, 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
f : P →ᴬ[R] Q
⊢ comp (id R Q) f = f

Tactic:
ext fun _ => rfl

Premises used: ContinuousAffineMap.ext, 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
f : P →ᴬ[R] Q
p₀ p₁ : P
c : R
rw :
  Eq.{u_5 + 1} (α := Q) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) ((AffineMap.lineMap p₀ p₁ : (a : R) → P) c : P) : Q)
    (((AffineMap.lineMap (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₀) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₁) : R →ᵃ[R] Q) :
          (a : R) → Q)
        c :
      Q)
rw₁ rw₂ :
  Eq.{u_5 + 1} (α := Q)
    (((AffineMap.lineMap (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₀) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₁) : R →ᵃ[R] Q) :
          (a : R) → Q)
        c :
      Q)
    (((AffineMap.lineMap (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₀) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₁) : R →ᵃ[R] Q) :
          (a : R) → Q)
        c :
      Q)
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) ((AffineMap.lineMap p₀ p₁ : (a : R) → P) c : P) : Q)
    (((AffineMap.lineMap ((f : (a : P) → Q) p₀) ((f : (a : P) → Q) p₁) : R →ᵃ[R] Q) : (a : R) → Q) c : Q)

Tactic:
rw [← ContinuousAffineMap.coe_toAffineMap, AffineMap.apply_lineMap]

Premises used: AffineMap.apply_lineMap, ContinuousAffineMap.coe_toAffineMap
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
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
p₀ p₁ : P
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace V
inst_7 : ContinuousSMul R V
inst_8 : ContinuousVAdd V P
⊢ Eq (α := R →ᵃ[R] P) (↑(lineMap p₀ p₁) : R →ᵃ[R] P) (AffineMap.lineMap p₀ p₁)

Tactic:
rfl

Premises used: AffineMap.lineMap, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
V : Type u_2
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
p₀ p₁ : P
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace V
inst_7 : ContinuousSMul R V
inst_8 : ContinuousVAdd V P
⊢ Eq (α := (a : R) → P) (⇑(lineMap p₀ p₁) : (a : R) → P) (⇑(AffineMap.lineMap p₀ p₁) : (a : R) → P)

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 R
inst_10 : TopologicalSpace V
inst_11 : TopologicalSpace W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
inst_14 : ContinuousVAdd V P
inst_15 : ContinuousVAdd W Q
f : P →ᴬ[R] Q
p₀ p₁ : P
c : R
simp_rw :
  Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) ((AffineMap.lineMap p₀ p₁ : (a : R) → P) c : P) : Q)
    (((AffineMap.lineMap ((f : (a : P) → Q) p₀) ((f : (a : P) → Q) p₁) : R →ᵃ[R] Q) : (a : R) → Q) c : Q)
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) ((lineMap p₀ p₁ : (a : R) → P) c : P) : Q)
    (((lineMap ((f : (a : P) → Q) p₀) ((f : (a : P) → Q) p₁) : R →ᴬ[R] Q) : (a : R) → Q) c : Q)

Tactic:
simp_rw [coe_lineMap_eq, apply_lineMap]

Premises used: ContinuousAffineMap.coe_lineMap_eq, ContinuousAffineMap.apply_lineMap
-- 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₂
inst_13 : TopologicalSpace V
inst_14 : IsTopologicalAddTorsor P
inst_15 : TopologicalSpace W
inst_16 : IsTopologicalAddTorsor Q
inst_17 : TopologicalSpace W₂
inst_18 : IsTopologicalAddTorsor Q₂
f : P →ᴬ[R] Q
rw : Continuous.{u_4, u_5} (X := P) (Y := Q) (⇑(↑f : P →ᵃ[R] Q) : (a : P) → Q)
⊢ Continuous.{u_2, u_3} (X := V) (Y := W) (⇑(↑f : P →ᵃ[R] Q).linear : (a : V) → W)

Tactic:
rw [AffineMap.continuous_linear_iff]

Premises used: AffineMap.continuous_linear_iff
-- 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₂
inst_13 : TopologicalSpace V
inst_14 : IsTopologicalAddTorsor P
inst_15 : TopologicalSpace W
inst_16 : IsTopologicalAddTorsor Q
inst_17 : TopologicalSpace W₂
inst_18 : IsTopologicalAddTorsor Q₂
f : P →ᴬ[R] Q
⊢ Continuous.{u_4, u_5} (X := P) (Y := Q) (⇑(↑f : P →ᵃ[R] Q) : (a : P) → Q)

Tactic:
f.cont

Premises used: ContinuousAffineMap.cont
-- 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₂
inst_13 : TopologicalSpace V
inst_14 : IsTopologicalAddTorsor P
inst_15 : TopologicalSpace W
inst_16 : IsTopologicalAddTorsor Q
inst_17 : TopologicalSpace W₂
inst_18 : IsTopologicalAddTorsor Q₂
f : P →ᴬ[R] Q
⊢ Continuous.{u_4, u_5} (X := P) (Y := Q) (⇑(↑f : P →ᵃ[R] Q) : (a : P) → Q)

Tactic:
exact f.cont

Premises used: ContinuousAffineMap.cont
-- 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
⊢ Eq (α := (a : V) → W) (⇑f.contLinear : (a : V) → W) (⇑(↑f : P →ᵃ[R] Q).linear : (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
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
⊢ (↑f.contLinear : V →ₗ[R] W) = (↑f : P →ᵃ[R] Q).linear

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 V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᵃ[R] Q
h : Continuous f.toFun
⊢ Eq (α := (a : V) → W) (⇑{ toAffineMap := f, cont := h : P →ᴬ[R] Q }.contLinear : (a : V) → W)
    (⇑f.linear : (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
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
⊢ Eq (α := (a : V) → W) (⇑(↑f : P →ᵃ[R] Q).linear : (a : V) → W) (⇑f.contLinear : (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
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
inst_9 : AddCommGroup W₂
inst_10 : Module R W₂
inst_11 : TopologicalSpace Q₂
inst_12 : AddTorsor W₂ Q₂
inst_13 : TopologicalSpace V
inst_14 : IsTopologicalAddTorsor P
inst_15 : TopologicalSpace W
inst_16 : IsTopologicalAddTorsor Q
inst_17 : TopologicalSpace W₂
inst_18 : IsTopologicalAddTorsor Q₂
f : P →ᴬ[R] Q
g : Q →ᴬ[R] Q₂
⊢ Eq (α := V →L[R] W₂) (g.comp f).contLinear (g.contLinear ∘SL f.contLinear)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, 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 V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
p : P
v : V
⊢ (f : (a : P) → Q) (v +ᵥ p) =
    HVAdd.hVAdd.{u_3, u_5, u_5} (α := W) (β := Q) ((f.contLinear : (a : V) → W) v : W) ((f : (a : P) → Q) p : Q)

Tactic:
f.map_vadd' p v

Premises used: AffineMap.map_vadd', 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
p₁ p₂ : P
⊢ (f.contLinear : (a : V) → W) (p₁ -ᵥ p₂) =
    VSub.vsub.{u_3, u_5} (P := Q) ((f : (a : P) → Q) p₁ : Q) ((f : (a : P) → Q) p₂ : Q)

Tactic:
f.toAffineMap.linearMap_vsub p₁ p₂

Premises used: AffineMap.linearMap_vsub, 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
q : Q
⊢ Eq (α := V →L[R] W) (contLinear (const R P q)) 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
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
⊢ Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0

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
refine_1 : ∀ (h : Eq (α := V →L[R] W) f.contLinear 0), (↑f : P →ᵃ[R] Q).linear = 0
refine_2 : ∀ (h : (↑f : P →ᵃ[R] Q).linear = 0), Eq (α := V →L[R] W) f.contLinear 0
⊢ Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0

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
refine_1 : ∀ (x : V), Eq.{u_3 + 1} (α := W) (((↑f : P →ᵃ[R] Q).linear : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)
⊢ (↑f : P →ᵃ[R] Q).linear = 0

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 : (↑f : P →ᵃ[R] Q).linear = 0
refine_2 : ∀ (x : V), Eq.{u_3 + 1} (α := W) ((f.contLinear : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)
⊢ Eq (α := V →L[R] W) f.contLinear 0

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
x : V
refine_1 : Eq.{u_3 + 1} (α := W) (((↑0 : V →ₗ[R] W) : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)
⊢ Eq.{u_3 + 1} (α := W) (((↑f : P →ᵃ[R] Q).linear : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)

Tactic:
rw [← coe_contLinear_eq_linear, h]

Premises used: ContinuousAffineMap.coe_contLinear_eq_linear
-- 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
x : V
⊢ Eq.{u_3 + 1} (α := W) (((↑0 : V →ₗ[R] W) : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)

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 : (↑f : P →ᵃ[R] Q).linear = 0
x : V
refine_2 : Eq.{u_3 + 1} (α := W) ((0 : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)
⊢ Eq.{u_3 + 1} (α := W) ((f.contLinear : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)

Tactic:
rw [← coe_linear_eq_coe_contLinear, h]

Premises used: ContinuousAffineMap.coe_linear_eq_coe_contLinear
-- 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 : (↑f : P →ᵃ[R] Q).linear = 0
x : V
⊢ Eq.{u_3 + 1} (α := W) ((0 : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)

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
⊢ Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0

Tactic:
have h₁ : f.contLinear = 0 ↔ (f : P →ᵃ[R] Q).linear = 0 := by
    refine ⟨fun h => ?_, fun h => ?_⟩ <;> ext
    · rw [← coe_contLinear_eq_linear, h]; rfl
    · rw [← coe_linear_eq_coe_contLinear, h]; rfl