harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_singleton_smul_le {S} [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M]
    (r : S) (x : M) : (R ∙ r • x) ≤ R ∙ x

Proof state:
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_9
inst✝³ : Monoid S
inst✝² : SMul S R
inst✝¹ : MulAction S M
inst✝ : IsScalarTower S R M
r : S
x : M
⊢ span R {r • x} ≤ span R {x}

Tactic:
rw [span_le, Set.singleton_subset_iff, SetLike.mem_coe]

Result:
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_9
inst✝³ : Monoid S
inst✝² : SMul S R
inst✝¹ : MulAction S M
inst✝ : IsScalarTower S R M
r : S
x : M
⊢ r • x ∈ span R {x}

Proof state:
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_9
inst✝³ : Monoid S
inst✝² : SMul S R
inst✝¹ : MulAction S M
inst✝ : IsScalarTower S R M
r : S
x : M
⊢ r • x ∈ span R {x}

Tactic:
exact smul_of_tower_mem _ _ (mem_span_singleton_self _)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem omega0_le_ord {a : Cardinal} : ω ≤ a.ord ↔ ℵ₀ ≤ a

Proof state:
a : Cardinal.{u_1}
⊢ ω ≤ a.ord ↔ ℵ₀ ≤ a

Tactic:
rw [← ord_aleph0, ord_le_ord]

Result:
no goals
-- Mathlib/Probability/Distributions/Gamma.lean
/-- The gamma pdf is nonnegative -/
lemma gammaPDFReal_nonneg {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) :
    0 ≤ gammaPDFReal a r x

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
⊢ 0 ≤ gammaPDFReal a r x

Tactic:
unfold gammaPDFReal

Result:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
⊢ 0 ≤ if 0 ≤ x then r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)) else 0

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
⊢ 0 ≤ if 0 ≤ x then r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)) else 0

Tactic:
split_ifs <;> positivity

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem agree_trivial {x : CofixA F 0} {y : CofixA F 1} : Agree x y

Proof state:
F : PFunctor.{u}
x : CofixA F 0
y : CofixA F 1
⊢ Agree x y

Tactic:
constructor

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem Function.Surjective.lieAlgebra_isNilpotent [h₁ : IsNilpotent L] {f : L →ₗ⁅R⁆ L'}
    (h₂ : Function.Surjective f) : IsNilpotent L'

Proof state:
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L L k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ⇑f
⊢ ∃ k, lowerCentralSeries R L' L' k = ⊥

Tactic:
peel h₁ with k hk

Result:
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L L k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ⇑f
k : ℕ
hk : lowerCentralSeries R L L k = ⊥
⊢ lowerCentralSeries R L' L' k = ⊥

Proof state:
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L L k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ⇑f
k : ℕ
hk : lowerCentralSeries R L L k = ⊥
⊢ lowerCentralSeries R L' L' k = ⊥

Tactic:
rw [← LieIdeal.lowerCentralSeries_map_eq k h₂, hk]

Result:
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L L k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ⇑f
k : ℕ
hk : lowerCentralSeries R L L k = ⊥
⊢ LieIdeal.map f ⊥ = ⊥

Proof state:
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieRing.IsNilpotent L
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ⇑f
⊢ LieRing.IsNilpotent L'

Tactic:
rw [LieRing.IsNilpotent, LieModule.isNilpotent_iff R] at h₁ ⊢

Result:
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L L k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ⇑f
⊢ ∃ k, lowerCentralSeries R L' L' k = ⊥

Proof state:
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L L k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ⇑f
k : ℕ
hk : lowerCentralSeries R L L k = ⊥
⊢ LieIdeal.map f ⊥ = ⊥

Tactic:
simp only [LieIdeal.map_eq_bot_iff, bot_le]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem eval₂_C_X_eq_coe : φ.eval₂ (PowerSeries.C R) PowerSeries.X = ↑φ

Proof state:
R : Type u_1
inst✝ : CommSemiring R
φ : R[X]
⊢ eval₂ (PowerSeries.C R) PowerSeries.X φ = ↑(eval₂ C X φ)

Tactic:
rw [← coeToPowerSeries.ringHom_apply, eval₂_eq_sum_range, eval₂_eq_sum_range, map_sum]

Result:
R : Type u_1
inst✝ : CommSemiring R
φ : R[X]
⊢ ∑ i ∈ Finset.range (φ.natDegree + 1), (PowerSeries.C R) (φ.coeff i) * PowerSeries.X ^ i =
    ∑ x ∈ Finset.range (φ.natDegree + 1), coeToPowerSeries.ringHom (C (φ.coeff x) * X ^ x)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
φ : R[X]
⊢ ∑ i ∈ Finset.range (φ.natDegree + 1), (PowerSeries.C R) (φ.coeff i) * PowerSeries.X ^ i =
    ∑ x ∈ Finset.range (φ.natDegree + 1), coeToPowerSeries.ringHom (C (φ.coeff x) * X ^ x)

Tactic:
apply Finset.sum_congr rfl

Result:
R : Type u_1
inst✝ : CommSemiring R
φ : R[X]
⊢ ∀ x ∈ Finset.range (φ.natDegree + 1),
    (PowerSeries.C R) (φ.coeff x) * PowerSeries.X ^ x = coeToPowerSeries.ringHom (C (φ.coeff x) * X ^ x)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
φ : R[X]
x✝ : ℕ
a✝ : x✝ ∈ Finset.range (φ.natDegree + 1)
⊢ (PowerSeries.C R) (φ.coeff x✝) * PowerSeries.X ^ x✝ = coeToPowerSeries.ringHom (C (φ.coeff x✝) * X ^ x✝)

Tactic:
rw [map_mul, map_pow, coeToPowerSeries.ringHom_apply,
  coeToPowerSeries.ringHom_apply, coe_C, coe_X]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
φ : R[X]
⊢ eval₂ (PowerSeries.C R) PowerSeries.X φ = ↑φ

Tactic:
nth_rw 2 [← eval₂_C_X (p := φ)]

Result:
R : Type u_1
inst✝ : CommSemiring R
φ : R[X]
⊢ eval₂ (PowerSeries.C R) PowerSeries.X φ = ↑(eval₂ C X φ)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
φ : R[X]
⊢ ∀ x ∈ Finset.range (φ.natDegree + 1),
    (PowerSeries.C R) (φ.coeff x) * PowerSeries.X ^ x = coeToPowerSeries.ringHom (C (φ.coeff x) * X ^ x)

Tactic:
intros

Result:
R : Type u_1
inst✝ : CommSemiring R
φ : R[X]
x✝ : ℕ
a✝ : x✝ ∈ Finset.range (φ.natDegree + 1)
⊢ (PowerSeries.C R) (φ.coeff x✝) * PowerSeries.X ^ x✝ = coeToPowerSeries.ringHom (C (φ.coeff x✝) * X ^ x✝)
-- Mathlib/NumberTheory/Cyclotomic/Three.lean
/-- We have that `λ ^ 2 = -3 * η`. -/
private lemma lambda_sq : λ ^ 2 = -3 * η

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ (↑hζ.toInteger - 1) ^ 2 = (algebraMap (𝓞 K) K) ↑η ^ 2 + (algebraMap (𝓞 K) K) ↑η + 1 - 3 * (algebraMap (𝓞 K) K) ↑η

Tactic:
simp only [RingOfIntegers.map_mk, IsUnit.unit_spec]

Result:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ (ζ - 1) ^ 2 = ζ ^ 2 + ζ + 1 - 3 * ζ

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ (ζ - 1) ^ 2 = ζ ^ 2 + ζ + 1 - 3 * ζ

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ λ ^ 2 = -3 * ↑η

Tactic:
ext

Result:
case h
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ ↑(λ ^ 2) = ↑(-3 * ↑η)

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ 0 < ↑3

Tactic:
decide

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ (algebraMap (𝓞 K) K) ↑η ^ 2 + (algebraMap (𝓞 K) K) ↑η + 1 - 3 * (algebraMap (𝓞 K) K) ↑η =
    0 - 3 * (algebraMap (𝓞 K) K) ↑η

Tactic:
simpa using hζ.isRoot_cyclotomic (by decide)

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ 0 - 3 * (algebraMap (𝓞 K) K) ↑η = -3 * (algebraMap (𝓞 K) K) ↑η

Tactic:
ring

Result:
no goals

Proof state:
case h
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ ↑(λ ^ 2) = ↑(-3 * ↑η)

Tactic:
calc (λ ^ 2 : K) = η ^ 2 + η + 1 - 3 * η := by
      simp only [RingOfIntegers.map_mk, IsUnit.unit_spec]; ring
_ = 0 - 3 * η := by simpa using hζ.isRoot_cyclotomic (by decide)
_ = -3 * η := by ring

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderivWithin_const (c : F) : fderivWithin 𝕜 (fun _ ↦ c) s = 0

Proof state:
case h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
c : F
x✝¹ x✝ : E
⊢ (fderivWithin 𝕜 (fun x => c) s x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
rw [fderivWithin_const_apply, Pi.zero_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
c : F
⊢ fderivWithin 𝕜 (fun x => c) s = 0

Tactic:
ext

Result:
case h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
c : F
x✝¹ x✝ : E
⊢ (fderivWithin 𝕜 (fun x => c) s x✝¹) x✝ = (0 x✝¹) x✝
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem forward_eq_nextn : forward = nextn

Proof state:
⊢ forward = nextn

Tactic:
funext it n

Result:
case h.h
it : Iterator
n : Nat
⊢ it.forward n = it.nextn n

Proof state:
case h.h
it : Iterator
n : Nat
⊢ it.forward n = it.nextn n

Tactic:
induction n generalizing it <;> simp [forward, nextn, *]

Result:
no goals
-- Mathlib/CategoryTheory/IsConnected.lean
theorem isPreconnected_induction [IsPreconnected J] (Z : J → Sort*)
    (h₁ : ∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), Z j₁ → Z j₂) (h₂ : ∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), Z j₂ → Z j₁)
    {j₀ : J} (x : Z j₀) (j : J) : Nonempty (Z j) :=
  (induct_on_objects { j | Nonempty (Z j) } ⟨x⟩
      (fun f => ⟨by rintro ⟨y⟩; exact ⟨h₁ f y⟩, by rintro ⟨y⟩; exact ⟨h₂ f y⟩⟩)
      j :)

Proof state:
case intro
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
y : Z j₁✝
⊢ j₂✝ ∈ {j | Nonempty (Z j)}

Tactic:
exact ⟨h₁ f y⟩

Result:
no goals

Proof state:
case intro
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
y : Z j₂✝
⊢ j₁✝ ∈ {j | Nonempty (Z j)}

Tactic:
exact ⟨h₂ f y⟩

Result:
no goals

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ j₁✝ ∈ {j | Nonempty (Z j)} → j₂✝ ∈ {j | Nonempty (Z j)}

Tactic:
rintro ⟨y⟩

Result:
case intro
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
y : Z j₁✝
⊢ j₂✝ ∈ {j | Nonempty (Z j)}

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ j₂✝ ∈ {j | Nonempty (Z j)} → j₁✝ ∈ {j | Nonempty (Z j)}

Tactic:
rintro ⟨y⟩

Result:
case intro
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
y : Z j₂✝
⊢ j₁✝ ∈ {j | Nonempty (Z j)}
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem sum_lof [DecidableEq ι] (j : ι) (x : AdicCompletion I (M j)) :
    sum I M ((DirectSum.lof (AdicCompletion I R) ι (fun i ↦ AdicCompletion I (M i)) j) x) =
      map I (lof R ι M j) x

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
j : ι
x : AdicCompletion I (M j)
⊢ (sum I M) ((lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) x) = (map I (lof R ι M j)) x

Tactic:
simp [sum]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma sub_le_iff_le_add {a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊤) (h₂ : b ≠ ⊤ ∨ c ≠ ⊥) :
    a - b ≤ c ↔ a ≤ c + b

Proof state:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ a + -b ≤ c ↔ a ≤ c - -b

Tactic:
refine (le_sub_iff_add_le ?_ ?_).symm <;> simpa

Result:
no goals

Proof state:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ a - b ≤ c ↔ a ≤ c + b

Tactic:
suffices a + (-b) ≤ c ↔ a ≤ c - (-b) by simpa [sub_eq_add_neg]

Result:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ a + -b ≤ c ↔ a ≤ c - -b

Proof state:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
this : a + -b ≤ c ↔ a ≤ c - -b
⊢ a - b ≤ c ↔ a ≤ c + b

Tactic:
simpa [sub_eq_add_neg]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma tilted_eq_withDensity_nnreal (μ : Measure α) (f : α → ℝ) :
    μ.tilted f = μ.withDensity (fun x ↦ ((↑) : ℝ≥0 → ℝ≥0∞)
      (⟨exp (f x) / ∫ x, exp (f x) ∂μ, by positivity⟩ : ℝ≥0))

Proof state:
case e_f.h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) = ↑⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩

Tactic:
rw [ENNReal.ofReal_eq_coe_nnreal]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ✝ : Measure α
f✝ : α → ℝ
μ : Measure α
f : α → ℝ
x : α
⊢ 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ (μ.withDensity fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) =
    μ.withDensity fun x => ↑⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩

Tactic:
congr with x

Result:
case e_f.h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) = ↑⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ μ.tilted f = μ.withDensity fun x => ↑⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩

Tactic:
rw [Measure.tilted]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ (μ.withDensity fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) =
    μ.withDensity fun x => ↑⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isLittleO_insert [TopologicalSpace α] {x : α} {s : Set α} {g : α → E'} {g' : α → F'}
    (h : g x = 0) : g =o[𝓝[insert x s] x] g' ↔ g =o[𝓝[s] x] g'

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ IsBigOWith c (𝓝[insert x s] x) g g' ↔ IsBigOWith c (𝓝[s] x) g g'

Tactic:
rw [isBigOWith_insert]

Result:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ ‖g x‖ ≤ c * ‖g' x‖

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
⊢ g =o[𝓝[insert x s] x] g' ↔ g =o[𝓝[s] x] g'

Tactic:
simp_rw [IsLittleO_def]

Result:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[insert x s] x) g g') ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[s] x) g g'

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ 0 ≤ c * ‖g' x‖

Tactic:
exact mul_nonneg hc.le (norm_nonneg _)

Result:
no goals

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[insert x s] x) g g') ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[s] x) g g'

Tactic:
refine forall_congr' fun c => forall_congr' fun hc => ?_

Result:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ IsBigOWith c (𝓝[insert x s] x) g g' ↔ IsBigOWith c (𝓝[s] x) g g'

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ ‖g x‖ ≤ c * ‖g' x‖

Tactic:
rw [h, norm_zero]

Result:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ 0 ≤ c * ‖g' x‖
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem tendsto_approxBounded_ae {β} {f : α → β} [NormedAddCommGroup β] [NormedSpace ℝ β]
    {m m0 : MeasurableSpace α} {μ : Measure α} (hf : StronglyMeasurable[m] f) {c : ℝ}
    (hf_bound : ∀ᵐ x ∂μ, ‖f x‖ ≤ c) :
    ∀ᵐ x ∂μ, Tendsto (fun n => hf.approxBounded c n x) atTop (𝓝 (f x))

Proof state:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m m0 : MeasurableSpace α
μ : Measure α
hf : StronglyMeasurable f
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => (hf.approxBounded c n) x) atTop (𝓝 (f x))

Tactic:
filter_upwards [hf_bound] with x hfx using tendsto_approxBounded_of_norm_le hf hfx

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem image_iUnion {f : α → β} {s : ι → Set α} : (f '' ⋃ i, s i) = ⋃ i, f '' s i

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set α
x : β
⊢ x ∈ f '' ⋃ i, s i ↔ x ∈ ⋃ i, f '' s i

Tactic:
simp only [mem_image, mem_iUnion, ← exists_and_right, ← exists_and_left]

Result:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set α
x : β
⊢ (∃ x_1 x_2, x_1 ∈ s x_2 ∧ f x_1 = x) ↔ ∃ i, ∃ x_1 ∈ s i, f x_1 = x

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set α
⊢ f '' ⋃ i, s i = ⋃ i, f '' s i

Tactic:
ext1 x

Result:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set α
x : β
⊢ x ∈ f '' ⋃ i, s i ↔ x ∈ ⋃ i, f '' s i

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set α
x : β
⊢ (∃ x_1 x_2, x_1 ∈ s x_2 ∧ f x_1 = x) ↔ ∃ i, ∃ x_1 ∈ s i, f x_1 = x

Tactic:
rw [exists_swap]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem strongEpi_of_strongEpiMonoFactorisation {X Y : C} {f : X ⟶ Y}
    (F : StrongEpiMonoFactorisation f) {F' : MonoFactorisation f} (hF' : IsImage F') :
    StrongEpi F'.e

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi (F.e ≫ (F.toMonoIsImage.isoExt hF').hom)

Tactic:
apply strongEpi_comp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi F'.e

Tactic:
rw [← IsImage.e_isoExt_hom F.toMonoIsImage hF']

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi (F.e ≫ (F.toMonoIsImage.isoExt hF').hom)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α}
    {v : β k} : (m.insertIfNew k v).contains a → (k == a) = false → m.contains a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true

Tactic:
simp_to_model [insertIfNew] using List.containsKey_of_containsKey_insertEntryIfNew

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem positivize_sat {s x v} (w : s.sat' x v) :
    (positivizeConstraint s x).sat' (positivizeCoeffs s x) v

Proof state:
s : Constraint
x v : Coeffs
w : s.sat' x v = true
⊢ (positivizeConstraint s x).sat' (positivizeCoeffs s x) v = true

Tactic:
dsimp [positivizeConstraint, positivizeCoeffs, positivize, positivize?]

Result:
s : Constraint
x v : Coeffs
w : s.sat' x v = true
⊢ ((if 0 ≤ x.leading then none else some (s.neg, x.smul (-1))).getD (s, x)).fst.sat'
      ((if 0 ≤ x.leading then none else some (s.neg, x.smul (-1))).getD (s, x)).snd v =
    true

Proof state:
case isFalse
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h✝ : ¬0 ≤ x.leading
⊢ s.neg.sat ((x.smul (-1)).dot v) = true

Tactic:
erw [Coeffs.dot_smul_left, ← Int.neg_eq_neg_one_mul]

Result:
case isFalse
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h✝ : ¬0 ≤ x.leading
⊢ s.neg.sat (-x.dot v) = true

Proof state:
case isFalse
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h✝ : ¬0 ≤ x.leading
⊢ ((some (s.neg, x.smul (-1))).getD (s, x)).fst.sat' ((some (s.neg, x.smul (-1))).getD (s, x)).snd v = true

Tactic:
simp [Constraint.sat']

Result:
case isFalse
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h✝ : ¬0 ≤ x.leading
⊢ s.neg.sat ((x.smul (-1)).dot v) = true

Proof state:
case isTrue
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h✝ : 0 ≤ x.leading
⊢ (none.getD (s, x)).fst.sat' (none.getD (s, x)).snd v = true

Tactic:
exact w

Result:
no goals

Proof state:
s : Constraint
x v : Coeffs
w : s.sat' x v = true
⊢ ((if 0 ≤ x.leading then none else some (s.neg, x.smul (-1))).getD (s, x)).fst.sat'
      ((if 0 ≤ x.leading then none else some (s.neg, x.smul (-1))).getD (s, x)).snd v =
    true

Tactic:
split

Result:
case isTrue
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h✝ : 0 ≤ x.leading
⊢ (none.getD (s, x)).fst.sat' (none.getD (s, x)).snd v = true

case isFalse
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h✝ : ¬0 ≤ x.leading
⊢ ((some (s.neg, x.smul (-1))).getD (s, x)).fst.sat' ((some (s.neg, x.smul (-1))).getD (s, x)).snd v = true

Proof state:
case isFalse
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h✝ : ¬0 ≤ x.leading
⊢ s.neg.sat (-x.dot v) = true

Tactic:
exact Constraint.neg_sat w

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Bounds.lean
/-- The values of a Dirichlet character with target a normed field have norm bounded by `1`. -/
lemma norm_le_one (a : ZMod n) : ‖χ a‖ ≤ 1

Proof state:
case neg
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : ¬IsUnit a
⊢ ‖χ a‖ ≤ 1

Tactic:
rw [χ.map_nonunit h, norm_zero]

Result:
case neg
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : ¬IsUnit a
⊢ 0 ≤ 1

Proof state:
case pos
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : IsUnit a
⊢ ‖χ a‖ ≤ 1

Tactic:
exact (χ.unit_norm_eq_one h.unit).le

Result:
no goals

Proof state:
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
⊢ ‖χ a‖ ≤ 1

Tactic:
by_cases h : IsUnit a

Result:
case pos
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : IsUnit a
⊢ ‖χ a‖ ≤ 1

case neg
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : ¬IsUnit a
⊢ ‖χ a‖ ≤ 1

Proof state:
case neg
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : ¬IsUnit a
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

Result:
no goals