feat: add Pi.ofNat_apply (#5928)

leanprover-community · Jul 15, 2023 · d31d954 · d31d954
1 parent d5cc6ec
commit d31d954
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/Mathlib/Data/Nat/Cast/Basic.lean b/Mathlib/Data/Nat/Cast/Basic.lean
@@ -328,6 +328,9 @@ theorem coe_nat (n : ℕ) : (n : ∀ a, π a) = fun _ ↦ ↑n :=
   rfl
 #align pi.coe_nat Pi.coe_nat
 
+@[simp]
+theorem ofNat_apply (n : ℕ) [n.AtLeastTwo] (a : α) : (OfNat.ofNat n : ∀ a, π a) a = n := rfl
+
 end Pi
 
 theorem Sum.elim_natCast_natCast {α β γ : Type _} [NatCast γ] (n : ℕ) :

diff --git a/Mathlib/Probability/Variance.lean b/Mathlib/Probability/Variance.lean
@@ -214,11 +214,8 @@ theorem variance_def' [@IsProbabilityMeasure Ω _ ℙ] {X : Ω → ℝ} (hX : Me
   · apply hX.integrable_sq.add
     convert @integrable_const Ω ℝ (_) ℙ _ _ (𝔼[X] ^ 2)
   · exact ((hX.integrable one_le_two).const_mul 2).mul_const' _
-  simp [integral_mul_right]
-  have : ∀ (a : Ω), @OfNat.ofNat (Ω → ℝ) 2 instOfNat a = (2 : ℝ) := fun a => rfl
-  conv_lhs => enter [2, 1, 2, a]; rw [this]
-  simp only [integral_mul_left (2 : ℝ)]
-  ring_nf
+  simp [integral_mul_right, integral_mul_left]
+  ring
 #align probability_theory.variance_def' ProbabilityTheory.variance_def'
 
 theorem variance_le_expectation_sq [@IsProbabilityMeasure Ω _ ℙ] {X : Ω → ℝ}