mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹⁸ : Ring R
inst✝¹⁷ : AddCommGroup V
inst✝¹⁶ : Module R V
inst✝¹⁵ : TopologicalSpace P
inst✝¹⁴ : AddTorsor V P
inst✝¹³ : AddCommGroup W
inst✝¹² : Module R W
inst✝¹¹ : TopologicalSpace Q
inst✝¹⁰ : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst✝⁹ : AddCommGroup W₂
inst✝⁸ : Module R W₂
inst✝⁷ : TopologicalSpace Q₂
inst✝⁶ : AddTorsor W₂ Q₂
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalAddTorsor P
inst✝³ : TopologicalSpace W
inst✝² : IsTopologicalAddTorsor Q
inst✝¹ : TopologicalSpace W₂
inst✝ : IsTopologicalAddTorsor Q₂
f : P →ᴬ[R] Q
⊢ Continuous ⇑↑f

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹⁸ : Ring R
inst✝¹⁷ : AddCommGroup V
inst✝¹⁶ : Module R V
inst✝¹⁵ : TopologicalSpace P
inst✝¹⁴ : AddTorsor V P
inst✝¹³ : AddCommGroup W
inst✝¹² : Module R W
inst✝¹¹ : TopologicalSpace Q
inst✝¹⁰ : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst✝⁹ : AddCommGroup W₂
inst✝⁸ : Module R W₂
inst✝⁷ : TopologicalSpace Q₂
inst✝⁶ : AddTorsor W₂ Q₂
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalAddTorsor P
inst✝³ : TopologicalSpace W
inst✝² : IsTopologicalAddTorsor Q
inst✝¹ : TopologicalSpace W₂
inst✝ : IsTopologicalAddTorsor Q₂
f : P →ᴬ[R] Q
⊢ Continuous ⇑↑f
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous fun a ↦ ((↑e₁).prodCongr ↑e₂).toFun a

Tactic:
;

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous fun a ↦ ((↑e₁).prodCongr ↑e₂).toFun a
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous fun a ↦ (e₁ a.1, e₂ a.2)

Tactic:
;

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous fun a ↦ (e₁ a.1, e₂ a.2)
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous fun a ↦ ((↑e₁).prodCongr ↑e₂).invFun a

Tactic:
;

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous fun a ↦ ((↑e₁).prodCongr ↑e₂).invFun a
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous fun a ↦ (e₁.symm a.1, e₂.symm a.2)

Tactic:
;

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous fun a ↦ (e₁.symm a.1, e₂.symm a.2)
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous fun a ↦ (AffineEquiv.prodAssoc k P₁ P₂ P₃).toFun a

Tactic:
;

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous fun a ↦ (AffineEquiv.prodAssoc k P₁ P₂ P₃).toFun a
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : f.contLinear = 0
x✝ : V
⊢ ↑0 x✝ = 0 x✝

Tactic:
;

Goal state after:
case refine_1
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : f.contLinear = 0
x✝ : V
⊢ ↑0 x✝ = 0 x✝
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous fun a ↦ (a.1.1, a.1.2, a.2)

Tactic:
;

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous fun a ↦ (a.1.1, a.1.2, a.2)
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous fun a ↦ (AffineEquiv.prodAssoc k P₁ P₂ P₃).invFun a

Tactic:
;

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous fun a ↦ (AffineEquiv.prodAssoc k P₁ P₂ P₃).invFun a
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous fun a ↦ ((a.1, a.2.1), a.2.2)

Tactic:
;

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous fun a ↦ ((a.1, a.2.1), a.2.2)
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: case refine_2
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : (↑f).linear = 0
x✝ : V
⊢ 0 x✝ = 0 x✝

Tactic:
;

Goal state after:
case refine_2
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : (↑f).linear = 0
x✝ : V
⊢ 0 x✝ = 0 x✝
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace P
inst✝² : AddTorsor V P
s : AffineSubspace R P
inst✝¹ inst✝ : Nonempty ↥s
__AffineEquiv✝ : ↥s ≃ᵃ[R] ↥s := AffineEquiv.ofEq s s ⋯
⊢ Continuous (AffineEquiv.ofEq s s ⋯).toFun

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace P
inst✝² : AddTorsor V P
s : AffineSubspace R P
inst✝¹ inst✝ : Nonempty ↥s
__AffineEquiv✝ : ↥s ≃ᵃ[R] ↥s := AffineEquiv.ofEq s s ⋯
⊢ Continuous (AffineEquiv.ofEq s s ⋯).toFun
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace P
inst✝² : AddTorsor V P
s : AffineSubspace R P
inst✝¹ inst✝ : Nonempty ↥s
__AffineEquiv✝ : ↥s ≃ᵃ[R] ↥s := AffineEquiv.ofEq s s ⋯
⊢ Continuous (AffineEquiv.ofEq s s ⋯).invFun

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace P
inst✝² : AddTorsor V P
s : AffineSubspace R P
inst✝¹ inst✝ : Nonempty ↥s
__AffineEquiv✝ : ↥s ≃ᵃ[R] ↥s := AffineEquiv.ofEq s s ⋯
⊢ Continuous (AffineEquiv.ofEq s s ⋯).invFun
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: case inl
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
inst✝ : T1Space V
⊢ IsClosed ↑⊥.direction ↔ IsClosed ↑⊥

pp: case inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
inst✝ : T1Space V
s : AffineSubspace R P
x : P
hx : x ∈ ↑s
⊢ IsClosed ↑s.direction ↔ IsClosed ↑s

Tactic:
;

Goal state after:
case inl
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
inst✝ : T1Space V
⊢ IsClosed ↑⊥.direction ↔ IsClosed ↑⊥

case inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
inst✝ : T1Space V
s : AffineSubspace R P
x : P
hx : x ∈ ↑s
⊢ IsClosed ↑s.direction ↔ IsClosed ↑s
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑(const R P q) p✝ = (AffineMap.const R P q) p✝

Tactic:
;

Goal state after:
case refine_1
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑(const R P q) p✝ = (AffineMap.const R P q) p✝
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝²⁹ : Ring R
inst✝²⁸ : AddCommGroup V
inst✝²⁷ : Module R V
inst✝²⁶ : TopologicalSpace P
inst✝²⁵ : AddTorsor V P
inst✝²⁴ : AddCommGroup W
inst✝²³ : Module R W
inst✝²² : TopologicalSpace Q
inst✝²¹ : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst✝²⁰ : AddCommGroup W₂
inst✝¹⁹ : Module R W₂
inst✝¹⁸ : TopologicalSpace Q₂
inst✝¹⁷ : 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✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₁ →ᴬ[k] P₃
⊢ Continuous fun a ↦ ((↑f).prod ↑g).toFun a

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝²⁹ : Ring R
inst✝²⁸ : AddCommGroup V
inst✝²⁷ : Module R V
inst✝²⁶ : TopologicalSpace P
inst✝²⁵ : AddTorsor V P
inst✝²⁴ : AddCommGroup W
inst✝²³ : Module R W
inst✝²² : TopologicalSpace Q
inst✝²¹ : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst✝²⁰ : AddCommGroup W₂
inst✝¹⁹ : Module R W₂
inst✝¹⁸ : TopologicalSpace Q₂
inst✝¹⁷ : 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✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₁ →ᴬ[k] P₃
⊢ Continuous fun a ↦ ((↑f).prod ↑g).toFun a
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝²⁹ : Ring R
inst✝²⁸ : AddCommGroup V
inst✝²⁷ : Module R V
inst✝²⁶ : TopologicalSpace P
inst✝²⁵ : AddTorsor V P
inst✝²⁴ : AddCommGroup W
inst✝²³ : Module R W
inst✝²² : TopologicalSpace Q
inst✝²¹ : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst✝²⁰ : AddCommGroup W₂
inst✝¹⁹ : Module R W₂
inst✝¹⁸ : TopologicalSpace Q₂
inst✝¹⁷ : 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✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₁ →ᴬ[k] P₃
⊢ Continuous fun a ↦ (f a, g a)

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝²⁹ : Ring R
inst✝²⁸ : AddCommGroup V
inst✝²⁷ : Module R V
inst✝²⁶ : TopologicalSpace P
inst✝²⁵ : AddTorsor V P
inst✝²⁴ : AddCommGroup W
inst✝²³ : Module R W
inst✝²² : TopologicalSpace Q
inst✝²¹ : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst✝²⁰ : AddCommGroup W₂
inst✝¹⁹ : Module R W₂
inst✝¹⁸ : TopologicalSpace Q₂
inst✝¹⁷ : 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✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₁ →ᴬ[k] P₃
⊢ Continuous fun a ↦ (f a, g a)