awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
x : Z
⊢ x ∈ e.source ↔ proj x ∈ e.baseSet
have rw : x ∈ proj ⁻¹' e.baseSet ↔ proj x ∈ e.baseSet
Tactic: rw [e.source_eq, mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
x : Z
rw : x ∈ proj ⁻¹' e.baseSet ↔ proj x ∈ e.baseSet
⊢ x ∈ e.source ↔ proj x ∈ e.baseSet
have rw₁ : proj x ∈ e.baseSet ↔ proj x ∈ e.baseSet
Tactic: rw [e.source_eq, mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ map proj (𝓝 x) = 𝓝 (proj x)
have rw : map proj (𝓝 x) = 𝓝 ((↑e : Z → B × F) x).1
Tactic: rw [← e.coe_fst ex, ← map_congr (e.coe_fst_eventuallyEq_proj ex), ← map_map, ← e.coe_coe,
    e.map_nhds_eq ex, map_fst_nhds]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
x : Z
ex : x ∈ e.source
rw : map proj (𝓝 x) = 𝓝 ((↑e : Z → B × F) x).1
⊢ map proj (𝓝 x) = 𝓝 (proj x)
have rw₁ : map (Prod.fst ∘ (↑e : Z → B × F)) (𝓝 x) = 𝓝 ((↑e : Z → B × F) x).1
Tactic: rw [← e.coe_fst ex, ← map_congr (e.coe_fst_eventuallyEq_proj ex), ← map_map, ← e.coe_coe,
    e.map_nhds_eq ex, map_fst_nhds]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
x : Z
ex : x ∈ e.source
rw : map proj (𝓝 x) = 𝓝 ((↑e : Z → B × F) x).1
rw₁ : map (Prod.fst ∘ (↑e : Z → B × F)) (𝓝 x) = 𝓝 ((↑e : Z → B × F) x).1
⊢ map proj (𝓝 x) = 𝓝 (proj x)
have rw₂ : map Prod.fst (map (↑e : Z → B × F) (𝓝 x)) = 𝓝 ((↑e : Z → B × F) x).1
Tactic: rw [← e.coe_fst ex, ← map_congr (e.coe_fst_eventuallyEq_proj ex), ← map_map, ← e.coe_coe,
    e.map_nhds_eq ex, map_fst_nhds]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
x : Z
ex : x ∈ e.source
rw : map proj (𝓝 x) = 𝓝 ((↑e : Z → B × F) x).1
rw₁ : map (Prod.fst ∘ (↑e : Z → B × F)) (𝓝 x) = 𝓝 ((↑e : Z → B × F) x).1
rw₂ : map Prod.fst (map (↑e : Z → B × F) (𝓝 x)) = 𝓝 ((↑e : Z → B × F) x).1
⊢ map proj (𝓝 x) = 𝓝 (proj x)
have rw₃ : map Prod.fst (map (↑e.toOpenPartialHomeomorph : Z → B × F) (𝓝 x)) = 𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x).1
Tactic: rw [← e.coe_fst ex, ← map_congr (e.coe_fst_eventuallyEq_proj ex), ← map_map, ← e.coe_coe,
    e.map_nhds_eq ex, map_fst_nhds]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
x : Z
ex : x ∈ e.source
rw : map proj (𝓝 x) = 𝓝 ((↑e : Z → B × F) x).1
rw₁ : map (Prod.fst ∘ (↑e : Z → B × F)) (𝓝 x) = 𝓝 ((↑e : Z → B × F) x).1
rw₂ : map Prod.fst (map (↑e : Z → B × F) (𝓝 x)) = 𝓝 ((↑e : Z → B × F) x).1
rw₃ :
  map Prod.fst (map (↑e.toOpenPartialHomeomorph : Z → B × F) (𝓝 x)) = 𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x).1
⊢ map proj (𝓝 x) = 𝓝 (proj x)
have rw₄ : map Prod.fst (𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x)) = 𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x).1
Tactic: rw [← e.coe_fst ex, ← map_congr (e.coe_fst_eventuallyEq_proj ex), ← map_map, ← e.coe_coe,
    e.map_nhds_eq ex, map_fst_nhds]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
x : Z
ex : x ∈ e.source
rw : map proj (𝓝 x) = 𝓝 ((↑e : Z → B × F) x).1
rw₁ : map (Prod.fst ∘ (↑e : Z → B × F)) (𝓝 x) = 𝓝 ((↑e : Z → B × F) x).1
rw₂ : map Prod.fst (map (↑e : Z → B × F) (𝓝 x)) = 𝓝 ((↑e : Z → B × F) x).1
rw₃ :
  map Prod.fst (map (↑e.toOpenPartialHomeomorph : Z → B × F) (𝓝 x)) = 𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x).1
rw₄ : map Prod.fst (𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x)) = 𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x).1
⊢ map proj (𝓝 x) = 𝓝 (proj x)
have rw₅ : 𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x).1 = 𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x).1
Tactic: rw [← e.coe_fst ex, ← map_congr (e.coe_fst_eventuallyEq_proj ex), ← map_map, ← e.coe_coe,
    e.map_nhds_eq ex, map_fst_nhds]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
⊢ Tendsto f l (𝓝 z) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
have rw : ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
      Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
    ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
  Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
Tactic: rw [e.nhds_eq_comap_inf_principal hz, tendsto_inf, tendsto_comap_iff, Prod.tendsto_iff, coe_coe,
    tendsto_principal, coe_fst _ hz]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
⊢ ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
        Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
have pos : ∀ (hl : ∀ᶠ (x : α) in l, f x ∈ e.source),
  ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
        Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
Tactic: by_cases hl : ∀ᶠ x in l, f x ∈ e.source
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
pos :
  ∀ (hl : ∀ᶠ (x : α) in l, f x ∈ e.source),
    ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
          Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
        ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
      Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧
        Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
⊢ ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
        Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
have neg : ∀ (hl : ¬∀ᶠ (x : α) in l, f x ∈ e.source),
  ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
        Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
Tactic: by_cases hl : ∀ᶠ x in l, f x ∈ e.source
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ∀ᶠ (x : α) in l, f x ∈ e.source
⊢ ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
        Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
have pos : Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
    Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2) ↔
  Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
Tactic: simp only [hl, and_true]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ∀ᶠ (x : α) in l, f x ∈ e.source
⊢ Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
      Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
have pos : (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) =ᶠ[l] proj ∘ f
Tactic: refine (tendsto_congr' ?_).and Iff.rfl
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ¬∀ᶠ (x : α) in l, f x ∈ e.source
⊢ ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
        Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
have neg : Tendsto (proj ∘ f) l (𝓝 (proj z)) → ¬Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
Tactic: simp only [hl, and_false, false_iff, not_and]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (hypothesis)
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
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ¬∀ᶠ (x : α) in l, f x ∈ e.source
⊢ Tendsto (proj ∘ f) l (𝓝 (proj z)) → ¬Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
have hz₁ : z ∈ proj ⁻¹' e.baseSet
Tactic: rw [e.source_eq] at hl hz
Cleared hypotheses: hz, hl
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (hypothesis)
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
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ¬∀ᶠ (x : α) in l, f x ∈ e.source
hz₁ : z ∈ proj ⁻¹' e.baseSet
⊢ Tendsto (proj ∘ f) l (𝓝 (proj z)) → ¬Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
have hl₁ : ¬∀ᶠ (x : α) in l, f x ∈ proj ⁻¹' e.baseSet
Tactic: rw [e.source_eq] at hl hz
Cleared hypotheses: hz, hl
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
z : Z
hz : z ∈ e.source
⊢ 𝓝 z = comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ (↑e : Z → B × F)) (𝓝 ((↑e : Z → B × F) z).2)
have refine : ∀ (l : Filter Z), l ≤ 𝓝 z ↔ l ≤ comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ (↑e : Z → B × F)) (𝓝 ((↑e : Z → B × F) z).2)
Tactic: refine eq_of_forall_le_iff fun l ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e : Trivialization F proj
z : Z
hz : z ∈ e.source
l : Filter Z
⊢ l ≤ 𝓝 z ↔ l ≤ comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ (↑e : Z → B × F)) (𝓝 ((↑e : Z → B × F) z).2)
have rw : l ≤ 𝓝 z ↔ Tendsto proj l (𝓝 (proj z)) ∧ Tendsto (Prod.snd ∘ (↑e : Z → B × F)) l (𝓝 ((↑e : Z → B × F) z).2)
Tactic: rw [le_inf_iff, ← tendsto_iff_comap, ← tendsto_iff_comap]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
b : B
hb : b ∈ e.baseSet
p : F
⊢ (↑e.symm : B × F → Z) (b, p) ∈ proj ⁻¹' {b}
have rw : Membership.mem (γ := Set B) {b} (proj ((↑e.symm : B × F → Z) (b, p)))
Tactic: rw [mem_preimage, e.proj_symm_apply' hb, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
b : B
hb : b ∈ e.baseSet
p : F
rw : Membership.mem (γ := Set B) {b} (proj ((↑e.symm : B × F → Z) (b, p)))
⊢ (↑e.symm : B × F → Z) (b, p) ∈ proj ⁻¹' {b}
have rw₁ : Membership.mem (γ := Set B) {b} b
Tactic: rw [mem_preimage, e.proj_symm_apply' hb, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
b : B
hb : b ∈ e.baseSet
p : F
rw : Membership.mem (γ := Set B) {b} (proj ((↑e.symm : B × F → Z) (b, p)))
rw₁ : Membership.mem (γ := Set B) {b} b
⊢ (↑e.symm : B × F → Z) (b, p) ∈ proj ⁻¹' {b}
have rw₂ : b = b
Tactic: rw [mem_preimage, e.proj_symm_apply' hb, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (hypothesis)
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
Z' : Type u_5
inst_4 : TopologicalSpace Z'
h : Z' ≃ₜ Z
p : Z'
hp : p ∈ (h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph).source
⊢ ((↑(h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph) : Z' → B × F) p).1 = (proj ∘ (⇑h : (a : Z') → Z)) p
have hp₁ : Membership.mem (α := Z) e.source ((h : (a : Z') → Z) p : Z)
Tactic: have hp : h p ∈ e.source := by simpa using hp
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
B' : Type u_5
inst_4 : TopologicalSpace B'
h : B ≃ₜ B'
⊢ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).source =
    preimage.{u_4, u_5} (β := B') ((⇑h : (a : B) → B') ∘ proj) ((⇑h.symm : (a : B') → B) ⁻¹' e.baseSet)
have h₁ : ∀ (x : Z),
  x ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).source ↔
    x ∈ preimage.{u_4, u_5} (β := B') ((⇑h : (a : B) → B') ∘ proj) ((⇑h.symm : (a : B') → B) ⁻¹' e.baseSet)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
B' : Type u_5
inst_4 : TopologicalSpace B'
h : B ≃ₜ B'
⊢ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).target =
    SProd.sprod (α := Set B') (β := Set F) ((⇑h.symm : (a : B') → B) ⁻¹' e.baseSet) univ
have h₁ : ∀ (x : B' × F),
  x ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).target ↔
    x ∈ SProd.sprod (α := Set B') (β := Set F) ((⇑h.symm : (a : B') → B) ⁻¹' e.baseSet) univ
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (hypothesis)
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
X : Type u_5
inst_3 : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ (↑e.symm : B × F → Z)) ((↑e : Z → B × F) z)
⊢ ContinuousAt f z
have hez : z ∈ e.symm.target
Tactic: have hez : z ∈ e.toPartialEquiv.symm.target := by
    rw [PartialEquiv.symm_target, e.mem_source]
    exact he
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
X : Type u_5
inst_3 : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ (↑e.symm : B × F → Z)) ((↑e : Z → B × F) z)
hez : z ∈ e.symm.target
⊢ ContinuousAt f z
have rwa : ContinuousAt (f ∘ (↑e.symm : B × F → Z)) ((↑e.symm.symm : Z → B × F) z)
Tactic: rwa [e.toOpenPartialHomeomorph.symm.continuousAt_iff_continuousAt_comp_right hez,
    OpenPartialHomeomorph.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
X : Type u_5
inst_3 : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ (↑e.symm : B × F → Z)) ((↑e : Z → B × F) z)
hez : z ∈ e.symm.target
rwa : ContinuousAt (f ∘ (↑e.symm : B × F → Z)) ((↑e.symm.symm : Z → B × F) z)
⊢ ContinuousAt f z
have rwa₁ : ContinuousAt (f ∘ (↑e.symm : B × F → Z)) ((↑e.toOpenPartialHomeomorph : Z → B × F) z)
Tactic: rwa [e.toOpenPartialHomeomorph.symm.continuousAt_iff_continuousAt_comp_right hez,
    OpenPartialHomeomorph.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
X : Type u_5
inst_3 : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt ((↑e : Z → B × F) ∘ f) x
⊢ ContinuousAt f x
have rw : ContinuousAt ((↑e.toOpenPartialHomeomorph : Z → B × F) ∘ f) x
Tactic: rw [e.continuousAt_iff_continuousAt_comp_left]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
X : Type u_5
inst_3 : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt ((↑e : Z → B × F) ∘ f) x
rw : ContinuousAt ((↑e.toOpenPartialHomeomorph : Z → B × F) ∘ f) x
⊢ ContinuousAt f x
have rw₁ : f ⁻¹' e.source ∈ 𝓝 x
Tactic: rw [e.continuousAt_iff_continuousAt_comp_left]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
X : Type u_5
inst_3 : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt ((↑e : Z → B × F) ∘ f) x
⊢ f ⁻¹' e.source ∈ 𝓝 x
have rw : proj ∘ f ⁻¹' e.baseSet ∈ 𝓝 x
Tactic: rw [e.source_eq, ← preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (x : B) → Zero (E x)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : B × F
hx : x.1 ∈ e.baseSet
right : Membership.mem (γ := Set F) univ x.2
⊢ TotalSpace.mk (E := E) x.1 (e.symm (E := E) x.1 x.2) = (↑e.symm : B × F → TotalSpace F E) x
have rw : (↑e.symm : B × F → TotalSpace F E) (x.1, x.2) = (↑e.symm : B × F → TotalSpace F E) x
Tactic: rw [e.mk_symm hx]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (hypothesis)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (x : B) → Zero (E x)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
⊢ ContinuousOn (Y := TotalSpace F E) (fun (z : B × F) ↦ TotalSpace.mk' (E := E) F z.1 (e.symm (E := E) z.1 z.2))
    (SProd.sprod (β := Set F) e.baseSet univ)
have this : ∀ z ∈ SProd.sprod (β := Set F) e.baseSet univ,
  TotalSpace.mk (E := E) z.1 (e.symm (E := E) z.1 z.2) = (↑e.symm : B × F → TotalSpace F E) z
Tactic: have : ∀ z ∈ e.baseSet ×ˢ (univ : Set F),
      TotalSpace.mk z.1 (e.symm z.1 z.2) = e.toOpenPartialHomeomorph.symm z := by
    rintro x ⟨hx : x.1 ∈ e.baseSet, _⟩
    rw [e.mk_symm hx]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (x : B) → Zero (E x)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
this :
  ∀ z ∈ SProd.sprod (β := Set F) e.baseSet univ,
    TotalSpace.mk (E := E) z.1 (e.symm (E := E) z.1 z.2) = (↑e.symm : B × F → TotalSpace F E) z
⊢ ContinuousOn (Y := TotalSpace F E) (fun (z : B × F) ↦ TotalSpace.mk' (E := E) F z.1 (e.symm (E := E) z.1 z.2))
    (SProd.sprod (β := Set F) e.baseSet univ)
have refine : ContinuousOn (↑e.symm : B × F → TotalSpace F E) (SProd.sprod (β := Set F) e.baseSet univ)
Tactic: refine ContinuousOn.congr ?_ this
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (x : B) → Zero (E x)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
this :
  ∀ z ∈ SProd.sprod (β := Set F) e.baseSet univ,
    TotalSpace.mk (E := E) z.1 (e.symm (E := E) z.1 z.2) = (↑e.symm : B × F → TotalSpace F E) z
⊢ ContinuousOn (↑e.symm : B × F → TotalSpace F E) (SProd.sprod (β := Set F) e.baseSet univ)
have rw : ContinuousOn (↑e.symm : B × F → TotalSpace F E) e.target
Tactic: rw [← e.target_eq]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, e₁.coordChange e₂ b x) = (↑e₂ : Z → B × F) ((↑e₁.symm : B × F → Z) (b, x))
have refine : (b, e₁.coordChange e₂ b x).1 = ((↑e₂ : Z → B × F) ((↑e₁.symm : B × F → Z) (b, x))).1
Tactic: refine Prod.ext ?_ rfl