harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Ring/Seminorm.lean
/-- Triangle inequality for `MulRingNorm` applied to a list. -/
@[deprecated "Use AbsoluteValue.listSum_le instead" (since := "2025-01-07")]
lemma mulRingNorm_sum_le_sum_mulRingNorm {R : Type*} [NonAssocRing R] (l : List R)
    (f : MulRingNorm R) : f l.sum ≤ (l.map f).sum

Proof state:
case nil
R : Type u_2
inst✝ : NonAssocRing R
f : MulRingNorm R
⊢ f [].sum ≤ (List.map ⇑f []).sum

Tactic:
simp only [List.sum_nil, map_zero, List.map_nil, le_refl]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : NonAssocRing R
l : List R
f : MulRingNorm R
⊢ f l.sum ≤ (List.map (⇑f) l).sum

Tactic:
induction l with
| nil => simp only [List.sum_nil, map_zero, List.map_nil, le_refl]
| cons head tail ih =>
  simp only [List.sum_cons, List.map_cons]
  calc f (head + List.sum tail) ≤ f head + f (List.sum tail) := by apply f.add_le'
    _ ≤ f head + List.sum (List.map f tail) := by simp only [add_le_add_iff_left, ih]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : NonAssocRing R
f : MulRingNorm R
head : R
tail : List R
ih : f tail.sum ≤ (List.map (⇑f) tail).sum
⊢ f head + f tail.sum ≤ f head + (List.map (⇑f) tail).sum

Tactic:
simp only [add_le_add_iff_left, ih]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : NonAssocRing R
f : MulRingNorm R
head : R
tail : List R
ih : f tail.sum ≤ (List.map (⇑f) tail).sum
⊢ f (head + tail.sum) ≤ f head + f tail.sum

Tactic:
apply f.add_le'

Result:
no goals

Proof state:
case cons
R : Type u_2
inst✝ : NonAssocRing R
f : MulRingNorm R
head : R
tail : List R
ih : f tail.sum ≤ (List.map (⇑f) tail).sum
⊢ f (head + tail.sum) ≤ f head + (List.map (⇑f) tail).sum

Tactic:
calc f (head + List.sum tail) ≤ f head + f (List.sum tail) := by apply f.add_le'
  _ ≤ f head + List.sum (List.map f tail) := by simp only [add_le_add_iff_left, ih]

Result:
no goals

Proof state:
case cons
R : Type u_2
inst✝ : NonAssocRing R
f : MulRingNorm R
head : R
tail : List R
ih : f tail.sum ≤ (List.map (⇑f) tail).sum
⊢ f (head :: tail).sum ≤ (List.map (⇑f) (head :: tail)).sum

Tactic:
simp only [List.sum_cons, List.map_cons]

Result:
case cons
R : Type u_2
inst✝ : NonAssocRing R
f : MulRingNorm R
head : R
tail : List R
ih : f tail.sum ≤ (List.map (⇑f) tail).sum
⊢ f (head + tail.sum) ≤ f head + (List.map (⇑f) tail).sum
-- Mathlib/Algebra/Lie/Free.lean
theorem hom_ext {F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L} (h : ∀ x, F₁ (of R x) = F₂ (of R x)) :
    F₁ = F₂ :=
  have h' : (lift R).symm F₁ = (lift R).symm F₂

Proof state:
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L
h : ∀ (x : X), F₁ (of R x) = F₂ (of R x)
⊢ (lift R).symm F₁ = (lift R).symm F₂

Tactic:
ext

Result:
case h
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L
h : ∀ (x : X), F₁ (of R x) = F₂ (of R x)
x✝ : X
⊢ (lift R).symm F₁ x✝ = (lift R).symm F₂ x✝

Proof state:
case h
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L
h : ∀ (x : X), F₁ (of R x) = F₂ (of R x)
x✝ : X
⊢ (lift R).symm F₁ x✝ = (lift R).symm F₂ x✝

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem card_support_eq {n : ℕ} :
    #f.support = n ↔
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ i, x i ≠ 0),
        f = ∑ i, C (x i) * X ^ k i

Proof state:
case zero
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ #f.support = 0 → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin 0), x i ≠ 0), f = ∑ i : Fin 0, C (x i) * X ^ k i

Tactic:
exact fun hf => ⟨0, 0, fun x => x.elim0, fun x => x.elim0, card_support_eq_zero.mp hf⟩

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem range_eq_map_top (φ : A →⋆ₐ[R] B) : φ.range = (⊤ : StarSubalgebra R A).map φ :=
  StarSubalgebra.ext fun x =>
    ⟨by rintro ⟨a, ha⟩; exact ⟨a, by simp, ha⟩, by rintro ⟨a, -, ha⟩; exact ⟨a, ha⟩⟩

Proof state:
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
a : A
ha : φ.toRingHom a = x
⊢ a ∈ ↑⊤.toSubsemiring

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
a : A
ha : ↑φ.toAlgHom a = x
⊢ x ∈ φ.range

Tactic:
exact ⟨a, ha⟩

Result:
no goals

Proof state:
case intro
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
a : A
ha : φ.toRingHom a = x
⊢ x ∈ map φ ⊤

Tactic:
exact ⟨a, by simp, ha⟩

Result:
no goals

Proof state:
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
⊢ x ∈ map φ ⊤ → x ∈ φ.range

Tactic:
rintro ⟨a, -, ha⟩

Result:
case intro.intro
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
a : A
ha : ↑φ.toAlgHom a = x
⊢ x ∈ φ.range

Proof state:
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
⊢ x ∈ φ.range → x ∈ map φ ⊤

Tactic:
rintro ⟨a, ha⟩

Result:
case intro
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
a : A
ha : φ.toRingHom a = x
⊢ x ∈ map φ ⊤
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem map_inv_of_isOneCocycle {f : G → A} (hf : IsOneCocycle f) (g : G) :
    g • f g⁻¹ = - f g

Proof state:
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G → A
hf : IsOneCocycle f
g : G
⊢ g • f g⁻¹ = -f g

Tactic:
rw [← add_eq_zero_iff_eq_neg, ← map_one_of_isOneCocycle hf, ← mul_inv_cancel g, hf g g⁻¹]

Result:
no goals
-- Mathlib/Order/Filter/IndicatorFunction.lean
theorem Monotone.mulIndicator_eventuallyEq_iUnion {ι} [Preorder ι] [One β] (s : ι → Set α)
    (hs : Monotone s) (f : α → β) (a : α) :
    (fun i => mulIndicator (s i) f a) =ᶠ[atTop] fun _ ↦ mulIndicator (⋃ i, s i) f a

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ (fun i => (s i).mulIndicator f a) =ᶠ[atTop] fun x => (⋃ i, s i).mulIndicator f a

Tactic:
exact hs.piecewise_eventually_eq_iUnion f 1 a

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ (fun i => (s i).mulIndicator f a) =ᶠ[atTop] fun x => (⋃ i, s i).mulIndicator f a

Tactic:
classical exact hs.piecewise_eventually_eq_iUnion f 1 a

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcd_eq_gcd_ab : (gcd x y : ℤ) = x * gcdA x y + y * gcdB x y

Proof state:
x y : ℕ
⊢ ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y

Tactic:
have := @xgcdAux_P x y x y 1 0 0 1 (by simp [P]) (by simp [P])

Result:
x y : ℕ
this : Nat.P x y (x.xgcdAux 1 0 y 0 1)
⊢ ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y

Proof state:
x y : ℕ
⊢ Nat.P x y (y, 0, 1)

Tactic:
simp [P]

Result:
no goals

Proof state:
x y : ℕ
⊢ Nat.P x y (x, 1, 0)

Tactic:
simp [P]

Result:
no goals

Proof state:
x y : ℕ
this : Nat.P x y (x.xgcdAux 1 0 y 0 1)
⊢ ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y

Tactic:
rwa [xgcdAux_val, xgcd_val] at this

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem IsOpen.lowerSemicontinuous_indicator (hs : IsOpen s) (hy : 0 ≤ y) :
    LowerSemicontinuous (indicator s fun _x => y)

Proof state:
case neg
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < s.indicator (fun _x => y) x'

Tactic:
refine Filter.Eventually.of_forall fun x' => ?_

Result:
case neg
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
⊢ z < s.indicator (fun _x => y) x'

Proof state:
case pos
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < s.indicator (fun _x => y) x'

Tactic:
filter_upwards [hs.mem_nhds h]

Result:
case h
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ a ∈ s, z < s.indicator (fun _x => y) a

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
hz : z < s.indicator (fun _x => y) x
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < s.indicator (fun _x => y) x'

Tactic:
by_cases h : x ∈ s <;> simp [h] at hz

Result:
case pos
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < s.indicator (fun _x => y) x'

case neg
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < s.indicator (fun _x => y) x'

Proof state:
case neg
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
⊢ z < s.indicator (fun _x => y) x'

Tactic:
by_cases h' : x' ∈ s <;> simp [h', hz.trans_le hy, hz]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ a ∈ s, z < s.indicator (fun _x => y) a

Tactic:
simp +contextual [hz]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
⊢ LowerSemicontinuous (s.indicator fun _x => y)

Tactic:
intro x z hz

Result:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
hz : z < s.indicator (fun _x => y) x
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < s.indicator (fun _x => y) x'
-- Mathlib/Data/Int/Interval.lean
theorem card_Ioo_of_lt (h : a < b) : (#(Ioo a b) : ℤ) = b - a - 1

Proof state:
a b : ℤ
h : a < b
⊢ ↑(#(Ioo a b)) = b - a - 1

Tactic:
rw [card_Ioo, sub_sub, toNat_sub_of_le h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem size_filterMap_eq_countP (f : α → Option β) (l : Array α) :
    (filterMap f l).size = countP (fun a => (f a).isSome) l

Proof state:
case mk
α : Type u_2
β : Type u_1
f : α → Option β
toList✝ : List α
⊢ (filterMap f { toList := toList✝ }).size = countP (fun a => (f a).isSome) { toList := toList✝ }

Tactic:
simp [List.length_filterMap_eq_countP]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
f : α → Option β
l : Array α
⊢ (filterMap f l).size = countP (fun a => (f a).isSome) l

Tactic:
cases l

Result:
case mk
α : Type u_2
β : Type u_1
f : α → Option β
toList✝ : List α
⊢ (filterMap f { toList := toList✝ }).size = countP (fun a => (f a).isSome) { toList := toList✝ }
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
/-- A version of `Finset.prod_map` and `Finset.prod_image`, but we do not assume that `f` is
injective. Rather, we assume that the image of `f` on `I` only overlaps where `g (f i) = 1`.
The conclusion is the same as in `prod_image`. -/
@[to_additive (attr := simp)
"A version of `Finset.sum_map` and `Finset.sum_image`, but we do not assume that `f` is
injective. Rather, we assume that the image of `f` on `I` only overlaps where `g (f i) = 0`.
The conclusion is the same as in `sum_image`."]
lemma prod_image_of_pairwise_eq_one [CommMonoid β] {f : ι → α} {g : α → β} {I : Finset ι}
    (hf : (I : Set ι).Pairwise fun i j ↦ f i = f j → g (f i) = 1) :
    ∏ s ∈ I.image f, g s = ∏ i ∈ I, g (f i)

Proof state:
α : Type u_6
β : Type u_7
ι : Type u_8
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
f : ι → α
g : α → β
I : Finset ι
hf : (↑I).Pairwise fun i j => f i = f j → g (f i) = 1
⊢ ∏ s ∈ image f I, g s = ∏ i ∈ I, g (f i)

Tactic:
rw [prod_image']

Result:
case eq
α : Type u_6
β : Type u_7
ι : Type u_8
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
f : ι → α
g : α → β
I : Finset ι
hf : (↑I).Pairwise fun i j => f i = f j → g (f i) = 1
⊢ ∀ i ∈ I, g (f i) = ∏ j ∈ filter (fun j => f j = f i) I, g (f j)

Proof state:
case eq
α : Type u_6
β : Type u_7
ι : Type u_8
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
f : ι → α
g : α → β
I : Finset ι
hf : (↑I).Pairwise fun i j => f i = f j → g (f i) = 1
⊢ ∀ i ∈ I, g (f i) = ∏ j ∈ filter (fun j => f j = f i) I, g (f j)

Tactic:
exact fun n hnI => (prod_filter_of_pairwise_eq_one hnI hf).symm

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isNClique_bot_iff : (⊥ : SimpleGraph α).IsNClique n s ↔ n ≤ 1 ∧ #s = n

Proof state:
α : Type u_1
n : ℕ
s : Finset α
⊢ ⊥.IsNClique n s ↔ n ≤ 1 ∧ #s = n

Tactic:
rw [isNClique_iff, isClique_bot_iff]

Result:
α : Type u_1
n : ℕ
s : Finset α
⊢ (↑s).Subsingleton ∧ #s = n ↔ n ≤ 1 ∧ #s = n

Proof state:
α : Type u_1
s : Finset α
⊢ (↑s).Subsingleton ↔ #s ≤ 1

Tactic:
exact card_le_one.symm

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
s : Finset α
⊢ (↑s).Subsingleton ∧ #s = n ↔ n ≤ 1 ∧ #s = n

Tactic:
refine and_congr_left ?_

Result:
α : Type u_1
n : ℕ
s : Finset α
⊢ #s = n → ((↑s).Subsingleton ↔ n ≤ 1)

Proof state:
α : Type u_1
n : ℕ
s : Finset α
⊢ #s = n → ((↑s).Subsingleton ↔ n ≤ 1)

Tactic:
rintro rfl

Result:
α : Type u_1
s : Finset α
⊢ (↑s).Subsingleton ↔ #s ≤ 1
-- Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
theorem tendsto_integral_exp_smul_cocompact_of_inner_product (μ : Measure V) [μ.IsAddHaarMeasure] :
    Tendsto (fun w : V →L[ℝ] ℝ => ∫ v, 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Proof state:
case hf
E : Type u_1
V : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
f : V → E
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
⊢ Tendsto (fun x => ∫ (v : V), 𝐞 (-x v) • f v ∂volume) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Tactic:
let A := (InnerProductSpace.toDual ℝ V).symm

Result:
case hf
E : Type u_1
V : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
f : V → E
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : NormedSpace.Dual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
⊢ Tendsto (fun x => ∫ (v : V), 𝐞 (-x v) • f v ∂volume) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Proof state:
E : Type u_1
V : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
f : V → E
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : NormedSpace.Dual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
⊢ (fun w => ∫ (v : V), 𝐞 (-w v) • f v) = (fun w => ∫ (v : V), 𝐞 (-inner v w) • f v) ∘ ⇑A

Tactic:
ext1 w

Result:
case h
E : Type u_1
V : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
f : V → E
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : NormedSpace.Dual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
w : V →L[ℝ] ℝ
⊢ ∫ (v : V), 𝐞 (-w v) • f v = ((fun w => ∫ (v : V), 𝐞 (-inner v w) • f v) ∘ ⇑A) w

Proof state:
case h
E : Type u_1
V : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
f : V → E
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : NormedSpace.Dual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
w : V →L[ℝ] ℝ
⊢ ∫ (v : V), 𝐞 (-w v) • f v = ((fun w => ∫ (v : V), 𝐞 (-inner v w) • f v) ∘ ⇑A) w

Tactic:
congr 1 with v : 1

Result:
case h.e_f.h
E : Type u_1
V : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
f : V → E
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : NormedSpace.Dual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
w : V →L[ℝ] ℝ
v : V
⊢ 𝐞 (-w v) • f v = 𝐞 (-inner v (A w)) • f v
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem associator_inv_naturality_left {X X' : C} (f : X ⟶ X') (Y Z : C) :
    f ▷ (Y ⊗ Z) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ f ▷ Y ▷ Z

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ f ▷ (Y ⊗ Z) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ f ▷ Y ▷ Z

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) :
    forIn l.toArray b f = forIn l b f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : List α
b : β
f : α → β → m (ForInStep β)
⊢ forIn l.toArray b f = forIn l b f

Tactic:
simpa using forIn'_toArray l b fun a m b => f a b

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem iterate_derivative_at_1_ne_zero [CharZero R] (n ν : ℕ) (h : ν ≤ n) :
    (Polynomial.derivative^[n - ν] (bernsteinPolynomial R n ν)).eval 1 ≠ 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval ν.succ (ascPochhammer ℕ (n - ν)) = 0

Tactic:
exact (ascPochhammer_pos _ _ (Nat.succ_pos ν)).ne'

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ eval 1 ((⇑derivative)^[n - ν] (bernsteinPolynomial R n ν)) ≠ 0

Tactic:
rw [bernsteinPolynomial.iterate_derivative_at_1 _ _ _ h, Ne, neg_one_pow_mul_eq_zero_iff, ←
  Nat.cast_succ, ← ascPochhammer_eval_cast, ← Nat.cast_zero, Nat.cast_inj]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval ν.succ (ascPochhammer ℕ (n - ν)) = 0
-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem ae_mem_limsup_atTop_iff (μ : Measure Ω) [IsFiniteMeasure μ] {s : ℕ → Set Ω}
    (hs : ∀ n, MeasurableSet[ℱ n] (s n)) : ∀ᵐ ω ∂μ, ω ∈ limsup s atTop ↔
    Tendsto (fun n => ∑ k ∈ Finset.range n,
      (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|ℱ k]) ω) atTop atTop

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ω ∈ {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator (fun x => 1) ω) atTop atTop} ↔
      Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑ℱ k]) ω) atTop atTop

Tactic:
exact tendsto_sum_indicator_atTop_iff' hs

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ω ∈ limsup s atTop ↔ Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑ℱ k]) ω) atTop atTop

Tactic:
rw [← limsup_nat_add s 1,
  Set.limsup_eq_tendsto_sum_indicator_atTop (zero_lt_one (α := ℝ)) (fun n ↦ s (n + 1))]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ω ∈ {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator (fun x => 1) ω) atTop atTop} ↔
      Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑ℱ k]) ω) atTop atTop
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem mul_ne_one : a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Proof state:
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
rw [not_iff_comm]

Result:
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
-- Mathlib/MeasureTheory/Integral/Asymptotics.lean
theorem LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_isNegInvariant
    [IsMeasurablyGenerated (atTop (α := α))] [MeasurableNeg α] [μ.IsNegInvariant]
    (hf : LocallyIntegrable f μ) (hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg) (ho : f =O[atTop] g)
    (hg : IntegrableAtFilter g atTop μ) : Integrable f μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁸ : TopologicalSpace α
inst✝⁷ : SecondCountableTopology α
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ Integrable f μ

Tactic:
have h_int := (hf.locallyIntegrableOn (Ici 0)).integrableOn_of_isBigO_atTop ho hg

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁸ : TopologicalSpace α
inst✝⁷ : SecondCountableTopology α
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ Integrable f μ
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem prime_pow (n : ℕ) : padicValNat p (p ^ n) = n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ padicValNat p (p ^ n) = n

Tactic:
rw [padicValNat.pow _ (@Fact.out p.Prime).ne_zero, padicValNat_self, mul_one]

Result:
no goals