harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem NNReal.lintegral_mul_le_Lp_mul_Lq {p q : ℝ} (hpq : p.IsConjExponent q) {f g : α → ℝ≥0}
    (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    (∫⁻ a, (f * g) a ∂μ) ≤
      (∫⁻ a, (f a : ℝ≥0∞) ^ p ∂μ) ^ (1 / p) * (∫⁻ a, (g a : ℝ≥0∞) ^ q ∂μ) ^ (1 / q)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), ↑(f a) * ↑(g a) ∂μ ≤ (∫⁻ (a : α), ↑(f a) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑(g a) ^ q ∂μ) ^ (1 / q)

Tactic:
exact ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq hf.coe_nnreal_ennreal hg.coe_nnreal_ennreal

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), ↑((f * g) a) ∂μ ≤ (∫⁻ (a : α), ↑(f a) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑(g a) ^ q ∂μ) ^ (1 / q)

Tactic:
simp_rw [Pi.mul_apply, ENNReal.coe_mul]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), ↑(f a) * ↑(g a) ∂μ ≤ (∫⁻ (a : α), ↑(f a) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑(g a) ^ q ∂μ) ^ (1 / q)
-- Mathlib/Probability/Kernel/Condexp.lean
lemma condExp_set_generateFrom_singleton (hs : MeasurableSet s) (ht : MeasurableSet t) :
    μ⟦t | generateFrom {s}⟧ =ᵐ[μ.restrict s] fun _ ↦ (μ[t|s]).toReal

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ[t.indicator fun ω => 1|MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun x =>
    ∫ (x : Ω), t.indicator 1 x ∂μ[|s]

Tactic:
exact condExp_generateFrom_singleton hs <| Integrable.indicator (integrable_const 1) ht

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ[t.indicator fun ω => 1|MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun x => μ[t | s].toReal

Tactic:
rw [← integral_indicator_one ht]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ[t.indicator fun ω => 1|MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun x =>
    ∫ (x : Ω), t.indicator 1 x ∂μ[|s]
-- Mathlib/Data/Nat/Factorization/Basic.lean
@[simp]
lemma factorizationLCRight_zero_left : factorizationLCMRight 0 b = 1

Proof state:
b : ℕ
⊢ factorizationLCMRight 0 b = 1

Tactic:
simp [factorizationLCMRight]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem associator_inv_naturality_middle (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) :
    f ◁ η ▷ h ≫ (α_ f g' h).inv = (α_ f g h).inv ≫ (f ◁ η) ▷ h

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ f ◁ η ▷ h ≫ (α_ f g' h).inv = (α_ f g h).inv ≫ (f ◁ η) ▷ h

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Ideal/Pointwise.lean
theorem subset_pointwise_smul_iff {a : M} {S T : Ideal R} : S ≤ a • T ↔ a⁻¹ • S ≤ T

Proof state:
M : Type u_1
R : Type u_2
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S T : Ideal R
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T

Tactic:
rw [← pointwise_smul_le_pointwise_smul_iff (a := a⁻¹), inv_smul_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem getElem_unattach
    {p : α → Prop} {l : List { x // p x }} (i : Nat) (h : i < l.unattach.length) :
    l.unattach[i] = (l[i]'(by simpa using h)).1

Proof state:
α : Type ?u.89766
p : α → Prop
l : List { x // p x }
i : Nat
h : i < l.unattach.length
⊢ i < l.length

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
i : Nat
h : i < l.unattach.length
⊢ l.unattach[i] = l[i].val

Tactic:
simp [unattach]

Result:
no goals
-- Mathlib/Data/Multiset/Lattice.lean
theorem sup_le {s : Multiset α} {a : α} : s.sup ≤ a ↔ ∀ b ∈ s, b ≤ a :=
  Multiset.induction_on s (by simp)
    (by simp +contextual [or_imp, forall_and])

Proof state:
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Multiset α
a : α
⊢ ∀ (a_1 : α) (s : Multiset α), (s.sup ≤ a ↔ ∀ b ∈ s, b ≤ a) → ((a_1 ::ₘ s).sup ≤ a ↔ ∀ b ∈ a_1 ::ₘ s, b ≤ a)

Tactic:
simp +contextual [or_imp, forall_and]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Multiset α
a : α
⊢ sup 0 ≤ a ↔ ∀ b ∈ 0, b ≤ a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem getElem_pmap {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α n)
    (hp : ∀ x ∈ v.toList, p x) {i : ℕ} (hi : i < n) :
    (v.pmap f hp)[i] = f v[i] (hp _ (by simp [getElem_def, List.getElem_mem]))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α n
hp : ∀ x ∈ v.toList, p x
i : ℕ
hi : i < n
⊢ v[i] ∈ v.toList

Tactic:
simp [getElem_def, List.getElem_mem]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α n
hp : ∀ x ∈ v.toList, p x
i : ℕ
hi : i < n
⊢ (pmap f v hp)[i] = f v[i] ⋯

Tactic:
simp only [getElem_def, toList_pmap, List.getElem_pmap]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_eq_U_sub_X_mul_U (n : ℤ) : T R n = U R n - X * U R (n - 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R n = U R n - X * U R (n - 1)

Tactic:
linear_combination (norm := ring_nf) - U_eq_X_mul_U_add_T R (n - 1)

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
theorem dual_ordConnectedSection (s : Set α) :
    ordConnectedSection (ofDual ⁻¹' s) = ofDual ⁻¹' ordConnectedSection s

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ (range fun x => ⋯.some) = ⇑ofDual ⁻¹' range fun x => ⋯.some

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : αᵒᵈ
⊢ (x ∈ range fun x => ⋯.some) ↔ x ∈ ⇑ofDual ⁻¹' range fun x => ⋯.some

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : αᵒᵈ
⊢ (x ∈ range fun x => ⋯.some) ↔ x ∈ ⇑ofDual ⁻¹' range fun x => ⋯.some

Tactic:
simp only [mem_range, Subtype.exists, mem_preimage, OrderDual.exists, dual_ordConnectedComponent,
  ofDual_toDual]

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : αᵒᵈ
⊢ (∃ a, ∃ (h : a ∈ s), ⋯.some = x) ↔ ∃ a, ∃ (h : a ∈ s), ⋯.some = ofDual x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ range (⇑ofDual ⁻¹' s).ordConnectedProj = ⇑ofDual ⁻¹' range s.ordConnectedProj

Tactic:
simp (config := { unfoldPartialApp := true }) only [ordConnectedProj]

Result:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ (range fun x => ⋯.some) = ⇑ofDual ⁻¹' range fun x => ⋯.some

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ (⇑ofDual ⁻¹' s).ordConnectedSection = ⇑ofDual ⁻¹' s.ordConnectedSection

Tactic:
simp only [ordConnectedSection]

Result:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ range (⇑ofDual ⁻¹' s).ordConnectedProj = ⇑ofDual ⁻¹' range s.ordConnectedProj

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : αᵒᵈ
⊢ (∃ a, ∃ (h : a ∈ s), ⋯.some = x) ↔ ∃ a, ∃ (h : a ∈ s), ⋯.some = ofDual x

Tactic:
tauto

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem uniformly_extend_spec [CompleteSpace γ] (a : α) : Tendsto f (comap e (𝓝 a)) (𝓝 (ψ a))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : IsUniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
a : α
⊢ Tendsto f (comap e (𝓝 a)) (𝓝 (⋯.extend f a))

Tactic:
simpa only [IsDenseInducing.extend] using
  tendsto_nhds_limUnder (uniformly_extend_exists h_e ‹_› h_f _)

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_cofinite_zero_of_tsum_ne_top {α} {f : α → ℝ≥0∞} (hf : ∑' x, f x ≠ ∞) :
    Tendsto f cofinite (𝓝 0)

Proof state:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ⊤
f_ne_top : ∀ (n : α), f n ≠ ⊤
h_f_coe : f = fun n => ↑(f n).toNNReal
⊢ Tendsto (fun n => (f n).toNNReal) cofinite (𝓝 0)

Tactic:
exact NNReal.tendsto_cofinite_zero_of_summable (summable_toNNReal_of_tsum_ne_top hf)

Result:
no goals

Proof state:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ⊤
f_ne_top : ∀ (n : α), f n ≠ ⊤
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
have h_f_coe : f = fun n => ((f n).toNNReal : ENNReal) :=
  funext fun n => (coe_toNNReal (f_ne_top n)).symm

Result:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ⊤
f_ne_top : ∀ (n : α), f n ≠ ⊤
h_f_coe : f = fun n => ↑(f n).toNNReal
⊢ Tendsto f cofinite (𝓝 0)

Proof state:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ⊤
f_ne_top : ∀ (n : α), f n ≠ ⊤
h_f_coe : f = fun n => ↑(f n).toNNReal
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
rw [h_f_coe, ← @coe_zero, tendsto_coe]

Result:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ⊤
f_ne_top : ∀ (n : α), f n ≠ ⊤
h_f_coe : f = fun n => ↑(f n).toNNReal
⊢ Tendsto (fun n => (f n).toNNReal) cofinite (𝓝 0)

Proof state:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ⊤
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
have f_ne_top : ∀ n, f n ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top hf

Result:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ⊤
f_ne_top : ∀ (n : α), f n ≠ ⊤
⊢ Tendsto f cofinite (𝓝 0)
-- Mathlib/Probability/Kernel/WithDensity.lean
@[simp]
lemma withDensity_one (κ : Kernel α β) [IsSFiniteKernel κ] :
    Kernel.withDensity κ 1 = κ

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.withDensity 1) a✝¹) s✝ = (κ a✝¹) s✝

Tactic:
rw [Kernel.withDensity_apply _ measurable_const]

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a✝¹).withDensity (1 a✝¹)) s✝ = (κ a✝¹) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a✝¹).withDensity (1 a✝¹)) s✝ = (κ a✝¹) s✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ κ.withDensity 1 = κ

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.withDensity 1) a✝¹) s✝ = (κ a✝¹) s✝
-- Mathlib/Analysis/Seminorm.lean
theorem finset_sup_le_sum (p : ι → Seminorm 𝕜 E) (s : Finset ι) : s.sup p ≤ ∑ i ∈ s, p i

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
⊢ s.sup p ≤ ∑ i ∈ s, p i

Tactic:
refine Finset.sup_le_iff.mpr ?_

Result:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
⊢ ∀ b ∈ s, p b ≤ ∑ i ∈ s, p i

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
⊢ s.sup p ≤ ∑ i ∈ s, p i

Tactic:
classical
refine Finset.sup_le_iff.mpr ?_
intro i hi
rw [Finset.sum_eq_sum_diff_singleton_add hi, le_add_iff_nonneg_left]
exact bot_le

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
⊢ ∀ b ∈ s, p b ≤ ∑ i ∈ s, p i

Tactic:
intro i hi

Result:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
i : ι
hi : i ∈ s
⊢ p i ≤ ∑ i ∈ s, p i

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
i : ι
hi : i ∈ s
⊢ 0 ≤ ∑ x ∈ s \ {i}, p x

Tactic:
exact bot_le

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
i : ι
hi : i ∈ s
⊢ p i ≤ ∑ i ∈ s, p i

Tactic:
rw [Finset.sum_eq_sum_diff_singleton_add hi, le_add_iff_nonneg_left]

Result:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
i : ι
hi : i ∈ s
⊢ 0 ≤ ∑ x ∈ s \ {i}, p x
-- Mathlib/Order/LiminfLimsup.lean
theorem limsInf_top : limsInf (⊤ : Filter α) = ⊥ :=
  bot_unique <| sSup_le <| by simpa [eq_univ_iff_forall] using fun b hb => bot_unique <| hb _

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
⊢ ∀ b ∈ {a | ∀ᶠ (n : α) in ⊤, a ≤ n}, b ≤ ⊥

Tactic:
simpa [eq_univ_iff_forall] using fun b hb => bot_unique <| hb _

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
lemma zeta_mul_zeta [Semiring 𝕜] [Preorder α] [LocallyFiniteOrder α] [DecidableRel (α := α) (· ≤ ·)]
    (a b : α) : (zeta 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) a b = (Icc a b).card

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1

Tactic:
rw [mem_Icc] at hx

Result:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1

Tactic:
rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
⊢ (zeta 𝕜 * zeta 𝕜) a b = ↑(#(Icc a b))

Tactic:
rw [mul_apply, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one]

Result:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, 1

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, 1

Tactic:
refine sum_congr rfl fun x hx ↦ ?_

Result:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive sum_lt_sum]
lemma prod_lt_prod' (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
    (s.map f).prod < (s.map g).prod

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : OrderedCancelCommMonoid α
s : Multiset ι
f g : ι → α
hle : ∀ i ∈ s, f i ≤ g i
hlt : ∃ i ∈ s, f i < g i
⊢ (map f s).prod < (map g s).prod

Tactic:
obtain ⟨l⟩ := s

Result:
case mk
ι : Type u_1
α : Type u_2
inst✝ : OrderedCancelCommMonoid α
s : Multiset ι
f g : ι → α
l : List ι
hle : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, f i ≤ g i
hlt : ∃ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, f i < g i
⊢ (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod < (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Proof state:
case mk
ι : Type u_1
α : Type u_2
inst✝ : OrderedCancelCommMonoid α
s : Multiset ι
f g : ι → α
l : List ι
hle : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, f i ≤ g i
hlt : ∃ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, f i < g i
⊢ (List.map f l).prod < (List.map g l).prod

Tactic:
exact List.prod_lt_prod' f g hle hlt

Result:
no goals

Proof state:
case mk
ι : Type u_1
α : Type u_2
inst✝ : OrderedCancelCommMonoid α
s : Multiset ι
f g : ι → α
l : List ι
hle : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, f i ≤ g i
hlt : ∃ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, f i < g i
⊢ (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod < (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]

Result:
case mk
ι : Type u_1
α : Type u_2
inst✝ : OrderedCancelCommMonoid α
s : Multiset ι
f g : ι → α
l : List ι
hle : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, f i ≤ g i
hlt : ∃ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, f i < g i
⊢ (List.map f l).prod < (List.map g l).prod
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem map_mod (a : Fin n.succ → ℕ) : map d a % d = a 0 % d

Proof state:
n d : ℕ
a : Fin n.succ → ℕ
⊢ (map d) a % d = a 0 % d

Tactic:
rw [map_succ, Nat.add_mul_mod_self_right]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mulPosMono_iff_covariant_pos :
    MulPosMono α ↔ CovariantClass α>0 α (fun x y => y * x) (· ≤ ·) :=
  ⟨@MulPosMono.to_covariantClass_pos_mul_le _ _ _ _, fun h =>
    { elim a b c h

Proof state:
case inl
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : CovariantClass α>0 α (fun x y => y * ↑x) fun x1 x2 => x1 ≤ x2
a : α≥0
b c : α
h : b ≤ c
ha : 0 = ↑a
⊢ b * ↑a ≤ c * ↑a

Tactic:
simp [← ha]

Result:
no goals

Proof state:
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : CovariantClass α>0 α (fun x y => y * ↑x) fun x1 x2 => x1 ≤ x2
a : α≥0
b c : α
h : b ≤ c
⊢ b * ↑a ≤ c * ↑a

Tactic:
obtain ha | ha := a.prop.eq_or_lt

Result:
case inl
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : CovariantClass α>0 α (fun x y => y * ↑x) fun x1 x2 => x1 ≤ x2
a : α≥0
b c : α
h : b ≤ c
ha : 0 = ↑a
⊢ b * ↑a ≤ c * ↑a

case inr
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : CovariantClass α>0 α (fun x y => y * ↑x) fun x1 x2 => x1 ≤ x2
a : α≥0
b c : α
h : b ≤ c
ha : 0 < ↑a
⊢ b * ↑a ≤ c * ↑a
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
lemma one_le_thickenedIndicator_apply' {X : Type _} [PseudoEMetricSpace X]
    {δ : ℝ} (δ_pos : 0 < δ) {F : Set X} {x : X} (hxF : x ∈ closure F) :
    1 ≤ thickenedIndicator δ_pos F x

Proof state:
X : Type u_2
inst✝ : PseudoEMetricSpace X
δ : ℝ
δ_pos : 0 < δ
F : Set X
x : X
hxF : x ∈ closure F
⊢ 1 ≤ (thickenedIndicator δ_pos F) x

Tactic:
rw [thickenedIndicator_one_of_mem_closure δ_pos F hxF]

Result:
no goals
-- Mathlib/Data/ENNReal/Holder.lean
lemma eq_top_iff_eq_one : p = ∞ ↔ q = 1

Proof state:
case mpr
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ q = 1 → p = ⊤

Tactic:
rintro rfl

Result:
case mpr
p : ℝ≥0∞
inst✝ : p.HolderConjugate 1
⊢ p = ⊤

Proof state:
case mp
q : ℝ≥0∞
inst✝ : ⊤.HolderConjugate q
⊢ (1 - ⊤⁻¹)⁻¹ = 1

Tactic:
simp

Result:
no goals

Proof state:
case mpr
p : ℝ≥0∞
inst✝ : p.HolderConjugate 1
⊢ p = ⊤

Tactic:
rw [← inv_inv p, ← one_sub_inv 1 p]

Result:
case mpr
p : ℝ≥0∞
inst✝ : p.HolderConjugate 1
⊢ (1 - 1⁻¹)⁻¹ = ⊤

Proof state:
case mpr
p : ℝ≥0∞
inst✝ : p.HolderConjugate 1
⊢ (1 - 1⁻¹)⁻¹ = ⊤

Tactic:
simp

Result:
no goals

Proof state:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ p = ⊤ ↔ q = 1

Tactic:
constructor

Result:
case mp
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ p = ⊤ → q = 1

case mpr
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ q = 1 → p = ⊤

Proof state:
case mp
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ p = ⊤ → q = 1

Tactic:
rintro rfl

Result:
case mp
q : ℝ≥0∞
inst✝ : ⊤.HolderConjugate q
⊢ q = 1

Proof state:
case mp
q : ℝ≥0∞
inst✝ : ⊤.HolderConjugate q
⊢ q = 1

Tactic:
rw [← inv_inv q, ← one_sub_inv ∞ q]

Result:
case mp
q : ℝ≥0∞
inst✝ : ⊤.HolderConjugate q
⊢ (1 - ⊤⁻¹)⁻¹ = 1
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
@[to_additive (attr := simp) abs_zsmul_eq_zero]
lemma zpow_abs_eq_one (a : G) (n : ℤ) : a ^ |n| = 1 ↔ a ^ n = 1

Proof state:
G : Type u_1
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ |n| = 1 ↔ a ^ n = 1

Tactic:
rw [← Int.natCast_natAbs, zpow_natCast, pow_natAbs_eq_one]

Result:
no goals
-- Mathlib/RingTheory/Trace/Defs.lean
theorem trace_algebraMap_of_basis (b : Basis ι R S) (x : R) :
    trace R S (algebraMap R S x) = Fintype.card ι • x

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ (trace R S) ((algebraMap R S) x) = Fintype.card ι • x

Tactic:
rw [trace_apply, LinearMap.trace_eq_matrix_trace R b, Matrix.trace]

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ ∑ i : ι, ((toMatrix b b) ((lmul R S) ((algebraMap R S) x))).diag i = Fintype.card ι • x

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
⊢ (trace R S) ((algebraMap R S) x) = Fintype.card ι • x

Tactic:
haveI := Classical.decEq ι

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ (trace R S) ((algebraMap R S) x) = Fintype.card ι • x

Proof state:
case h.e'_2.a
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ ((toMatrix b b) ((lmul R S) ((algebraMap R S) x))).diag x✝ = x

Tactic:
simp [-coe_lmul_eq_mul]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ ∑ i : ι, ((toMatrix b b) ((lmul R S) ((algebraMap R S) x))).diag i = Fintype.card ι • x

Tactic:
convert Finset.sum_const x

Result:
case h.e'_2.a
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ ((toMatrix b b) ((lmul R S) ((algebraMap R S) x))).diag x✝ = x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.insertManyIfNewUnit_val {ρ : Type w} [ForIn Id ρ α] [BEq α] [Hashable α]
    {m : Raw₀ α (fun _ => Unit)} {l : ρ} :
    Raw.Const.insertManyIfNewUnit m.val l = Raw₀.Const.insertManyIfNewUnit m l

Proof state:
α : Type u
ρ : Type w
inst✝² : ForIn Id ρ α
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
l : ρ
⊢ Raw.Const.insertManyIfNewUnit m.val l = (Raw₀.Const.insertManyIfNewUnit m l).val.val

Tactic:
simp [Raw.Const.insertManyIfNewUnit, m.2]

Result:
no goals