-- Mathlib/Topology/Path.lean
theorem trans_continuous_family {ι : Type*} [TopologicalSpace ι]
    {a b c : ι → X} (γ₁ : ∀ t : ι, Path (a t) (b t)) (h₁ : Continuous ↿γ₁)
    (γ₂ : ∀ t : ι, Path (b t) (c t)) (h₂ : Continuous ↿γ₂) :
    Continuous ↿fun t => (γ₁ t).trans (γ₂ t)

Proof state:
case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
⊢ Continuous ((fun p => (γ₁ p.1).extend p.2) ∘ Prod.map id fun x => 2 * ↑x)

Tactic:
exact h₁'.comp (continuous_id.prodMap <| continuous_const.mul continuous_subtype_val)

Result:
no goals

Proof state:
case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
⊢ Continuous ((fun p => (γ₂ p.1).extend p.2) ∘ Prod.map id fun x => 2 * ↑x - 1)

Tactic:
exact
  h₂'.comp
    (continuous_id.prodMap <|
      (continuous_const.mul continuous_subtype_val).sub continuous_const)

Result:
no goals

Proof state:
case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
st : ι × ↑I
hst : ↑st.2 = 1 / 2
⊢ (γ₁ st.1).extend (2 * ↑st.2) = (γ₂ st.1).extend (2 * ↑st.2 - 1)

Tactic:
simp [hst, mul_inv_cancel₀ (two_ne_zero' ℝ)]

Result:
no goals

Proof state:
case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
⊢ Continuous fun p => (γ₂ p.1).extend (2 * ↑p.2 - 1)

Tactic:
change
  Continuous ((fun p : ι × ℝ => (γ₂ p.1).extend p.2) ∘ Prod.map id (fun x => 2 * x - 1 : I → ℝ))

Result:
case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
⊢ Continuous ((fun p => (γ₂ p.1).extend p.2) ∘ Prod.map id fun x => 2 * ↑x - 1)

Proof state:
case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
⊢ Continuous fun p => (γ₁ p.1).extend (2 * ↑p.2)

Tactic:
change
  Continuous ((fun p : ι × ℝ => (γ₁ p.1).extend p.2) ∘ Prod.map id (fun x => 2 * x : I → ℝ))

Result:
case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
⊢ Continuous ((fun p => (γ₁ p.1).extend p.2) ∘ Prod.map id fun x => 2 * ↑x)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
⊢ Continuous ↿fun t => (γ₁ t).trans (γ₂ t)

Tactic:
have h₂' := Path.continuous_uncurry_extend_of_continuous_family γ₂ h₂

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
⊢ Continuous ↿fun t => (γ₁ t).trans (γ₂ t)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
⊢ Continuous fun p =>
    { toFun := (fun t => if t ≤ 1 / 2 then (γ₁ p.1).extend (2 * t) else (γ₂ p.1).extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      p.2

Tactic:
refine Continuous.if_le ?_ ?_ (continuous_subtype_val.comp continuous_snd) continuous_const ?_

Result:
case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
⊢ Continuous fun p => (γ₁ p.1).extend (2 * ↑p.2)

case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
⊢ Continuous fun p => (γ₂ p.1).extend (2 * ↑p.2 - 1)

case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
⊢ ∀ (x : ι × ↑I), ↑x.2 = 1 / 2 → (γ₁ x.1).extend (2 * ↑x.2) = (γ₂ x.1).extend (2 * ↑x.2 - 1)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
⊢ Continuous ↿fun t => (γ₁ t).trans (γ₂ t)

Tactic:
have h₁' := Path.continuous_uncurry_extend_of_continuous_family γ₁ h₁

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
⊢ Continuous ↿fun t => (γ₁ t).trans (γ₂ t)

Proof state:
case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
⊢ ∀ (x : ι × ↑I), ↑x.2 = 1 / 2 → (γ₁ x.1).extend (2 * ↑x.2) = (γ₂ x.1).extend (2 * ↑x.2 - 1)

Tactic:
rintro st hst

Result:
case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous ↿γ₂
h₁' : Continuous ↿fun t => (γ₁ t).extend
h₂' : Continuous ↿fun t => (γ₂ t).extend
st : ι × ↑I
hst : ↑st.2 = 1 / 2
⊢ (γ₁ st.1).extend (2 * ↑st.2) = (γ₂ st.1).extend (2 * ↑st.2 - 1)