awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
refine_1 : ContMDiff I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω) fun (x : M) ↦ f x / (f x + g x)
refine_2 : Subset (α := Set ℝ) (range fun (x : M) ↦ f x / (f x + g x)) (Icc 0 1)
refine_3 : (support (M := ℝ) fun (x : M) ↦ f x / (f x + g x)) = s
refine_4 : ∀ (x : M), x ∈ t ↔ Eq (α := ℝ) ((fun (x : M) ↦ f x / (f x + g x)) x) 1
⊢ ∃ (f : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1

Tactic:
refine ⟨fun x ↦ f x / (f x + g x), ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ ContMDiff I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω) fun (x : M) ↦ f x / (f x + g x)

Tactic:
f_diff.div₀ (f_diff.add g_diff) (fun x ↦ ne_of_gt (A x))

Premises used: ContMDiff.div₀, ne_of_gt, ContMDiff.add
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ ContMDiff I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω) fun (x : M) ↦ f x / (f x + g x)

Tactic:
exact f_diff.div₀ (f_diff.add g_diff) (fun x ↦ ne_of_gt (A x))

Premises used: ContMDiff.div₀, ne_of_gt, ContMDiff.add
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ Subset (α := Set ℝ) (range fun (x : M) ↦ f x / (f x + g x)) (Icc 0 1)

Tactic:
range_subset_iff.2 (fun x ↦ ⟨div_nonneg (f_pos x) (A x).le, ?_⟩)

Premises used: Iff.mpr, LT.lt.le, And.intro, div_nonneg, Set.range_subset_iff
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
refine_2 : ∀ (x : M), f x / (f x + g x) ≤ 1
⊢ Subset (α := Set ℝ) (range fun (x : M) ↦ f x / (f x + g x)) (Icc 0 1)

Tactic:
refine range_subset_iff.2 (fun x ↦ ⟨div_nonneg (f_pos x) (A x).le, ?_⟩)
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
x : M
apply : f x ≤ f x + g x
⊢ f x / (f x + g x) ≤ 1

Tactic:
apply div_le_one_of_le₀ _ (A x).le

Premises used: div_le_one_of_le₀, LT.lt.le
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
x : M
⊢ f x ≤ f x + g x

Tactic:
simpa only [le_add_iff_nonneg_right] using g_pos x

Premises used: le_add_iff_nonneg_right
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ Eq.{uM + 1} (α := Set M) (support (M := ℝ) fun (x : M) ↦ f x + g x) univ

Tactic:
have B : support (fun x ↦ f x + g x) = univ := eq_univ_of_forall (fun x ↦ (A x).ne')
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
B : Eq.{uM + 1} (α := Set M) (support (M := ℝ) fun (x : M) ↦ f x + g x) univ
⊢ (support (M := ℝ) fun (x : M) ↦ f x / (f x + g x)) = s

Tactic:
simp only [support_div, f_supp, B, inter_univ]

Premises used: Set.inter_univ, Function.support_div
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
x : M
⊢ x ∈ t ↔ Eq (α := ℝ) ((fun (x : M) ↦ f x / (f x + g x)) x) 1

Tactic:
simp [div_eq_one_iff_eq (A x).ne', left_eq_add, ← notMem_support, g_supp]

Premises used: left_eq_add, div_eq_one_iff_eq, Function.notMem_support, LT.lt.ne'
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
rcases :
  ∀ (f : M → ℝ) (f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f) (f_range : range f ⊆ Icc 0 1) (fs : support f = sᶜ)
    (ft : ∀ (x : M), x ∈ t ↔ f x = 1),
    ∃ (f : M → ℝ),
      ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1
⊢ ∃ (f : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1

Tactic:
rcases exists_contMDiff_support_eq_eq_one_iff I hs.isOpen_compl ht hd.subset_compl_left with
    ⟨f, f_diff, f_range, fs, ft⟩

Premises used: IsClosed.isOpen_compl, Disjoint.subset_compl_left, exists_contMDiff_support_eq_eq_one_iff
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
f : M → ℝ
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_range : range f ⊆ Icc 0 1
fs : support f = sᶜ
ft : ∀ (x : M), x ∈ t ↔ f x = 1
⊢ ∃ (f : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1

Tactic:
⟨f, f_diff, f_range, ?_, ft⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
f : M → ℝ
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_range : range f ⊆ Icc 0 1
fs : support f = sᶜ
ft : ∀ (x : M), x ∈ t ↔ f x = 1
refine : ∀ (x : M), x ∈ s ↔ f x = 0
⊢ ∃ (f : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1

Tactic:
refine ⟨f, f_diff, f_range, ?_, ft⟩
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
f : M → ℝ
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_range : range f ⊆ Icc 0 1
fs : support f = sᶜ
ft : ∀ (x : M), x ∈ t ↔ f x = 1
⊢ ∀ (x : M), x ∈ s ↔ f x = 0

Tactic:
simp [← notMem_support, fs]

Premises used: Function.notMem_support
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x : F
change : IsVonNBounded.{0, u_4} ℝ (E := F) {v : F | ⟪v, v⟫ < 1}
⊢ IsVonNBounded.{0, u_4} ℝ (E := TangentSpace 𝓘(ℝ, F) x)
    {v : TangentSpace 𝓘(ℝ, F) x |
      LT.lt (α := ℝ)
        ((((innerSL ℝ : (a : TangentSpace 𝓘(ℝ, F) x) → TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) v :
                TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) :
              (a : TangentSpace 𝓘(ℝ, F) x) → ℝ)
            v :
          ℝ)
        (1 : ℝ)}

Tactic:
change IsVonNBounded ℝ {v : F | ⟪v, v⟫ < 1}

Premises used: Real, Bornology.IsVonNBounded, Inner.inner, setOf, LT.lt, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x : F
h : ∀ (v : F), Membership.mem (γ := Set F) (Metric.ball 0 1) v ↔ Membership.mem (γ := Set F) {v : F | ⟪v, v⟫ < 1} v
⊢ Eq.{u_4 + 1} (α := Set F) (Metric.ball 0 1) {v : F | ⟪v, v⟫ < 1}

Tactic:
ext v
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x v : F
h : √⟪v, v⟫ < 1 ↔ ⟪v, v⟫ < 1
⊢ Membership.mem (γ := Set F) (Metric.ball 0 1) v ↔ Membership.mem (γ := Set F) {v : F | ⟪v, v⟫ < 1} v

Tactic:
simp only [Metric.mem_ball, dist_zero_right, norm_eq_sqrt_re_inner (𝕜 := ℝ),
        RCLike.re_to_real, Set.mem_setOf_eq]

Premises used: RCLike.re_to_real, Set.mem_setOf_eq, Metric.mem_ball, norm_eq_sqrt_re_inner, dist_zero_right
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x v : F
⊢ 1 = √1

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x v : F
rw : √⟪v, v⟫ < √1
| √⟪v, v⟫ < 1

Tactic:
rw [show (1 : ℝ) = √1 by simp]
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x v : F
h : √⟪v, v⟫ < √1 ↔ ⟪v, v⟫ < 1
⊢ √⟪v, v⟫ < 1 ↔ ⟪v, v⟫ < 1

Tactic:
conv_lhs => rw [show (1 : ℝ) = √1 by simp]
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x v : F
h : 0 ≤ ⟪v, v⟫
⊢ √⟪v, v⟫ < √1 ↔ ⟪v, v⟫ < 1

Tactic:
rw [Real.sqrt_lt_sqrt_iff]

Premises used: Real.sqrt_lt_sqrt_iff
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x v : F
⊢ 0 ≤ ⟪v, v⟫

Tactic:
real_inner_self_nonneg

Premises used: real_inner_self_nonneg
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x v : F
⊢ 0 ≤ ⟪v, v⟫

Tactic:
exact real_inner_self_nonneg

Premises used: real_inner_self_nonneg
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x : F
⊢ Eq.{u_4 + 1} (α := Set F) (Metric.ball 0 1) {v : F | ⟪v, v⟫ < 1}

Tactic:
have : Metric.ball (0 : F) 1 = {v : F | ⟪v, v⟫ < 1} := by
      ext v
      simp only [Metric.mem_ball, dist_zero_right, norm_eq_sqrt_re_inner (𝕜 := ℝ),
        RCLike.re_to_real, Set.mem_setOf_eq]
      conv_lhs => rw [show (1 : ℝ) = √1 by simp]
      rw [Real.sqrt_lt_sqrt_iff]
      exact real_inner_self_nonneg
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x : F
this : Eq.{u_4 + 1} (α := Set F) (Metric.ball 0 1) {v : F | ⟪v, v⟫ < 1}
rw : IsVonNBounded.{0, u_4} ℝ (E := F) (Metric.ball 0 1)
⊢ IsVonNBounded.{0, u_4} ℝ (E := F) {v : F | ⟪v, v⟫ < 1}

Tactic:
rw [← this]
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x : F
this : Eq.{u_4 + 1} (α := Set F) (Metric.ball 0 1) {v : F | ⟪v, v⟫ < 1}
⊢ IsVonNBounded.{0, u_4} ℝ (E := F) (Metric.ball 0 1)

Tactic:
NormedSpace.isVonNBounded_ball ℝ F 1

Premises used: Real, NormedSpace.isVonNBounded_ball, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x : F
this : Eq.{u_4 + 1} (α := Set F) (Metric.ball 0 1) {v : F | ⟪v, v⟫ < 1}
⊢ IsVonNBounded.{0, u_4} ℝ (E := F) (Metric.ball 0 1)

Tactic:
exact NormedSpace.isVonNBounded_ball ℝ F 1

Premises used: Real, NormedSpace.isVonNBounded_ball, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x : F
rw :
  ContMDiffAt 𝓘(ℝ, F) (E' := F →L[ℝ] F →L[ℝ] ℝ) 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ) (M' := F →L[ℝ] F →L[ℝ] ℝ) ω
    (fun (x_1 : F) ↦
      ((↑(trivializationAt (F →L[ℝ] F →L[ℝ] ℝ)
                (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) x) :
            (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) →
              F × (F →L[ℝ] F →L[ℝ] ℝ))
          ⟨x_1, innerSL ℝ⟩).2)
    x
⊢ ContMDiffAt 𝓘(ℝ, F) (E' := F × (F →L[ℝ] F →L[ℝ] ℝ)) (ModelWithCorners.prod 𝓘(ℝ, F) 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
    TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) fun (b : F) ↦ TangentSpace 𝓘(ℝ, F) b →L[ℝ] TangentSpace 𝓘(ℝ, F) b →L[ℝ] ℝ) ω
    (fun (b : F) ↦ ⟨b, innerSL ℝ⟩) x

Tactic:
rw [contMDiffAt_section]

Premises used: Bundle.contMDiffAt_section
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x : F
⊢ ContMDiffAt 𝓘(ℝ, F) (E' := F →L[ℝ] F →L[ℝ] ℝ) 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ) (M' := F →L⋆[ℝ] F →L[ℝ] ℝ) ω
    (fun (x : F) ↦ innerSL ℝ) x

Tactic:
contMDiffAt_const (c := innerSL ℝ)

Premises used: contMDiffAt_const
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x : F
h :
  ∀ (x_1 : F),
    Eq (α := F →L[ℝ] F →L[ℝ] ℝ)
      ((↑(trivializationAt (F →L[ℝ] F →L[ℝ] ℝ)
                (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) x) :
            (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) →
              F × (F →L[ℝ] F →L[ℝ] ℝ))
          ⟨x_1, innerSL ℝ⟩).2
      (innerSL ℝ)
⊢ ContMDiffAt 𝓘(ℝ, F) (E' := F →L[ℝ] F →L[ℝ] ℝ) 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ) (M' := F →L[ℝ] F →L[ℝ] ℝ) ω
    (fun (x_1 : F) ↦
      ((↑(trivializationAt (F →L[ℝ] F →L[ℝ] ℝ)
                (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) x) :
            (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) →
              F × (F →L[ℝ] F →L[ℝ] ℝ))
          ⟨x_1, innerSL ℝ⟩).2)
    x

Tactic:
convert! contMDiffAt_const (c := innerSL ℝ)

Premises used: contMDiffAt_const
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x x_1 : F
h :
  ∀ (v w : F),
    Eq (α := ℝ)
      ((((((↑(trivializationAt (F →L[ℝ] F →L[ℝ] ℝ)
                            (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) x) :
                        (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) fun (x : F) ↦
                            TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) →
                          F × (F →L[ℝ] F →L[ℝ] ℝ))
                      ⟨x_1, innerSL ℝ⟩).2 :
                  (a : F) → F →L[ℝ] ℝ)
                v :
              F →L[ℝ] ℝ) :
            (a : F) → ℝ)
          w :
        ℝ)
      ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) v : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ Eq (α := F →L[ℝ] F →L[ℝ] ℝ)
    ((↑(trivializationAt (F →L[ℝ] F →L[ℝ] ℝ) (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ)
              x) :
          (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) →
            F × (F →L[ℝ] F →L[ℝ] ℝ))
        ⟨x_1, innerSL ℝ⟩).2
    (innerSL ℝ)

Tactic:
ext v w