awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
h₂₃₁ : π / 2 ≤ 0
h₂₃ : ¬p₂ = p₃
linarith : π / 3 ≤ π / 2 → 3 / 3 = 1
linarith₁ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₂ : π / 3 ≤ π / 2 → 2 / 2 = 1
linarith₃ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₄ : π / 3 ≤ π / 2 → GT.gt (α := ℝ) 6 0
linarith₅ : π / 3 ≤ π / 2 → 2 / 2 = 1
linarith₆ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : π / 3 ≤ π / 2 → GT.gt (α := ℝ) 2 0
linarith₈ : π / 3 ≤ π / 2 → 1 * π - HMul.hMul (α := ℝ) 2 0 + (0 - π) = 0
⊢ π / 2 < π / 3

Tactic:
linarith [Real.pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Geometry.Euclidean.Triangle
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₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
neg : ∀ (hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁), ∠ p₁ p₂ p₃ < π / 3
neg₁ : ∀ (hne : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂), ∠ p₁ p₂ p₃ < π / 3
neg₂ : ∀ (hne : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂), ∠ p₁ p₂ p₃ < π / 3
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
rcases hne with hne | hne | hne
-- Module: Mathlib.Geometry.Euclidean.Triangle
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₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
neg : ∀ (hne : ∠ p₁ p₂ p₃ < ∠ p₂ p₃ p₁), ∠ p₁ p₂ p₃ < π / 3
neg₁ : ∀ (hne : ∠ p₂ p₃ p₁ < ∠ p₁ p₂ p₃), ∠ p₁ p₂ p₃ < π / 3
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
rcases hne.lt_or_gt with hne | hne

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Geometry.Euclidean.Triangle
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₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
neg : ∀ (hne : ∠ p₁ p₂ p₃ < ∠ p₃ p₁ p₂), ∠ p₁ p₂ p₃ < π / 3
neg₁ : ∀ (hne : ∠ p₃ p₁ p₂ < ∠ p₁ p₂ p₃), ∠ p₁ p₂ p₃ < π / 3
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
rcases hne.lt_or_gt with hne | hne

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Geometry.Euclidean.Triangle
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₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
neg : ∀ (hne : ∠ p₂ p₃ p₁ < ∠ p₃ p₁ p₂), ∠ p₁ p₂ p₃ < π / 3
neg₁ : ∀ (hne : ∠ p₃ p₁ p₂ < ∠ p₂ p₃ p₁), ∠ p₁ p₂ p₃ < π / 3
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
rcases hne.lt_or_gt with hne | hne

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Geometry.Euclidean.Triangle
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₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₁ p₂ p₃ < ∠ p₂ p₃ p₁
linarith : π / 3 ≤ ∠ p₁ p₂ p₃ → 3 / 3 = 1
linarith₁ : π / 3 ≤ ∠ p₁ p₂ p₃ → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 ≤ ∠ p₁ p₂ p₃ → GT.gt (α := ℝ) 3 0
linarith₃ :
  π / 3 ≤ ∠ p₁ p₂ p₃ →
    ∠ p₁ p₂ p₃ - ∠ p₃ p₁ p₂ + (∠ p₁ p₂ p₃ - ∠ p₂ p₃ p₁) + (1 * π - 3 * ∠ p₁ p₂ p₃) +
        (∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ - π) =
      0
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Triangle
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₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₂ p₃ p₁ < ∠ p₁ p₂ p₃
linarith : π / 3 ≤ ∠ p₁ p₂ p₃ → 3 / 3 = 1
linarith₁ : π / 3 ≤ ∠ p₁ p₂ p₃ → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 ≤ ∠ p₁ p₂ p₃ → GT.gt (α := ℝ) 3 0
linarith₃ : π / 3 ≤ ∠ p₁ p₂ p₃ → ∠ p₁ p₂ p₃ - ∠ p₂ p₃ p₁ + (∠ p₂ p₃ p₁ - ∠ p₁ p₂ p₃) = 0
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Triangle
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₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ < ∠ p₃ p₁ p₂
linarith : π / 3 ≤ ∠ p₁ p₂ p₃ → 3 / 3 = 1
linarith₁ : π / 3 ≤ ∠ p₁ p₂ p₃ → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 ≤ ∠ p₁ p₂ p₃ → GT.gt (α := ℝ) 3 0
linarith₃ :
  π / 3 ≤ ∠ p₁ p₂ p₃ →
    ∠ p₁ p₂ p₃ - ∠ p₂ p₃ p₁ + (∠ p₁ p₂ p₃ - ∠ p₃ p₁ p₂) + (1 * π - 3 * ∠ p₁ p₂ p₃) +
        (∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ - π) =
      0
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Triangle
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₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₁ p₂ p₃
linarith : π / 3 ≤ ∠ p₁ p₂ p₃ → 3 / 3 = 1
linarith₁ : π / 3 ≤ ∠ p₁ p₂ p₃ → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 ≤ ∠ p₁ p₂ p₃ → GT.gt (α := ℝ) 3 0
linarith₃ : π / 3 ≤ ∠ p₁ p₂ p₃ → ∠ p₁ p₂ p₃ - ∠ p₃ p₁ p₂ + (∠ p₃ p₁ p₂ - ∠ p₁ p₂ p₃) = 0
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Triangle
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₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₂ p₃ p₁ < ∠ p₃ p₁ p₂
linarith : π / 3 ≤ ∠ p₁ p₂ p₃ → 3 / 3 = 1
linarith₁ : π / 3 ≤ ∠ p₁ p₂ p₃ → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 ≤ ∠ p₁ p₂ p₃ → GT.gt (α := ℝ) 3 0
linarith₃ :
  π / 3 ≤ ∠ p₁ p₂ p₃ →
    2 * (∠ p₁ p₂ p₃ - ∠ p₂ p₃ p₁) + (∠ p₂ p₃ p₁ - ∠ p₃ p₁ p₂) + (1 * π - 3 * ∠ p₁ p₂ p₃) +
        (∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ - π) =
      0
linarith₄ : π / 3 ≤ ∠ p₁ p₂ p₃ → GT.gt (α := ℝ) 2 0
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Triangle
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₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₂ p₃ p₁
linarith : π / 3 ≤ ∠ p₁ p₂ p₃ → 3 / 3 = 1
linarith₁ : π / 3 ≤ ∠ p₁ p₂ p₃ → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 ≤ ∠ p₁ p₂ p₃ → GT.gt (α := ℝ) 3 0
linarith₃ :
  π / 3 ≤ ∠ p₁ p₂ p₃ →
    2 * (∠ p₁ p₂ p₃ - ∠ p₃ p₁ p₂) + (∠ p₃ p₁ p₂ - ∠ p₂ p₃ p₁) + (1 * π - 3 * ∠ p₁ p₂ p₃) +
        (∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ - π) =
      0
linarith₄ : π / 3 ≤ ∠ p₁ p₂ p₃ → GT.gt (α := ℝ) 2 0
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
d : ℕ
⊢ IsAddHaarMeasure (G := EuclideanSpace ℝ (Fin d)) μH[(↑d : ℝ)]

Tactic:
simpa using MeasureTheory.isAddHaarMeasure_hausdorffMeasure (E := EuclideanSpace ℝ (Fin d))

Premises used: MeasureTheory.isAddHaarMeasure_hausdorffMeasure
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℕ
⊢ μHE[d] =
    HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)]) μH[(↑d : ℝ)]

Tactic:
rfl
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
⊢ Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
    (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))

Tactic:
simp [parallelepiped]

Premises used: parallelepiped
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
⊢ Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
    (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))

Tactic:
have heq : ({0} : Set (EuclideanSpace ℝ (Fin 0))) = parallelepiped basis := by
    simp [parallelepiped]
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq :
  Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
    (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))
⊢ volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)]

Tactic:
obtain h := isAddLeftInvariant_eq_smul (volume : Measure (EuclideanSpace ℝ (Fin 0))) μH[(0 : ℕ)]

Premises used: MeasureTheory.Measure.hausdorffMeasure, Nat.cast, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, MeasureTheory.Measure.isAddLeftInvariant_eq_smul
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq :
  Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
    (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))
h :
  volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)]
⊢ Eq (α := ENNReal)
    ((HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
            (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)] :
          (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal)
        {0} :
      ENNReal)
    ((volume : (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal) {0} : ENNReal)

Tactic:
obtain h := congr($h.symm {0})
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq :
  Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
    (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))
h_1 :
  volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)]
h :
  Eq (α := ENNReal)
    ((HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
            (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)] :
          (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal)
        {0} :
      ENNReal)
    ((volume : (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal) {0} : ENNReal)
rw : 1
| ((volume : (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal) {0} : ENNReal)

Tactic:
rw [heq, OrthonormalBasis.volume_parallelepiped]

Premises used: OrthonormalBasis.volume_parallelepiped
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq :
  Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
    (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))
h_1 :
  volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)]
h :
  Eq (α := ENNReal)
    ((HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
            (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)] :
          (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal)
        {0} :
      ENNReal)
    ((volume : (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal) {0} : ENNReal)
⊢ Eq (α := ENNReal)
    ((HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
            (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)] :
          (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal)
        {0} :
      ENNReal)
    (1 : ENNReal)

Tactic:
conv_rhs at h => rw [heq, OrthonormalBasis.volume_parallelepiped]

Premises used: OrthonormalBasis.volume_parallelepiped
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq :
  Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
    (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))
h_1 :
  volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)]
h :
  Eq (α := ENNReal)
    ((HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
            (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)] :
          (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal)
        {0} :
      ENNReal)
    (1 : ENNReal)
⊢ addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[0] = 1

Tactic:
simp_rw [CharP.cast_eq_zero, smul_apply, hausdorffMeasure_zero_singleton, ENNReal.smul_def,
    smul_eq_mul, mul_one, ENNReal.coe_eq_one] at h

Premises used: CharP.cast_eq_zero, ENNReal.coe_eq_one, MeasureTheory.Measure.hausdorffMeasure_zero_singleton, ENNReal.smul_def, MeasureTheory.Measure.smul_apply, smul_eq_mul, mul_one
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq :
  Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
    (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))
h_1 :
  volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)]
h : addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[0] = 1
⊢ Eq.{u_1 + 1} (α := Measure X) μHE[0] μH[0]

Tactic:
simp [euclideanHausdorffMeasure_def, h]

Premises used: MeasureTheory.Measure.euclideanHausdorffMeasure_def
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
d : ℕ
h0 : addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)] = 0
⊢ volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin d)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)]) μH[(↑d : ℝ)]

Tactic:
obtain h := isAddLeftInvariant_eq_smul (volume : Measure (EuclideanSpace ℝ (Fin d))) μH[d]

Premises used: MeasureTheory.Measure.hausdorffMeasure, Nat.cast, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.isAddLeftInvariant_eq_smul
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
d : ℕ
h0 : addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)] = 0
h :
  volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin d)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)]) μH[(↑d : ℝ)]
⊢ Eq (α := ENNReal)
    ((volume : (a : Set (EuclideanSpace ℝ (Fin d))) → ENNReal)
        (parallelepiped (ι := Fin (finrank ℝ (EuclideanSpace ℝ (Fin d))))
          (⇑(stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin d))) :
            (a : Fin (finrank ℝ (EuclideanSpace ℝ (Fin d)))) → EuclideanSpace ℝ (Fin d))) :
      ENNReal)
    ((HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin d)))
            (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)]) μH[(↑d : ℝ)] :
          (a : Set (EuclideanSpace ℝ (Fin d))) → ENNReal)
        (parallelepiped (ι := Fin (finrank ℝ (EuclideanSpace ℝ (Fin d))))
          (⇑(stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin d))) :
            (a : Fin (finrank ℝ (EuclideanSpace ℝ (Fin d)))) → EuclideanSpace ℝ (Fin d))) :
      ENNReal)

Tactic:
obtain h := congr($h (parallelepiped (stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin d)))))
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
d : ℕ
h0 : addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)] = 0
h_1 :
  volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin d)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)]) μH[(↑d : ℝ)]
h :
  Eq (α := ENNReal)
    ((volume : (a : Set (EuclideanSpace ℝ (Fin d))) → ENNReal)
        (parallelepiped (ι := Fin (finrank ℝ (EuclideanSpace ℝ (Fin d))))
          (⇑(stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin d))) :
            (a : Fin (finrank ℝ (EuclideanSpace ℝ (Fin d)))) → EuclideanSpace ℝ (Fin d))) :
      ENNReal)
    ((HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin d)))
            (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)]) μH[(↑d : ℝ)] :
          (a : Set (EuclideanSpace ℝ (Fin d))) → ENNReal)
        (parallelepiped (ι := Fin (finrank ℝ (EuclideanSpace ℝ (Fin d))))
          (⇑(stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin d))) :
            (a : Fin (finrank ℝ (EuclideanSpace ℝ (Fin d)))) → EuclideanSpace ℝ (Fin d))) :
      ENNReal)
⊢ False

Tactic:
simp [OrthonormalBasis.volume_parallelepiped, h0] at h

Premises used: OrthonormalBasis.volume_parallelepiped
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
Y : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : EMetricSpace Y
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_3
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
⊢ (↑(addHaarScalarFactor (G := EuclideanSpace ℝ (Fin (finrank ℝ E))) volume μH[(↑(finrank ℝ E) : ℝ)]) : ENNReal) ≠ 0

Tactic:
simpa using addHaarScalarFactor_volume_hausdorffMeasure_ne_zero (Module.finrank ℝ E)

Premises used: Real, MeasureTheory.Measure.addHaarScalarFactor_volume_hausdorffMeasure_ne_zero, Module.finrank
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
Y : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : EMetricSpace Y
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_3
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
⊢ (↑(addHaarScalarFactor (G := EuclideanSpace ℝ (Fin (finrank ℝ E))) volume μH[(↑(finrank ℝ E) : ℝ)]) : ENNReal) ≠ ⊤

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
Y : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : EMetricSpace Y
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_3
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
⊢ (HSMul.hSMul (β := Measure E)
      (↑(addHaarScalarFactor (G := EuclideanSpace ℝ (Fin (finrank ℝ E))) volume μH[(↑(finrank ℝ E) : ℝ)]) : ENNReal)
      μH[(↑(finrank ℝ E) : ℝ)]).IsAddHaarMeasure

Tactic:
exact IsAddHaarMeasure.smul _
    (by simpa using addHaarScalarFactor_volume_hausdorffMeasure_ne_zero (Module.finrank ℝ E))
    (by simp)

Premises used: MeasureTheory.Measure.IsAddHaarMeasure.smul
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℕ
h : d₁ < d₂
s : Set X
⊢ LT.lt (α := ℝ) (↑d₁ : ℝ) (↑d₂ : ℝ)

Tactic:
simpa using h
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℕ
h : d₁ < d₂
s : Set X
inl :
  ∀ (h : Eq (α := ENNReal) (((μH[(↑d₂ : ℝ)] : Measure X) : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)),
    Eq (α := ENNReal)
        ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₂)) volume μH[(↑d₂ : ℝ)])
                μH[(↑d₂ : ℝ)] :
              (a : Set X) → ENNReal)
            s :
          ENNReal)
        (0 : ENNReal) ∨
      Eq (α := ENNReal)
        ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)])
                μH[(↑d₁ : ℝ)] :
              (a : Set X) → ENNReal)
            s :
          ENNReal)
        (⊤ : ENNReal)
inr :
  ∀ (h : Eq (α := ENNReal) (((μH[(↑d₁ : ℝ)] : Measure X) : (a : Set X) → ENNReal) s : ENNReal) (⊤ : ENNReal)),
    Eq (α := ENNReal)
        ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₂)) volume μH[(↑d₂ : ℝ)])
                μH[(↑d₂ : ℝ)] :
              (a : Set X) → ENNReal)
            s :
          ENNReal)
        (0 : ENNReal) ∨
      Eq (α := ENNReal)
        ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)])
                μH[(↑d₁ : ℝ)] :
              (a : Set X) → ENNReal)
            s :
          ENNReal)
        (⊤ : ENNReal)
⊢ Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₂)) volume μH[(↑d₂ : ℝ)])
              μH[(↑d₂ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (0 : ENNReal) ∨
    Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)])
              μH[(↑d₁ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (⊤ : ENNReal)

Tactic:
obtain h | h := hausdorffMeasure_zero_or_top (show (d₁ : ℝ) < d₂ by simpa using h) s

Premises used: MeasureTheory.Measure.hausdorffMeasure_zero_or_top
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℕ
h_1 : d₁ < d₂
s : Set X
h : Eq (α := ENNReal) (((μH[(↑d₂ : ℝ)] : Measure X) : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₂)) volume μH[(↑d₂ : ℝ)])
              μH[(↑d₂ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (0 : ENNReal) ∨
    Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)])
              μH[(↑d₁ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (⊤ : ENNReal)

Tactic:
simp [h]