-- Mathlib/Topology/Algebra/Affine.lean
theorem continuous_iff {f : E →ᵃ[R] F} : Continuous f ↔ Continuous f.linear

Proof state:
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ⇑f
⊢ Continuous ⇑f.linear

Tactic:
rw [decomp' f]

Result:
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ⇑f
⊢ Continuous (⇑f - fun x => f 0)

Proof state:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
⊢ Continuous ⇑f ↔ Continuous ⇑f.linear

Tactic:
constructor

Result:
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
⊢ Continuous ⇑f → Continuous ⇑f.linear

case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
⊢ Continuous ⇑f.linear → Continuous ⇑f

Proof state:
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ⇑f.linear
⊢ Continuous (⇑f.linear + fun x => f 0)

Tactic:
exact hc.add continuous_const

Result:
no goals

Proof state:
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
⊢ Continuous ⇑f → Continuous ⇑f.linear

Tactic:
intro hc

Result:
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ⇑f
⊢ Continuous ⇑f.linear

Proof state:
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ⇑f
⊢ Continuous (⇑f - fun x => f 0)

Tactic:
exact hc.sub continuous_const

Result:
no goals

Proof state:
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
⊢ Continuous ⇑f.linear → Continuous ⇑f

Tactic:
intro hc

Result:
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ⇑f.linear
⊢ Continuous ⇑f

Proof state:
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ⇑f.linear
⊢ Continuous ⇑f

Tactic:
rw [decomp f]

Result:
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ⇑f.linear
⊢ Continuous (⇑f.linear + fun x => f 0)