awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : ContinuousRiemannianMetric F E
b : B
e : ContinuousLinearEquiv.{0, 0, u_6, u_5} (RingHom.id ℝ) (E b) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E b) b ⋯
m : ContinuousLinearEquiv.{0, 0, u_6, u_5} (RingHom.id ℝ) (E b →L[ℝ] E b →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) :=
  e.arrowCongr (e.arrowCongr (ContinuousLinearEquiv.refl ℝ ℝ))
A :
  ∀ (v : E b),
    Eq (α := ℝ) ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) v : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v : ℝ)
      (((fun (w : F) ↦
              (((((m : (a : E b →L[ℝ] E b →L[ℝ] ℝ) → F →L[ℝ] F →L[ℝ] ℝ) (g.inner (E := E) b) : F →L[ℝ] F →L[ℝ] ℝ) :
                        (a : F) → F →L[ℝ] ℝ)
                      w :
                    F →L[ℝ] ℝ) :
                  (a : F) → ℝ)
                w) ∘
            (⇑e : (a : E b) → F))
          v :
        ℝ)
⊢ ContinuousAt (Y := ℝ)
    (fun (v : E b) ↦
      ((fun (w : F) ↦
            (((((m : (a : E b →L[ℝ] E b →L[ℝ] ℝ) → F →L[ℝ] F →L[ℝ] ℝ) (g.inner (E := E) b) : F →L[ℝ] F →L[ℝ] ℝ) :
                      (a : F) → F →L[ℝ] ℝ)
                    w :
                  F →L[ℝ] ℝ) :
                (a : F) → ℝ)
              w) ∘
          (⇑e : (a : E b) → F))
        v)
    0

Tactic:
fun_prop
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : ContinuousRiemannianMetric F E
this : RiemannianBundle E := RiemannianBundle.mk (E := E) (g.toRiemannianMetric (E := E))
⊢ IsContinuousRiemannianBundle F E

Tactic:
⟨⟨g.inner, g.continuous, fun b v w ↦ rfl⟩⟩

Premises used: Bundle.ContinuousRiemannianMetric.continuous, IsContinuousRiemannianBundle.mk, Bundle.ContinuousRiemannianMetric.inner, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : ContinuousRiemannianMetric F E
this : RiemannianBundle E := RiemannianBundle.mk (E := E) (g.toRiemannianMetric (E := E))
⊢ IsContinuousRiemannianBundle F E

Tactic:
exact ⟨⟨g.inner, g.continuous, fun b v w ↦ rfl⟩⟩
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
x : X
⊢ (toTopology t x).ofTopology = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
x : WithTopology X t
⊢ toTopology t x.ofTopology = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := WithTopology X t) ofTopology

Tactic:
Function.RightInverse.surjective <| ofTopology_toTopology _

Premises used: WithTopology.ofTopology_toTopology, Function.RightInverse.surjective
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
⊢ Function.Surjective (toTopology t)

Tactic:
Function.RightInverse.surjective <| toTopology_ofTopology _

Premises used: WithTopology.toTopology_ofTopology, Function.RightInverse.surjective
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := WithTopology X t) ofTopology

Tactic:
Function.LeftInverse.injective <| toTopology_ofTopology _

Premises used: Function.LeftInverse.injective, WithTopology.toTopology_ofTopology
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
⊢ Function.Injective (toTopology t)

Tactic:
Function.LeftInverse.injective <| ofTopology_toTopology _

Premises used: Function.LeftInverse.injective, WithTopology.ofTopology_toTopology
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := WithTopology X t) ofTopology

Tactic:
⟨ofTopology_injective t, ofTopology_surjective t⟩

Premises used: WithTopology.ofTopology_injective, And.intro, Function.Bijective, WithTopology.ofTopology_surjective
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
⊢ Function.Bijective (toTopology t)

Tactic:
⟨toTopology_injective t, toTopology_surjective t⟩

Premises used: WithTopology.toTopology_injective, And.intro, Function.Bijective, WithTopology.toTopology_surjective
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
x y : X
⊢ toTopology t x = toTopology t y ↔ x = y

Tactic:
(toTopology_injective t).eq_iff

Premises used: Function.Injective.eq_iff, WithTopology.toTopology_injective
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
x y : WithTopology X t
⊢ x.ofTopology = y.ofTopology ↔ x = y

Tactic:
(ofTopology_injective t).eq_iff

Premises used: WithTopology.ofTopology_injective, Function.Injective.eq_iff
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
s : Set (WithTopology X t)
⊢ ofTopology '' s = toTopology t ⁻¹' s

Tactic:
WithTopology.equiv X t |>.symm.image_symm_eq_preimage _

Premises used: WithTopology.equiv, Equiv.symm, Equiv.image_symm_eq_preimage
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
s : Set (WithTopology X t)
⊢ toTopology t ⁻¹' s = ofTopology '' s

Tactic:
(image_ofTopology t s).symm

Premises used: WithTopology.image_ofTopology, Eq.symm
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
s : Set X
⊢ toTopology t '' s = ofTopology ⁻¹' s

Tactic:
WithTopology.equiv X t |>.symm.image_eq_preimage_symm _

Premises used: Equiv.image_eq_preimage_symm, WithTopology.equiv, Equiv.symm
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
s : Set X
⊢ ofTopology ⁻¹' s = toTopology t '' s

Tactic:
(image_toTopology t s).symm

Premises used: Eq.symm, WithTopology.image_toTopology
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
inst : Nonempty X
⊢ Nonempty.{u_1 + 1} (WithTopology X t)

Tactic:
(WithTopology.equiv X t).nonempty

Premises used: WithTopology.equiv, Equiv.nonempty
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
inst : Subsingleton X
⊢ Subsingleton.{u_1 + 1} (WithTopology X t)

Tactic:
(WithTopology.equiv X t).subsingleton

Premises used: WithTopology.equiv, Equiv.subsingleton
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
inst : Finite X
⊢ Finite.{u_1 + 1} (WithTopology X t)

Tactic:
.of_equiv _ (WithTopology.equiv X t).symm

Premises used: Finite.of_equiv, WithTopology.equiv, Equiv.symm
-- Module: Mathlib.Topology.WithTopology
Goal:
X : Type u_1
t : TopologicalSpace X
inst : Infinite X
⊢ Infinite.{u_1 + 1} (WithTopology X t)

Tactic:
.of_injective _ <| toTopology_injective _

Premises used: Infinite.of_injective, WithTopology.toTopology_injective
-- Module: Mathlib.Util.CompileInductive
Goal:
⊢ val = valImpl

Tactic:
rfl

Premises used: _private.0.Float.valImpl, rfl
-- Module: Mathlib.Util.CompileInductive
Goal:
⊢ mk = mkImpl

Tactic:
rfl

Premises used: _private.0.Float.mkImpl, rfl
-- Module: Mathlib.Util.Qq
Goal:
u : Level
α : Q(Sort u)
a : Q(«$α»)
⊢ «$a» =Q «$a»

Tactic:
⟨⟩

Premises used: Qq.QuotedDefEq.unsafeIntro
-- Module: Mathlib.Util.SleepHeartbeats
Goal:
⊢ Eq (α := Nat) 1 1

Tactic:
rfl