awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
e : Pretrivialization F proj
x : Z
ex : proj x ∈ e.baseSet
⊢ ((↑e : Z → B × F) x).1 = proj x

Tactic:
e.coe_fst (e.mem_source.2 ex)

Premises used: Iff.mpr, Bundle.Pretrivialization.mem_source, Bundle.Pretrivialization.coe_fst
-- 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
e : Pretrivialization F proj
⊢ EqOn (Prod.fst ∘ (↑e : Z → B × F)) proj e.source

Tactic:
fun _ hx => e.coe_fst hx

Premises used: Set.EqOn, Bundle.Pretrivialization.coe_fst
-- 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
e : Pretrivialization F proj
x : Z
ex : x ∈ e.source
⊢ (proj x, ((↑e : Z → B × F) x).2) = (↑e : Z → B × F) x

Tactic:
Prod.ext (e.coe_fst ex).symm rfl

Premises used: Prod.ext, Eq.symm, rfl, Bundle.Pretrivialization.coe_fst
-- 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
e : Pretrivialization F proj
x : Z
ex : proj x ∈ e.baseSet
⊢ (proj x, ((↑e : Z → B × F) x).2) = (↑e : Z → B × F) x

Tactic:
Prod.ext (e.coe_fst' ex).symm rfl

Premises used: Prod.ext, Bundle.Pretrivialization.coe_fst', Eq.symm, rfl
-- 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
e : Pretrivialization F proj
x : B × F
rw : x ∈ SProd.sprod (β := Set F) e.baseSet univ ↔ x.1 ∈ e.baseSet
rw₁ : Membership.mem (γ := Set (B × F)) (Prod.fst ⁻¹' e.baseSet) x ↔ x.1 ∈ e.baseSet
rw₂ rw₃ : x.1 ∈ e.baseSet ↔ x.1 ∈ e.baseSet
⊢ x ∈ e.target ↔ x.1 ∈ e.baseSet

Tactic:
rw [e.target_eq, prod_univ, mem_preimage]

Premises used: Set.prod_univ, Bundle.Pretrivialization.target_eq, Set.mem_preimage
-- 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
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
⊢ proj ((↑e.symm : B × F → Z) x) = ((↑e : Z → B × F) ((↑e.symm : B × F → Z) x)).1

Tactic:
have := (e.coe_fst (e.map_target hx)).symm
-- 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
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
this : proj ((↑e.symm : B × F → Z) x) = ((↑e : Z → B × F) ((↑e.symm : B × F → Z) x)).1
rwa :
  ∀ (this : proj ((↑e.symm : B × F → Z) x) = ((↑e.toPartialEquiv : Z → B × F) ((↑e.symm : B × F → Z) x)).1),
    proj ((↑e.symm : B × F → Z) x) = x.1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : proj ((↑e.symm : B × F → Z) x) = x.1), proj ((↑e.symm : B × F → Z) x) = x.1
⊢ proj ((↑e.symm : B × F → Z) x) = x.1

Tactic:
rwa [← e.coe_coe, e.right_inv hx] at this

Premises used: Bundle.Pretrivialization.coe_coe, PartialEquiv.right_inv, Bundle.Pretrivialization.toPartialEquiv
-- 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
e : Pretrivialization F proj
b : B
x : F
hx : b ∈ e.baseSet
⊢ proj ((↑e.symm : B × F → Z) (b, x)) = b

Tactic:
e.proj_symm_apply (e.mem_target.2 hx)

Premises used: Iff.mpr, Bundle.Pretrivialization.mem_target, Bundle.Pretrivialization.proj_symm_apply
-- 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
e : Pretrivialization F proj
inst_2 : Nonempty F
⊢ SurjOn proj e.source e.baseSet

Tactic:
fun b hb =>
  let ⟨y⟩ := ‹Nonempty F›
  ⟨e.toPartialEquiv.symm (b, y), e.toPartialEquiv.map_target <| e.mem_target.2 hb,
    e.proj_symm_apply' hb⟩

Premises used: Iff.mpr, PartialEquiv.map_target, Bundle.Pretrivialization.mem_target, Set.SurjOn, Membership.mem, PartialEquiv.symm, Prod.mk, Set.Subset, Bundle.Pretrivialization.toPartialEquiv, And.intro, Exists.intro, PartialEquiv.source, Set.image, PartialEquiv.toFun, Bundle.Pretrivialization.proj_symm_apply', _private.0.Bundle.Pretrivialization.proj_surjOn_baseSet.match_1
-- 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
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
⊢ (↑e : Z → B × F) ((↑e.symm : B × F → Z) x) = x

Tactic:
e.toPartialEquiv.right_inv hx

Premises used: PartialEquiv.right_inv, Bundle.Pretrivialization.toFun', Bundle.Pretrivialization.toPartialEquiv
-- 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
e : Pretrivialization F proj
b : B
x : F
hx : b ∈ e.baseSet
⊢ (↑e : Z → B × F) ((↑e.symm : B × F → Z) (b, x)) = (b, x)

Tactic:
e.apply_symm_apply (e.mem_target.2 hx)

Premises used: Iff.mpr, Bundle.Pretrivialization.mem_target, Bundle.Pretrivialization.apply_symm_apply
-- 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
e : Pretrivialization F proj
x : Z
hx : x ∈ e.source
⊢ (↑e.symm : B × F → Z) ((↑e : Z → B × F) x) = x

Tactic:
e.toPartialEquiv.left_inv hx

Premises used: Bundle.Pretrivialization.toFun', Bundle.Pretrivialization.toPartialEquiv, PartialEquiv.left_inv
-- 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
e : Pretrivialization F proj
x : Z
ex : x ∈ e.source
rw : (↑e.symm : B × F → Z) (((↑e : Z → B × F) x).1, ((↑e : Z → B × F) x).2) = x
rw₁ : (↑e.symm : B × F → Z) (((↑e.toPartialEquiv : Z → B × F) x).1, ((↑e.toPartialEquiv : Z → B × F) x).2) = x
rw₂ rw₃ : x = x
⊢ (↑e.symm : B × F → Z) (proj x, ((↑e : Z → B × F) x).2) = x

Tactic:
rw [← e.coe_fst ex, ← e.coe_coe, e.left_inv ex]

Premises used: Bundle.Pretrivialization.coe_coe, Bundle.Pretrivialization.toPartialEquiv, PartialEquiv.left_inv, Bundle.Pretrivialization.coe_fst
-- 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
e : Pretrivialization F proj
⊢ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e.baseSet ∩ e.target = e.target

Tactic:
inter_eq_right.mpr fun x hx => ?_

Premises used: Iff.mpr, Set.inter_eq_right
-- 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
e : Pretrivialization F proj
refine : ∀ (x : B × F) (hx : x ∈ e.target), x ∈ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e.baseSet
⊢ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e.baseSet ∩ e.target = e.target

Tactic:
refine inter_eq_right.mpr fun x hx => ?_

Premises used: Iff.mpr, Set.inter_eq_right
-- 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
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
simp : x.1 ∈ e.baseSet
⊢ x ∈ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e.baseSet

Tactic:
simp only [mem_preimage, e.proj_symm_apply hx]

Premises used: Bundle.Pretrivialization.proj_symm_apply, Set.mem_preimage
-- 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
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
⊢ x.1 ∈ e.baseSet

Tactic:
e.mem_target.mp hx

Premises used: Bundle.Pretrivialization.mem_target, Iff.mp
-- 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
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
⊢ x.1 ∈ e.baseSet

Tactic:
exact e.mem_target.mp hx

Premises used: Bundle.Pretrivialization.mem_target, Iff.mp
-- 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
e : Pretrivialization F proj
s : Set B
h :
  ∀ (x : B) (y : F),
    (x, y) ∈ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' s ∩ SProd.sprod (β := Set F) e.baseSet univ ↔
      (x, y) ∈ SProd.sprod (β := Set F) (s ∩ e.baseSet) univ
⊢ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' s ∩ SProd.sprod (β := Set F) e.baseSet univ =
    SProd.sprod (β := Set F) (s ∩ e.baseSet) univ

Tactic:
ext ⟨x, y⟩
-- 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
e : Pretrivialization F proj
s : Set B
x : B
y : F
this : x ∈ e.baseSet → (proj ((↑e.symm : B × F → Z) (x, y)) ∈ s ↔ x ∈ s)
⊢ (x, y) ∈ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' s ∩ SProd.sprod (β := Set F) e.baseSet univ ↔
    (x, y) ∈ SProd.sprod (β := Set F) (s ∩ e.baseSet) univ

Tactic:
simpa only [prodMk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ, and_congr_left_iff]

Premises used: and_true, Set.mem_inter_iff, Set.prodMk_mem_set_prod_eq, and_congr_left_iff, Set.mem_univ
-- 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
e : Pretrivialization F proj
s : Set B
x : B
y : F
h : x ∈ e.baseSet → (proj ((↑e.symm : B × F → Z) (x, y)) ∈ s ↔ x ∈ s)
⊢ (x, y) ∈ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' s ∩ SProd.sprod (β := Set F) e.baseSet univ ↔
    (x, y) ∈ SProd.sprod (β := Set F) (s ∩ e.baseSet) univ

Tactic:
suffices x ∈ e.baseSet → (proj (e.toPartialEquiv.symm (x, y)) ∈ s ↔ x ∈ s) by
    simpa only [prodMk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ, and_congr_left_iff]
-- 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
e : Pretrivialization F proj
s : Set B
x : B
y : F
h : x ∈ e.baseSet
h₁ h₂ : x ∈ s ↔ x ∈ s
⊢ proj ((↑e.symm : B × F → Z) (x, y)) ∈ s ↔ x ∈ s

Tactic:
rw [e.proj_symm_apply' h]

Premises used: Bundle.Pretrivialization.proj_symm_apply'
-- 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
e f : Pretrivialization F proj
rw : (↑f.symm : B × F → Z) ⁻¹' e.source ∩ f.target = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
rw₁ :
  (↑f.symm : B × F → Z) ⁻¹' e.source ∩ SProd.sprod (β := Set F) f.baseSet univ =
    SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
rw₂ :
  (↑f.symm : B × F → Z) ⁻¹' proj ⁻¹' e.baseSet ∩ SProd.sprod (β := Set F) f.baseSet univ =
    SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
rw₃ rw₄ : SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
⊢ f.target ∩ (↑f.symm : B × F → Z) ⁻¹' e.source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ

Tactic:
rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter]

Premises used: Bundle.Pretrivialization.preimage_symm_proj_inter, Bundle.Pretrivialization.target_eq, Bundle.Pretrivialization.source_eq, Set.inter_comm
-- 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
e f : Pretrivialization F proj
rw : f.symm.source ∩ (↑f.symm : B × F → Z) ⁻¹' e.source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
rw₁ : f.target ∩ (↑f.symm : B × F → Z) ⁻¹' e.source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
rw₂ rw₃ : SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
⊢ (f.symm.trans e.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ

Tactic:
rw [PartialEquiv.trans_source, PartialEquiv.symm_source, e.target_inter_preimage_symm_source_eq]

Premises used: PartialEquiv.trans_source, PartialEquiv.symm_source, Bundle.Pretrivialization.target_inter_preimage_symm_source_eq
-- 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
e e' : Pretrivialization F proj
rw : e'.symm.trans e.symm.symm = e'.symm.trans e.toPartialEquiv
rw₁ rw₂ : e'.symm.trans e.toPartialEquiv = e'.symm.trans e.toPartialEquiv
⊢ (e.symm.trans e'.toPartialEquiv).symm = e'.symm.trans e.toPartialEquiv

Tactic:
rw [PartialEquiv.trans_symm_eq_symm_trans_symm, PartialEquiv.symm_symm]

Premises used: PartialEquiv.symm_symm, PartialEquiv.trans_symm_eq_symm_trans_symm
-- 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
e e' : Pretrivialization F proj
rw : e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' e'.source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₁ :
  e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₂ : e.target ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₃ :
  SProd.sprod (β := Set F) e.baseSet univ ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet =
    SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₄ :
  (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet ∩ SProd.sprod (β := Set F) e.baseSet univ =
    SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₅ : SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₆ rw₇ :
  SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
⊢ (e.symm.trans e'.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ

Tactic:
rw [PartialEquiv.trans_source, e'.source_eq, PartialEquiv.symm_source, e.target_eq, inter_comm,
    e.preimage_symm_proj_inter, inter_comm]

Premises used: Bundle.Pretrivialization.preimage_symm_proj_inter, PartialEquiv.trans_source, Bundle.Pretrivialization.target_eq, Bundle.Pretrivialization.source_eq, PartialEquiv.symm_source, Set.inter_comm
-- 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
e e' : Pretrivialization F proj
rw : (e.symm.trans e'.toPartialEquiv).symm.source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₁ : (e'.symm.trans e.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₂ : SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₃ rw₄ :
  SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
⊢ (e.symm.trans e'.toPartialEquiv).target = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ

Tactic:
rw [← PartialEquiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm]

Premises used: Bundle.Pretrivialization.symm_trans_source_eq, PartialEquiv.symm_source, Set.inter_comm, Bundle.Pretrivialization.symm_trans_symm
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
⊢ TotalSpace.mk (E := E) b y ∈ e'.source ↔ b ∈ e'.baseSet

Tactic:
e'.mem_source

Premises used: Bundle.Pretrivialization.mem_source, Set.Mem
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
hb : b ∈ e'.baseSet
⊢ ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).1 = b

Tactic:
simp [hb]
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : B
y : F
⊢ (x, y) ∈ e'.target ↔ x ∈ e'.baseSet

Tactic:
e'.mem_target

Premises used: Bundle.Pretrivialization.mem_target, Set.Mem
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
x : B
y : F
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
h : x ∈ e'.baseSet
⊢ ((↑e'.symm : B × F → TotalSpace F E) (x, y)).proj (E := E) = x

Tactic:
e'.proj_symm_apply' h

Premises used: Bundle.Pretrivialization.proj_symm_apply'
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → Zero (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
hb : b ∈ e.baseSet
y : F
⊢ e.symm (E := E) b y = cast ⋯ (((↑e.symm : B × F → TotalSpace F E) (b, y)).snd (E := E))

Tactic:
dif_pos hb

Premises used: dif_pos, Bundle.Pretrivialization.symm
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → Zero (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
hb : b ∉ e.baseSet
y : F
⊢ e.symm (E := E) b y = 0

Tactic:
dif_neg hb

Premises used: dif_neg, Bundle.Pretrivialization.symm
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → Zero (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
hb : b ∉ e.baseSet
⊢ e.symm (E := E) b = 0

Tactic:
funext fun _ => dif_neg hb

Premises used: dif_neg, funext
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → Zero (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
hb : b ∈ e.baseSet
y : F
⊢ TotalSpace.mk (E := E) b (e.symm (E := E) b y) = (↑e.symm : B × F → TotalSpace F E) (b, y)

Tactic:
simp only [e.symm_apply hb, TotalSpace.mk_cast (e.proj_symm_apply' hb), TotalSpace.eta]

Premises used: Bundle.TotalSpace.mk_cast, Bundle.TotalSpace.eta, Bundle.Pretrivialization.symm_apply, Bundle.Pretrivialization.proj_symm_apply'
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → Zero (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
z : TotalSpace F E
hz : z.proj (E := E) ∈ e.baseSet
rw :
  cast ⋯ (((↑e.symm : B × F → TotalSpace F E) (z.proj (E := E), ((↑e : TotalSpace F E → B × F) z).2)).snd (E := E)) =
    z.snd (E := E)
rw₁ :
  ((↑e.symm : B × F → TotalSpace F E) (z.proj (E := E), ((↑e : TotalSpace F E → B × F) z).2)).snd (E := E) ≍
    z.snd (E := E)
rw₂ : ((↑e.symm : B × F → TotalSpace F E) ((↑e : TotalSpace F E → B × F) z)).snd (E := E) ≍ z.snd (E := E)
rw₃ rw₄ : z.snd (E := E) ≍ z.snd (E := E)
⊢ e.symm (E := E) (z.proj (E := E)) ((↑e : TotalSpace F E → B × F) z).2 = z.snd (E := E)

Tactic:
rw [e.symm_apply hz, cast_eq_iff_heq, e.mk_proj_snd' hz, e.symm_apply_apply (e.mem_source.mpr hz)]

Premises used: Iff.mpr, Bundle.Pretrivialization.mem_source, Bundle.Pretrivialization.symm_apply_apply, Bundle.Pretrivialization.mk_proj_snd', cast_eq_iff_heq, Bundle.Pretrivialization.symm_apply
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → Zero (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
hb : b ∈ e.baseSet
y : E b
⊢ e.symm (E := E) b ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 = y

Tactic:
e.symm_proj_apply ⟨b, y⟩ hb

Premises used: Bundle.Pretrivialization.symm_proj_apply, Bundle.TotalSpace.mk
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → Zero (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
hb : b ∈ e.baseSet
y : F
rw : (↑e : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, y)) = (b, y)
rw₁ rw₂ : (b, y) = (b, y)
⊢ (↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y)) = (b, y)

Tactic:
rw [e.mk_symm hb, e.apply_symm_apply (e.mk_mem_target.mpr hb)]

Premises used: Iff.mpr, Bundle.Pretrivialization.apply_symm_apply, Bundle.Pretrivialization.mk_mem_target, Bundle.Pretrivialization.mk_symm
-- 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
e_1 : Pretrivialization F proj
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
x : Prod.{u_1, u_2} (↑s : Type u_1) F
h : ((↑x.1 : B), x.2) ∈ e.target
⊢ e.invFun ((↑x.1 : B), x.2) ∈ proj ⁻¹' s

Tactic:
simpa only [mem_preimage, ← e.proj_toFun _ (e.map_target' h), e.right_inv' h] using x.1.2

Premises used: PartialEquiv.right_inv', Prod.fst, Bundle.Pretrivialization.toPartialEquiv, Bundle.Pretrivialization.proj_toFun, PartialEquiv.map_target', Set.mem_preimage, Subtype.property
-- 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
e_1 : Pretrivialization F proj
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
x : Prod.{u_1, u_2} (↑s : Type u_1) F
⊢ (↑(proj ⁻¹' s) : Type u_4)

Tactic:
exact if h : (x.1.1, x.2) ∈ e.target then ⟨e.invFun (x.1, x.2), by
      simpa only [mem_preimage, ← e.proj_toFun _ (e.map_target' h), e.right_inv' h] using x.1.2⟩
    else Classical.arbitrary (s → F → _) x.1 x.2

Premises used: PartialEquiv.target, Prod.mk, Prod.fst, Bundle.Pretrivialization.toPartialEquiv, Classical.arbitrary, Subtype.val, Prod.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
e_1 : Pretrivialization F proj
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
x : Prod.{u_1, u_2} (↑s : Type u_1) F
⊢ (↑(proj ⁻¹' s) : Type u_4)

Tactic:
classical exact if h : (x.1.1, x.2) ∈ e.target then ⟨e.invFun (x.1, x.2), by
      simpa only [mem_preimage, ← e.proj_toFun _ (e.map_target' h), e.right_inv' h] using x.1.2⟩
    else Classical.arbitrary (s → F → _) x.1 x.2

Premises used: PartialEquiv.target, Prod.mk, Prod.fst, Bundle.Pretrivialization.toPartialEquiv, Classical.arbitrary, Subtype.val, Prod.snd