awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
rw : SProd.sprod (β := Set F) e.baseSet univ ⊓ SProd.sprod (β := Set F) e'.baseSet univ ≤ ⊥
⊢ Disjoint e.target e'.target

Tactic:
rw [e.target_eq, e'.target_eq, disjoint_iff_inf_le]

Premises used: Bundle.Trivialization.target_eq, disjoint_iff_inf_le
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x_1 : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
x : B × F
hx : x ∈ SProd.sprod (β := Set F) e.baseSet univ ⊓ SProd.sprod (β := Set F) e'.baseSet univ
⊢ Membership.mem (γ := Set (B × F)) ⊥ x

Tactic:
H.le_bot ⟨hx.1.1, hx.2.1⟩

Premises used: Disjoint.le_bot, Set.Mem, And.right, And.left, And.intro
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x_1 : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
x : B × F
hx : x ∈ SProd.sprod (β := Set F) e.baseSet univ ⊓ SProd.sprod (β := Set F) e'.baseSet univ
⊢ Membership.mem (γ := Set (B × F)) ⊥ x

Tactic:
exact H.le_bot ⟨hx.1.1, hx.2.1⟩

Premises used: Disjoint.le_bot, And.right, And.left, And.intro
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp : p ∈ e.source
inl : (e.source.piecewise (β := fun (a : Z) ↦ B × F) (↑e : Z → B × F) (↑e' : Z → B × F) p).1 = proj p
⊢ ((↑(e.disjointUnion e'.toOpenPartialHomeomorph ⋯ ⋯) : Z → B × F) p).1 = proj p

Tactic:
change (e.source.piecewise e e' p).1 = proj p

Premises used: Bundle.Trivialization.toFun', Prod.fst, PartialEquiv.source, Set.piecewise, OpenPartialHomeomorph.toPartialEquiv, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp inl inl₁ : p ∈ e.source
⊢ (e.source.piecewise (β := fun (a : Z) ↦ B × F) (↑e : Z → B × F) (↑e' : Z → B × F) p).1 = proj p

Tactic:
rw [piecewise_eq_of_mem, e.coe_fst]

Premises used: Bundle.Trivialization.coe_fst, Set.piecewise_eq_of_mem
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp : p ∈ e.source
⊢ p ∈ e.source

Tactic:
hp
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp : p ∈ e.source
⊢ p ∈ e.source

Tactic:
exact hp
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp' : p ∈ e'.source
inr : (e.source.piecewise (β := fun (a : Z) ↦ B × F) (↑e : Z → B × F) (↑e' : Z → B × F) p).1 = proj p
⊢ ((↑(e.disjointUnion e'.toOpenPartialHomeomorph ⋯ ⋯) : Z → B × F) p).1 = proj p

Tactic:
change (e.source.piecewise e e' p).1 = proj p

Premises used: Bundle.Trivialization.toFun', Prod.fst, PartialEquiv.source, Set.piecewise, OpenPartialHomeomorph.toPartialEquiv, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp' : p ∈ e'.source
inr : p ∉ e.source
⊢ (e.source.piecewise (β := fun (a : Z) ↦ B × F) (↑e : Z → B × F) (↑e' : Z → B × F) p).1 = proj p

Tactic:
rw [piecewise_eq_of_notMem, e'.coe_fst hp']

Premises used: Set.piecewise_eq_of_notMem, Bundle.Trivialization.coe_fst
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp' : p ∈ e'.source
inr : ∀ (hp' : p ∈ proj ⁻¹' e'.baseSet), p ∉ proj ⁻¹' e.baseSet
⊢ p ∉ e.source

Tactic:
simp only [source_eq] at hp' ⊢

Premises used: Bundle.Trivialization.source_eq
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp' : p ∈ proj ⁻¹' e'.baseSet
⊢ p ∉ proj ⁻¹' e.baseSet

Tactic:
fun h => H.le_bot ⟨h, hp'⟩

Premises used: Disjoint.le_bot, Set.Mem, And.intro, Not
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp' : p ∈ proj ⁻¹' e'.baseSet
⊢ p ∉ proj ⁻¹' e.baseSet

Tactic:
exact fun h => H.le_bot ⟨h, hp'⟩

Premises used: Disjoint.le_bot, And.intro
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
T : Trivialization F proj
z : Z
he : proj z ∈ T.baseSet
⊢ T.lift z (proj z) = z

Tactic:
symm_apply_mk_proj _ <| T.mem_source.2 he

Premises used: Iff.mpr, OpenPartialHomeomorph.toFun', Bundle.Trivialization.lift, Bundle.Trivialization.mem_source, Bundle.Trivialization.symm_apply_mk_proj
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
T : Trivialization F proj
z : Z
b : B
hx : b ∈ T.baseSet
⊢ proj (T.lift z b) = b

Tactic:
T.proj_symm_apply <| T.mem_target.2 hx

Premises used: Iff.mpr, OpenPartialHomeomorph.toFun', Bundle.Trivialization.lift, Bundle.Trivialization.proj_symm_apply, Bundle.Trivialization.mem_target
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
ex : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)
⊢ ((↑ex.2 : B), ((↑T : Z → B × F) (↑ex.1 : Z)).2) ∈ T.target

Tactic:
simp [mem_target]

Premises used: Bundle.Trivialization.mem_target
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
h :
  Continuous[instTopologicalSpaceProd, inst_2]
    fun (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦ T.lift (↑x.1 : Z) (↑x.2 : B)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceSubtype]
    fun (ex : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦
    Subtype.mk (p := fun (x : Z) ↦ x ∈ T.source) (T.lift (↑ex.1 : Z) (↑ex.2 : B)) ⋯

Tactic:
apply Continuous.subtype_mk

Premises used: Continuous.subtype_mk
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ ∀ (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)),
    ((↑x.2 : B), ((↑T : Z → B × F) (↑x.1 : Z)).2) ∈ T.target

Tactic:
simp [mem_target]

Premises used: Bundle.Trivialization.mem_target
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
h :
  Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd]
    fun (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦
    ((↑x.2 : B), ((↑T : Z → B × F) (↑x.1 : Z)).2)
⊢ Continuous[instTopologicalSpaceProd, inst_2]
    fun (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦ T.lift (↑x.1 : Z) (↑x.2 : B)

Tactic:
refine T.continuousOn_invFun.comp_continuous ?_ (by simp [mem_target])

Premises used: ContinuousOn.comp_continuous, OpenPartialHomeomorph.continuousOn_invFun, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ Continuous[instTopologicalSpaceProd, inst] fun (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦
    (↑x.2 : B)

Tactic:
fun_prop
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
h :
  Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd]
    fun (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦ (↑T : Z → B × F) (↑x.1 : Z)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd]
    fun (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦
    ((↑x.2 : B), ((↑T : Z → B × F) (↑x.1 : Z)).2)

Tactic:
refine .prodMk (by fun_prop) (.snd ?_)
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ Continuous[instTopologicalSpaceProd, inst_2]
    fun (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦ (↑x.1 : Z)

Tactic:
fun_prop
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ ∀ (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)), (↑x.1 : Z) ∈ T.source

Tactic:
simp
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd]
    fun (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦ (↑T : Z → B × F) (↑x.1 : Z)

Tactic:
exact T.continuousOn_toFun.comp_continuous (by fun_prop) (by simp)

Premises used: ContinuousOn.comp_continuous, OpenPartialHomeomorph.continuousOn_toFun, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
ι : Type u_5
inst_4 : TopologicalSpace ι
inst_5 : LocallyCompactPair.{u_5, u_1} ι (↑T_1.baseSet : Type u_1)
γ : ContinuousMap.{u_5, u_1} ι (↑T_1.baseSet : Type u_1)
i : ι
e : (↑T_1.source : Type u_4)
T : Trivialization F proj
inst_6 : LocallyCompactPair.{u_5, u_1} ι (↑T.baseSet : Type u_1)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd]
    fun (eγt : ((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)) × ι) ↦ (eγt.1.2, eγt.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
ι : Type u_5
inst_4 : TopologicalSpace ι
inst_5 : LocallyCompactPair.{u_5, u_1} ι (↑T_1.baseSet : Type u_1)
γ : ContinuousMap.{u_5, u_1} ι (↑T_1.baseSet : Type u_1)
i : ι
e : (↑T_1.source : Type u_4)
T : Trivialization F proj
inst_6 : LocallyCompactPair.{u_5, u_1} ι (↑T.baseSet : Type u_1)
Ψ : C(((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)) × ι,
  ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1) × ι) :=
  {
    toFun := fun (eγt : ((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)) × ι) ↦
      (eγt.1.2, eγt.2),
    continuous_toFun := ⋯ }
refine :
  Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd]
    fun (eγt : ((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)) × ι) ↦
    (eγt.1.1, (eγt.1.2 : (a : ι) → (↑T.baseSet : Type u_1)) eγt.2)
⊢ C((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1),
    ContinuousMap.{u_5, u_4} ι (↑T.source : Type u_4))

Tactic:
refine ContinuousMap.curry <| T.liftCM.comp <| ⟨fun eγt => ⟨eγt.1.1, eγt.1.2 eγt.2⟩, ?_⟩

Premises used: ContinuousMap.curry, ContinuousMap.comp, Bundle.Trivialization.liftCM
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
ι : Type u_5
inst_4 : TopologicalSpace ι
inst_5 : LocallyCompactPair.{u_5, u_1} ι (↑T_1.baseSet : Type u_1)
γ : ContinuousMap.{u_5, u_1} ι (↑T_1.baseSet : Type u_1)
i : ι
e : (↑T_1.source : Type u_4)
T : Trivialization F proj
inst_6 : LocallyCompactPair.{u_5, u_1} ι (↑T.baseSet : Type u_1)
Ψ : C(((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)) × ι,
  ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1) × ι) :=
  {
    toFun := fun (eγt : ((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)) × ι) ↦
      (eγt.1.2, eγt.2),
    continuous_toFun := ⋯ }
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceSubtype]
    fun (x : ((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)) × ι) ↦ x.1.1

Tactic:
fun_prop
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
ι : Type u_5
inst_4 : TopologicalSpace ι
inst_5 : LocallyCompactPair.{u_5, u_1} ι (↑T_1.baseSet : Type u_1)
γ : ContinuousMap.{u_5, u_1} ι (↑T_1.baseSet : Type u_1)
i : ι
e : (↑T_1.source : Type u_4)
T : Trivialization F proj
inst_6 : LocallyCompactPair.{u_5, u_1} ι (↑T.baseSet : Type u_1)
Ψ : C(((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)) × ι,
  ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1) × ι) :=
  {
    toFun := fun (eγt : ((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)) × ι) ↦
      (eγt.1.2, eγt.2),
    continuous_toFun := ⋯ }
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd]
    fun (eγt : ((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)) × ι) ↦
    (eγt.1.1, (eγt.1.2 : (a : ι) → (↑T.baseSet : Type u_1)) eγt.2)

Tactic:
simpa using ⟨by fun_prop, ContinuousEval.continuous_eval.comp Ψ.continuous⟩
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
T : Trivialization F proj
ι : Type u_5
inst_3 : TopologicalSpace ι
inst_4 : LocallyCompactPair.{u_5, u_1} ι (↑T.baseSet : Type u_1)
γ : ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)
i : ι
e : (↑T.source : Type u_4)
h : proj (↑e : Z) = (↑((γ : (a : ι) → (↑T.baseSet : Type u_1)) i) : B)
⊢ proj (↑e : Z) ∈ T.baseSet

Tactic:
simp [h]
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
T : Trivialization F proj
ι : Type u_5
inst_3 : TopologicalSpace ι
inst_4 : LocallyCompactPair.{u_5, u_1} ι (↑T.baseSet : Type u_1)
γ : ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)
i : ι
e : (↑T.source : Type u_4)
h : proj (↑e : Z) = (↑((γ : (a : ι) → (↑T.baseSet : Type u_1)) i) : B)
⊢ proj (↑e : Z) ∈ T.baseSet

Tactic:
have : proj e ∈ T.baseSet := by simp [h]
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
T : Trivialization F proj
ι : Type u_5
inst_3 : TopologicalSpace ι
inst_4 : LocallyCompactPair.{u_5, u_1} ι (↑T.baseSet : Type u_1)
γ : ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)
i : ι
e : (↑T.source : Type u_4)
h : proj (↑e : Z) = (↑((γ : (a : ι) → (↑T.baseSet : Type u_1)) i) : B)
this : proj (↑e : Z) ∈ T.baseSet
⊢ (((T.clift : (a : (↑T.source : Type u_4) × C(ι, (↑T.baseSet : Type u_1))) → C(ι, (↑T.source : Type u_4))) (e, γ) :
          ContinuousMap.{u_5, u_4} ι (↑T.source : Type u_4)) :
        (a : ι) → (↑T.source : Type u_4))
      i =
    e

Tactic:
simp [clift, liftCM, ← h, lift_self, this]

Premises used: Bundle.Trivialization.liftCM, Bundle.Trivialization.clift, Bundle.Trivialization.lift_self
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
T : Trivialization F proj
ι : Type u_5
inst_3 : TopologicalSpace ι
inst_4 : LocallyCompactPair.{u_5, u_1} ι (↑T.baseSet : Type u_1)
γ : ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)
i : ι
e : (↑T.source : Type u_4)
⊢ proj
      (↑((((T.clift : (a : (↑T.source : Type u_4) × C(ι, (↑T.baseSet : Type u_1))) → C(ι, (↑T.source : Type u_4)))
                  (e, γ) :
                ContinuousMap.{u_5, u_4} ι (↑T.source : Type u_4)) :
              (a : ι) → (↑T.source : Type u_4))
            i) :
        Z) =
    (↑((γ : (a : ι) → (↑T.baseSet : Type u_1)) i) : B)

Tactic:
simp [clift, liftCM, proj_lift]

Premises used: Bundle.Trivialization.proj_lift, Bundle.Trivialization.liftCM, Bundle.Trivialization.clift
-- Module: Mathlib.Topology.FiberPartition
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
⊢ ∀ (i : Fiber f),
    Continuous (Y := S) fun (a : (↑(↑i : Set S) : Type u_1)) ↦
      match (motive := (x : Fiber f) × (↑(↑x : Set S) : Type u_1) → S)
        Sigma.mk (β := fun (x : Fiber f) ↦ (↑(↑x : Set S) : Type u_1)) i a with
      | ⟨a, x⟩ => (↑x : S)

Tactic:
fun_prop