harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem Filter.Tendsto.atBot_mul {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atBot)
    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atBot

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x => (Neg.neg ∘ f) x * g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot

Tactic:
simpa [Function.comp_def] using tendsto_neg_atTop_atBot.comp this

Result:
no goals

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => f x * g x) l atBot

Tactic:
have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul hC hg

Result:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x => (Neg.neg ∘ f) x * g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem exists_nonempty_inter_of_measure_univ_lt_sum_measure {m : MeasurableSpace α} (μ : Measure α)
    {s : Finset ι} {t : ι → Set α} (h : ∀ i ∈ s, NullMeasurableSet (t i) μ)
    (H : μ (univ : Set α) < ∑ i ∈ s, μ (t i)) :
    ∃ i ∈ s, ∃ j ∈ s, ∃ _h : i ≠ j, (t i ∩ t j).Nonempty

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : μ univ < ∑ i ∈ s, μ (t i)
⊢ ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty

Tactic:
contrapose! H

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → t i ∩ t j = ∅
⊢ ∑ i ∈ s, μ (t i) ≤ μ univ

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → t i ∩ t j = ∅
⊢ (↑s).Pairwise (AEDisjoint μ on t)

Tactic:
intro i hi j hj hij

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → t i ∩ t j = ∅
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
⊢ (AEDisjoint μ on t) i j

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → t i ∩ t j = ∅
⊢ ∑ i ∈ s, μ (t i) ≤ μ univ

Tactic:
apply sum_measure_le_measure_univ h

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → t i ∩ t j = ∅
⊢ (↑s).Pairwise (AEDisjoint μ on t)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → t i ∩ t j = ∅
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
⊢ (AEDisjoint μ on t) i j

Tactic:
exact (disjoint_iff_inter_eq_empty.mpr (H i hi j hj hij)).aedisjoint

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Support.lean
theorem HasCompactMulSupport.sup {f g : X → M} (hf : HasCompactMulSupport f)
    (hg : HasCompactMulSupport g) :  HasCompactMulSupport (f ⊔ g)

Proof state:
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeSup M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ mulTSupport (f ⊔ g) ⊆ mulTSupport f ∪ mulTSupport g

Tactic:
rw [mulTSupport, mulTSupport, mulTSupport, ← closure_union]

Result:
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeSup M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ closure (Function.mulSupport (f ⊔ g)) ⊆ closure (Function.mulSupport f ∪ Function.mulSupport g)

Proof state:
case h
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeSup M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ Function.mulSupport (f ⊔ g) ⊆ Function.mulSupport f ∪ Function.mulSupport g

Tactic:
exact Function.mulSupport_sup f g

Result:
no goals

Proof state:
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeSup M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ HasCompactMulSupport (f ⊔ g)

Tactic:
apply IsCompact.of_isClosed_subset (IsCompact.union hf hg) (isClosed_mulTSupport _)

Result:
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeSup M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ mulTSupport (f ⊔ g) ⊆ mulTSupport f ∪ mulTSupport g

Proof state:
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeSup M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ closure (Function.mulSupport (f ⊔ g)) ⊆ closure (Function.mulSupport f ∪ Function.mulSupport g)

Tactic:
apply closure_mono

Result:
case h
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeSup M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ Function.mulSupport (f ⊔ g) ⊆ Function.mulSupport f ∪ Function.mulSupport g
-- Mathlib/Data/Nat/Log.lean
theorem log_eq_one_iff' {b n : ℕ} : log b n = 1 ↔ b ≤ n ∧ n < b * b

Proof state:
b n : ℕ
⊢ log b n = 1 ↔ b ≤ n ∧ n < b * b

Tactic:
rw [log_eq_iff (Or.inl Nat.one_ne_zero), Nat.pow_add, Nat.pow_one]

Result:
no goals
-- Mathlib/Data/Finsupp/SMul.lean
theorem smul_single' {_ : Semiring R} (c : R) (a : α) (b : R) :
    c • Finsupp.single a b = Finsupp.single a (c * b)

Proof state:
α : Type u_1
R : Type u_6
x✝ : Semiring R
c : R
a : α
b : R
⊢ c • single a b = single a (c * b)

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_list_eq_sum_pow (α : Type u) : #(List α) = sum fun n : ℕ => #α ^ n :=
  calc
    #(List α) = #(Σn, List.Vector α n) := mk_congr (Equiv.sigmaFiberEquiv List.length).symm
    _ = sum fun n : ℕ => #α ^ n

Proof state:
α : Type u
⊢ #((n : ℕ) × List.Vector α n) = sum fun n => #α ^ n

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Dirac.lean
theorem mem_ae_dirac_iff {a : α} (hs : MeasurableSet s) : s ∈ ae (dirac a) ↔ a ∈ s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
⊢ s ∈ ae (dirac a) ↔ a ∈ s

Tactic:
by_cases a ∈ s <;> simp [mem_ae_iff, dirac_apply', hs.compl, indicator_apply, *]

Result:
no goals
-- Mathlib/NumberTheory/ZetaValues.lean
theorem hasDerivAt_bernoulliFun (k : ℕ) (x : ℝ) :
    HasDerivAt (bernoulliFun k) (k * bernoulliFun (k - 1) x) x

Proof state:
k : ℕ
x : ℝ
⊢ HasDerivAt (bernoulliFun k) (↑k * bernoulliFun (k - 1) x) x

Tactic:
convert ((Polynomial.bernoulli k).map <| algebraMap ℚ ℝ).hasDerivAt x using 1

Result:
case h.e'_9
k : ℕ
x : ℝ
⊢ ↑k * bernoulliFun (k - 1) x =
    Polynomial.eval x (Polynomial.derivative (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)))

Proof state:
case h.e'_9
k : ℕ
x : ℝ
⊢ ↑k * bernoulliFun (k - 1) x =
    Polynomial.eval x (Polynomial.derivative (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)))

Tactic:
simp only [bernoulliFun, Polynomial.derivative_map, Polynomial.derivative_bernoulli k,
  Polynomial.map_mul, Polynomial.map_natCast, Polynomial.eval_mul, Polynomial.eval_natCast]

Result:
no goals
-- Mathlib/Topology/Algebra/Support.lean
theorem is_one_at_infty {f : α → γ} [TopologicalSpace γ]
    (h : HasCompactMulSupport f) : Tendsto f (cocompact α) (𝓝 1)

Proof state:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ (mulTSupport f)ᶜ
⊢ 1 ∈ N

Tactic:
exact mem_of_mem_nhds hN

Result:
no goals

Proof state:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ (mulTSupport f)ᶜ ⊆ f ⁻¹' N

Tactic:
intro v hv

Result:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ (mulTSupport f)ᶜ
⊢ v ∈ f ⁻¹' N

Proof state:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ ∃ t, IsCompact t ∧ (f ⁻¹' N)ᶜ ⊆ t

Tactic:
refine ⟨mulTSupport f, h.isCompact, ?_⟩

Result:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ (f ⁻¹' N)ᶜ ⊆ mulTSupport f

Proof state:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
⊢ Tendsto f (cocompact α) (𝓝 1)

Tactic:
intro N hN

Result:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ N ∈ map f (cocompact α)

Proof state:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ (f ⁻¹' N)ᶜ ⊆ mulTSupport f

Tactic:
rw [compl_subset_comm]

Result:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ (mulTSupport f)ᶜ ⊆ f ⁻¹' N

Proof state:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ (mulTSupport f)ᶜ
⊢ v ∈ f ⁻¹' N

Tactic:
rw [mem_preimage, image_eq_one_of_nmem_mulTSupport hv]

Result:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ (mulTSupport f)ᶜ
⊢ 1 ∈ N

Proof state:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ N ∈ map f (cocompact α)

Tactic:
rw [mem_map, mem_cocompact']

Result:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ ∃ t, IsCompact t ∧ (f ⁻¹' N)ᶜ ⊆ t
-- Mathlib/Analysis/Normed/Operator/Banach.lean
theorem coe_ofSeqClosedGraph
    (hg : ∀ (u : ℕ → E) (x y), Tendsto u atTop (𝓝 x) → Tendsto (g ∘ u) atTop (𝓝 y) → y = g x) :
    ↑(ContinuousLinearMap.ofSeqClosedGraph hg) = g

Proof state:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x
x✝ : E
⊢ ↑(ofSeqClosedGraph hg) x✝ = g x✝

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x
⊢ ↑(ofSeqClosedGraph hg) = g

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x
x✝ : E
⊢ ↑(ofSeqClosedGraph hg) x✝ = g x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem isHashSelf_mapₘ [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β}
    {f : (a : α) → β a → δ a} (h : Raw.WFImp m.1) : IsHashSelf (m.mapₘ f).1.buckets

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → δ a
h : Raw.WFImp m.val
⊢ IsHashSelf (m.mapₘ f).val.buckets

Tactic:
refine h.buckets_hash_self.updateAllBuckets (fun l p hp => ?_)

Result:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → δ a
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × δ a
hp : p ∈ (AssocList.map f l).toList
⊢ containsKey p.fst l.toList = true

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → δ a
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × δ a
hp : p ∈ (AssocList.map f l).toList
⊢ containsKey p.fst l.toList = true

Tactic:
have hp := AssocList.toList_map.mem_iff.1 hp

Result:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → δ a
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × δ a
hp✝ : p ∈ (AssocList.map f l).toList
hp : p ∈ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l.toList
⊢ containsKey p.fst l.toList = true

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → δ a
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × δ a
hp✝ : p ∈ (AssocList.map f l).toList
hp : p ∈ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l.toList
⊢ containsKey p.fst l.toList = true

Tactic:
obtain ⟨p, hp₁, rfl⟩ := mem_map.1 hp

Result:
case intro.intro
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → δ a
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hp₁ : p ∈ l.toList
hp✝ : ⟨p.fst, f p.fst p.snd⟩ ∈ (AssocList.map f l).toList
hp : ⟨p.fst, f p.fst p.snd⟩ ∈ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l.toList
⊢ containsKey ⟨p.fst, f p.fst p.snd⟩.fst l.toList = true

Proof state:
case intro.intro
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → δ a
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hp₁ : p ∈ l.toList
hp✝ : ⟨p.fst, f p.fst p.snd⟩ ∈ (AssocList.map f l).toList
hp : ⟨p.fst, f p.fst p.snd⟩ ∈ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l.toList
⊢ containsKey ⟨p.fst, f p.fst p.snd⟩.fst l.toList = true

Tactic:
exact containsKey_of_mem hp₁

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem single_of_single_apply (a a' : α) (b : M) :
    single a ((single a' b) a) = single a' (single a' b) a

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
a✝ : α
h : ¬a' = a
⊢ (single a 0) a✝ = 0 a✝

Tactic:
rw [zero_apply, single_apply, ite_self]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
⊢ single a ((single a' b) a) = (single a' (single a' b)) a

Tactic:
rw [single_apply, single_apply]

Result:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
⊢ single a (if a' = a then b else 0) = if a' = a then single a' b else 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
⊢ single a (if a' = a then b else 0) = if a' = a then single a' b else 0

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
a✝ : α
⊢ (single a (if a' = a then b else 0)) a✝ = (if a' = a then single a' b else 0) a✝

Proof state:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
a✝ : α
h : a' = a
⊢ (single a b) a✝ = (single a' b) a✝

Tactic:
rw [h]

Result:
no goals

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
a✝ : α
⊢ (single a (if a' = a then b else 0)) a✝ = (if a' = a then single a' b else 0) a✝

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
a✝ : α
h : a' = a
⊢ (single a b) a✝ = (single a' b) a✝

case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
a✝ : α
h : ¬a' = a
⊢ (single a 0) a✝ = 0 a✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem IsPrefix.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁.erase a <+: l₂.erase a

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
h : l₁ <+: l₂
⊢ eraseP (fun x => x == a) l₁ <+: eraseP (fun x => x == a) l₂

Tactic:
exact h.eraseP

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
h : l₁ <+: l₂
⊢ l₁.erase a <+: l₂.erase a

Tactic:
simp only [erase_eq_eraseP']

Result:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
h : l₁ <+: l₂
⊢ eraseP (fun x => x == a) l₁ <+: eraseP (fun x => x == a) l₂
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem cos_eq_neg_one_iff {x : ℂ} : cos x = -1 ↔ ∃ k : ℤ, π + k * (2 * π) = x

Proof state:
x : ℂ
⊢ cos x = -1 ↔ ∃ k, ↑π + ↑k * (2 * ↑π) = x

Tactic:
rw [← neg_eq_iff_eq_neg, ← cos_sub_pi, cos_eq_one_iff]

Result:
x : ℂ
⊢ (∃ k, ↑k * (2 * ↑π) = x - ↑π) ↔ ∃ k, ↑π + ↑k * (2 * ↑π) = x

Proof state:
x : ℂ
⊢ (∃ k, ↑k * (2 * ↑π) = x - ↑π) ↔ ∃ k, ↑π + ↑k * (2 * ↑π) = x

Tactic:
simp only [eq_sub_iff_add_eq']

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
@[simp] lemma maxNilpotentSubmodule_eq_top_of_isNilpotent [LieModule.IsNilpotent L M] :
    maxNilpotentSubmodule R L M = ⊤

Proof state:
case a
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
⊢ ⊤ ∈ {N | IsNilpotent L ↥N}

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
⊢ ⊤ ≤ maxNilpotentSubmodule R L M

Tactic:
apply le_sSup

Result:
case a
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
⊢ ⊤ ∈ {N | IsNilpotent L ↥N}

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
⊢ maxNilpotentSubmodule R L M = ⊤

Tactic:
rw [eq_top_iff]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
⊢ ⊤ ≤ maxNilpotentSubmodule R L M
-- Mathlib/Data/Real/EReal.lean
lemma left_distrib_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) :
    c * (a + b) = c * a + c * b

Proof state:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = a * c + b * c

Tactic:
exact right_distrib_of_nonneg ha hb

Result:
no goals

Proof state:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = c * a + c * b

Tactic:
nth_rewrite 2 [EReal.mul_comm]

Result:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = a * c + c * b

Proof state:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = a * c + c * b

Tactic:
nth_rewrite 3 [EReal.mul_comm]

Result:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = a * c + b * c

Proof state:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ c * (a + b) = c * a + c * b

Tactic:
nth_rewrite 1 [EReal.mul_comm]

Result:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = c * a + c * b
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem pow_sub_le_descFactorial (n : ℕ) : ∀ k : ℕ, (n + 1 - k) ^ k ≤ n.descFactorial k
  | 0 => by rw [descFactorial_zero, Nat.pow_zero]
  | k + 1 => by
    rw [descFactorial_succ, Nat.pow_succ, succ_sub_succ, Nat.mul_comm]
    apply Nat.mul_le_mul_left
    exact (le_trans (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) k)
      (pow_sub_le_descFactorial n k))

Proof state:
case h
n k : ℕ
⊢ (n - k) ^ k ≤ n.descFactorial k

Tactic:
exact (le_trans (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) k)
  (pow_sub_le_descFactorial n k))

Result:
no goals

Proof state:
n k : ℕ
⊢ (n - k) * (n - k) ^ k ≤ (n - k) * n.descFactorial k

Tactic:
apply Nat.mul_le_mul_left

Result:
case h
n k : ℕ
⊢ (n - k) ^ k ≤ n.descFactorial k

Proof state:
n k : ℕ
⊢ (n + 1 - (k + 1)) ^ (k + 1) ≤ n.descFactorial (k + 1)

Tactic:
rw [descFactorial_succ, Nat.pow_succ, succ_sub_succ, Nat.mul_comm]

Result:
n k : ℕ
⊢ (n - k) * (n - k) ^ k ≤ (n - k) * n.descFactorial k

Proof state:
n : ℕ
⊢ (n + 1 - 0) ^ 0 ≤ n.descFactorial 0

Tactic:
rw [descFactorial_zero, Nat.pow_zero]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma ofENat_le_nat {m : ℕ∞} {n : ℕ} : ofENat m ≤ n ↔ m ≤ n

Proof state:
m : ℕ∞
n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Data/PEquiv.lean
theorem ofSet_eq_refl {s : Set α} [DecidablePred (· ∈ s)] :
    ofSet s = PEquiv.refl α ↔ s = Set.univ :=
  ⟨fun h => by
    rw [Set.eq_univ_iff_forall]
    intro
    rw [← mem_ofSet_self_iff, h]
    exact rfl, fun h => by simp only [← ofSet_univ, h]⟩

Proof state:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
h : ofSet s = PEquiv.refl α
x✝ : α
⊢ x✝ ∈ (PEquiv.refl α) x✝

Tactic:
exact rfl

Result:
no goals

Proof state:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
h : s = Set.univ
⊢ ofSet s = PEquiv.refl α

Tactic:
simp only [← ofSet_univ, h]

Result:
no goals

Proof state:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
h : ofSet s = PEquiv.refl α
⊢ ∀ (x : α), x ∈ s

Tactic:
intro

Result:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
h : ofSet s = PEquiv.refl α
x✝ : α
⊢ x✝ ∈ s

Proof state:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
h : ofSet s = PEquiv.refl α
⊢ s = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Result:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
h : ofSet s = PEquiv.refl α
⊢ ∀ (x : α), x ∈ s

Proof state:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
h : ofSet s = PEquiv.refl α
x✝ : α
⊢ x✝ ∈ s

Tactic:
rw [← mem_ofSet_self_iff, h]

Result:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
h : ofSet s = PEquiv.refl α
x✝ : α
⊢ x✝ ∈ (PEquiv.refl α) x✝
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem isFiniteMeasure_withDensity {f : α → ℝ≥0∞} (hf : ∫⁻ a, f a ∂μ ≠ ∞) :
    IsFiniteMeasure (μ.withDensity f) :=
  { measure_univ_lt_top

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
⊢ (μ.withDensity f) univ < ⊤

Tactic:
rwa [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ, lt_top_iff_ne_top]

Result:
no goals