harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
lemma withDensity_mono {f g : α → ℝ≥0∞} (hfg : f ≤ᵐ[μ] g) :
    μ.withDensity f ≤ μ.withDensity g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x

Tactic:
filter_upwards [hfg] with x h_le using fun _ ↦ h_le

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
⊢ μ.withDensity f ≤ μ.withDensity g

Tactic:
refine le_iff.2 fun s hs ↦ ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity f) s ≤ (μ.withDensity g) s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
refine setLIntegral_mono_ae' hs ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity f) s ≤ (μ.withDensity g) s

Tactic:
rw [withDensity_apply _ hs, withDensity_apply _ hs]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem aevalTower_ofId : aevalTower (Algebra.ofId S A') = aeval

Proof state:
S : Type v
A' : Type u_1
inst✝² : CommSemiring A'
inst✝¹ : CommSemiring S
inst✝ : Algebra S A'
⊢ aevalTower (Algebra.ofId S A') = aeval

Tactic:
ext

Result:
case h.hX
S : Type v
A' : Type u_1
inst✝² : CommSemiring A'
inst✝¹ : CommSemiring S
inst✝ : Algebra S A'
x✝ : A'
⊢ (aevalTower (Algebra.ofId S A') x✝) X = (aeval x✝) X

Proof state:
case h.hX
S : Type v
A' : Type u_1
inst✝² : CommSemiring A'
inst✝¹ : CommSemiring S
inst✝ : Algebra S A'
x✝ : A'
⊢ (aevalTower (Algebra.ofId S A') x✝) X = (aeval x✝) X

Tactic:
simp only [aeval_X, aevalTower_X]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem prepartition_isPartition {B : Box ι} (hB : hasIntegralVertices B) :
    (prepartition n B).IsPartition

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
⊢ (prepartition n B).IsPartition

Tactic:
refine fun x hx ↦ ⟨box n (index n x), ?_, mem_box_iff_index.mpr rfl⟩

Result:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
⊢ box n (index n x) ∈ (prepartition n B).toPrepartition

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
⊢ ∃ ν ∈ admissibleIndex n B, box n ν = box n (index n x)

Tactic:
exact ⟨index n x, mem_admissibleIndex_of_mem_box n hB hx, rfl⟩

Result:
no goals

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
⊢ box n (index n x) ∈ (prepartition n B).toPrepartition

Tactic:
rw [TaggedPrepartition.mem_toPrepartition, mem_prepartition_iff]

Result:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
⊢ ∃ ν ∈ admissibleIndex n B, box n ν = box n (index n x)
-- Mathlib/Data/Real/IsNonarchimedean.lean
theorem nsmul_le {F α : Type*} [AddGroup α] [FunLike F α ℝ]
    [AddGroupSeminormClass F α ℝ] {f : F} (hna : IsNonarchimedean f) {n : ℕ} {a : α} :
    f (n • a) ≤ f a

Proof state:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
⊢ f (n • a) ≤ f a

Tactic:
let _ := AddGroupSeminormClass.toSeminormedAddGroup f

Result:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
x✝ : SeminormedAddGroup α := AddGroupSeminormClass.toSeminormedAddGroup f
⊢ f (n • a) ≤ f a

Proof state:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
x✝ : SeminormedAddGroup α := AddGroupSeminormClass.toSeminormedAddGroup f
this : IsUltrametricDist α
⊢ f (n • a) ≤ f a

Tactic:
simp only [← AddGroupSeminormClass.toSeminormedAddGroup_norm_eq]

Result:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
x✝ : SeminormedAddGroup α := AddGroupSeminormClass.toSeminormedAddGroup f
this : IsUltrametricDist α
⊢ ‖n • a‖ ≤ ‖a‖

Proof state:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
x✝ : SeminormedAddGroup α := AddGroupSeminormClass.toSeminormedAddGroup f
⊢ f (n • a) ≤ f a

Tactic:
have := AddGroupSeminormClass.isUltrametricDist hna

Result:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
x✝ : SeminormedAddGroup α := AddGroupSeminormClass.toSeminormedAddGroup f
this : IsUltrametricDist α
⊢ f (n • a) ≤ f a

Proof state:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
x✝ : SeminormedAddGroup α := AddGroupSeminormClass.toSeminormedAddGroup f
this : IsUltrametricDist α
⊢ ‖n • a‖ ≤ ‖a‖

Tactic:
exact norm_nsmul_le _ _

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem prod_ofPNatMultiset (v : Multiset ℕ+) (h) : ((ofPNatMultiset v h).prod : ℕ+) = v.prod

Proof state:
v : Multiset ℕ+
h : ∀ p ∈ v, p.Prime
⊢ (ofPNatMultiset v h).toPNatMultiset.prod = v.prod

Tactic:
rw [to_ofPNatMultiset]

Result:
no goals

Proof state:
v : Multiset ℕ+
h : ∀ p ∈ v, p.Prime
⊢ (ofPNatMultiset v h).prod = v.prod

Tactic:
dsimp [prod]

Result:
v : Multiset ℕ+
h : ∀ p ∈ v, p.Prime
⊢ (ofPNatMultiset v h).toPNatMultiset.prod = v.prod
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem trunc_C (n) (a : R) : trunc (n + 1) (C R a) = Polynomial.C a :=
  Polynomial.ext fun m => by
    rw [coeff_trunc, coeff_C, Polynomial.coeff_C]
    split_ifs with H <;> first |rfl|try simp_all

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
⊢ (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0

Tactic:
split_ifs with H <;> first |rfl|try simp_all

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
⊢ (trunc (n + 1) ((C R) a)).coeff m = (Polynomial.C a).coeff m

Tactic:
rw [coeff_trunc, coeff_C, Polynomial.coeff_C]

Result:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
⊢ (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h✝ : m = 0
⊢ 0 = a

Tactic:
try simp_all

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h✝ : m = 0
⊢ 0 = a

Tactic:
simp_all

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h✝ : ¬m = 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma CotangentSpace.fst_compEquiv :
    LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
      (compEquiv Q P).toLinearMap = Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom

Proof state:
case a.h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : (Q.comp P).vars
j : Q.vars
⊢ (Q.cotangentSpaceBasis.repr
        ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
          ((Q.comp P).cotangentSpaceBasis i)))
      j =
    (Q.cotangentSpaceBasis.repr
        ((Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ((Q.comp P).cotangentSpaceBasis i)))
      j

Tactic:
simp only [compEquiv, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ofComp_val,
  LinearEquiv.trans_apply, Basis.repr_self, LinearMap.fst_apply, repr_CotangentSpaceMap]

Result:
case a.h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : (Q.comp P).vars
j : Q.vars
⊢ (Q.cotangentSpaceBasis.repr
        ((Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)).repr.symm (Finsupp.single i 1)).1)
      j =
    (aeval Q.val) ((pderiv j) (Sum.elim X (⇑C ∘ P.val) i))
-- Mathlib/Data/Nat/Bitwise.lean
theorem zero_of_testBit_eq_false {n : ℕ} (h : ∀ i, testBit n i = false) : n = 0

Proof state:
b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
⊢ b = false

Tactic:
simpa using h 0

Result:
no goals

Proof state:
case f
b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
⊢ bit b n = 0

Tactic:
have : b = false := by simpa using h 0

Result:
case f
b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
this : b = false
⊢ bit b n = 0

Proof state:
n : ℕ
h : ∀ (i : ℕ), n.testBit i = false
⊢ n = 0

Tactic:
induction' n using Nat.binaryRec with b n hn

Result:
case z
h : ∀ (i : ℕ), testBit 0 i = false
⊢ 0 = 0

case f
b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
⊢ bit b n = 0

Proof state:
case z
h : ∀ (i : ℕ), testBit 0 i = false
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
this : b = false
i : ℕ
⊢ n.testBit i = false

Tactic:
rw [← h (i + 1), testBit_bit_succ]

Result:
no goals

Proof state:
case f
b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
this : b = false
⊢ bit b n = 0

Tactic:
rw [this, bit_false, hn fun i => by rw [← h (i + 1), testBit_bit_succ]]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem resolve_left_ineq (a c d p x : Int) (a_pos : 0 < a) (b_pos : 0 < b)
    (h₁ : p ≤ a * x) (h₂ : b * x ≤ q) :
    b * resolve_left a c d p x + b * p ≤ a * q

Proof state:
b q a c d p x : Int
a_pos : 0 < a
b_pos : 0 < b
h₁ : p ≤ a * x
h₂ : b * x ≤ q
⊢ b * ↑((add_of_le h₁).val % a.lcm (a * d / ↑((a * d).gcd c))) + b * p ≤ a * q

Tactic:
obtain ⟨k', w⟩ := add_of_le h₁

Result:
case mk
b q a c d p x : Int
a_pos : 0 < a
b_pos : 0 < b
h₁ : p ≤ a * x
h₂ : b * x ≤ q
k' : Nat
w : a * x = p + ↑k'
⊢ b * ↑(⟨k', w⟩.val % a.lcm (a * d / ↑((a * d).gcd c))) + b * p ≤ a * q

Proof state:
case mk
b q a c d p x : Int
a_pos : 0 < a
b_pos : 0 < b
h₁ : p ≤ a * x
k' : Nat
w : a * x = p + ↑k'
h₂ : a * b * x ≤ a * q
⊢ b * ↑(⟨k', w⟩.val % a.lcm (a * d / ↑((a * d).gcd c))) + b * p ≤ a * q

Tactic:
rw [Int.mul_right_comm, w, Int.add_mul, Int.mul_comm p b, Int.mul_comm _ b] at h₂

Result:
case mk
b q a c d p x : Int
a_pos : 0 < a
b_pos : 0 < b
h₁ : p ≤ a * x
k' : Nat
w : a * x = p + ↑k'
h₂ : b * p + b * ↑k' ≤ a * q
⊢ b * ↑(⟨k', w⟩.val % a.lcm (a * d / ↑((a * d).gcd c))) + b * p ≤ a * q

Proof state:
b q a c d p x : Int
a_pos : 0 < a
b_pos : 0 < b
h₁ : p ≤ a * x
h₂ : b * x ≤ q
⊢ b * resolve_left a c d p x + b * p ≤ a * q

Tactic:
simp only [h₁, resolve_left_eq, resolve_left']

Result:
b q a c d p x : Int
a_pos : 0 < a
b_pos : 0 < b
h₁ : p ≤ a * x
h₂ : b * x ≤ q
⊢ b * ↑((add_of_le h₁).val % a.lcm (a * d / ↑((a * d).gcd c))) + b * p ≤ a * q

Proof state:
case mk
b q a c d p x : Int
a_pos : 0 < a
b_pos : 0 < b
h₁ : p ≤ a * x
k' : Nat
w : a * x = p + ↑k'
h₂ : b * p + b * ↑k' ≤ a * q
⊢ b * ↑(⟨k', w⟩.val % a.lcm (a * d / ↑((a * d).gcd c))) + b * p ≤ a * q

Tactic:
rw [Int.add_comm]

Result:
case mk
b q a c d p x : Int
a_pos : 0 < a
b_pos : 0 < b
h₁ : p ≤ a * x
k' : Nat
w : a * x = p + ↑k'
h₂ : b * p + b * ↑k' ≤ a * q
⊢ b * p + b * ↑(⟨k', w⟩.val % a.lcm (a * d / ↑((a * d).gcd c))) ≤ a * q

Proof state:
case mk
b q a c d p x : Int
a_pos : 0 < a
b_pos : 0 < b
h₁ : p ≤ a * x
k' : Nat
w : a * x = p + ↑k'
h₂ : b * p + b * ↑k' ≤ a * q
⊢ b * p + b * ↑(⟨k', w⟩.val % a.lcm (a * d / ↑((a * d).gcd c))) ≤ a * q

Tactic:
calc
  _ ≤ _ := Int.add_le_add_left (Int.mul_le_mul_of_nonneg_left
              (Int.ofNat_le.mpr <| Nat.mod_le _ _) (Int.le_of_lt b_pos)) _
  _ ≤ _ := h₂

Result:
no goals

Proof state:
case mk
b q a c d p x : Int
a_pos : 0 < a
b_pos : 0 < b
h₁ : p ≤ a * x
h₂ : b * x ≤ q
k' : Nat
w : a * x = p + ↑k'
⊢ b * ↑(⟨k', w⟩.val % a.lcm (a * d / ↑((a * d).gcd c))) + b * p ≤ a * q

Tactic:
replace h₂ : a * b * x ≤ a * q :=
  Int.mul_assoc _ _ _ ▸ Int.mul_le_mul_of_nonneg_left h₂ (Int.le_of_lt a_pos)

Result:
case mk
b q a c d p x : Int
a_pos : 0 < a
b_pos : 0 < b
h₁ : p ≤ a * x
k' : Nat
w : a * x = p + ↑k'
h₂ : a * b * x ≤ a * q
⊢ b * ↑(⟨k', w⟩.val % a.lcm (a * d / ↑((a * d).gcd c))) + b * p ≤ a * q
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_mul_le_iff {x y z : ℝ≥0∞} (h1 : x ≠ 0) (h2 : x ≠ ∞) :
    x⁻¹ * y ≤ z ↔ y ≤ x * z

Proof state:
x y z : ℝ≥0∞
h1 : x ≠ 0
h2 : x ≠ ⊤
⊢ x⁻¹ * y ≤ z ↔ y ≤ x * z

Tactic:
rw [← mul_le_mul_left h1 h2, ← mul_assoc, ENNReal.mul_inv_cancel h1 h2, one_mul]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem deriv_sub_const (c : F) : deriv (fun y => f y - c) x = deriv f x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
c : F
⊢ deriv (fun y => f y - c) x = deriv f x

Tactic:
simp only [deriv, fderiv_sub_const]

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem integral_eq (huX : IsUniform X s ℙ) :
    ∫ x, X x ∂ℙ = (volume s)⁻¹.toReal * ∫ x in s, x

Proof state:
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂(volume s)⁻¹ • volume.restrict s

Tactic:
rw [← huX]

Result:
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ

Proof state:
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : IsUniform X s ℙ volume
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂(volume s)⁻¹ • volume.restrict s

Tactic:
dsimp only [IsUniform, ProbabilityTheory.cond] at huX

Result:
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂(volume s)⁻¹ • volume.restrict s

Proof state:
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ

Tactic:
by_cases hX : AEMeasurable X ℙ

Result:
case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : AEMeasurable X ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ

case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : ¬AEMeasurable X ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ

Proof state:
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : IsUniform X s ℙ volume
⊢ ∫ (x : Ω), X x ∂ℙ = (volume s)⁻¹.toReal * ∫ (x : ℝ) in s, x

Tactic:
rw [← smul_eq_mul, ← integral_smul_measure]

Result:
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : IsUniform X s ℙ volume
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂(volume s)⁻¹ • volume.restrict s

Proof state:
case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : ¬AEMeasurable X ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ

Tactic:
rw [map_of_not_aemeasurable hX, integral_zero_measure, integral_non_aestronglyMeasurable]

Result:
case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : ¬AEMeasurable X ℙ
⊢ ¬AEStronglyMeasurable X ℙ

Proof state:
case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : ¬AEMeasurable X ℙ
⊢ ¬AEStronglyMeasurable X ℙ

Tactic:
rwa [aestronglyMeasurable_iff_aemeasurable]

Result:
no goals

Proof state:
case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : AEMeasurable X ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ

Tactic:
exact (integral_map hX aestronglyMeasurable_id).symm

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem count_inv (I : FractionalIdeal R⁰ K) :
    count K v (I⁻¹) = - count K v I

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
⊢ count K v I⁻¹ = -count K v I

Tactic:
rw [← zpow_neg_one, count_neg_zpow K v (1 : ℤ) I, zpow_one]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
lemma δ_rightUnshift {a n' : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n)
    (m m' : ℤ) (hm' : m' + a = m) :
    δ n m (γ.rightUnshift n hn) = a.negOnePow • (δ n' m' γ).rightUnshift m hm'

Proof state:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' n : ℤ
hn : n' + a = n
m m' : ℤ
hm' : m' + a = m
γ' : Cochain K L n
⊢ δ n m (((rightShiftAddEquiv K L n a n' hn) γ').rightUnshift n hn) =
    a.negOnePow • (δ n' m' ((rightShiftAddEquiv K L n a n' hn) γ')).rightUnshift m hm'

Tactic:
dsimp

Result:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' n : ℤ
hn : n' + a = n
m m' : ℤ
hm' : m' + a = m
γ' : Cochain K L n
⊢ δ n m ((γ'.rightShift a n' hn).rightUnshift n hn) = a.negOnePow • (δ n' m' (γ'.rightShift a n' hn)).rightUnshift m hm'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
m m' : ℤ
hm' : m' + a = m
⊢ δ n m (γ.rightUnshift n hn) = a.negOnePow • (δ n' m' γ).rightUnshift m hm'

Tactic:
obtain ⟨γ', rfl⟩ := (rightShiftAddEquiv K L n a n' hn).surjective γ

Result:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' n : ℤ
hn : n' + a = n
m m' : ℤ
hm' : m' + a = m
γ' : Cochain K L n
⊢ δ n m (((rightShiftAddEquiv K L n a n' hn) γ').rightUnshift n hn) =
    a.negOnePow • (δ n' m' ((rightShiftAddEquiv K L n a n' hn) γ')).rightUnshift m hm'

Proof state:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' n : ℤ
hn : n' + a = n
m m' : ℤ
hm' : m' + a = m
γ' : Cochain K L n
⊢ δ n m ((γ'.rightShift a n' hn).rightUnshift n hn) = a.negOnePow • (δ n' m' (γ'.rightShift a n' hn)).rightUnshift m hm'

Tactic:
simp only [rightUnshift_rightShift, γ'.δ_rightShift a n' m' hn m hm', rightUnshift_units_smul,
  smul_smul, Int.units_mul_self, one_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem Pi.basisFun_det_apply (v : ι → ι → R) :
    (Pi.basisFun R ι).det v = (Matrix.of v).det

Proof state:
R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → ι → R
⊢ detRowAlternating v = (of v).det

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → ι → R
⊢ (basisFun R ι).det v = (of v).det

Tactic:
rw [Pi.basisFun_det]

Result:
R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → ι → R
⊢ detRowAlternating v = (of v).det
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_sq_add_S_sq (n : ℤ) : S R n ^ 2 + S R (n + 1) ^ 2 - X * S R n * S R (n + 1) = 1

Proof state:
case hn
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : S R (-↑n) ^ 2 + S R (-↑n + 1) ^ 2 - X * S R (-↑n) * S R (-↑n + 1) = 1
h₁ : S R (-↑n - 1) = X * S R (-↑n) - S R (-↑n + 1)
⊢ S R (-↑n - 1) ^ 2 + S R (-↑n - 1 + 1) ^ 2 - X * S R (-↑n - 1) * S R (-↑n - 1 + 1) = 1

Tactic:
linear_combination (norm := ring_nf) (S R (-1 - n) - S R (1 - n)) * h₁ + ih

Result:
no goals

Proof state:
case hz
R : Type u_1
inst✝ : CommRing R
⊢ S R 0 ^ 2 + S R (0 + 1) ^ 2 - X * S R 0 * S R (0 + 1) = 1

Tactic:
simp

Result:
case hz
R : Type u_1
inst✝ : CommRing R
⊢ 1 + X ^ 2 - X * X = 1

Proof state:
case hp
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : S R ↑n ^ 2 + S R (↑n + 1) ^ 2 - X * S R ↑n * S R (↑n + 1) = 1
⊢ S R (↑n + 1) ^ 2 + S R (↑n + 1 + 1) ^ 2 - X * S R (↑n + 1) * S R (↑n + 1 + 1) = 1

Tactic:
have h₁ := S_add_two R n

Result:
case hp
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : S R ↑n ^ 2 + S R (↑n + 1) ^ 2 - X * S R ↑n * S R (↑n + 1) = 1
h₁ : S R (↑n + 2) = X * S R (↑n + 1) - S R ↑n
⊢ S R (↑n + 1) ^ 2 + S R (↑n + 1 + 1) ^ 2 - X * S R (↑n + 1) * S R (↑n + 1 + 1) = 1

Proof state:
case hp
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : S R ↑n ^ 2 + S R (↑n + 1) ^ 2 - X * S R ↑n * S R (↑n + 1) = 1
h₁ : S R (↑n + 2) = X * S R (↑n + 1) - S R ↑n
⊢ S R (↑n + 1) ^ 2 + S R (↑n + 1 + 1) ^ 2 - X * S R (↑n + 1) * S R (↑n + 1 + 1) = 1

Tactic:
linear_combination (norm := ring_nf) (S R (2 + n) - S R n) * h₁ + ih

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ S R n ^ 2 + S R (n + 1) ^ 2 - X * S R n * S R (n + 1) = 1

Tactic:
induction n with
| hz => simp; ring
| hp n ih =>
  have h₁ := S_add_two R n
  linear_combination (norm := ring_nf) (S R (2 + n) - S R n) * h₁ + ih
| hn n ih =>
  have h₁ := S_sub_one R (-n)
  linear_combination (norm := ring_nf) (S R (-1 - n) - S R (1 - n)) * h₁ + ih

Result:
no goals

Proof state:
case hn
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : S R (-↑n) ^ 2 + S R (-↑n + 1) ^ 2 - X * S R (-↑n) * S R (-↑n + 1) = 1
⊢ S R (-↑n - 1) ^ 2 + S R (-↑n - 1 + 1) ^ 2 - X * S R (-↑n - 1) * S R (-↑n - 1 + 1) = 1

Tactic:
have h₁ := S_sub_one R (-n)

Result:
case hn
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : S R (-↑n) ^ 2 + S R (-↑n + 1) ^ 2 - X * S R (-↑n) * S R (-↑n + 1) = 1
h₁ : S R (-↑n - 1) = X * S R (-↑n) - S R (-↑n + 1)
⊢ S R (-↑n - 1) ^ 2 + S R (-↑n - 1 + 1) ^ 2 - X * S R (-↑n - 1) * S R (-↑n - 1 + 1) = 1

Proof state:
case hz
R : Type u_1
inst✝ : CommRing R
⊢ 1 + X ^ 2 - X * X = 1

Tactic:
ring

Result:
no goals