awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Calculus (goal)
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
⊢ HasFDerivAt (fun (x : F) ↦ HPow.hPow (β := ℕ) (R / dist x c) 2 • (x -ᵥ c) +ᵥ c)
    (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)
have simp_rw : HasFDerivAt (fun (x : F) ↦ (HPow.hPow (β := ℕ) R 2 * (HPow.hPow (β := ℕ) ‖x - c‖ 2)⁻¹) • (x -ᵥ c) +ᵥ c)
  (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)
Tactic: simp_rw [dist_eq_norm, div_pow, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Calculus (hypothesis)
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
⊢ HasFDerivAt (fun (x : F) ↦ (HPow.hPow (β := ℕ) R 2 * (HPow.hPow (β := ℕ) ‖x - c‖ 2)⁻¹) • (x -ᵥ c) +ᵥ c)
    (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)
have A : HasFDerivAt (fun (x : F) ↦ _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)
Tactic: have A := (hasFDerivAt_id (𝕜 := ℝ) (c + x)).sub_const c
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Calculus (hypothesis)
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
A : HasFDerivAt (fun (x : F) ↦ _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)
⊢ HasFDerivAt (fun (x : F) ↦ (HPow.hPow (β := ℕ) R 2 * (HPow.hPow (β := ℕ) ‖x - c‖ 2)⁻¹) • (x -ᵥ c) +ᵥ c)
    (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)
have B : HasFDerivAt
  (fun (y : F) ↦
    HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) y)
  (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)))
  (c + x)
Tactic: have B := ((hasDerivAt_inv <| by simpa using hx).comp_hasFDerivAt _ A.norm_sq).const_mul
      (R ^ 2)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Calculus (hypothesis)
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
⊢ HasFDerivAt (inversion c R)
    (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))
    ((fun (x : F) ↦ c + x) x)
have 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)
Tactic: have : HasFDerivAt (inversion c R) (?_ : F →L[ℝ] F) (c + x) := by
    simp +unfoldPartialApp only [inversion]
    simp_rw [dist_eq_norm, div_pow, div_eq_mul_inv]
    have A := (hasFDerivAt_id (𝕜 := ℝ) (c + x)).sub_const c
    have B := ((hasDerivAt_inv <| by simpa using hx).comp_hasFDerivAt _ A.norm_sq).const_mul
      (R ^ 2)
    exact (B.smul A).add_const c
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Calculus (goal)
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)
⊢ HasFDerivAt (inversion c R)
    (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))
    ((fun (x : F) ↦ c + x) x)
have refine_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: refine this.congr_fderiv (LinearMap.ext_on_codisjoint
    (Submodule.isCompl_orthogonal_of_hasOrthogonalProjection (K := ℝ ∙ x)).codisjoint
    (LinearMap.eqOn_span' ?_) fun y hy ↦ ?_)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Calculus (goal)
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)⁻¹
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 / HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖x‖ 2) 2 = (HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
Tactic: rw [← div_eq_inv_mul, sq (‖x‖ ^ 2), div_self_mul_self']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Calculus (goal)
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)⁻¹
⊢ (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖x‖ 2) 2)⁻¹ * HPow.hPow (β := ℕ) ‖x‖ 2 = (HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
have rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 / (HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℕ) ‖x‖ 2) = (HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
Tactic: rw [← div_eq_inv_mul, sq (‖x‖ ^ 2), div_self_mul_self']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Calculus (goal)
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)⁻¹
⊢ (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖x‖ 2) 2)⁻¹ * HPow.hPow (β := ℕ) ‖x‖ 2 = (HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
have rw₂ : (HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹ = (HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
Tactic: rw [← div_eq_inv_mul, sq (‖x‖ ^ 2), div_self_mul_self']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Calculus (hypothesis)
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)
⊢ 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}
have this₁ : (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']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane (goal)
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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector c (inversion c R y)) (inversion c R x) ↔ dist x y = dist y c
have 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
Tactic: rw [mem_perpBisector_iff_dist_eq, dist_inversion_inversion hx hy, dist_inversion_center]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane (goal)
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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector c (inversion c R y)) (inversion c R x) ↔
    dist x y = dist y c ∧ x ≠ c
have 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
Tactic: rcases eq_or_ne x c with rfl | hx
Cleared hypotheses: c, hy
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane (goal)
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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector c (inversion c R y)) (inversion c R x) ↔
    dist x y = dist y c ∧ x ≠ c
have 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
Tactic: rcases eq_or_ne x c with rfl | hx
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane (goal)
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
⊢ inversion c R ⁻¹' (↑(perpBisector c y) : Set P) = sphere (inversion c R y) (HPow.hPow (β := ℕ) R 2 / dist y c) \ {c}
have rw : inversion c R y ≠ c
Tactic: rw [← dist_inversion_center, ← preimage_inversion_perpBisector_inversion hR,
    inversion_inversion]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane (goal)
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 y) : Set P) = sphere (inversion c R y) (HPow.hPow (β := ℕ) R 2 / dist y c) \ {c}
have rw : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane (goal)
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}
⊢ inversion c R '' (↑(perpBisector c y) : Set P) = sphere (inversion c R y) (HPow.hPow (β := ℕ) R 2 / dist y c) \ {c}
have 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}
Tactic: rw [image_eq_preimage_of_inverse (inversion_involutive _ hR) (inversion_involutive _ hR),
    preimage_inversion_perpBisector hR hy]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane (goal)
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 ⁻¹' sphere y (dist y c) = insert c (↑(perpBisector c (inversion c R y)) : Set P)
have h : ∀ (x : P), x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c (↑(perpBisector c (inversion c R y)) : Set P)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane (goal)
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
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c (↑(perpBisector c (inversion c R y)) : Set P)
have h : ∀ (hy : y ≠ x), x ∈ inversion x R ⁻¹' sphere y (dist y x) ↔ x ∈ insert x (↑(perpBisector x (inversion x R y)) : Set P)
Tactic: rcases eq_or_ne x c with rfl | hx
Cleared hypotheses: c, hy
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane (goal)
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)
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c (↑(perpBisector c (inversion c R y)) : Set P)
have h₁ : ∀ (hx : x ≠ c), 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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane (goal)
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
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c (↑(perpBisector c (inversion c R y)) : Set P)
have 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)
Tactic: rw [mem_preimage, mem_sphere, ← inversion_mem_perpBisector_inversion_iff hR]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane (goal)
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)
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c (↑(perpBisector c (inversion c R y)) : Set P)
have h₁ : inversion c R x ≠ c
Tactic: rw [mem_preimage, mem_sphere, ← inversion_mem_perpBisector_inversion_iff hR]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane (goal)
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 '' sphere y (dist y c) = insert c (↑(perpBisector c (inversion c R y)) : Set P)
have rw : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane (goal)
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)
⊢ inversion c R '' sphere y (dist y c) = insert c (↑(perpBisector c (inversion c R y)) : Set P)
have rw₁ : insert c (↑(perpBisector c (inversion c R y)) : Set P) = 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
⊢ (s.reindex e).mongePoint = s.mongePoint
have 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
Tactic: simp_rw [mongePoint, circumcenter_reindex, centroid_def, reindex]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
⊢ 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
have 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
Tactic: obtain rfl : n = m := by simpa using Fintype.card_eq.2 ⟨e⟩
Cleared hypotheses: m, e