harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem le_iff_forall_one_lt_le_mul₀ {α : Type*} [LinearOrderedSemifield α]
    {a b : α} (hb : 0 ≤ b) : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε

Proof state:
α : Type u_4
inst✝ : LinearOrderedSemifield α
a b : α
hb : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
⊢ a ≤ b

Tactic:
obtain rfl|hb := hb.eq_or_lt

Result:
case inl
α : Type u_4
inst✝ : LinearOrderedSemifield α
a : α
hb : 0 ≤ 0
h : ∀ (ε : α), 1 < ε → a ≤ 0 * ε
⊢ a ≤ 0

case inr
α : Type u_4
inst✝ : LinearOrderedSemifield α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
⊢ a ≤ b

Proof state:
case inl
α : Type u_4
inst✝ : LinearOrderedSemifield α
a : α
hb : 0 ≤ 0
h : ∀ (ε : α), 1 < ε → a ≤ 0
⊢ a ≤ 0

Tactic:
exact h 2 one_lt_two

Result:
no goals

Proof state:
case h.e'_4
α : Type u_4
inst✝ : LinearOrderedSemifield α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
x : α
hbx : b < x
⊢ x = b * (x / b)

Tactic:
rw [mul_div_cancel₀ _ hb.ne']

Result:
no goals

Proof state:
α : Type u_4
inst✝ : LinearOrderedSemifield α
a b : α
hb : 0 ≤ b
⊢ a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε

Tactic:
refine ⟨fun h _ hε ↦ h.trans <| le_mul_of_one_le_right hb hε.le, fun h ↦ ?_⟩

Result:
α : Type u_4
inst✝ : LinearOrderedSemifield α
a b : α
hb : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
⊢ a ≤ b

Proof state:
case inr
α : Type u_4
inst✝ : LinearOrderedSemifield α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
⊢ a ≤ b

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun x hbx => ?_

Result:
case inr
α : Type u_4
inst✝ : LinearOrderedSemifield α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
x : α
hbx : b < x
⊢ a ≤ x

Proof state:
case inr
α : Type u_4
inst✝ : LinearOrderedSemifield α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
x : α
hbx : b < x
⊢ a ≤ x

Tactic:
convert h (x / b) ((one_lt_div hb).mpr hbx)

Result:
case h.e'_4
α : Type u_4
inst✝ : LinearOrderedSemifield α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
x : α
hbx : b < x
⊢ x = b * (x / b)

Proof state:
case inl
α : Type u_4
inst✝ : LinearOrderedSemifield α
a : α
hb : 0 ≤ 0
h : ∀ (ε : α), 1 < ε → a ≤ 0 * ε
⊢ a ≤ 0

Tactic:
simp_rw [zero_mul] at h

Result:
case inl
α : Type u_4
inst✝ : LinearOrderedSemifield α
a : α
hb : 0 ≤ 0
h : ∀ (ε : α), 1 < ε → a ≤ 0
⊢ a ≤ 0
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean
theorem hasTerminal_of_hasTerminal_of_preservesLimit [PreservesLimit (Functor.empty.{0} C) G] :
    HasTerminal D := ⟨fun F => by
  haveI := HasLimit.mk ⟨_, isLimitOfHasTerminalOfPreservesLimit G⟩
  apply hasLimitOfIso F.uniqueFromEmpty.symm⟩

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : PreservesLimit (Functor.empty C) G
F : Discrete PEmpty.{1} ⥤ D
this : HasLimit (Functor.empty D)
⊢ HasLimit F

Tactic:
apply hasLimitOfIso F.uniqueFromEmpty.symm

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : PreservesLimit (Functor.empty C) G
F : Discrete PEmpty.{1} ⥤ D
⊢ HasLimit F

Tactic:
haveI := HasLimit.mk ⟨_, isLimitOfHasTerminalOfPreservesLimit G⟩

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : PreservesLimit (Functor.empty C) G
F : Discrete PEmpty.{1} ⥤ D
this : HasLimit (Functor.empty D)
⊢ HasLimit F
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem map_zero : map I (0 : M →ₗ[R] N) = 0

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ map I 0 = 0

Tactic:
ext

Result:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a✝ : AdicCauchySequence I M
n✝ : ℕ
⊢ ↑((map I 0) ((mk I M) a✝)) n✝ = ↑(0 ((mk I M) a✝)) n✝

Proof state:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a✝ : AdicCauchySequence I M
n✝ : ℕ
⊢ ↑((map I 0) ((mk I M) a✝)) n✝ = ↑(0 ((mk I M) a✝)) n✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem degree_linear (ha : a ≠ 0) : degree (C a * X + C b) = 1

Proof state:
R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X + C b).degree = 1

Tactic:
rw [degree_add_eq_left_of_degree_lt <| degree_C_lt_degree_C_mul_X ha, degree_C_mul_X ha]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
lemma map_pmap {Q : β → Prop} (f : α → β) (g : ∀ b, Q b → γ) (z : Sym2 α) (h : ∀ b ∈ z.map f, Q b):
    (z.map f).pmap g h =
    z.pmap (fun a ha => g (f a) (h (f a) (mem_map.mpr ⟨a, ha, rfl⟩))) (fun _ ha => ha)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
Q : β → Prop
f : α → β
g : (b : β) → Q b → γ
z : Sym2 α
h : ∀ b ∈ map f z, Q b
⊢ pmap g (map f z) h = pmap (fun a ha => g (f a) ⋯) z ⋯

Tactic:
induction' z with x y

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
Q : β → Prop
f : α → β
g : (b : β) → Q b → γ
x y : α
h : ∀ b ∈ map f s(x, y), Q b
⊢ pmap g (map f s(x, y)) h = pmap (fun a ha => g (f a) ⋯) s(x, y) ⋯

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
Q : β → Prop
f : α → β
g : (b : β) → Q b → γ
x y : α
h : ∀ b ∈ map f s(x, y), Q b
⊢ pmap g (map f s(x, y)) h = pmap (fun a ha => g (f a) ⋯) s(x, y) ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem norm_iteratedFDeriv_le_seminorm (f : 𝓢(E, F)) (n : ℕ) (x₀ : E) :
    ‖iteratedFDeriv ℝ n f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 n) f

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
x₀ : E
⊢ ‖iteratedFDeriv ℝ n (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 n) f

Tactic:
have := SchwartzMap.le_seminorm 𝕜 0 n f x₀

Result:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
x₀ : E
this : ‖x₀‖ ^ 0 * ‖iteratedFDeriv ℝ n (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 n) f
⊢ ‖iteratedFDeriv ℝ n (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 n) f

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
x₀ : E
this : ‖x₀‖ ^ 0 * ‖iteratedFDeriv ℝ n (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 n) f
⊢ ‖iteratedFDeriv ℝ n (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 n) f

Tactic:
rwa [pow_zero, one_mul] at this

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem Surjective.image_surjective (hf : Surjective f) : Surjective (image f)

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ f '' (f ⁻¹' s) = s

Tactic:
rw [hf.image_preimage]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ Surjective (image f)

Tactic:
intro s

Result:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ ∃ a, f '' a = s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ ∃ a, f '' a = s

Tactic:
use f ⁻¹' s

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ f '' (f ⁻¹' s) = s
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma _root_.MeasureTheory.AEStronglyMeasurable.ae_of_compProd [SFinite μ] [IsSFiniteKernel κ]
    {E : Type*} [NormedAddCommGroup E] {f : α → β → E}
    (hf : AEStronglyMeasurable f.uncurry (μ ⊗ₘ κ)) :
    ∀ᵐ x ∂μ, AEStronglyMeasurable (f x) (κ x)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : IsSFiniteKernel κ
E : Type u_3
inst✝ : NormedAddCommGroup E
f : α → β → E
hf : AEStronglyMeasurable (Function.uncurry f) (μ ⊗ₘ κ)
⊢ ∀ᵐ (x : α) ∂μ, AEStronglyMeasurable (f x) (κ x)

Tactic:
simpa using hf.compProd_mk_left

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem map_const : p.map (Function.const α b) = pure b

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
b : β
⊢ map (Function.const α b) p = pure b

Tactic:
simp only [map, Function.comp_def, bind_const, Function.const]

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem ofFn_const : ∀ (n : ℕ) (c : α), (ofFn fun _ : Fin n => c) = replicate n c
  | 0, c => by rw [ofFn_zero, replicate_zero]
  | n+1, c => by rw [replicate, ← ofFn_const n]; simp

Proof state:
α : Type u
n : ℕ
c : α
⊢ (ofFn fun x => c) = replicate (n + 1) c

Tactic:
rw [replicate, ← ofFn_const n]

Result:
α : Type u
n : ℕ
c : α
⊢ (ofFn fun x => c) = c :: ofFn fun x => c

Proof state:
α : Type u
c : α
⊢ (ofFn fun x => c) = replicate 0 c

Tactic:
rw [ofFn_zero, replicate_zero]

Result:
no goals

Proof state:
α : Type u
n : ℕ
c : α
⊢ (ofFn fun x => c) = c :: ofFn fun x => c

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma mutuallySingular_of_mutuallySingular_compProd {ξ : Measure α}
    [SFinite μ] [SFinite ν] [IsSFiniteKernel κ] [IsSFiniteKernel η]
    (h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η) (hμ : ξ ≪ μ) (hν : ξ ≪ ν) :
    ∀ᵐ x ∂ξ, κ x ⟂ₘ η x

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : (fun a => (κ a) (Prod.mk a ⁻¹' h.nullSet)) =ᶠ[ae μ] 0
hν_zero : ∫⁻ (a : α), (η a) (Prod.mk a ⁻¹' h.nullSetᶜ) ∂ν = 0
⊢ AEMeasurable (fun a => (η a) (Prod.mk a ⁻¹' h.nullSetᶜ)) ν

Tactic:
exact (Kernel.measurable_kernel_prod_mk_left hs.compl).aemeasurable

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : (fun a => (κ a) (Prod.mk a ⁻¹' h.nullSet)) =ᶠ[ae μ] 0
hν_zero : (fun a => (η a) (Prod.mk a ⁻¹' h.nullSetᶜ)) =ᶠ[ae ν] 0
x : α
hxμ : (κ x) (Prod.mk x ⁻¹' h.nullSet) = 0 x
hxν : (η x) (Prod.mk x ⁻¹' h.nullSetᶜ) = 0 x
⊢ κ x ⟂ₘ η x

Tactic:
exact ⟨Prod.mk x ⁻¹' h.nullSet, measurable_prod_mk_left hs, ⟨hxμ, hxν⟩⟩

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem permutationsAux2_comp_append {t : α} {ts ys : List α} {r : List β} (f : List α → β) :
    ((permutationsAux2 t [] r ys) fun x => f (x ++ ts)).2 = (permutationsAux2 t ts r ys f).2

Proof state:
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t [] r [] fun x => f (x ++ ts)).2 = (permutationsAux2 t ts r [] f).2

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih : ∀ (f : List α → β), (permutationsAux2 t [] r tail✝ fun x => f (x ++ ts)).2 = (permutationsAux2 t ts r tail✝ f).2
f : List α → β
⊢ (permutationsAux2 t [] r (ys_hd :: tail✝) fun x => f (x ++ ts)).2 = (permutationsAux2 t ts r (ys_hd :: tail✝) f).2

Tactic:
simp [ys_ih fun xs => f (ys_hd :: xs)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t [] r ys fun x => f (x ++ ts)).2 = (permutationsAux2 t ts r ys f).2

Tactic:
induction' ys with ys_hd _ ys_ih generalizing f

Result:
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t [] r [] fun x => f (x ++ ts)).2 = (permutationsAux2 t ts r [] f).2

case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih : ∀ (f : List α → β), (permutationsAux2 t [] r tail✝ fun x => f (x ++ ts)).2 = (permutationsAux2 t ts r tail✝ f).2
f : List α → β
⊢ (permutationsAux2 t [] r (ys_hd :: tail✝) fun x => f (x ++ ts)).2 = (permutationsAux2 t ts r (ys_hd :: tail✝) f).2
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsBigO.multisetProd {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜]
    {s : Multiset ι} {f : ι → α → R} {g : ι → α → 𝕜} (hf : ∀ i ∈ s, f i =O[l] g i) :
    (fun x ↦ (s.map (f · x)).prod) =O[l] (fun x ↦ (s.map (g · x)).prod)

Proof state:
case intro
α : Type u_1
l✝ : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst✝¹ : SeminormedCommRing R
inst✝ : NormedField 𝕜
f : ι → α → R
g : ι → α → 𝕜
l : List ι
hf : ∀ i ∈ ↑l, f i =O[l✝] g i
⊢ (fun x => (Multiset.map (fun x_1 => f x_1 x) ↑l).prod) =O[l✝] fun x => (Multiset.map (fun x_1 => g x_1 x) ↑l).prod

Tactic:
exact mod_cast IsBigO.listProd hf

Result:
no goals

Proof state:
α : Type u_1
l : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst✝¹ : SeminormedCommRing R
inst✝ : NormedField 𝕜
s : Multiset ι
f : ι → α → R
g : ι → α → 𝕜
hf : ∀ i ∈ s, f i =O[l] g i
⊢ (fun x => (Multiset.map (fun x_1 => f x_1 x) s).prod) =O[l] fun x => (Multiset.map (fun x_1 => g x_1 x) s).prod

Tactic:
obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s

Result:
case intro
α : Type u_1
l✝ : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst✝¹ : SeminormedCommRing R
inst✝ : NormedField 𝕜
f : ι → α → R
g : ι → α → 𝕜
l : List ι
hf : ∀ i ∈ ↑l, f i =O[l✝] g i
⊢ (fun x => (Multiset.map (fun x_1 => f x_1 x) ↑l).prod) =O[l✝] fun x => (Multiset.map (fun x_1 => g x_1 x) ↑l).prod
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_countable' [Countable α] [MeasurableSingletonClass α] {μ : Measure α}
    {f : α → E} (hf : Integrable f μ) :
    ∫ a, f a ∂μ = ∑' a, (μ {a}).toReal • f a

Proof state:
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝² : NormedSpace ℝ E
m : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
f : α → E
hf : Integrable f (Measure.sum fun a => μ {a} • Measure.dirac a)
⊢ ∑' (i : α), ∫ (a : α), f a ∂μ {i} • Measure.dirac i =
    ∑' (a : α), ((Measure.sum fun a => μ {a} • Measure.dirac a) {a}).toReal • f a

Tactic:
congr 1 with a : 1

Result:
case e_f.h
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝² : NormedSpace ℝ E
m : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
f : α → E
hf : Integrable f (Measure.sum fun a => μ {a} • Measure.dirac a)
a : α
⊢ ∫ (a : α), f a ∂μ {a} • Measure.dirac a = ((Measure.sum fun a => μ {a} • Measure.dirac a) {a}).toReal • f a

Proof state:
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝² : NormedSpace ℝ E
m : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
f : α → E
hf : Integrable f (Measure.sum fun a => μ {a} • Measure.dirac a)
⊢ ∫ (a : α), f a ∂μ = ∑' (a : α), (μ {a}).toReal • f a

Tactic:
rw [← Measure.sum_smul_dirac μ, integral_sum_measure hf]

Result:
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝² : NormedSpace ℝ E
m : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
f : α → E
hf : Integrable f (Measure.sum fun a => μ {a} • Measure.dirac a)
⊢ ∑' (i : α), ∫ (a : α), f a ∂μ {i} • Measure.dirac i =
    ∑' (a : α), ((Measure.sum fun a => μ {a} • Measure.dirac a) {a}).toReal • f a

Proof state:
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝² : NormedSpace ℝ E
m : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
f : α → E
hf : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = ∑' (a : α), (μ {a}).toReal • f a

Tactic:
rw [← Measure.sum_smul_dirac μ] at hf

Result:
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝² : NormedSpace ℝ E
m : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
f : α → E
hf : Integrable f (Measure.sum fun a => μ {a} • Measure.dirac a)
⊢ ∫ (a : α), f a ∂μ = ∑' (a : α), (μ {a}).toReal • f a

Proof state:
case e_f.h
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝² : NormedSpace ℝ E
m : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
f : α → E
hf : Integrable f (Measure.sum fun a => μ {a} • Measure.dirac a)
a : α
⊢ ∫ (a : α), f a ∂μ {a} • Measure.dirac a = ((Measure.sum fun a => μ {a} • Measure.dirac a) {a}).toReal • f a

Tactic:
rw [integral_smul_measure, integral_dirac, Measure.sum_smul_dirac]

Result:
no goals
-- Mathlib/NumberTheory/Multiplicity.lean
theorem Int.emultiplicity_pow_add_pow {x y : ℤ} (hxy : ↑p ∣ x + y) (hx : ¬↑p ∣ x)
    {n : ℕ} (hn : Odd n) :
    emultiplicity (↑p) (x ^ n + y ^ n) = emultiplicity (↑p) (x + y) + emultiplicity p n

Proof state:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x + y
hx : ¬↑p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity (↑p) (x ^ n + y ^ n) = emultiplicity (↑p) (x + y) + emultiplicity p n

Tactic:
rw [← sub_neg_eq_add] at hxy

Result:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - -y
hx : ¬↑p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity (↑p) (x ^ n + y ^ n) = emultiplicity (↑p) (x + y) + emultiplicity p n

Proof state:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - -y
hx : ¬↑p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity (↑p) (x ^ n - (-y) ^ n) = emultiplicity (↑p) (x - -y) + emultiplicity p n

Tactic:
exact Int.emultiplicity_pow_sub_pow hp hp1 hxy hx n

Result:
no goals

Proof state:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - -y
hx : ¬↑p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity (↑p) (x ^ n + y ^ n) = emultiplicity (↑p) (x + y) + emultiplicity p n

Tactic:
rw [← sub_neg_eq_add, ← sub_neg_eq_add, ← Odd.neg_pow hn]

Result:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - -y
hx : ¬↑p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity (↑p) (x ^ n - (-y) ^ n) = emultiplicity (↑p) (x - -y) + emultiplicity p n
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem pullback_map_self [HasPullbacks C] (f : X ⟶ Y) [Mono f] (g : Subobject X) :
    (pullback f).obj ((map f).obj g) = g

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasPullbacks C
f : X ⟶ Y
inst✝ : Mono f
⊢ ∀ (g : Subobject X), (pullback f).obj ((map f).obj g) = g

Tactic:
exact Quotient.ind (fun g' => Quotient.sound ⟨(MonoOver.pullbackMapSelf f).app _⟩)

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasPullbacks C
f : X ⟶ Y
inst✝ : Mono f
g : Subobject X
⊢ (pullback f).obj ((map f).obj g) = g

Tactic:
revert g

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasPullbacks C
f : X ⟶ Y
inst✝ : Mono f
⊢ ∀ (g : Subobject X), (pullback f).obj ((map f).obj g) = g
-- Mathlib/Data/Set/Function.lean
theorem InjOn.exists_subset_injOn_subset_range_eq {r : Set α} (hinj : InjOn f r) (hrs : r ⊆ s) :
    ∃ u : Set α, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → β
r : Set α
hinj : InjOn f r
hrs : r ⊆ s
u : Set α
hru : r ⊆ u
hus : u ⊆ s
h : BijOn f u (f '' s)
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u

Tactic:
exact ⟨u, hru, hus, h.image_eq, h.injOn⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
r : Set α
hinj : InjOn f r
hrs : r ⊆ s
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u

Tactic:
obtain ⟨u, hru, hus, h⟩ := hinj.bijOn_image.exists_extend_of_subset hrs
  (image_subset f hrs) Subset.rfl

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → β
r : Set α
hinj : InjOn f r
hrs : r ⊆ s
u : Set α
hru : r ⊆ u
hus : u ⊆ s
h : BijOn f u (f '' s)
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u
-- 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 images of `f` are disjoint on `I`, and `g ⊥ = 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 images of `f` are disjoint on `I`, and `g ⊥ = 0`. The
conclusion is the same as in `sum_image`."
]
lemma prod_image_of_disjoint [CommMonoid β] [PartialOrder α] [OrderBot α] {f : ι → α} {g : α → β}
    (hg_bot : g ⊥ = 1) {I : Finset ι} (hf_disj : (I : Set ι).PairwiseDisjoint f) :
    ∏ 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 β
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
f : ι → α
g : α → β
hg_bot : g ⊥ = 1
I : Finset ι
hf_disj : (↑I).PairwiseDisjoint f
i j : ι
hdisj : Disjoint (f i) (f j)
hfij : f i = f j
⊢ g (f i) = 1

Tactic:
rw [← hfij, disjoint_self] at hdisj

Result:
α : Type u_6
β : Type u_7
ι : Type u_8
inst✝³ : DecidableEq α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
f : ι → α
g : α → β
hg_bot : g ⊥ = 1
I : Finset ι
hf_disj : (↑I).PairwiseDisjoint f
i j : ι
hdisj : f i = ⊥
hfij : f i = f j
⊢ g (f i) = 1

Proof state:
α : Type u_6
β : Type u_7
ι : Type u_8
inst✝³ : DecidableEq α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
f : ι → α
g : α → β
hg_bot : g ⊥ = 1
I : Finset ι
hf_disj : (↑I).PairwiseDisjoint f
⊢ ∏ s ∈ image f I, g s = ∏ i ∈ I, g (f i)

Tactic:
refine prod_image_of_pairwise_eq_one <| hf_disj.imp fun i j (hdisj : Disjoint _ _) hfij ↦ ?_

Result:
α : Type u_6
β : Type u_7
ι : Type u_8
inst✝³ : DecidableEq α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
f : ι → α
g : α → β
hg_bot : g ⊥ = 1
I : Finset ι
hf_disj : (↑I).PairwiseDisjoint f
i j : ι
hdisj : Disjoint (f i) (f j)
hfij : f i = f j
⊢ g (f i) = 1

Proof state:
α : Type u_6
β : Type u_7
ι : Type u_8
inst✝³ : DecidableEq α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
f : ι → α
g : α → β
hg_bot : g ⊥ = 1
I : Finset ι
hf_disj : (↑I).PairwiseDisjoint f
i j : ι
hdisj : f i = ⊥
hfij : f i = f j
⊢ g (f i) = 1

Tactic:
rw [hdisj, hg_bot]

Result:
no goals