awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
this :
  HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)
rw : HPow.hPow (β := ℕ) ‖x‖ 2 / HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖x‖ 2) 2 = (HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 / (HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℕ) ‖x‖ 2) = (HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
rw₂ rw₃ : (HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹ = (HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
⊢ (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖x‖ 2) 2)⁻¹ * HPow.hPow (β := ℕ) ‖x‖ 2 = (HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹

Tactic:
rw [← div_eq_inv_mul, sq (‖x‖ ^ 2), div_self_mul_self']

Premises used: Norm.norm, div_self_mul_self', sq, HPow.hPow, div_eq_inv_mul, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
this :
  HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)
⊢ (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖x‖ 2) 2)⁻¹ * HPow.hPow (β := ℕ) ‖x‖ 2 = (HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹

Tactic:
have : ((‖x‖ ^ 2) ^ 2)⁻¹ * (‖x‖ ^ 2) = (‖x‖ ^ 2)⁻¹ := by
      rw [← div_eq_inv_mul, sq (‖x‖ ^ 2), div_self_mul_self']
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
this_1 :
  HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)
this : (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖x‖ 2) 2)⁻¹ * HPow.hPow (β := ℕ) ‖x‖ 2 = (HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
⊢ EqOn (α := F) (β := F)
    (⇑(↑(HSMul.hSMul (β := F →L[ℝ] F)
                (HPow.hPow (β := ℕ) R 2 *
                  ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
                (ContinuousLinearMap.id ℝ F) +
              (HPow.hPow (β := ℕ) R 2 •
                    -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
                      HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                          ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c))
                          (ContinuousLinearMap.id ℝ F))).smulRight
                (_root_.id (c + x) - c)) :
          F →ₗ[ℝ] F) :
      (a : F) → F)
    (⇑(↑(HSMul.hSMul (β := F →L[ℝ] F) (HPow.hPow (β := ℕ) (R / dist ((fun (x : F) ↦ c + x) x) c) 2)
              (↑(↑(Submodule.reflection (ℝ ∙ ((fun (x : F) ↦ c + x) x - c))ᗮ) : F ≃L[ℝ] F) : F →L[ℝ] F)) :
          F →ₗ[ℝ] F) :
      (a : F) → F)
    {x}

Tactic:
simp [Submodule.reflection_orthogonalComplement_singleton_eq_neg,
      two_mul, this, div_eq_mul_inv, mul_add, add_smul, mul_pow]

Premises used: Submodule.reflection_orthogonalComplement_singleton_eq_neg, two_mul, div_eq_mul_inv, add_smul, mul_add, mul_pow
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
this :
  HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)
y : F
hy : y ∈ (↑(ℝ ∙ x)ᗮ : Set F)
⊢ Eq (α := F)
    ((HSMul.hSMul (β := F →L[ℝ] F)
              (HPow.hPow (β := ℕ) R 2 *
                ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
              (ContinuousLinearMap.id ℝ F) +
            (HPow.hPow (β := ℕ) R 2 •
                  -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
                    HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                        ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c))
                        (ContinuousLinearMap.id ℝ F))).smulRight
              (_root_.id (c + x) - c) :
          (a : F) → F)
        y :
      F)
    ((HSMul.hSMul (β := F →L[ℝ] F) (HPow.hPow (β := ℕ) (R / dist ((fun (x : F) ↦ c + x) x) c) 2)
            (↑(↑(Submodule.reflection (ℝ ∙ ((fun (x : F) ↦ c + x) x - c))ᗮ) : F ≃L[ℝ] F) : F →L[ℝ] F) :
          (a : F) → F)
        y :
      F)

Tactic:
simp [Submodule.mem_orthogonal_singleton_iff_inner_right.1 hy,
      Submodule.reflection_mem_subspace_eq_self hy, div_eq_mul_inv, mul_pow]

Premises used: Submodule.mem_orthogonal_singleton_iff_inner_right, div_eq_mul_inv, Iff.mp, Submodule.reflection_mem_subspace_eq_self, mul_pow
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
rw : HPow.hPow (β := ℕ) R 2 / dist x c = HPow.hPow (β := ℕ) R 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector c (inversion c R y)) (inversion c R x) ↔ dist x y = dist y c

Tactic:
rw [mem_perpBisector_iff_dist_eq, dist_inversion_inversion hx hy, dist_inversion_center]

Premises used: EuclideanGeometry.dist_inversion_inversion, AffineSubspace.mem_perpBisector_iff_dist_eq, EuclideanGeometry.dist_inversion_center
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
⊢ HPow.hPow (β := ℕ) R 2 / dist x c = HPow.hPow (β := ℕ) R 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c

Tactic:
simp [field, eq_comm, ↓hx, ↓hy]

Premises used: eq_comm
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
inl :
  ∀ (hy : y ≠ x),
    Membership.mem (γ := AffineSubspace ℝ P) (perpBisector x (inversion x R y)) (inversion x R x) ↔
      dist x y = dist y x ∧ x ≠ x
inr :
  ∀ (hx : x ≠ c),
    Membership.mem (γ := AffineSubspace ℝ P) (perpBisector c (inversion c R y)) (inversion c R x) ↔
      dist x y = dist y c ∧ x ≠ c
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector c (inversion c R y)) (inversion c R x) ↔
    dist x y = dist y c ∧ x ≠ c

Tactic:
rcases eq_or_ne x c with rfl | hx

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ x
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector x (inversion x R y)) (inversion x R x) ↔
    dist x y = dist y x ∧ x ≠ x

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
hx : x ≠ c
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector c (inversion c R y)) (inversion c R x) ↔
    dist x y = dist y c ∧ x ≠ c

Tactic:
simp [inversion_mem_perpBisector_inversion_iff hR hx hy, hx]

Premises used: EuclideanGeometry.inversion_mem_perpBisector_inversion_iff
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R ⁻¹' (↑(perpBisector c (inversion c R y)) : Set P) = sphere y (dist y c) \ {c}

Tactic:
Set.ext fun _ ↦ inversion_mem_perpBisector_inversion_iff' hR hy

Premises used: Set.ext, EuclideanGeometry.inversion_mem_perpBisector_inversion_iff'
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
hR₁ : R ≠ 0
rw : inversion c R y ≠ c
⊢ inversion c R ⁻¹' (↑(perpBisector c y) : Set P) = sphere (inversion c R y) (HPow.hPow (β := ℕ) R 2 / dist y c) \ {c}

Tactic:
rw [← dist_inversion_center, ← preimage_inversion_perpBisector_inversion hR,
    inversion_inversion]

Premises used: EuclideanGeometry.preimage_inversion_perpBisector_inversion, EuclideanGeometry.inversion_inversion, EuclideanGeometry.dist_inversion_center
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ R ≠ 0

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R y ≠ c

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
rw :
  inversion c R ⁻¹' (↑(perpBisector c y) : Set P) = sphere (inversion c R y) (HPow.hPow (β := ℕ) R 2 / dist y c) \ {c}
rw₁ rw₂ :
  sphere (inversion c R y) (HPow.hPow (β := ℕ) R 2 / dist y c) \ {c} =
    sphere (inversion c R y) (HPow.hPow (β := ℕ) R 2 / dist y c) \ {c}
⊢ inversion c R '' (↑(perpBisector c y) : Set P) = sphere (inversion c R y) (HPow.hPow (β := ℕ) R 2 / dist y c) \ {c}

Tactic:
rw [image_eq_preimage_of_inverse (inversion_involutive _ hR) (inversion_involutive _ hR),
    preimage_inversion_perpBisector hR hy]

Premises used: EuclideanGeometry.inversion_involutive, EuclideanGeometry.preimage_inversion_perpBisector, Set.image_eq_preimage_of_inverse
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
h : ∀ (x : P), x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c (↑(perpBisector c (inversion c R y)) : Set P)
⊢ inversion c R ⁻¹' sphere y (dist y c) = insert c (↑(perpBisector c (inversion c R y)) : Set P)

Tactic:
ext x
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
h :
  ∀ (hy : y ≠ x), x ∈ inversion x R ⁻¹' sphere y (dist y x) ↔ x ∈ insert x (↑(perpBisector x (inversion x R y)) : Set P)
h₁ :
  ∀ (hx : x ≠ c), x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c (↑(perpBisector c (inversion c R y)) : Set P)
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c (↑(perpBisector c (inversion c R y)) : Set P)

Tactic:
rcases eq_or_ne x c with rfl | hx

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
y : P
R : ℝ
hR : R ≠ 0
x : P
hy : y ≠ x
⊢ x ∈ inversion x R ⁻¹' sphere y (dist y x) ↔ x ∈ insert x (↑(perpBisector x (inversion x R y)) : Set P)

Tactic:
simp [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
h :
  Membership.mem (γ := AffineSubspace ℝ P) (perpBisector c (inversion c R y)) (inversion c R (inversion c R x)) ↔
    x ∈ insert c (↑(perpBisector c (inversion c R y)) : Set P)
h₁ : inversion c R x ≠ c
h₂ : y ≠ c
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c (↑(perpBisector c (inversion c R y)) : Set P)

Tactic:
rw [mem_preimage, mem_sphere, ← inversion_mem_perpBisector_inversion_iff hR]

Premises used: Metric.mem_sphere, EuclideanGeometry.inversion_mem_perpBisector_inversion_iff, Set.mem_preimage
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector c (inversion c R y)) (inversion c R (inversion c R x)) ↔
    x ∈ insert c (↑(perpBisector c (inversion c R y)) : Set P)

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
⊢ inversion c R x ≠ c

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
⊢ y ≠ c

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
rw : inversion c R ⁻¹' sphere y (dist y c) = insert c (↑(perpBisector c (inversion c R y)) : Set P)
rw₁ rw₂ :
  insert c (↑(perpBisector c (inversion c R y)) : Set P) = insert c (↑(perpBisector c (inversion c R y)) : Set P)
⊢ inversion c R '' sphere y (dist y c) = insert c (↑(perpBisector c (inversion c R y)) : Set P)

Tactic:
rw [image_eq_preimage_of_inverse (inversion_involutive _ hR) (inversion_involutive _ hR),
    preimage_inversion_sphere_dist_center hR hy]

Premises used: EuclideanGeometry.inversion_involutive, EuclideanGeometry.preimage_inversion_sphere_dist_center, Set.image_eq_preimage_of_inverse
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c : P
R : ℝ
p : AffineSubspace ℝ P
hp : c ∈ p
⊢ MapsTo (inversion c R) (↑p : Set P) (↑p : Set P)

Tactic:
fun _ ↦ AffineMap.lineMap_mem _ hp

Premises used: Set.Mem, Pow.pow, AffineMap.lineMap_mem, HDiv.hDiv, EuclideanGeometry.inversion, Set.MapsTo, Dist.dist, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
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
c : P
R : ℝ
p : AffineSubspace ℝ P
hR : R ≠ 0
hp : c ∈ p
⊢ inversion c R '' (↑p : Set P) = (↑p : Set P)

Tactic:
(mapsTo_inversion_affineSubspace_of_mem hp).image_subset.antisymm fun x hx ↦
    ⟨inversion c R x, mapsTo_inversion_affineSubspace_of_mem hp hx, inversion_inversion _ hR _⟩

Premises used: EuclideanGeometry.inversion_inversion, EuclideanGeometry.inversion, HasSubset.Subset.antisymm, And.intro, Exists.intro, Set.MapsTo.image_subset, EuclideanGeometry.mapsTo_inversion_affineSubspace_of_mem
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
n : ℕ
s : Simplex ℝ P n
⊢ s.mongePoint =
    HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) +ᵥ
      s.circumcenter

Tactic:
rfl

Premises used: Affine.Simplex.mongePoint, rfl
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
simp_rw :
  HDiv.hDiv (α := ℝ) (↑(m + 1) : ℝ) (↑(m - 1) : ℝ) •
        ((affineCombination ℝ univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) : (a : Fin (m + 1) → ℝ) → P)
            (centroidWeights ℝ univ) -ᵥ
          s.circumcenter) +ᵥ
      s.circumcenter =
    HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
        ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) (centroidWeights ℝ univ) -ᵥ s.circumcenter) +ᵥ
      s.circumcenter
⊢ (s.reindex e).mongePoint = s.mongePoint

Tactic:
simp_rw [mongePoint, circumcenter_reindex, centroid_def, reindex]

Premises used: Affine.Simplex.circumcenter_reindex, Affine.Simplex.reindex, Affine.Simplex.mongePoint, Finset.centroid_def
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ n = m

Tactic:
simpa using Fintype.card_eq.2 ⟨e⟩

Premises used: Iff.mpr, Fintype.card_eq, Nonempty.intro
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
obtain :
  ∀ (e : Fin (n + 1) ≃ Fin (n + 1)),
    HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
          ((affineCombination ℝ univ (s.points ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (n + 1))) :
                (a : Fin (n + 1) → ℝ) → P)
              (centroidWeights ℝ univ) -ᵥ
            s.circumcenter) +ᵥ
        s.circumcenter =
      HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
          ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) (centroidWeights ℝ univ) -ᵥ
            s.circumcenter) +ᵥ
        s.circumcenter
⊢ HDiv.hDiv (α := ℝ) (↑(m + 1) : ℝ) (↑(m - 1) : ℝ) •
        ((affineCombination ℝ univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) : (a : Fin (m + 1) → ℝ) → P)
            (centroidWeights ℝ univ) -ᵥ
          s.circumcenter) +ᵥ
      s.circumcenter =
    HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
        ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) (centroidWeights ℝ univ) -ᵥ s.circumcenter) +ᵥ
      s.circumcenter

Tactic:
obtain rfl : n = m := by simpa using Fintype.card_eq.2 ⟨e⟩

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (n + 1)
e_a :
  Eq.{u_2 + 1} (α := P)
    ((affineCombination ℝ univ (s.points ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (n + 1))) : (a : Fin (n + 1) → ℝ) → P)
        (centroidWeights ℝ univ) :
      P)
    ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) (centroidWeights ℝ univ) : P)
⊢ HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
        ((affineCombination ℝ univ (s.points ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (n + 1))) : (a : Fin (n + 1) → ℝ) → P)
            (centroidWeights ℝ univ) -ᵥ
          s.circumcenter) +ᵥ
      s.circumcenter =
    HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
        ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) (centroidWeights ℝ univ) -ᵥ s.circumcenter) +ᵥ
      s.circumcenter

Tactic:
congr 3
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (n + 1)
⊢ Eq.{u_2 + 1} (α := P)
    ((affineCombination ℝ (Finset.map e.toEmbedding univ) (s.points ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (n + 1))) :
          (a : Fin (n + 1) → ℝ) → P)
        (centroidWeights ℝ univ) :
      P)
    ((affineCombination ℝ univ
            (Function.comp (β := Fin (n + 1)) (s.points ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (n + 1)))
              (⇑e.toEmbedding : (a : Fin (n + 1)) → Fin (n + 1))) :
          (a : Fin (n + 1) → ℝ) → P)
        (Function.comp (β := Fin (n + 1)) (centroidWeights ℝ univ) (⇑e.toEmbedding : (a : Fin (n + 1)) → Fin (n + 1))) :
      P)

Tactic:
Finset.univ.affineCombination_map e.toEmbedding _ _

Premises used: Finset.univ, Finset.affineCombination_map, Equiv.toEmbedding
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (n + 1)
h : univ = Finset.map e.toEmbedding univ
h₁ :
  s.points =
    Function.comp (β := Fin (n + 1)) (s.points ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (n + 1)))
      (⇑e.toEmbedding : (a : Fin (n + 1)) → Fin (n + 1))
⊢ Eq.{u_2 + 1} (α := P)
    ((affineCombination ℝ univ (s.points ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (n + 1))) : (a : Fin (n + 1) → ℝ) → P)
        (centroidWeights ℝ univ) :
      P)
    ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) (centroidWeights ℝ univ) : P)

Tactic:
convert! Finset.univ.affineCombination_map e.toEmbedding _ _

Premises used: Finset.univ, Finset.affineCombination_map, Equiv.toEmbedding
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (n + 1)
⊢ univ = Finset.map e.toEmbedding univ

Tactic:
simp [Function.comp_assoc]

Premises used: Function.comp_assoc