harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
lemma isIntegralCurve_iff_isIntegralCurveAt :
    IsIntegralCurve γ v ↔ ∀ t : ℝ, IsIntegralCurveAt γ v t :=
  ⟨fun h ↦ h.isIntegralCurveAt, fun h t ↦ by
    obtain ⟨s, hs, h⟩ := isIntegralCurveAt_iff.mp (h t)
    exact h t (mem_of_mem_nhds hs)⟩

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
h : ∀ (t : ℝ), IsIntegralCurveAt γ v t
t : ℝ
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))

Tactic:
obtain ⟨s, hs, h⟩ := isIntegralCurveAt_iff.mp (h t)

Result:
case intro.intro
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
h✝ : ∀ (t : ℝ), IsIntegralCurveAt γ v t
t : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t
h : IsIntegralCurveOn γ v s
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))

Proof state:
case intro.intro
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
h✝ : ∀ (t : ℝ), IsIntegralCurveAt γ v t
t : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t
h : IsIntegralCurveOn γ v s
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))

Tactic:
exact h t (mem_of_mem_nhds hs)

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some
    (hx : AlgebraicIndependent R x) (i) :
    hx.mvPolynomialOptionEquivPolynomialAdjoin (X (some i)) =
      Polynomial.C (hx.aevalEquiv (X i))

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
i : ι
⊢ hx.mvPolynomialOptionEquivPolynomialAdjoin (X (some i)) = Polynomial.C (hx.aevalEquiv (X i))

Tactic:
rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim,
  Polynomial.map_C, RingHom.coe_coe]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem comap_codRestrict (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (hf p') :
    Submodule.comap (codRestrict p f hf) p' = Submodule.comap f (map p.subtype p') :=
  Submodule.ext fun x => ⟨fun h => ⟨⟨_, hf x⟩, h, rfl⟩, by rintro ⟨⟨_, _⟩, h, ⟨⟩⟩; exact h⟩

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₂₁ : R₂ →+* R
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
hf : ∀ (c : M₂), f c ∈ p
p' : Submodule R ↥p
x : M₂
⊢ x ∈ comap f (map p.subtype p') → x ∈ comap (codRestrict p f hf) p'

Tactic:
rintro ⟨⟨_, _⟩, h, ⟨⟩⟩

Result:
case intro.mk.intro.refl
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₂₁ : R₂ →+* R
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
hf : ∀ (c : M₂), f c ∈ p
p' : Submodule R ↥p
x : M₂
property✝ : f.toAddHom.1 x ∈ p
h : ⟨f.toAddHom.1 x, property✝⟩ ∈ ↑p'
⊢ x ∈ comap (codRestrict p f hf) p'

Proof state:
case intro.mk.intro.refl
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₂₁ : R₂ →+* R
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
hf : ∀ (c : M₂), f c ∈ p
p' : Submodule R ↥p
x : M₂
property✝ : f.toAddHom.1 x ∈ p
h : ⟨f.toAddHom.1 x, property✝⟩ ∈ ↑p'
⊢ x ∈ comap (codRestrict p f hf) p'

Tactic:
exact h

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem inv_mul_eq_of_eq_mul (h : b = a * c) : a⁻¹ * b = c

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : b = a * c
⊢ a⁻¹ * b = c

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_iSup (f : ι → UpperSet α) : (↑(⨆ i, f i) : Set α) = ⋂ i, f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → UpperSet α
⊢ ↑(⨆ i, f i) = ⋂ i, ↑(f i)

Tactic:
simp [iSup]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/SuperFactorial.lean
theorem superFactorial_four_mul (n : ℕ) :
    sf (4 * n) = ((∏ i ∈ range (2 * n), (2 * i + 1) !) * 2 ^ n) ^ 2 * (2 * n) ! :=
  calc
    sf (4 * n) = (∏ i ∈ range (2 * n), (2 * i + 1) !) ^ 2 * 2 ^ (2 * n) * (2 * n) !

Proof state:
n : ℕ
⊢ sf 4 * n = (∏ i ∈ range (2 * n), (2 * i + 1)!) ^ 2 * 2 ^ (2 * n) * (2 * n)!

Tactic:
rw [← superFactorial_two_mul, ← mul_assoc, Nat.mul_two]

Result:
no goals

Proof state:
n : ℕ
⊢ (∏ i ∈ range (2 * n), (2 * i + 1)!) ^ 2 * 2 ^ (2 * n) * (2 * n)! =
    ((∏ i ∈ range (2 * n), (2 * i + 1)!) * 2 ^ n) ^ 2 * (2 * n)!

Tactic:
rw [pow_mul', mul_pow]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma compProd_sum_right {ι : Type*} [Countable ι] {κ : ι → Kernel α β}
    [h : ∀ i, IsSFiniteKernel (κ i)] :
    μ ⊗ₘ (Kernel.sum κ) = sum (fun i ↦ μ ⊗ₘ (κ i))

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ι : Type u_3
inst✝ : Countable ι
κ : ι → Kernel α β
h : ∀ (i : ι), IsSFiniteKernel (κ i)
⊢ μ ⊗ₘ Kernel.sum κ = sum fun i => μ ⊗ₘ κ i

Tactic:
rw [compProd, ← Kernel.sum_prodMkLeft, Kernel.compProd_sum_right]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ι : Type u_3
inst✝ : Countable ι
κ : ι → Kernel α β
h : ∀ (i : ι), IsSFiniteKernel (κ i)
⊢ (Kernel.sum fun i => Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit (κ i)) () = sum fun i => μ ⊗ₘ κ i

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ι : Type u_3
inst✝ : Countable ι
κ : ι → Kernel α β
h : ∀ (i : ι), IsSFiniteKernel (κ i)
⊢ (Kernel.sum fun i => Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit (κ i)) () = sum fun i => μ ⊗ₘ κ i

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem xgcd_zero_left {s t r' s' t'} : xgcdAux 0 s t r' s' t' = (r', s', t')

Proof state:
s t : ℤ
r' : ℕ
s' t' : ℤ
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')

Tactic:
simp [xgcdAux]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem isComplete_image_iff {m : α → β} {s : Set α} (hm : IsUniformInducing m) :
    IsComplete (m '' s) ↔ IsComplete s

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ IsComplete (m '' s) ↔ IsComplete s

Tactic:
have fact2 : MapsTo (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := mapsTo_image .. |>.filter_map_Iic

Result:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ IsComplete (m '' s) ↔ IsComplete s

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ IsComplete (m '' s) ↔ IsComplete s

Tactic:
simp_rw [IsComplete, imp.swap (a := Cauchy _), ← mem_Iic (b := 𝓟 _), fact1.forall fact2,
  hm.cauchy_map_iff, exists_mem_image, map_le_iff_le_comap, hm.isInducing.nhds_eq_comap]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
⊢ IsComplete (m '' s) ↔ IsComplete s

Tactic:
have fact1 : SurjOn (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := surjOn_image .. |>.filter_map_Iic

Result:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ IsComplete (m '' s) ↔ IsComplete s
-- Mathlib/Analysis/Convex/Segment.lean
theorem image_segment (f : E →ᵃ[𝕜] F) (a b : E) : f '' [a -[𝕜] b] = [f a -[𝕜] f b] :=
  Set.ext fun x => by
    simp_rw [segment_eq_image_lineMap, mem_image, exists_exists_and_eq_and, AffineMap.apply_lineMap]

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ x ∈ ⇑f '' [a-[𝕜]b] ↔ x ∈ [f a-[𝕜]f b]

Tactic:
simp_rw [segment_eq_image_lineMap, mem_image, exists_exists_and_eq_and, AffineMap.apply_lineMap]

Result:
no goals
-- Mathlib/GroupTheory/Archimedean.lean
theorem Subgroup.cyclic_of_isolated_one {H : Subgroup G} {a : G} (h₀ : 1 < a)
    (hd : Disjoint (H : Set G) (Ioo 1 a)) : ∃ b, H = closure {b}

Proof state:
case inr
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hbot : H ≠ ⊥
⊢ ∃ b, H = closure {b}

Tactic:
exact (exists_isLeast_one_lt hbot h₀ hd).imp fun _ => cyclic_of_min

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
⊢ ∃ b, H = closure {b}

Tactic:
rcases eq_or_ne H ⊥ with rfl | hbot

Result:
case inl
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
a : G
h₀ : 1 < a
hd : Disjoint (↑⊥) (Ioo 1 a)
⊢ ∃ b, ⊥ = closure {b}

case inr
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hbot : H ≠ ⊥
⊢ ∃ b, H = closure {b}

Proof state:
case inl
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
a : G
h₀ : 1 < a
hd : Disjoint (↑⊥) (Ioo 1 a)
⊢ ∃ b, ⊥ = closure {b}

Tactic:
exact ⟨1, closure_singleton_one.symm⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem drop_replicate (a : α) : ∀ n m : Nat, drop n (replicate m a) = replicate (m - n) a
  | n, 0 => by simp
  | 0, m => by simp
  | succ n, succ m => by simp [replicate_succ, succ_sub_succ, drop_replicate]

Proof state:
α : Type u_1
a : α
m : Nat
⊢ drop 0 (replicate m a) = replicate (m - 0) a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
n m : Nat
⊢ drop n.succ (replicate m.succ a) = replicate (m.succ - n.succ) a

Tactic:
simp [replicate_succ, succ_sub_succ, drop_replicate]

Result:
no goals

Proof state:
α : Type u_1
a : α
n : Nat
⊢ drop n (replicate 0 a) = replicate (0 - n) a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem pi_div_two_le_two : π / 2 ≤ 2

Proof state:
⊢ π / 2 ≤ 2

Tactic:
rw [Real.pi, mul_div_cancel_left₀ _ (two_ne_zero' ℝ)]

Result:
⊢ Classical.choose exists_cos_eq_zero ≤ 2

Proof state:
⊢ Classical.choose exists_cos_eq_zero ≤ 2

Tactic:
exact (Classical.choose_spec exists_cos_eq_zero).1.2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_push_lt {v : Vector α n} {x : α} {i : Nat} (h : i < n) :
    (v.push x)[i] = v[i]

Proof state:
α : Type u_1
n : Nat
v : Vector α n
x : α
i : Nat
h : i < n
⊢ (v.push x)[i] = v[i]

Tactic:
rcases v with ⟨data, rfl⟩

Result:
case mk
α : Type u_1
x : α
i : Nat
data : Array α
h : i < data.size
⊢ ({ toArray := data, size_toArray := ⋯ }.push x)[i] = { toArray := data, size_toArray := ⋯ }[i]

Proof state:
case mk
α : Type u_1
x : α
i : Nat
data : Array α
h : i < data.size
⊢ ({ toArray := data, size_toArray := ⋯ }.push x)[i] = { toArray := data, size_toArray := ⋯ }[i]

Tactic:
simp [Array.getElem_push_lt, h]

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem replace_toFinmap (a : α) (b : β a) (s : AList β) :
    replace a b ⟦s⟧ = (⟦s.replace a b⟧ : Finmap β)

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ replace a b ⟦s⟧ = ⟦AList.replace a b s⟧

Tactic:
simp [replace]

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem integrable_stoppedProcess_of_mem_finset (hτ : IsStoppingTime ℱ τ)
    (hu : ∀ n, Integrable (u n) μ) (n : ι) {s : Finset ι} (hbdd : ∀ ω, τ ω < n → τ ω ∈ s) :
    Integrable (stoppedProcess u τ n) μ

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
⊢ Integrable (stoppedProcess u τ n) μ

Tactic:
simp_rw [← memLp_one_iff_integrable] at hu ⊢

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
hu : ∀ (n : ι), MemLp (u n) 1 μ
⊢ MemLp (stoppedProcess u τ n) 1 μ

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
hu : ∀ (n : ι), MemLp (u n) 1 μ
⊢ MemLp (stoppedProcess u τ n) 1 μ

Tactic:
exact memLp_stoppedProcess_of_mem_finset hτ hu n hbdd

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Free.lean
theorem basis_repr_symm_apply' (a : A) (i : ι) : a • basis A b i = a ⊗ₜ b i

Proof state:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
i : ι
⊢ a • (basis A b) i = a ⊗ₜ[R] b i

Tactic:
simpa using basis_repr_symm_apply b a i

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem Injective.nonempty_apply_iff {f : Set α → Set β} (hf : Injective f) (h2 : f ∅ = ∅)
    {s : Set α} : (f s).Nonempty ↔ s.Nonempty

Proof state:
α : Type u_1
β : Type u_2
f : Set α → Set β
hf : Injective f
h2 : f ∅ = ∅
s : Set α
⊢ (f s).Nonempty ↔ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty, ← h2, nonempty_iff_ne_empty, hf.ne_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem enorm_integral_le_lintegral_enorm (f : α → G) : ‖∫ a, f a ∂μ‖ₑ ≤ ∫⁻ a, ‖f a‖ₑ ∂μ

Proof state:
case h
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
exact norm_integral_le_lintegral_norm f

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ‖∫ (a : α), f a ∂μ‖ₑ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
simp_rw [← ofReal_norm_eq_enorm]

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ENNReal.ofReal ‖∫ (a : α), f a ∂μ‖ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ENNReal.ofReal ‖∫ (a : α), f a ∂μ‖ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ

Tactic:
apply ENNReal.ofReal_le_of_le_toReal

Result:
case h
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem smeval_C_mul (r : R) : (C r * f).smeval x = r • (f.smeval x)

Proof state:
case h_add
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (C r * p).smeval x = r • p.smeval x
hq : (C r * q).smeval x = r • q.smeval x
⊢ (C r * (p + q)).smeval x = r • (p + q).smeval x

Tactic:
rw [mul_add, smeval_add, smeval_add, smul_add, hp, hq]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
⊢ (C r * f).smeval x = r • f.smeval x

Tactic:
induction f using LaurentPolynomial.induction_on' with
| h_add p q hp hq=>
  rw [mul_add, smeval_add, smeval_add, smul_add, hp, hq]
| h_C_mul_T n s =>
  rw [← mul_assoc, ← map_mul, smeval_C_mul_T_n, smeval_C_mul_T_n, mul_smul]

Result:
no goals

Proof state:
case h_C_mul_T
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
n : ℤ
s : R
⊢ (C r * (C s * T n)).smeval x = r • (C s * T n).smeval x

Tactic:
rw [← mul_assoc, ← map_mul, smeval_C_mul_T_n, smeval_C_mul_T_n, mul_smul]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
@[simp] lemma commAlgEquiv_C (p) : commAlgEquiv R S₁ S₂ (.C p) = .map C p

Proof state:
case hf
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial S₂ R
x : S₂
⊢ ((↑(commAlgEquiv R S₁ S₂)).comp (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))))
      (X x) =
    (mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R))) (X x)

Tactic:
simp [commAlgEquiv]

Result:
no goals

Proof state:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial S₂ R
this :
  (↑(commAlgEquiv R S₁ S₂)).comp (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))) =
    mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R))
⊢ (commAlgEquiv R S₁ S₂) (C p) = (map C) p

Tactic:
exact DFunLike.congr_fun this p

Result:
no goals

Proof state:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial S₂ R
⊢ (commAlgEquiv R S₁ S₂) (C p) = (map C) p

Tactic:
suffices (commAlgEquiv R S₁ S₂).toAlgHom.comp
    (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) _) = mapAlgHom (Algebra.ofId _ _) by
  exact DFunLike.congr_fun this p

Result:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial S₂ R
⊢ (↑(commAlgEquiv R S₁ S₂)).comp (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))) =
    mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R))

Proof state:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial S₂ R
⊢ (↑(commAlgEquiv R S₁ S₂)).comp (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))) =
    mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R))

Tactic:
ext x : 1

Result:
case hf
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial S₂ R
x : S₂
⊢ ((↑(commAlgEquiv R S₁ S₂)).comp (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))))
      (X x) =
    (mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R))) (X x)
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem differentiableAt_mulExpNegMulSq (y : ℝ) :
    DifferentiableAt ℝ (mulExpNegMulSq ε) y :=
  DifferentiableAt.mul differentiableAt_id' (by fun_prop)

Proof state:
ε y : ℝ
⊢ DifferentiableAt ℝ (fun y => rexp (-(ε * y * y))) y

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
/-- Interpreting as a base `p` number and dividing by `p^i` is the same as dropping `i`.
-/
lemma ofDigits_div_pow_eq_ofDigits_drop
    {p : ℕ} (i : ℕ) (hpos : 0 < p) (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p) :
    ofDigits p digits / p ^ i = ofDigits p (digits.drop i)

Proof state:
p i : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)

Tactic:
induction' i with i hi

Result:
case zero
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits / p ^ 0 = ofDigits p (List.drop 0 digits)

case succ
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
⊢ ofDigits p digits / p ^ (i + 1) = ofDigits p (List.drop (i + 1) digits)

Proof state:
case succ
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
⊢ ofDigits p digits / p ^ (i + 1) = ofDigits p (List.drop (i + 1) digits)

Tactic:
rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi, ofDigits_div_eq_ofDigits_tail hpos
  (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ← List.drop_one,
  List.drop_drop, add_comm]

Result:
no goals

Proof state:
case zero
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits / p ^ 0 = ofDigits p (List.drop 0 digits)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeries.term_smul (f : ℕ → ℂ) (c s : ℂ) : term (c • f) s = c • term f s

Proof state:
f : ℕ → ℂ
c s : ℂ
⊢ term (c • f) s = c • term f s

Tactic:
ext ⟨- | n⟩ <;>
simp [mul_div_assoc]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem l_ciSup (gc : GaloisConnection l u) {f : ι → α} (hf : BddAbove (range f)) :
    l (⨆ i, f i) = ⨆ i, l (f i)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hf : BddAbove (range f)
⊢ l (⨆ i, f i) = ⨆ i, l (f i)

Tactic:
rw [iSup, gc.l_csSup (range_nonempty _) hf, iSup_range']

Result:
no goals
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem HasGradientWithinAt.congr (h : HasGradientWithinAt f f' s x) (hs : ∀ x ∈ s, f₁ x = f x)
    (hx : f₁ x = f x) : HasGradientWithinAt f₁ f' s x :=
  h.congr_mono hs hx (by tauto)

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
f' x : F
s : Set F
f₁ : F → 𝕜
h : HasGradientWithinAt f f' s x
hs : ∀ x ∈ s, f₁ x = f x
hx : f₁ x = f x
⊢ s ⊆ s

Tactic:
tauto

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem tendsto_comp_coe_Ioo_atBot (h : a < b) :
    Tendsto (fun x : Ioo a b => f x) atBot l ↔ Tendsto f (𝓝[>] a) l

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
l : Filter β
f : α → β
h : a < b
⊢ Tendsto (fun x => f ↑x) atBot l ↔ Tendsto (f ∘ Subtype.val) atBot l

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
l : Filter β
f : α → β
h : a < b
⊢ Tendsto (fun x => f ↑x) atBot l ↔ Tendsto f (𝓝[>] a) l

Tactic:
rw [← map_coe_Ioo_atBot h, tendsto_map'_iff]

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
l : Filter β
f : α → β
h : a < b
⊢ Tendsto (fun x => f ↑x) atBot l ↔ Tendsto (f ∘ Subtype.val) atBot l