-- Mathlib/Analysis/Complex/Liouville.lean
theorem apply_eq_apply_of_bounded {f : E → F} (hf : Differentiable ℂ f) (hb : IsBounded (range f))
    (z w : E) : f z = f w

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
this : g 0 = g 1
⊢ f z = f w

Tactic:
simpa [g]

Result:
no goals

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ g 0 = g 1

Tactic:
apply liouville_theorem_aux

Result:
case hf
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ Differentiable ℂ g

case hb
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ Bornology.IsBounded (range g)

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ f z = f w

Tactic:
suffices g 0 = g 1 by simpa [g]

Result:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ g 0 = g 1

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
⊢ f z = f w

Tactic:
set g : ℂ → F := f ∘ fun t : ℂ => t • (w - z) + z

Result:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ f z = f w

Proof state:
case hf
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ Differentiable ℂ g

case hb
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ Bornology.IsBounded (range g)

Tactic:
exacts [hf.comp ((differentiable_id.smul_const (w - z)).add_const z),
  hb.subset (range_comp_subset_range _ _)]

Result:
no goals