harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma tilted_apply_eq_ofReal_integral [SFinite μ] (f : α → ℝ) (s : Set α) :
    μ.tilted f s = ENNReal.ofReal (∫ a in s, exp (f a) / ∫ x, exp (f x) ∂μ ∂μ)

Proof state:
case pos.f_nn
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (fun x => rexp (f x)) μ
⊢ 0 ≤ᶠ[ae (μ.restrict s)] fun a => rexp (f a) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
exact ae_of_all _ (fun _ ↦ by positivity)

Result:
no goals

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (fun x => rexp (f x)) μ
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Tactic:
rw [tilted_apply _ _, ← ofReal_integral_eq_lintegral_ofReal]

Result:
case pos.hfi
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (fun x => rexp (f x)) μ
⊢ Integrable (fun a => rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)

case pos.f_nn
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (fun x => rexp (f x)) μ
⊢ 0 ≤ᶠ[ae (μ.restrict s)] fun a => rexp (f a) / ∫ (x : α), rexp (f x) ∂μ

Proof state:
case pos.hfi
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (fun x => rexp (f x)) μ
⊢ Integrable (fun a => rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)

Tactic:
exact hf.integrableOn.div_const _

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (fun x => rexp (f x)) μ
x✝ : α
⊢ 0 x✝ ≤ (fun a => rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) x✝

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Tactic:
by_cases hf : Integrable (fun x ↦ exp (f x)) μ

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (fun x => rexp (f x)) μ
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : ¬Integrable (fun x => rexp (f x)) μ
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : ¬Integrable (fun x => rexp (f x)) μ
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Tactic:
simp [tilted_of_not_integrable hf, integral_undef hf]

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem keys_subset_keys_of_entries_subset_entries
    {s₁ s₂ : AList β} (h : s₁.entries ⊆ s₂.entries) : s₁.keys ⊆ s₂.keys

Proof state:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this : DecidableEq α := Classical.decEq α
⊢ k ∈ s₂.keys

Tactic:
have := h (mem_lookup_iff.1 (Option.get_mem (lookup_isSome.2 hk)))

Result:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : ⟨k, (lookup k s₁).get ⋯⟩ ∈ s₂.entries
⊢ k ∈ s₂.keys

Proof state:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : ⟨k, (lookup k s₁).get ⋯⟩ ∈ s₂.entries
⊢ k ∈ s₂.keys

Tactic:
rw [← mem_lookup_iff, Option.mem_def] at this

Result:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : lookup k s₂ = some ((lookup k s₁).get ⋯)
⊢ k ∈ s₂.keys

Proof state:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : lookup k s₂ = some ((lookup k s₁).get ⋯)
⊢ (some ((lookup k s₁).get ⋯)).isSome = true

Tactic:
exact Option.isSome_some

Result:
no goals

Proof state:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
⊢ k ∈ s₂.keys

Tactic:
letI : DecidableEq α := Classical.decEq α

Result:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this : DecidableEq α := Classical.decEq α
⊢ k ∈ s₂.keys

Proof state:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
⊢ s₁.keys ⊆ s₂.keys

Tactic:
intro k hk

Result:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
⊢ k ∈ s₂.keys

Proof state:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : lookup k s₂ = some ((lookup k s₁).get ⋯)
⊢ k ∈ s₂.keys

Tactic:
rw [← mem_keys, ← lookup_isSome, this]

Result:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : lookup k s₂ = some ((lookup k s₁).get ⋯)
⊢ (some ((lookup k s₁).get ⋯)).isSome = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem dvd_add_iff_left {k m n : Nat} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n

Proof state:
k m n : Nat
h : k ∣ n
⊢ k ∣ m ↔ k ∣ n + m

Tactic:
exact Nat.dvd_add_iff_right h

Result:
no goals

Proof state:
k m n : Nat
h : k ∣ n
⊢ k ∣ m ↔ k ∣ m + n

Tactic:
rw [Nat.add_comm]

Result:
k m n : Nat
h : k ∣ n
⊢ k ∣ m ↔ k ∣ n + m
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingDist_triangle (x y z : ∀ i, β i) :
    hammingDist x z ≤ hammingDist x y + hammingDist y z

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ #(filter (fun i => x i ≠ z i) univ) ≤ #(filter (fun i => x i ≠ y i) univ) + #(filter (fun i => y i ≠ z i) univ)

Tactic:
refine le_trans (card_mono ?_) (card_union_le _ _)

Result:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ filter (fun i => x i ≠ z i) univ ≤ filter (fun i => x i ≠ y i) univ ∪ filter (fun i => y i ≠ z i) univ

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ hammingDist x z ≤ hammingDist x y + hammingDist y z

Tactic:
classical
  unfold hammingDist
  refine le_trans (card_mono ?_) (card_union_le _ _)
  rw [← filter_or]
  exact monotone_filter_right _ fun i h ↦ (h.ne_or_ne _).imp_right Ne.symm

Result:
no goals

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ hammingDist x z ≤ hammingDist x y + hammingDist y z

Tactic:
unfold hammingDist

Result:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ #(filter (fun i => x i ≠ z i) univ) ≤ #(filter (fun i => x i ≠ y i) univ) + #(filter (fun i => y i ≠ z i) univ)

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ filter (fun i => x i ≠ z i) univ ≤ filter (fun a => x a ≠ y a ∨ y a ≠ z a) univ

Tactic:
exact monotone_filter_right _ fun i h ↦ (h.ne_or_ne _).imp_right Ne.symm

Result:
no goals

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ filter (fun i => x i ≠ z i) univ ≤ filter (fun i => x i ≠ y i) univ ∪ filter (fun i => y i ≠ z i) univ

Tactic:
rw [← filter_or]

Result:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ filter (fun i => x i ≠ z i) univ ≤ filter (fun a => x a ≠ y a ∨ y a ≠ z a) univ
-- Mathlib/Data/ZMod/Basic.lean
theorem natCast_comp_val [NeZero n] : ((↑) : ℕ → R) ∘ (val : ZMod n → ℕ) = cast

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero n
⊢ Nat.cast ∘ val = cast

Tactic:
cases n

Result:
case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero 0
⊢ Nat.cast ∘ val = cast

case succ
R : Type u_1
inst✝¹ : Ring R
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ Nat.cast ∘ val = cast

Proof state:
case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero 0
⊢ Nat.cast ∘ val = cast

Tactic:
cases NeZero.ne 0 rfl

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : Ring R
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ Nat.cast ∘ val = cast

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AddContent.lean
lemma addContent_union' (hs : s ∈ C) (ht : t ∈ C) (hst : s ∪ t ∈ C) (h_dis : Disjoint s t) :
    m (s ∪ t) = m s + m t

Proof state:
case h.e'_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
hs_eq_t : s = t
⊢ s = ∅

Tactic:
rw [← hs_eq_t] at h_dis

Result:
case h.e'_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s s
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
hs_eq_t : s = t
⊢ s = ∅
-- Mathlib/Data/Set/Monotone.lean
theorem _root_.StrictMonoOn.congr (h₁ : StrictMonoOn f₁ s) (h : s.EqOn f₁ f₂) :
    StrictMonoOn f₂ s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₁ a < f₁ b

Tactic:
exact h₁ ha hb hab

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₂ a < f₂ b

Tactic:
rw [← h ha, ← h hb]

Result:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₁ a < f₁ b

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
⊢ StrictMonoOn f₂ s

Tactic:
intro a ha b hb hab

Result:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₂ a < f₂ b
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem card_support_eraseLead_add_one (h : f ≠ 0) : #f.eraseLead.support + 1 = #f.support

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ n✝ + 1 - 1 + 1 = n✝ + 1

Tactic:
rfl

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ #f.eraseLead.support + 1 = n✝ + 1

Tactic:
case succ =>
  rw [eraseLead_support, card_erase_of_mem (natDegree_mem_support_of_nonzero h), ← hc, h₁]
  rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ #f.eraseLead.support + 1 = #f.support

Tactic:
set c := #f.support with hc

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
⊢ #f.eraseLead.support + 1 = c

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
x✝ : ¬#f.eraseLead.support + 1 = 0
⊢ False

Tactic:
exact h (card_support_eq_zero.mp h₁)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ #f.eraseLead.support + 1 = n✝ + 1

Tactic:
rw [eraseLead_support, card_erase_of_mem (natDegree_mem_support_of_nonzero h), ← hc, h₁]

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ n✝ + 1 - 1 + 1 = n✝ + 1

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
⊢ #f.eraseLead.support + 1 = c

Tactic:
cases h₁ : c

Result:
case zero
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
⊢ #f.eraseLead.support + 1 = 0

case succ
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ #f.eraseLead.support + 1 = n✝ + 1

Proof state:
case zero
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
⊢ #f.eraseLead.support + 1 = 0

case succ
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ #f.eraseLead.support + 1 = n✝ + 1

Tactic:
case zero =>
  by_contra
  exact h (card_support_eq_zero.mp h₁)

Result:
case succ
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ #f.eraseLead.support + 1 = n✝ + 1

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
⊢ #f.eraseLead.support + 1 = 0

Tactic:
by_contra

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
x✝ : ¬#f.eraseLead.support + 1 = 0
⊢ False
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem exists_smul_of_dvd_count (s : Multiset α) {k : ℕ}
    (h : ∀ a : α, a ∈ s → k ∣ Multiset.count a s) : ∃ u : Multiset α, s = k • u

Proof state:
α : Type u_3
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
x : α
hx : x ∈ s.toFinset
⊢ k • (count x s / k) • {x} = count x s • {x}

Tactic:
rw [← mul_nsmul', Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))]

Result:
no goals

Proof state:
case h
α : Type u_3
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ s = k • ∑ a ∈ s.toFinset, (count a s / k) • {a}

Tactic:
have h₂ :
  (∑ x ∈ s.toFinset, k • (count x s / k) • ({x} : Multiset α)) =
    ∑ x ∈ s.toFinset, count x s • {x} := by
  apply Finset.sum_congr rfl
  intro x hx
  rw [← mul_nsmul', Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))]

Result:
case h
α : Type u_3
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
h₂ : ∑ x ∈ s.toFinset, k • (count x s / k) • {x} = ∑ x ∈ s.toFinset, count x s • {x}
⊢ s = k • ∑ a ∈ s.toFinset, (count a s / k) • {a}

Proof state:
α : Type u_3
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ ∀ x ∈ s.toFinset, k • (count x s / k) • {x} = count x s • {x}

Tactic:
intro x hx

Result:
α : Type u_3
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
x : α
hx : x ∈ s.toFinset
⊢ k • (count x s / k) • {x} = count x s • {x}

Proof state:
α : Type u_3
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ ∃ u, s = k • u

Tactic:
use ∑ a ∈ s.toFinset, (s.count a / k) • {a}

Result:
case h
α : Type u_3
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ s = k • ∑ a ∈ s.toFinset, (count a s / k) • {a}

Proof state:
case h
α : Type u_3
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
h₂ : ∑ x ∈ s.toFinset, k • (count x s / k) • {x} = ∑ x ∈ s.toFinset, count x s • {x}
⊢ s = k • ∑ a ∈ s.toFinset, (count a s / k) • {a}

Tactic:
rw [← Finset.sum_nsmul, h₂, toFinset_sum_count_nsmul_eq]

Result:
no goals

Proof state:
α : Type u_3
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ ∑ x ∈ s.toFinset, k • (count x s / k) • {x} = ∑ x ∈ s.toFinset, count x s • {x}

Tactic:
apply Finset.sum_congr rfl

Result:
α : Type u_3
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ ∀ x ∈ s.toFinset, k • (count x s / k) • {x} = count x s • {x}
-- Mathlib/Data/Holor.lean
theorem cprankMax_mul [Ring α] :
    ∀ (n : ℕ) (x : Holor α [d]) (y : Holor α ds), CPRankMax n y → CPRankMax n (x ⊗ y)
  | 0, x, _, CPRankMax.zero => by simp [mul_zero x, CPRankMax.zero]
  | n + 1, x, _, CPRankMax.succ _ y₁ y₂ hy₁ hy₂ => by
    rw [mul_left_distrib]
    rw [Nat.add_comm]
    apply cprankMax_add
    · exact cprankMax_1 (CPRankMax1.cons _ _ hy₁)
    · exact cprankMax_mul _ x y₂ hy₂

Proof state:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (1 + n) (x ⊗ y₁ + x ⊗ y₂)

Tactic:
apply cprankMax_add

Result:
case a
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax 1 (x ⊗ y₁)

case a
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax n (x ⊗ y₂)

Proof state:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α [d]
⊢ CPRankMax 0 (x ⊗ 0)

Tactic:
simp [mul_zero x, CPRankMax.zero]

Result:
no goals

Proof state:
case a
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax 1 (x ⊗ y₁)

Tactic:
exact cprankMax_1 (CPRankMax1.cons _ _ hy₁)

Result:
no goals

Proof state:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ (y₁ + y₂))

Tactic:
rw [mul_left_distrib]

Result:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ y₁ + x ⊗ y₂)

Proof state:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ y₁ + x ⊗ y₂)

Tactic:
rw [Nat.add_comm]

Result:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (1 + n) (x ⊗ y₁ + x ⊗ y₂)

Proof state:
case a
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax n (x ⊗ y₂)

Tactic:
exact cprankMax_mul _ x y₂ hy₂

Result:
no goals
-- Mathlib/Data/Prod/Lex.lean
/-- Variant of `Prod.Lex.toLex_le_toLex` for partial orders. -/
lemma toLex_le_toLex' : toLex x ≤ toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 ≤ y.2)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ toLex x ≤ toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 ≤ y.2)

Tactic:
simp only [toLex_le_toLex, lt_iff_le_not_le, le_antisymm_iff]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ↔ x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ↔ x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)

Tactic:
tauto

Result:
no goals
-- Mathlib/Deprecated/Cardinal/PartENat.lean
theorem toPartENat_congr {β : Type v} (e : α ≃ β) : toPartENat #α = toPartENat #β

Proof state:
α : Type u
β : Type v
e : α ≃ β
⊢ toPartENat #α = toPartENat #β

Tactic:
rw [← toPartENat_lift, lift_mk_eq.{_, _,v}.mpr ⟨e⟩, toPartENat_lift]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_push_of_ne (h : b ≠ a) (l : Array α) : count a (l.push b) = count a l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
h : b ≠ a
l : Array α
⊢ count a (l.push b) = count a l

Tactic:
simp_all [count_push, h]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem relindex_comap (f : G' →* G) (K : Subgroup G') :
    relindex (comap f H) K = relindex H (map f K)

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
K : Subgroup G'
⊢ (comap f H).relindex K = H.relindex (map f K)

Tactic:
rw [relindex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.range_subtype]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_image (e : E ≃L[𝕜] F) (s : Set E) : dimH (e '' s) = dimH s :=
  le_antisymm (e.lipschitz.dimH_image_le s) <| by
    simpa only [e.symm_image_image] using e.symm.lipschitz.dimH_image_le (e '' s)

Proof state:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
s : Set E
⊢ dimH s ≤ dimH (⇑e '' s)

Tactic:
simpa only [e.symm_image_image] using e.symm.lipschitz.dimH_image_le (e '' s)

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem divMod_to_nat (d n : PosNum) :
    (n / d : ℕ) = (divMod d n).1 ∧ (n % d : ℕ) = (divMod d n).2

Proof state:
case bit1.mk
d n : PosNum
q r : Num
IH : ↑(q, r).2 + ↑d * ↑(q, r).1 = ↑n ∧ ↑(q, r).2 < ↑d
⊢ ↑(match (q, r) with
            | (q, r₁) => d.divModAux q r₁.bit1).2 +
        ↑d *
          ↑(match (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit1).1 =
      ↑n.bit1 ∧
    ↑(match (q, r) with
          | (q, r₁) => d.divModAux q r₁.bit1).2 <
      ↑d

Tactic:
simp only [divMod] at IH ⊢

Result:
case bit1.mk
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑(d.divModAux q r.bit1).2 + ↑d * ↑(d.divModAux q r.bit1).1 = ↑n.bit1 ∧ ↑(d.divModAux q r.bit1).2 < ↑d

Proof state:
case bit1.mk
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑(d.divModAux q r.bit1).2 + ↑d * ↑(d.divModAux q r.bit1).1 = ↑n.bit1 ∧ ↑(d.divModAux q r.bit1).2 < ↑d

Tactic:
apply divMod_to_nat_aux <;> simp only [Num.cast_bit1, cast_bit1]

Result:
case bit1.mk.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + 1 + ↑d * (↑q + ↑q) = ↑n + ↑n + 1

case bit1.mk.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + 1 < 2 * ↑d

Proof state:
case bit0
d n : PosNum
⊢ ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d →
    ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit0).2 +
          ↑d *
            ↑(match d.divMod n with
                | (q, r₁) => d.divModAux q r₁.bit0).1 =
        ↑n.bit0 ∧
      ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit0).2 <
        ↑d

Tactic:
obtain ⟨q, r⟩ := divMod d n

Result:
case bit0.mk
d n : PosNum
q r : Num
⊢ ↑(q, r).2 + ↑d * ↑(q, r).1 = ↑n ∧ ↑(q, r).2 < ↑d →
    ↑(match (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit0).2 +
          ↑d *
            ↑(match (q, r) with
                | (q, r₁) => d.divModAux q r₁.bit0).1 =
        ↑n.bit0 ∧
      ↑(match (q, r) with
            | (q, r₁) => d.divModAux q r₁.bit0).2 <
        ↑d

Proof state:
case bit1.mk
d n : PosNum
q r : Num
⊢ ↑(q, r).2 + ↑d * ↑(q, r).1 = ↑n ∧ ↑(q, r).2 < ↑d →
    ↑(match (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit1).2 +
          ↑d *
            ↑(match (q, r) with
                | (q, r₁) => d.divModAux q r₁.bit1).1 =
        ↑n.bit1 ∧
      ↑(match (q, r) with
            | (q, r₁) => d.divModAux q r₁.bit1).2 <
        ↑d

Tactic:
intro IH

Result:
case bit1.mk
d n : PosNum
q r : Num
IH : ↑(q, r).2 + ↑d * ↑(q, r).1 = ↑n ∧ ↑(q, r).2 < ↑d
⊢ ↑(match (q, r) with
            | (q, r₁) => d.divModAux q r₁.bit1).2 +
        ↑d *
          ↑(match (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit1).1 =
      ↑n.bit1 ∧
    ↑(match (q, r) with
          | (q, r₁) => d.divModAux q r₁.bit1).2 <
      ↑d
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
lemma compProd_eq_comp_prod (μ : Measure α) [SFinite μ] (κ : Kernel α β) [IsSFiniteKernel κ] :
    μ ⊗ₘ κ = (Kernel.id ×ₖ κ) ∘ₘ μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = ⇑(Kernel.id ×ₖ κ) ∘ₘ μ

Tactic:
rw [compProd, Kernel.compProd_prodMkLeft_eq_comp]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ (Kernel.id ×ₖ κ ∘ₖ Kernel.const Unit μ) () = ⇑(Kernel.id ×ₖ κ) ∘ₘ μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ (Kernel.id ×ₖ κ ∘ₖ Kernel.const Unit μ) () = ⇑(Kernel.id ×ₖ κ) ∘ₘ μ

Tactic:
rfl

Result:
no goals