awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Z.Fiber x
hx : x ∈ Z.baseSet i
⊢ Eq (α := Z.TotalSpace)
    (TotalSpace.mk (E := Z.Fiber)
      (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v),
          Z.coordChange (Z.indexAt (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))) i
            (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))
            (TotalSpace.snd (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))).1
      (Z.coordChange i
        (Z.indexAt
          (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v),
              Z.coordChange (Z.indexAt (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))) i
                (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))
                (TotalSpace.snd (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))).1)
        (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v),
            Z.coordChange (Z.indexAt (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))) i
              (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))
              (TotalSpace.snd (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))).1
        (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v),
            Z.coordChange (Z.indexAt (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))) i
              (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))
              (TotalSpace.snd (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))).2))
    (TotalSpace.mk (E := Z.Fiber) x v)
have dsimp : Eq (α := Z.TotalSpace)
  (TotalSpace.mk (E := Z.Fiber) x (Z.coordChange i (Z.indexAt x) x (Z.coordChange (Z.indexAt x) i x v)))
  (TotalSpace.mk (E := Z.Fiber) x v)
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Z.Fiber x
hx : x ∈ Z.baseSet i
⊢ Eq (α := Z.TotalSpace)
    (TotalSpace.mk (E := Z.Fiber) x (Z.coordChange i (Z.indexAt x) x (Z.coordChange (Z.indexAt x) i x v)))
    (TotalSpace.mk (E := Z.Fiber) x v)
have a : x ∈ Z.baseSet (Z.indexAt x)
Tactic: rw [Z.coordChange_comp, Z.coordChange_self]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Z.Fiber x
hx : x ∈ Z.baseSet i
a : x ∈ Z.baseSet (Z.indexAt x)
⊢ Eq (α := Z.TotalSpace)
    (TotalSpace.mk (E := Z.Fiber) x (Z.coordChange i (Z.indexAt x) x (Z.coordChange (Z.indexAt x) i x v)))
    (TotalSpace.mk (E := Z.Fiber) x v)
have a₁ : x ∈ Z.baseSet (Z.indexAt x) ∩ Z.baseSet i ∩ Z.baseSet (Z.indexAt x)
Tactic: rw [Z.coordChange_comp, Z.coordChange_self]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : F
hx : (x, v) ∈ SProd.sprod (β := Set F) (Z.baseSet i) univ
⊢ (TotalSpace.proj (F := F) (E := Z.Fiber)
        (TotalSpace.mk (E := Z.Fiber) (x, v).1 (Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2)),
      Z.coordChange
        (Z.indexAt
          (TotalSpace.proj (F := F) (E := Z.Fiber)
            (TotalSpace.mk (E := Z.Fiber) (x, v).1 (Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2))))
        i
        (TotalSpace.proj (F := F) (E := Z.Fiber)
          (TotalSpace.mk (E := Z.Fiber) (x, v).1 (Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2)))
        (TotalSpace.snd (E := Z.Fiber)
          (TotalSpace.mk (E := Z.Fiber) (x, v).1 (Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2)))) =
    (x, v)
have hx₁ : x ∈ Z.baseSet i
Tactic: simp only [prodMk_mem_set_prod_eq, and_true, mem_univ] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : F
hx : x ∈ Z.baseSet i
⊢ (TotalSpace.proj (F := F) (E := Z.Fiber)
        (TotalSpace.mk (E := Z.Fiber) (x, v).1 (Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2)),
      Z.coordChange
        (Z.indexAt
          (TotalSpace.proj (F := F) (E := Z.Fiber)
            (TotalSpace.mk (E := Z.Fiber) (x, v).1 (Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2))))
        i
        (TotalSpace.proj (F := F) (E := Z.Fiber)
          (TotalSpace.mk (E := Z.Fiber) (x, v).1 (Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2)))
        (TotalSpace.snd (E := Z.Fiber)
          (TotalSpace.mk (E := Z.Fiber) (x, v).1 (Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2)))) =
    (x, v)
have dsimp : (x, Z.coordChange (Z.indexAt x) i x (Z.coordChange i (Z.indexAt x) x v)) = (x, v)
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : F
hx a : x ∈ Z.baseSet i
⊢ (x, Z.coordChange (Z.indexAt x) i x (Z.coordChange i (Z.indexAt x) x v)) = (x, v)
have a₁ : x ∈ Z.baseSet i ∩ Z.baseSet (Z.indexAt x) ∩ Z.baseSet i
Tactic: rw [Z.coordChange_comp, Z.coordChange_self]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ (Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j) ≈ (Z.trivChange i j).toPartialEquiv
have left : ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source = (Z.trivChange i j).source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
left : ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source = (Z.trivChange i j).source
⊢ (Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j) ≈ (Z.trivChange i j).toPartialEquiv
have right : EqOn (↑((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)) : B × F → B × F)
  (↑(Z.trivChange i j).toPartialEquiv : B × F → B × F)
  ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source = (Z.trivChange i j).source
have left : ∀ (x : B × F),
  x ∈ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source ↔ x ∈ (Z.trivChange i j).source
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B × F
⊢ x ∈ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source ↔ x ∈ (Z.trivChange i j).source
have left : x.1 ∈ Z.baseSet i ∧
    (↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) x ∈ (Z.localTrivAsPartialEquiv j).source ↔
  x.1 ∈ Z.baseSet i ∧ x.1 ∈ Z.baseSet j
Tactic: simp only [mem_localTrivAsPartialEquiv_target, mfld_simps]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : (x, v) ∈ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source
⊢ (↑((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)) : B × F → B × F) (x, v) =
    (↑(Z.trivChange i j).toPartialEquiv : B × F → B × F) (x, v)
have right : ∀ (hx : (x ∈ Z.baseSet i ∧ True) ∧ x ∈ Z.baseSet j),
  True ∧ Z.coordChange (Z.indexAt x) j x (Z.coordChange i (Z.indexAt x) x v) = Z.coordChange i j x v
Tactic: simp only [trivChange, localTrivAsPartialEquiv, PartialEquiv.symm,
      Prod.mk_inj, prodMk_mem_set_prod_eq, PartialEquiv.trans_source, mem_inter_iff,
      mem_preimage, proj, mem_univ, (· ∘ ·),
      PartialEquiv.coe_trans] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ IsOpen (Z.localTrivAsPartialEquiv i).source
have a : Membership.mem (γ := Set (Set (Bundle.TotalSpace F Z.Fiber)))
  (⋃ (i : ι),
    ⋃ (s : Set (B × F)),
      ⋃ (_ : IsOpen[instTopologicalSpaceProd] s),
        {(Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s})
  (Z.localTrivAsPartialEquiv i).source
Tactic: apply TopologicalSpace.GenerateOpen.basic
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ Membership.mem (γ := Set (Set (Bundle.TotalSpace F Z.Fiber)))
    (⋃ (i : ι),
      ⋃ (s : Set (B × F)),
        ⋃ (_ : IsOpen[instTopologicalSpaceProd] s),
          {(Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s})
    (Z.localTrivAsPartialEquiv i).source
have a : ∃ (i_1 : ι) (i_2 : Set (B × F)),
  IsOpen[instTopologicalSpaceProd] i_2 ∧
    (Z.localTrivAsPartialEquiv i).source =
      (Z.localTrivAsPartialEquiv i_1).source ∩ (↑(Z.localTrivAsPartialEquiv i_1) : Z.TotalSpace → B × F) ⁻¹' i_2
Tactic: simp only [exists_prop, mem_iUnion, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ ∃ (i_1 : ι) (i_2 : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] i_2 ∧
      (Z.localTrivAsPartialEquiv i).source =
        (Z.localTrivAsPartialEquiv i_1).source ∩ (↑(Z.localTrivAsPartialEquiv i_1) : Z.TotalSpace → B × F) ⁻¹' i_2
have a : (Z.localTrivAsPartialEquiv i).source =
  (Z.localTrivAsPartialEquiv i).source ∩
    (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' SProd.sprod (β := Set F) (Z.baseSet i) univ
Tactic: refine ⟨i, Z.baseSet i ×ˢ univ, (Z.isOpen_baseSet i).prod isOpen_univ, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ (Z.localTrivAsPartialEquiv i).source =
    (Z.localTrivAsPartialEquiv i).source ∩
      (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' SProd.sprod (β := Set F) (Z.baseSet i) univ
have a : ∀ (p : Z.TotalSpace),
  p ∈ (Z.localTrivAsPartialEquiv i).source ↔
    p ∈
      (Z.localTrivAsPartialEquiv i).source ∩
        (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' SProd.sprod (β := Set F) (Z.baseSet i) univ
Tactic: ext p
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
⊢ ContinuousOn (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) (Z.localTrivAsPartialEquiv i).source
have rw : ∀ (t : Set (B × F)),
  IsOpen[instTopologicalSpaceProd] t →
    IsOpen ((Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' t)
Tactic: rw [continuousOn_open_iff (Z.open_source' i)]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
⊢ IsOpen ((Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s)
have a₁ : Membership.mem (γ := Set (Set (Bundle.TotalSpace F Z.Fiber)))
  (⋃ (i : ι),
    ⋃ (s : Set (B × F)),
      ⋃ (_ : IsOpen[instTopologicalSpaceProd] s),
        {(Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s})
  ((Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s)
Tactic: apply TopologicalSpace.GenerateOpen.basic
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
⊢ Membership.mem (γ := Set (Set (Bundle.TotalSpace F Z.Fiber)))
    (⋃ (i : ι),
      ⋃ (s : Set (B × F)),
        ⋃ (_ : IsOpen[instTopologicalSpaceProd] s),
          {(Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s})
    ((Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s)
have a₁ : ∃ (i_2 : ι) (i_3 : Set (B × F)),
  IsOpen[instTopologicalSpaceProd] i_3 ∧
    (Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s =
      (Z.localTrivAsPartialEquiv i_2).source ∩ (↑(Z.localTrivAsPartialEquiv i_2) : Z.TotalSpace → B × F) ⁻¹' i_3
Tactic: simp only [exists_prop, mem_iUnion, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
⊢ ContinuousOn (Z.localTrivAsPartialEquiv i).invFun (Z.localTrivAsPartialEquiv i).target
have refine : ∀ (t : Set Z.TotalSpace)
  (ht :
    Membership.mem (γ := Set (Set Z.TotalSpace))
      (⋃ (i : ι),
        ⋃ (s : Set (B × F)),
          ⋃ (_ : IsOpen[instTopologicalSpaceProd] s),
            {(Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s})
      t),
  IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)
Tactic: refine continuousOn_isOpen_of_generateFrom fun t ht ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
ht :
  Membership.mem (γ := Set (Set Z.TotalSpace))
    (⋃ (i : ι),
      ⋃ (s : Set (B × F)),
        ⋃ (_ : IsOpen[instTopologicalSpaceProd] s),
          {(Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s})
    t
⊢ IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)
have ht₁ : ∃ (i : ι) (i_2 : Set (B × F)),
  IsOpen[instTopologicalSpaceProd] i_2 ∧
    t = (Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' i_2
Tactic: simp only [exists_prop, mem_iUnion, mem_singleton_iff] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
ht :
  ∃ (i : ι) (i_2 : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] i_2 ∧
      t = (Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' i_2
⊢ IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)
have obtain : ∀ (j : ι) (s : Set (B × F)) (s_open : IsOpen[instTopologicalSpaceProd] s)
  (ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s),
  IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)
Tactic: obtain ⟨j, s, s_open, ts⟩ : ∃ j s, IsOpen s ∧
      t = (localTrivAsPartialEquiv Z j).source ∩ localTrivAsPartialEquiv Z j ⁻¹' s := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s
⊢ IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)
have rw : IsOpen[instTopologicalSpaceProd]
  ((Z.localTrivAsPartialEquiv i).target ∩
    (Z.localTrivAsPartialEquiv i).invFun ⁻¹'
      ((Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s))
Tactic: rw [ts]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      (Z.localTrivAsPartialEquiv i).invFun ⁻¹'
        ((Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s))
have simp : IsOpen[instTopologicalSpaceProd]
  ((Z.localTrivAsPartialEquiv i).target ∩
    ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
      (Z.localTrivAsPartialEquiv i).invFun ⁻¹' (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s))
Tactic: simp only [preimage_inter]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
⊢ IsOpen[instTopologicalSpaceProd] (f.source ∩ (↑f : B × F → B × F) ⁻¹' s)
have rw : IsOpen[instTopologicalSpaceProd]
  ((Z.trivChange i j).source ∩ (↑(Z.trivChange i j).toPartialEquiv : B × F → B × F) ⁻¹' s)
Tactic: rw [PartialEquiv.EqOnSource.source_inter_preimage_eq (Z.localTrivAsPartialEquiv_trans i j)]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s))
have this : IsOpen[instTopologicalSpaceProd] (f.source ∩ (↑f : B × F → B × F) ⁻¹' s)
Tactic: have : IsOpen (f.source ∩ f ⁻¹' s) := by
      rw [PartialEquiv.EqOnSource.source_inter_preimage_eq (Z.localTrivAsPartialEquiv_trans i j)]
      exact (continuousOn_open_iff (Z.trivChange i j).open_source).1
        (Z.trivChange i j).continuousOn _ s_open
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
this : IsOpen[instTopologicalSpaceProd] (f.source ∩ (↑f : B × F → B × F) ⁻¹' s)
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s))
have h : (Z.localTrivAsPartialEquiv i).target ∩
    ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
      (Z.localTrivAsPartialEquiv i).invFun ⁻¹' (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s) =
  f.source ∩ (↑f : B × F → B × F) ⁻¹' s
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
this : IsOpen[instTopologicalSpaceProd] (f.source ∩ (↑f : B × F → B × F) ⁻¹' s)
⊢ (Z.localTrivAsPartialEquiv i).target ∩
      ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s) =
    f.source ∩ (↑f : B × F → B × F) ⁻¹' s
have h : (Z.localTrivAsPartialEquiv i).target ∩
    ((↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
      (↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) ⁻¹'
        (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s) =
  e.target ∩ (↑e.symm : B × F → Z.TotalSpace) ⁻¹' e'.source ∩
    (↑e' : Z.TotalSpace → B × F) ∘ (↑e.symm : B × F → Z.TotalSpace) ⁻¹' s
Tactic: dsimp [f, PartialEquiv.trans_source]