awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
hp :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
              ContDiff ℝ ∞ f →
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X))
                  {p : EuclideanSpace ℝ (Fin m) → X |
                    ∀ (d : DiffeologicalSpace X),
                      g ⊆ d.toPlots → Sigma.mk (β := fun (n : ℕ) ↦ EuclideanSpace ℝ (Fin n) → X) m p ∈ d.toPlots}
                  (p ∘ f)
d : DiffeologicalSpace X
hd : g ⊆ d.toPlots
x : EuclideanSpace ℝ (Fin n)
u : Set (EuclideanSpace ℝ (Fin n))
hxu : IsOpen u
hu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
      ContDiff ℝ ∞ f →
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X))
          {p : EuclideanSpace ℝ (Fin m) → X |
            ∀ (d : DiffeologicalSpace X),
              g ⊆ d.toPlots → Sigma.mk (β := fun (n : ℕ) ↦ EuclideanSpace ℝ (Fin n) → X) m p ∈ d.toPlots}
          (p ∘ f)
⊢ ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
    IsOpen u ∧
      x ∈ u ∧
        ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
          (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
            ContDiff ℝ ∞ f → Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) (plots m) (p ∘ f)

Tactic:
⟨u, hxu, hu, fun {m f} hfu hf ↦ (hu' hfu hf) _ hd⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
hp :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
              ContDiff ℝ ∞ f →
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X))
                  {p : EuclideanSpace ℝ (Fin m) → X |
                    ∀ (d : DiffeologicalSpace X),
                      g ⊆ d.toPlots → Sigma.mk (β := fun (n : ℕ) ↦ EuclideanSpace ℝ (Fin n) → X) m p ∈ d.toPlots}
                  (p ∘ f)
d : DiffeologicalSpace X
hd : g ⊆ d.toPlots
x : EuclideanSpace ℝ (Fin n)
u : Set (EuclideanSpace ℝ (Fin n))
hxu : IsOpen u
hu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
      ContDiff ℝ ∞ f →
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X))
          {p : EuclideanSpace ℝ (Fin m) → X |
            ∀ (d : DiffeologicalSpace X),
              g ⊆ d.toPlots → Sigma.mk (β := fun (n : ℕ) ↦ EuclideanSpace ℝ (Fin n) → X) m p ∈ d.toPlots}
          (p ∘ f)
⊢ ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
    IsOpen u ∧
      x ∈ u ∧
        ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
          (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
            ContDiff ℝ ∞ f → Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) (plots m) (p ∘ f)

Tactic:
exact ⟨u, hxu, hu, fun {m f} hfu hf ↦ (hu' hfu hf) _ hd⟩
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
⊢ g ⊆ (generateFrom g).toPlots

Tactic:
fun _ hd _ h ↦ h hd

Premises used: Set.Mem, setOf, Diffeology.IsPlot, Set.Subset, DiffeologicalSpace.toPlots
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
hp : Sigma.mk (β := fun (n : ℕ) ↦ EuclideanSpace ℝ (Fin n) → X) n p ∈ g
⊢ IsPlot p

Tactic:
self_subset_toPlots_generateFrom g hp

Premises used: Set.Mem, setOf, Diffeology.IsPlot, DiffeologicalSpace.toPlots, DiffeologicalSpace.self_subset_toPlots_generateFrom
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d₁ d₂ : DiffeologicalSpace X
⊢ d₁ ≤ d₂ ↔ d₁.toPlots ⊆ d₂.toPlots

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d₁ d₂ : DiffeologicalSpace X
⊢ d₁ ≤ d₂ ↔ ∀ (n : ℕ), Subset.{u_1} (α := Set (EuclideanSpace ℝ (Fin n) → X)) (plots n) (plots n)

Tactic:
le_def.trans ⟨fun h n p h' ↦ (h h' : ⟨n, p⟩ ∈ d₂.toPlots), fun h _ hp ↦ h _ hp⟩

Premises used: DiffeologicalSpace.le_def, Sigma.fst, Iff.intro, Iff.trans
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d₁ d₂ : DiffeologicalSpace X
⊢ d₁ ≤ d₂ ↔ ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), IsPlot p → IsPlot p

Tactic:
le_iff

Premises used: Diffeology.IsPlot, Set.Subset, DiffeologicalSpace.le_iff
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
d : DiffeologicalSpace X
⊢ generateFrom g ≤ d ↔ g ⊆ d.toPlots

Tactic:
⟨fun h ↦ (self_subset_toPlots_generateFrom g).trans h, fun h _ hp ↦ hp _ h⟩

Premises used: HasSubset.Subset.trans, Iff.intro, DiffeologicalSpace.self_subset_toPlots_generateFrom
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
d : DiffeologicalSpace X
⊢ generateFrom g ≤ d ↔
    ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X),
      Sigma.mk (β := fun (n : ℕ) ↦ EuclideanSpace ℝ (Fin n) → X) n p ∈ g → IsPlot p

Tactic:
generateFrom_le_iff_subset_toPlots.trans ⟨fun h _ _ hp ↦ h hp, fun h _ hp ↦ h _ _ hp⟩

Premises used: DiffeologicalSpace.generateFrom_le_iff_subset_toPlots, Sigma.fst, Iff.intro, Iff.trans, Sigma.snd
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
hg : (generateFrom g).toPlots = g
⊢ DiffeologicalSpace.mkOfClosure g hg = generateFrom g

Tactic:
injective_toPlots hg.symm

Premises used: Eq.symm, DiffeologicalSpace.injective_toPlots
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_2
⊢ GaloisConnection.{u_2, u_2} (α := Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))) generateFrom toPlots

Tactic:
@generateFrom_le_iff_subset_toPlots X

Premises used: DiffeologicalSpace.generateFrom_le_iff_subset_toPlots, GaloisConnection
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
g₁ g₂ : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
h : g₁ ⊆ g₂
⊢ generateFrom g₁ ≤ generateFrom g₂

Tactic:
(gc_generateFrom _).monotone_l h

Premises used: DiffeologicalSpace.gc_generateFrom, GaloisConnection.monotone_l
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d : DiffeologicalSpace X
⊢ generateFrom d.toPlots = d

Tactic:
(giGenerateFrom X).l_u_eq d

Premises used: DiffeologicalSpace.giGenerateFrom, GaloisInsertion.l_u_eq
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
⊢ Function.LeftInverse.{u_1 + 1, u_1 + 1} (α := DiffeologicalSpace X) generateFrom toPlots

Tactic:
(giGenerateFrom X).leftInverse_l_u

Premises used: DiffeologicalSpace.giGenerateFrom, GaloisInsertion.leftInverse_l_u
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))) generateFrom

Tactic:
(giGenerateFrom X).l_surjective

Premises used: DiffeologicalSpace.giGenerateFrom, GaloisInsertion.l_surjective
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
g₁ g₂ : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
⊢ generateFrom (g₁ ∪ g₂) = generateFrom g₁ ⊔ generateFrom g₂

Tactic:
(gc_generateFrom X).l_sup

Premises used: DiffeologicalSpace.gc_generateFrom, GaloisConnection.l_sup
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
ι : Type u_2
g : ι → Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
⊢ Eq.{u_1 + 1} (α := DiffeologicalSpace X) (generateFrom (⋃ (i : ι), g i)) (⨆ (i : ι), generateFrom (g i))

Tactic:
(gc_generateFrom X).l_iSup

Premises used: GaloisConnection.l_iSup, DiffeologicalSpace.gc_generateFrom, Set.iUnion
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
G : Set (Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X)))
⊢ generateFrom (⋃₀ G) = ⨆ s ∈ G, generateFrom s

Tactic:
(gc_generateFrom X).l_sSup

Premises used: Set.sUnion, GaloisConnection.l_sSup, DiffeologicalSpace.gc_generateFrom
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d₁ d₂ : DiffeologicalSpace X
⊢ (d₁ ⊓ d₂).toPlots = d₁.toPlots ∩ d₂.toPlots

Tactic:
rfl

Premises used: Set.Mem, setOf, Diffeology.IsPlot, Set.inter, DiffeologicalSpace.toPlots, rfl
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
ι : Type u_2
D : ι → DiffeologicalSpace X
⊢ Eq.{u_1 + 1} (α := Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))) (toPlots (⨅ (i : ι), D i))
    (⋂ (i : ι), (D i).toPlots)

Tactic:
(gc_generateFrom X).u_iInf

Premises used: Set.iInter, GaloisConnection.u_iInf, DiffeologicalSpace.gc_generateFrom
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
D : Set (DiffeologicalSpace X)
⊢ (sInf D).toPlots = ⋂ d ∈ D, d.toPlots

Tactic:
(gc_generateFrom X).u_sInf

Premises used: Set.iInter, DiffeologicalSpace.gc_generateFrom, GaloisConnection.u_sInf
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d₁ d₂ : DiffeologicalSpace X
⊢ generateFrom (d₁.toPlots ∪ d₂.toPlots) = d₁ ⊔ d₂

Tactic:
(giGenerateFrom X).l_sup_u _ _

Premises used: GaloisInsertion.l_sup_u, DiffeologicalSpace.giGenerateFrom
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
ι : Type u_2
D : ι → DiffeologicalSpace X
⊢ Eq.{u_1 + 1} (α := DiffeologicalSpace X) (generateFrom (⋃ (i : ι), (D i).toPlots)) (⨆ (i : ι), D i)

Tactic:
(giGenerateFrom X).l_iSup_u _

Premises used: DiffeologicalSpace.giGenerateFrom, GaloisInsertion.l_iSup_u, Set.iUnion
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d₁ d₂ : DiffeologicalSpace X
⊢ generateFrom (d₁.toPlots ∩ d₂.toPlots) = d₁ ⊓ d₂

Tactic:
(giGenerateFrom X).l_inf_u _ _

Premises used: DiffeologicalSpace.giGenerateFrom, GaloisInsertion.l_inf_u
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
ι : Type u_2
D : ι → DiffeologicalSpace X
⊢ Eq.{u_1 + 1} (α := DiffeologicalSpace X) (generateFrom (⋂ (i : ι), (D i).toPlots)) (⨅ (i : ι), D i)

Tactic:
(giGenerateFrom X).l_iInf_u _

Premises used: Set.iInter, DiffeologicalSpace.giGenerateFrom, GaloisInsertion.l_iInf_u
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
ι : Type u_2
G : ι → Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
hG : ∀ (i : ι), (generateFrom (G i)).toPlots = G i
⊢ Eq.{u_1 + 1} (α := DiffeologicalSpace X) (generateFrom (⋂ (i : ι), G i)) (⨅ (i : ι), generateFrom (G i))

Tactic:
(giGenerateFrom X).l_iInf_of_u_l_eq_self G hG

Premises used: Set.iInter, DiffeologicalSpace.giGenerateFrom, GaloisInsertion.l_iInf_of_u_l_eq_self
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d₁ d₂ : DiffeologicalSpace X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
⊢ IsPlot p ↔ IsPlot p ∧ IsPlot p

Tactic:
Set.ext_iff.1 (toPlots_inf d₁ d₂) ⟨n, p⟩

Premises used: Set.Mem, setOf, Diffeology.IsPlot, Set.inter, Iff.mp, DiffeologicalSpace.toPlots, Set.ext_iff, DiffeologicalSpace.toPlots_inf, Sigma.mk
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
ι : Type u_2
D : ι → DiffeologicalSpace X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
⊢ IsPlot p ↔ ∀ (i : ι), IsPlot p

Tactic:
(Set.ext_iff.1 (toPlots_iInf (D := D)) ⟨n, p⟩).trans Set.mem_iInter

Premises used: Set.Mem, setOf, Diffeology.IsPlot, DiffeologicalSpace.toPlots_iInf, Set.mem_iInter, Iff.mp, Iff.trans, DiffeologicalSpace.toPlots, Set.ext_iff, Sigma.mk
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
D : Set (DiffeologicalSpace X)
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
⊢ IsPlot p ↔ ∀ d ∈ D, IsPlot p

Tactic:
(Set.ext_iff.1 (toPlots_sInf (D := D)) ⟨n, p⟩).trans Set.mem_iInter₂

Premises used: Set.Mem, DiffeologicalSpace.toPlots_sInf, setOf, Set.mem_iInter₂, Diffeology.IsPlot, Iff.mp, Iff.trans, DiffeologicalSpace.toPlots, Set.ext_iff, Sigma.mk
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
⊢ Nonempty.{u_2 + 1} ↥s₁

Tactic:
have : Nonempty s₁ := ⟨p', hp'₁⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this : Nonempty.{u_2 + 1} ↥s₁
⊢ Nonempty.{u_2 + 1} ↥s₂

Tactic:
have : Nonempty s₂ := ⟨p', hp'₂⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
refine_1 :
  ∀
    (h :
      dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)),
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
refine_2 :
  ∀
    (h :
      ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
        ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)),
    dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h :
  dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
refine_1 :
  ∀ (h : dist p p = dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)),
    ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
rw [orthogonalProjection_eq_self_iff.2 h'] at h ⊢

Premises used: Iff.mpr, EuclideanGeometry.orthogonalProjection_eq_self_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : dist p p = dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ p ∈ s₂

Tactic:
rw [dist_self, zero_eq_dist, eq_comm, orthogonalProjection_eq_self_iff] at h

Premises used: zero_eq_dist, eq_comm, dist_self, EuclideanGeometry.orthogonalProjection_eq_self_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : p ∈ s₂
refine_1 refine_1₁ : ∠ p p' p = ∠ p p' p
⊢ ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
rw [orthogonalProjection_eq_self_iff.2 h]

Premises used: Iff.mpr, EuclideanGeometry.orthogonalProjection_eq_self_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h :
  ∠ p p' (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
refine_2 :
  ∀ (h : ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)),
    dist p p = dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ dist p (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
rw [orthogonalProjection_eq_self_iff.2 h'] at h ⊢

Premises used: Iff.mpr, EuclideanGeometry.orthogonalProjection_eq_self_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
refine_2 : p ∈ s₂
⊢ dist p p = dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
rw [dist_self, zero_eq_dist, eq_comm, orthogonalProjection_eq_self_iff]

Premises used: zero_eq_dist, eq_comm, dist_self, EuclideanGeometry.orthogonalProjection_eq_self_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
refine_2 :
  ∀ (hp'₁ : p ∈ s₁) (hp'₂ : p ∈ s₂) (h : ∠ p p p = ∠ p p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)), p ∈ s₂
refine_2₁ : ∀ (hpp' : p ≠ p'), p ∈ s₂
⊢ p ∈ s₂

Tactic:
obtain rfl | hpp' := eq_or_ne p p'

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
hp'₁ : p ∈ s₁
hp'₂ : p ∈ s₂
h : ∠ p p p = ∠ p p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ p ∈ s₂

Tactic:
hp'₂

Premises used: Set.Mem
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
hp'₁ : p ∈ s₁
hp'₂ : p ∈ s₂
h : ∠ p p p = ∠ p p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ p ∈ s₂

Tactic:
exact hp'₂
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
hpp' : p ≠ p'
refine_2 : ∀ (hn : p ∉ s₂), False
⊢ p ∈ s₂

Tactic:
by_contra hn
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : ∠ p p' p = ∠ p p' (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
hpp' : p ≠ p'
hn : p ∉ s₂
refine_2 :
  ∀ (h : dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) = 0 ∨ dist p p' = 0) (hpp' : p ≠ p') (hn : p ∉ s₂),
    False
refine_2₁ :
  ∀ (h : 0 = ∠ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) p' p) (hpp' : p ≠ p') (hn : p ∉ s₂),
    p ≠ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ∨ p' ≠ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ False

Tactic:
rw [angle_self_of_ne hpp', angle_comm,
        angle_eq_arcsin_of_angle_eq_pi_div_two (angle_self_orthogonalProjection p hp'₂),
        Real.zero_eq_arcsin_iff, div_eq_zero_iff] at h

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_self_of_ne, Real.zero_eq_arcsin_iff, EuclideanGeometry.angle_eq_arcsin_of_angle_eq_pi_div_two, EuclideanGeometry.angle_self_orthogonalProjection, div_eq_zero_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
h : dist p (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) = 0 ∨ dist p p' = 0
hpp' : p ≠ p'
hn : p ∉ s₂
⊢ p = (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)

Tactic:
simp only [dist_eq_zero, hpp', or_false] at h

Premises used: dist_eq_zero, or_false
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst_4 : s₁.direction.HasOrthogonalProjection
inst_5 : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this_1 : Nonempty.{u_2 + 1} ↥s₁
this : Nonempty.{u_2 + 1} ↥s₂
hpp' : p ≠ p'
hn : p ∉ s₂
h : p = (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) = p

Tactic:
rw [eq_comm] at h

Premises used: eq_comm