awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F₁ : Type u_2
inst_1 : TopologicalSpace F₁
E₁ : B → Type u_3
inst_2 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst_3 : TopologicalSpace F₂
E₂ : B → Type u_5
inst_4 : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_5 : (x : B) → Zero (E₁ x)
inst_6 : (x : B) → Zero (E₂ x)
⊢ ContinuousOn (invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂) (SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ)
have rw : ContinuousOn (Y := TotalSpace F₁ E₁ × TotalSpace F₂ E₂)
  ((fun (p : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ↦
      (TotalSpace.mk (E := E₁) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
          p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).1,
        TotalSpace.mk (E := E₂) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
          p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).2)) ∘
    invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂)
  (SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ)
Tactic: rw [(Prod.isInducing_diag F₁ E₁ F₂ E₂).continuousOn_iff]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (hypothesis)
Goal:
B : Type u_1
inst : TopologicalSpace B
F₁ : Type u_2
inst_1 : TopologicalSpace F₁
E₁ : B → Type u_3
inst_2 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst_3 : TopologicalSpace F₂
E₂ : B → Type u_5
inst_4 : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_5 : (x : B) → Zero (E₁ x)
inst_6 : (x : B) → Zero (E₂ x)
⊢ ContinuousOn (Y := TotalSpace F₁ E₁ × TotalSpace F₂ E₂)
    ((fun (p : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ↦
        (TotalSpace.mk (E := E₁) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
            p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).1,
          TotalSpace.mk (E := E₂) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
            p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).2)) ∘
      invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂)
    (SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ)
have H₁ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : B × F₁ × F₂) ↦ ((p.1, p.2.1), p.1, p.2.2)
Tactic: have H₁ : Continuous fun p : B × F₁ × F₂ ↦ ((p.1, p.2.1), (p.1, p.2.2)) := by fun_prop
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F₁ : Type u_2
inst_1 : TopologicalSpace F₁
E₁ : B → Type u_3
inst_2 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst_3 : TopologicalSpace F₂
E₂ : B → Type u_5
inst_4 : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_5 : (x : B) → Zero (E₁ x)
inst_6 : (x : B) → Zero (E₂ x)
H₁ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : B × F₁ × F₂) ↦ ((p.1, p.2.1), p.1, p.2.2)
⊢ ContinuousOn (Y := TotalSpace F₁ E₁ × TotalSpace F₂ E₂)
    ((fun (p : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ↦
        (TotalSpace.mk (E := E₁) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
            p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).1,
          TotalSpace.mk (E := E₂) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
            p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).2)) ∘
      invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂)
    (SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ)
have refine : MapsTo (fun (p : B × F₁ × F₂) ↦ ((p.1, p.2.1), p.1, p.2.2))
  (SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ)
  (SProd.sprod (β := Set F₁) e₁.baseSet univ ×ˢ SProd.sprod (β := Set F₂) e₂.baseSet univ)
Tactic: refine (e₁.continuousOn_symm.prodMap e₂.continuousOn_symm).comp H₁.continuousOn ?_
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F₁ : Type u_2
inst_1 : TopologicalSpace F₁
E₁ : B → Type u_3
inst_2 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst_3 : TopologicalSpace F₂
E₂ : B → Type u_5
inst_4 : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_5 : (x : B) → Zero (E₁ x)
inst_6 : (x : B) → Zero (E₂ x)
⊢ IsOpen[Prod.topologicalSpace F₁ E₁ F₂ E₂]
    (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
have h : Eq (α := Set (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
  (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
  ((fun (p : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ↦
      (TotalSpace.mk (E := E₁) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
          p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).1,
        TotalSpace.mk (E := E₂) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
          p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).2)) ⁻¹'
    e₁.source ×ˢ e₂.source)
Tactic: convert!
      (e₁.open_source.prod e₂.open_source).preimage
        (FiberBundle.Prod.isInducing_diag F₁ E₁ F₂ E₂).continuous
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F₁ : Type u_2
inst_1 : TopologicalSpace F₁
E₁ : B → Type u_3
inst_2 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst_3 : TopologicalSpace F₂
E₂ : B → Type u_5
inst_4 : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_5 : (x : B) → Zero (E₁ x)
inst_6 : (x : B) → Zero (E₂ x)
⊢ Eq (α := Set (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
    (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
    ((fun (p : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ↦
        (TotalSpace.mk (E := E₁) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
            p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).1,
          TotalSpace.mk (E := E₂) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
            p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).2)) ⁻¹'
      e₁.source ×ˢ e₂.source)
have h : ∀ (x : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)),
  Membership.mem (γ := Set (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
      (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet)) x ↔
    Membership.mem (γ := Set (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
      ((fun (p : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ↦
          (TotalSpace.mk (E := E₁) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
              p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).1,
            TotalSpace.mk (E := E₂) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
              p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).2)) ⁻¹'
        e₁.source ×ˢ e₂.source)
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F₁ : Type u_2
inst_1 : TopologicalSpace F₁
E₁ : B → Type u_3
inst_2 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst_3 : TopologicalSpace F₂
E₂ : B → Type u_5
inst_4 : TopologicalSpace (TotalSpace F₂ E₂)
inst_5 : (x : B) → Zero (E₁ x)
inst_6 : (x : B) → Zero (E₂ x)
inst_7 : (x : B) → TopologicalSpace (E₁ x)
inst_8 : (x : B) → TopologicalSpace (E₂ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : FiberBundle F₂ E₂
b : B
⊢ IsInducing (X := Prod.{u_3, u_5} (E₁ b) (E₂ b)) (Y :=
    TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x))
    (TotalSpace.mk (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b)
have rw : IsInducing (X := Prod.{u_3, u_5} (E₁ b) (E₂ b)) (Y := TotalSpace F₁ E₁ × TotalSpace F₂ E₂)
  ((fun (p : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ↦
        (TotalSpace.mk (E := E₁) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
            p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).1,
          TotalSpace.mk (E := E₂) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
            p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).2)) ∘
      TotalSpace.mk (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b :
    Prod.{u_3, u_5} (E₁ b) (E₂ b) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂)
Tactic: rw [← (Prod.isInducing_diag F₁ E₁ F₂ E₂).of_comp_iff]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Continuous[TotalSpace.topologicalSpace F E f, inst] (TotalSpace.proj (E := f *ᵖ E))
have rw : induced (TotalSpace.proj (E := f *ᵖ E)) inst ⊓ induced (Pullback.lift (E := E) f) inst_1 ≤
  induced (TotalSpace.proj (E := f *ᵖ E)) inst
Tactic: rw [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Continuous[TotalSpace.topologicalSpace F E f, inst_1] (Pullback.lift (E := E) f)
have rw : induced (TotalSpace.proj (E := f *ᵖ E)) inst ⊓ induced (Pullback.lift (E := E) f) inst_1 ≤
  induced (Pullback.lift (E := E) f) inst_1
Tactic: rw [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ IsInducing (X := TotalSpace F (f *ᵖ E)) (pullbackTotalSpaceEmbedding (E := E) f)
have eq_induced : Pullback.TotalSpace.topologicalSpace F E f = induced (pullbackTotalSpaceEmbedding (E := E) f) instTopologicalSpaceProd
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Pullback.TotalSpace.topologicalSpace F E f = induced (pullbackTotalSpaceEmbedding (E := E) f) instTopologicalSpaceProd
have eq_induced : induced (TotalSpace.proj (E := f *ᵖ E)) inst ⊓ induced (Pullback.lift (E := E) f) inst_1 =
  induced (Prod.fst ∘ pullbackTotalSpaceEmbedding (E := E) f) inst ⊓
    induced (Prod.snd ∘ pullbackTotalSpaceEmbedding (E := E) f) inst_1
Tactic: simp_rw [instTopologicalSpaceProd, induced_inf, induced_compose,
    Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (x : B) → TopologicalSpace (E x)
inst_5 : FiberBundle F E
f : B' → B
x : B'
⊢ Continuous[instTopologicalSpacePullback E f x, TotalSpace.topologicalSpace F E f] (TotalSpace.mk (E := f *ᵖ E) x)
have simp : instTopologicalSpacePullback E f x ≤
  induced (fun (x_1 : (f *ᵖ E) x) ↦ Pullback.lift (E := E) f (TotalSpace.mk (E := f *ᵖ E) x x_1)) inst_1
Tactic: simp only [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, induced_compose,
    induced_inf, Function.comp_def, induced_const, top_inf_eq, pullbackTopology_def]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (hypothesis)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)
h :
  Membership.mem (γ := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.source) x
⊢ (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
      ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2) ∈
    SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ
have h₁ : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) : B)
Tactic: simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) : B)
⊢ (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
      ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2) ∈
    SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ
have simp_rw : Membership.mem (γ := Set B') ((⇑f : (a : B') → B) ⁻¹' e.baseSet) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) ∧
  Membership.mem (γ := Set F) univ ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2
Tactic: simp_rw [prodMk_mem_set_prod_eq, mem_univ, and_true, mem_preimage, h]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) : B)
simp_rw :
  Membership.mem (γ := Set B') ((⇑f : (a : B') → B) ⁻¹' e.baseSet) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) ∧
    Membership.mem (γ := Set F) univ ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2
⊢ (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
      ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2) ∈
    SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ
have simp_rw₁ : Membership.mem (γ := Set B') ((⇑f : (a : B') → B) ⁻¹' e.baseSet) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) ∧ True
Tactic: simp_rw [prodMk_mem_set_prod_eq, mem_univ, and_true, mem_preimage, h]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) : B)
simp_rw :
  Membership.mem (γ := Set B') ((⇑f : (a : B') → B) ⁻¹' e.baseSet) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) ∧
    Membership.mem (γ := Set F) univ ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2
simp_rw₁ :
  Membership.mem (γ := Set B') ((⇑f : (a : B') → B) ⁻¹' e.baseSet) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) ∧ True
⊢ (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
      ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2) ∈
    SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ
have simp_rw₂ : Membership.mem (γ := Set B') ((⇑f : (a : B') → B) ⁻¹' e.baseSet) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E))
Tactic: simp_rw [prodMk_mem_set_prod_eq, mem_univ, and_true, mem_preimage, h]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (hypothesis)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
y : B' × F
h : y ∈ SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ
⊢ Membership.mem (γ := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.source)
    (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))
have h₁ : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) y.1 : B) ∧ Membership.mem (γ := Set F) univ y.2
Tactic: rw [mem_prod, mem_preimage] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
y : B' × F
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) y.1 : B) ∧ Membership.mem (γ := Set F) univ y.2
⊢ Membership.mem (γ := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.source)
    (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))
have simp_rw : Membership.mem (γ := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
  (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' TotalSpace.proj (E := E) ⁻¹' e.baseSet)
  (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))
Tactic: simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj, h.1]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
y : B' × F
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) y.1 : B) ∧ Membership.mem (γ := Set F) univ y.2
simp_rw :
  Membership.mem (γ := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' TotalSpace.proj (E := E) ⁻¹' e.baseSet)
    (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))
⊢ Membership.mem (γ := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.source)
    (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))
have simp_rw₁ : TotalSpace.proj.{u, v, w₁} (F := F) (E := E)
    (Pullback.lift (E := E) (⇑f : (a : B') → B)
      (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))) ∈
  e.baseSet
Tactic: simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj, h.1]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
y : B' × F
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) y.1 : B) ∧ Membership.mem (γ := Set F) univ y.2
simp_rw :
  Membership.mem (γ := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' TotalSpace.proj (E := E) ⁻¹' e.baseSet)
    (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))
simp_rw₁ :
  TotalSpace.proj.{u, v, w₁} (F := F) (E := E)
      (Pullback.lift (E := E) (⇑f : (a : B') → B)
        (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))) ∈
    e.baseSet
⊢ Membership.mem (γ := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.source)
    (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))
have simp_rw₂ : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) y.1 : B)
Tactic: simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj, h.1]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (hypothesis)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)
h :
  Membership.mem (γ := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.source) x
⊢ TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E)
      (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
          ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2).1
      (e.symm (E := E)
        ((f : (a : B') → B)
          (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
              ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2).1)
        (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
            ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2).2) =
    x
have h₁ : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) : B)
Tactic: simp_rw [mem_preimage, e.mem_source, Pullback.lift_proj] at h
Cleared hypotheses: h