awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsHomeomorph f ↔ IsQuotientMap f ∧ Injective f

Tactic:
⟨fun h ↦ ⟨h.isQuotientMap, h.injective⟩,
    fun h ↦ ⟨h.1.continuous, fun s hs ↦ ?_, h.2, h.1.surjective⟩⟩

Premises used: IsHomeomorph.isQuotientMap, IsHomeomorph.injective, Topology.IsQuotientMap.surjective, IsHomeomorph.mk, And.right, And.left, Topology.IsQuotientMap.continuous, And.intro, Iff.intro
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
refine : ∀ (h : IsQuotientMap f ∧ Injective f) (s : Set X) (hs : IsOpen[inst] s), IsOpen[inst_1] (f '' s)
⊢ IsHomeomorph f ↔ IsQuotientMap f ∧ Injective f

Tactic:
refine ⟨fun h ↦ ⟨h.isQuotientMap, h.injective⟩,
    fun h ↦ ⟨h.1.continuous, fun s hs ↦ ?_, h.2, h.1.surjective⟩⟩
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsQuotientMap f ∧ Injective f
s : Set X
hs : IsOpen[inst] s
rwa : IsOpen[inst] (f ⁻¹' f '' s)
rwa₁ rwa₂ rwa₃ rwa₄ : IsOpen[inst] s
⊢ IsOpen[inst_1] (f '' s)

Tactic:
rwa [← h.1.isOpen_preimage, Set.preimage_image_eq _ h.2]

Premises used: Topology.IsCoinducing.isOpen_preimage, And.right, And.left, Topology.IsQuotientMap.isCoinducing, Set.preimage_image_eq
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsHomeomorph f ↔ Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ Bijective f

Tactic:
⟨fun hf => ⟨hf.continuous, hf.isClosedMap, hf.bijective⟩, fun ⟨hf, hf', hf''⟩ =>
    ⟨hf, fun _ hu => isClosed_compl_iff.1 (image_compl_eq hf'' ▸ hf' _ hu.isClosed_compl), hf''⟩⟩

Premises used: Compl.compl, IsHomeomorph.mk, Set.image_compl_eq, Eq.rec, IsOpen.isClosed_compl, IsHomeomorph.continuous, And.intro, IsHomeomorph.bijective, Iff.intro, Iff.mp, IsHomeomorph.isClosedMap, _private.0.isHomeomorph_iff_continuous_isClosedMap_bijective.match_1, IsHomeomorph, isClosed_compl_iff
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
rw : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ Bijective f ↔ Continuous[inst, inst_1] f ∧ Bijective f
⊢ IsHomeomorph f ↔ Continuous[inst, inst_1] f ∧ Bijective f

Tactic:
rw [isHomeomorph_iff_continuous_isClosedMap_bijective]

Premises used: isHomeomorph_iff_continuous_isClosedMap_bijective
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
⊢ Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ Bijective f ↔ Continuous[inst, inst_1] f ∧ Bijective f

Tactic:
and_congr_right fun hf ↦ ?_

Premises used: and_congr_right
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
refine : ∀ (hf : Continuous[inst, inst_1] f), IsClosedMap f ∧ Bijective f ↔ Bijective f
⊢ Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ Bijective f ↔ Continuous[inst, inst_1] f ∧ Bijective f

Tactic:
refine and_congr_right fun hf ↦ ?_

Premises used: and_congr_right
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
hf : Continuous[inst, inst_1] f
rw : True ∧ Bijective f ↔ Bijective f
rw₁ rw₂ : Bijective f ↔ Bijective f
⊢ IsClosedMap f ∧ Bijective f ↔ Bijective f

Tactic:
rw [eq_true hf.isClosedMap, true_and]

Premises used: Continuous.isClosedMap, eq_true, true_and
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
W : Type u_5
inst_3 : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsHomeomorph f
hg : IsHomeomorph g
⊢ IsHomeomorph (Sum.map f g)

Tactic:
⟨hf.1.sumMap hg.1, hf.2.sumMap hg.2, hf.3.sumMap hg.3⟩

Premises used: Continuous.sumMap, IsHomeomorph.mk, IsHomeomorph.isOpenMap, IsHomeomorph.continuous, IsHomeomorph.bijective, Function.Bijective.sumMap, IsOpenMap.sumMap
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
W : Type u_5
inst_3 : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsHomeomorph f
hg : IsHomeomorph g
⊢ IsHomeomorph (Prod.map f g)

Tactic:
⟨hf.1.prodMap hg.1, hf.2.prodMap hg.2, hf.3.prodMap hg.3⟩

Premises used: IsOpenMap.prodMap, Continuous.prodMap, IsHomeomorph.mk, IsHomeomorph.isOpenMap, IsHomeomorph.continuous, IsHomeomorph.bijective, Function.Bijective.prodMap
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
ι : Type u_6
κ : Type u_7
X : ι → Type u_8
Y : κ → Type u_9
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : κ) → TopologicalSpace (Y i)
f : ι → κ
hf : Bijective f
g : (i : ι) → X i → Y (f i)
hg : ∀ (i : ι), IsHomeomorph (g i)
simp_rw :
  ∀ (hg : ∀ (i : ι), IsEmbedding (g i) ∧ Surjective (g i)),
    IsEmbedding (Sigma.map (β₁ := X) (β₂ := Y) f g) ∧ Surjective (Sigma.map (β₁ := X) (β₂ := Y) f g)
⊢ IsHomeomorph (Sigma.map (β₁ := X) (β₂ := Y) f g)

Tactic:
simp_rw [isHomeomorph_iff_isEmbedding_surjective] at hg ⊢

Premises used: isHomeomorph_iff_isEmbedding_surjective
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
ι : Type u_6
κ : Type u_7
X : ι → Type u_8
Y : κ → Type u_9
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : κ) → TopologicalSpace (Y i)
f : ι → κ
hf : Bijective f
g : (i : ι) → X i → Y (f i)
hg : ∀ (i : ι), IsEmbedding (g i) ∧ Surjective (g i)
⊢ IsEmbedding (Sigma.map (β₁ := X) (β₂ := Y) f g) ∧ Surjective (Sigma.map (β₁ := X) (β₂ := Y) f g)

Tactic:
⟨(isEmbedding_sigmaMap hf.1).2 fun i ↦ (hg i).1, hf.2.sigma_map fun i ↦ (hg i).2⟩

Premises used: Iff.mpr, Topology.isEmbedding_sigmaMap, And.right, And.left, And.intro, Function.Surjective.sigma_map
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
ι : Type u_6
κ : Type u_7
X : ι → Type u_8
Y : κ → Type u_9
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : κ) → TopologicalSpace (Y i)
f : ι → κ
hf : Bijective f
g : (i : ι) → X i → Y (f i)
hg : ∀ (i : ι), IsEmbedding (g i) ∧ Surjective (g i)
⊢ IsEmbedding (Sigma.map (β₁ := X) (β₂ := Y) f g) ∧ Surjective (Sigma.map (β₁ := X) (β₂ := Y) f g)

Tactic:
exact ⟨(isEmbedding_sigmaMap hf.1).2 fun i ↦ (hg i).1, hf.2.sigma_map fun i ↦ (hg i).2⟩
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
ι : Type u_6
X : ι → Type u_7
Y : ι → Type u_8
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h : ∀ (i : ι), IsHomeomorph (f i)
⊢ IsHomeomorph (Y := (i : ι) → Y i) fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)

Tactic:
(Homeomorph.piCongrRight fun i ↦ (h i).homeomorph (f i)).isHomeomorph

Premises used: IsHomeomorph.homeomorph, Homeomorph.piCongrRight, Pi.map, Homeomorph.isHomeomorph
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : DiscreteTopology X
inst_3 : DiscreteTopology Y
f : X ≃ Y
⊢ IsHomeomorph.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)

Tactic:
(Homeomorph.ofDiscrete f).isHomeomorph

Premises used: Homeomorph.ofDiscrete, Homeomorph.isHomeomorph
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
W_1 : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
W : Type u_5
inst_3 : TopologicalSpace W
f_1 f : X → Y
hf : IsCoinducing f
hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})
⊢ Bijective ⋯.connectedComponentsMap

Tactic:
have hbij := hf.connectedComponentsMap_bijective hf'
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
W_1 : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
W : Type u_5
inst_3 : TopologicalSpace W
f_1 f : X → Y
hf : IsCoinducing f
hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})
hbij : Bijective ⋯.connectedComponentsMap
⊢ IsHomeomorph ⋯.connectedComponentsMap

Tactic:
⟨hf.continuous.connectedComponentsMap_continuous,
      hf.connectedComponentsMap.isOpenMap_of_injective hbij.injective, hbij⟩

Premises used: IsHomeomorph.mk, Function.Bijective.injective, Topology.IsCoinducing.continuous, Continuous.connectedComponentsMap_continuous, Topology.IsCoinducing.isOpenMap_of_injective, Topology.IsCoinducing.connectedComponentsMap
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
W_1 : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
W : Type u_5
inst_3 : TopologicalSpace W
f_1 f : X → Y
hf : IsCoinducing f
hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})
hbij : Bijective ⋯.connectedComponentsMap
⊢ IsHomeomorph ⋯.connectedComponentsMap

Tactic:
exact ⟨hf.continuous.connectedComponentsMap_continuous,
      hf.connectedComponentsMap.isOpenMap_of_injective hbij.injective, hbij⟩
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})
x : X
⊢ Eq.{u_2 + 1} (α := ConnectedComponents Y)
    ((hf.connectedComponentsHomeomorph hf' : (a : ConnectedComponents X) → ConnectedComponents Y)
        (ConnectedComponents.mk x) :
      ConnectedComponents Y)
    (ConnectedComponents.mk (f x) : ConnectedComponents Y)

Tactic:
rfl

Premises used: Quotient.liftOn', ConnectedComponents.mk, Continuous.connectedComponentsLift, Continuous.connectedComponentsMap, rfl
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})
x : X
⊢ Eq.{u_2 + 1} (α := ConnectedComponents Y)
    ((hf.connectedComponentsHomeomorph hf' : (a : ConnectedComponents X) → ConnectedComponents Y)
        (((hf.connectedComponentsHomeomorph hf').symm : (a : ConnectedComponents Y) → ConnectedComponents X)
          (ConnectedComponents.mk (f x))) :
      ConnectedComponents Y)
    ((hf.connectedComponentsHomeomorph hf' : (a : ConnectedComponents X) → ConnectedComponents Y)
        (ConnectedComponents.mk x) :
      ConnectedComponents Y)

Tactic:
simp
-- Module: Mathlib.Topology.Homeomorph.Quotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
rX : X → X → Prop
rY : Y → Y → Prop
e : X ≃ₜ Y
eq : ∀ (x₁ x₂ : X), rX x₁ x₂ ↔ rY ((e : (a : X) → Y) x₁) ((e : (a : X) → Y) x₂)
x y : X
⊢ rX x y → rY (((↑e : X ≃ Y) : (a : X) → Y) x) (((↑e : X ≃ Y) : (a : X) → Y) y)

Tactic:
simp [eq]
-- Module: Mathlib.Topology.Homeomorph.Quotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
rX : X → X → Prop
rY : Y → Y → Prop
e : X ≃ₜ Y
eq : ∀ (x₁ x₂ : X), rX x₁ x₂ ↔ rY ((e : (a : X) → Y) x₁) ((e : (a : X) → Y) x₂)
x y : Y
⊢ rY x y → rX (((↑e : X ≃ Y).symm : (a : Y) → X) x) (((↑e : X ≃ Y).symm : (a : Y) → X) y)

Tactic:
simp [eq]
-- Module: Mathlib.Topology.Homeomorph.Quotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
r : X → X → Prop
e : X ≃ₜ Y
x x_1 : X
⊢ r x x_1 ↔ r ((e.symm : (a : Y) → X) ((e : (a : X) → Y) x : Y)) ((e.symm : (a : Y) → X) ((e : (a : X) → Y) x_1 : Y))

Tactic:
simp only [e.symm_apply_apply]

Premises used: Homeomorph.symm_apply_apply
-- Module: Mathlib.Topology.Homeomorph.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
simp : Continuous.{u_3, u_2} (X := β) (Y := α) (⇑e.symm : (a : β) → α)
⊢ Continuous e.invFun

Tactic:
simp only [Equiv.invFun_as_coe]

Premises used: Equiv.invFun_as_coe
-- Module: Mathlib.Topology.Homeomorph.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
⊢ Continuous.{u_3, u_2} (X := β) (Y := α) (⇑e.symm : (a : β) → α)

Tactic:
continuous_coinduced_rng

Premises used: continuous_coinduced_rng
-- Module: Mathlib.Topology.Homeomorph.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
h : e.topologicalSpace = TopologicalSpace.coinduced (⇑e.symm : (a : β) → α) inst
⊢ Continuous.{u_3, u_2} (X := β) (Y := α) (⇑e.symm : (a : β) → α)

Tactic:
convert! continuous_coinduced_rng

Premises used: continuous_coinduced_rng
-- Module: Mathlib.Topology.Homeomorph.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
h h₁ : e.topologicalSpace = TopologicalSpace.induced (⇑e : (a : α) → β) inst
⊢ e.topologicalSpace = TopologicalSpace.coinduced (⇑e.symm : (a : β) → α) inst

Tactic:
rw [e.coinduced_symm]

Premises used: Equiv.coinduced_symm
-- Module: Mathlib.Topology.Homotopy.Affine
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
f g : C(X, E)
dsimp :
  Continuous.{u_1, u_2} (Y := E) fun (x : (↑unitInterval : Type) × X) ↦
    HAdd.hAdd (β := E)
      ((↑x.1 : ℝ) • HSub.hSub (α := E) (β := E) ((g : (a : X) → E) x.2 : E) ((f : (a : X) → E) x.2 : E))
      ((f : (a : X) → E) x.2 : E)
⊢ Continuous.{u_1, u_2} (Y := E) fun (x : (↑unitInterval : Type) × X) ↦
    ((Path.segment ((f : (a : X) → E) x.2) ((g : (a : X) → E) x.2) :
          Path (X := E) ((f : (a : X) → E) x.2 : E) ((g : (a : X) → E) x.2 : E)) :
        (a : (↑unitInterval : Type)) → E)
      x.1

Tactic:
dsimp [AffineMap.lineMap_apply]

Premises used: AffineMap.lineMap_apply
-- Module: Mathlib.Topology.Homotopy.Affine
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
f g : C(X, E)
⊢ Continuous.{u_1, u_2} (Y := E) fun (x : (↑unitInterval : Type) × X) ↦
    HAdd.hAdd (β := E)
      ((↑x.1 : ℝ) • HSub.hSub (α := E) (β := E) ((g : (a : X) → E) x.2 : E) ((f : (a : X) → E) x.2 : E))
      ((f : (a : X) → E) x.2 : E)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homotopy.Affine
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
f g : C(X, E)
⊢ ∀ (x : X),
    Eq.{u_2 + 1} (α := E)
      (((Path.segment ((f : (a : X) → E) (0, x).2) ((g : (a : X) → E) (0, x).2) :
              Path (X := E) ((f : (a : X) → E) (0, x).2 : E) ((g : (a : X) → E) (0, x).2 : E)) :
            (a : (↑unitInterval : Type)) → E)
          (0, x).1 :
        E)
      ((f : (a : X) → E) x : E)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Affine
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
f g : C(X, E)
⊢ ∀ (x : X),
    Eq.{u_2 + 1} (α := E)
      (((Path.segment ((f : (a : X) → E) (1, x).2) ((g : (a : X) → E) (1, x).2) :
              Path (X := E) ((f : (a : X) → E) (1, x).2 : E) ((g : (a : X) → E) (1, x).2 : E)) :
            (a : (↑unitInterval : Type)) → E)
          (1, x).1 :
        E)
      ((g : (a : X) → E) x : E)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Affine
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
f g : C(X, E)
x : X
⊢ (affine f g).evalAt x = Path.segment ((f : (a : X) → E) x) ((g : (a : X) → E) x)

Tactic:
rfl

Premises used: ContinuousMap.Homotopy.evalAt, Path.segment, rfl
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
f g : f₀.Homotopy f₁
h :
  Eq (α := (a : (↑I : Type) × X) → Y) ((fun (f : f₀.Homotopy f₁) ↦ f.toFun) f) ((fun (f : f₀.Homotopy f₁) ↦ f.toFun) g)
obtain :
  ∀ (toFun : (↑I : Type) × X → Y) (continuous_toFun : Continuous toFun)
    (map_zero_left :
      ∀ (x : X),
        { toFun := toFun, continuous_toFun := continuous_toFun : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun
            (0, x) =
          (f₀ : (a : X) → Y) x)
    (map_one_left :
      ∀ (x : X),
        { toFun := toFun, continuous_toFun := continuous_toFun : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun
            (1, x) =
          (f₁ : (a : X) → Y) x)
    (h :
      Eq (α := (a : (↑I : Type) × X) → Y)
        ((fun (f : f₀.Homotopy f₁) ↦ f.toFun)
          { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left,
            map_one_left := map_one_left })
        ((fun (f : f₀.Homotopy f₁) ↦ f.toFun) g)),
    { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left,
        map_one_left := map_one_left : f₀.Homotopy f₁ } =
      g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
g : f₀.Homotopy f₁
toFun : (↑I : Type) × X → Y
continuous_toFun : Continuous toFun
map_zero_left :
  ∀ (x : X),
    { toFun := toFun, continuous_toFun := continuous_toFun : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun (0, x) =
      (f₀ : (a : X) → Y) x
map_one_left :
  ∀ (x : X),
    { toFun := toFun, continuous_toFun := continuous_toFun : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun (1, x) =
      (f₁ : (a : X) → Y) x
h :
  Eq (α := (a : (↑I : Type) × X) → Y)
    ((fun (f : f₀.Homotopy f₁) ↦ f.toFun)
      { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left,
        map_one_left := map_one_left })
    ((fun (f : f₀.Homotopy f₁) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : (↑I : Type) × X → Y) (continuous_toFun_1 : Continuous toFun_1)
    (map_zero_left_1 :
      ∀ (x : X),
        { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun
            (0, x) =
          (f₀ : (a : X) → Y) x)
    (map_one_left_1 :
      ∀ (x : X),
        { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun
            (1, x) =
          (f₁ : (a : X) → Y) x)
    (h :
      Eq (α := (a : (↑I : Type) × X) → Y)
        ((fun (f : f₀.Homotopy f₁) ↦ f.toFun)
          { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left,
            map_one_left := map_one_left })
        ((fun (f : f₀.Homotopy f₁) ↦ f.toFun)
          { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_zero_left := map_zero_left_1,
            map_one_left := map_one_left_1 })),
    { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left,
        map_one_left := map_one_left : f₀.Homotopy f₁ } =
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_zero_left := map_zero_left_1,
        map_one_left := map_one_left_1 }
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left, map_one_left := map_one_left :
      f₀.Homotopy f₁ } =
    g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
toFun : (↑I : Type) × X → Y
continuous_toFun : Continuous toFun
map_zero_left :
  ∀ (x : X),
    { toFun := toFun, continuous_toFun := continuous_toFun : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun (0, x) =
      (f₀ : (a : X) → Y) x
map_one_left :
  ∀ (x : X),
    { toFun := toFun, continuous_toFun := continuous_toFun : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun (1, x) =
      (f₁ : (a : X) → Y) x
toFun_1 : (↑I : Type) × X → Y
continuous_toFun_1 : Continuous toFun_1
map_zero_left_1 :
  ∀ (x : X),
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun
        (0, x) =
      (f₀ : (a : X) → Y) x
map_one_left_1 :
  ∀ (x : X),
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun
        (1, x) =
      (f₁ : (a : X) → Y) x
h :
  Eq (α := (a : (↑I : Type) × X) → Y)
    ((fun (f : f₀.Homotopy f₁) ↦ f.toFun)
      { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left,
        map_one_left := map_one_left })
    ((fun (f : f₀.Homotopy f₁) ↦ f.toFun)
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_zero_left := map_zero_left_1,
        map_one_left := map_one_left_1 })
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left, map_one_left := map_one_left :
      f₀.Homotopy f₁ } =
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_zero_left := map_zero_left_1,
      map_one_left := map_one_left_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F G : f₀.Homotopy f₁
h :
  ∀ (x : (↑I : Type) × X),
    Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) x : Y) ((G : (a : (↑I : Type) × X) → Y) x : Y)
⊢ F = G

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ Continuous.{u, v} (X := (↑I : Type) × X) (Y := Y) (⇑F : (a : (↑I : Type) × X) → Y)

Tactic:
F.continuous_toFun

Premises used: ContinuousMap.Homotopy.toContinuousMap, ContinuousMap.continuous_toFun
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
x : X
⊢ Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (0, x) : Y) ((f₀ : (a : X) → Y) x : Y)

Tactic:
F.map_zero_left x

Premises used: ContinuousMap.Homotopy.map_zero_left
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
x : X
⊢ Eq.{v + 1} (α := Y) ((F : (a : (↑I : Type) × X) → Y) (1, x) : Y) ((f₁ : (a : X) → Y) x : Y)

Tactic:
F.map_one_left x

Premises used: ContinuousMap.Homotopy.map_one_left
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ Eq (α := (a : (↑I : Type) × X) → Y) (⇑F.toContinuousMap : (a : (↑I : Type) × X) → Y) (⇑F : (a : (↑I : Type) × X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : (↑I : Type)
x : X
⊢ Eq.{v + 1} (α := Y) ((((F.curry : (a : (↑I : Type)) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y)
    ((F : (a : (↑I : Type) × X) → Y) (t, x) : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
h :
  ∀ (a : X),
    Eq.{v + 1} (α := Y) ((((F.curry : (a : (↑I : Type)) → C(X, Y)) 0 : C(X, Y)) : (a : X) → Y) a : Y)
      ((f₀ : (a : X) → Y) a : Y)
⊢ (F.curry : (a : (↑I : Type)) → C(X, Y)) 0 = f₀

Tactic:
ext
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
a : X
⊢ Eq.{v + 1} (α := Y) ((((F.curry : (a : (↑I : Type)) → C(X, Y)) 0 : C(X, Y)) : (a : X) → Y) a : Y)
    ((f₀ : (a : X) → Y) a : Y)

Tactic:
simp