harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma rnDeriv_singularPart (κ ν : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel ν] (a : α) :
    rnDeriv (singularPart κ ν) ν a =ᵐ[ν a] 0

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ ν : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
⊢ (κ.singularPart ν).rnDeriv ν a =ᶠ[ae (ν a)] 0

Tactic:
filter_upwards [(singularPart κ ν).rnDeriv_eq_rnDeriv_measure,
  (Measure.rnDeriv_eq_zero _ _).mpr (mutuallySingular_singularPart κ ν a)] with x h1 h2

Result:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ ν : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
x : γ
h1 : (κ.singularPart ν).rnDeriv ν a x = (∂(κ.singularPart ν) a/∂ν a) x
h2 : (∂(κ.singularPart ν) a/∂ν a) x = 0 x
⊢ (κ.singularPart ν).rnDeriv ν a x = 0 x

Proof state:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ ν : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
x : γ
h1 : (κ.singularPart ν).rnDeriv ν a x = (∂(κ.singularPart ν) a/∂ν a) x
h2 : (∂(κ.singularPart ν) a/∂ν a) x = 0 x
⊢ (κ.singularPart ν).rnDeriv ν a x = 0 x

Tactic:
rw [h1, h2]

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem isOpen_compl_image_coe {s : Set X} :
    IsOpen ((↑) '' s : Set (OnePoint X))ᶜ ↔ IsClosed s ∧ IsCompact s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ ∞ ∈ (some '' s)ᶜ

Tactic:
exact infty_not_mem_image_coe

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsOpen (some '' s)ᶜ ↔ IsClosed s ∧ IsCompact s

Tactic:
rw [isOpen_iff_of_mem, ← preimage_compl, compl_compl, preimage_image_eq _ coe_injective]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ ∞ ∈ (some '' s)ᶜ
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma succAbove_ne_last_last {a : Fin (n + 2)} (h : a ≠ last (n + 1)) :
    a.succAbove (last n) = last (n + 1)

Proof state:
n : ℕ
a : Fin (n + 2)
h : a ≠ last (n + 1)
⊢ a.succAbove (last n) = last (n + 1)

Tactic:
rw [succAbove_of_lt_succ _ _ (succ_last _ ▸ lt_last_iff_ne_last.2 h), succ_last]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_div_intCast_eq_div_intCast_mod {m : ℤ} {n : ℕ} :
    fract ((m : k) / n) = ↑(m % n) / n

Proof state:
case inr.intro.inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n

Tactic:
calc
  fract ((Int.cast (-(m₀ : ℤ)) : k) / (n : k))
    = fract (-(m₀ : k) / n) := by simp
  _ = fract ((m₁ : k) / n) := ?_
  _ = Int.cast (m₁ % (n : ℤ)) / Nat.cast n := this hm₁
  _ = Int.cast (-(↑m₀ : ℤ) % ↑n) / Nat.cast n := ?_

Result:
case inr.intro.inr.calc_1
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (-↑m₀ / ↑n) = fract (↑m₁ / ↑n)

case inr.intro.inr.calc_2
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ ↑(m₁ % ↑n) / ↑n = ↑(-↑m₀ % ↑n) / ↑n

Proof state:
case inr.intro.inr.calc_2.e_a.e_a
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ m₁ % ↑n = -↑m₀ % ↑n

Tactic:
simp only [m₁]

Result:
case inr.intro.inr.calc_2.e_a.e_a
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ (q * ↑n - ↑m₀) % ↑n = -↑m₀ % ↑n

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : n > 0
⊢ 0 < ↑n

Tactic:
norm_cast

Result:
no goals

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (↑(-↑m₀) / ↑n) = fract (-↑m₀ / ↑n)

Tactic:
simp

Result:
no goals

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
⊢ ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n

Tactic:
intros l hl

Result:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l : ℤ
hl : 0 ≤ l
⊢ fract (↑l / ↑n) = ↑(l % ↑n) / ↑n

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Result:
case inl
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
⊢ fract (↑m / ↑0) = ↑(m % ↑0) / ↑0

case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : n > 0
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
-- Mathlib/NumberTheory/FLT/Polynomial.lean
private lemma find_contract {a : k[X]}
    (ha : a ≠ 0) (hda : derivative a = 0) (chn0 : ringChar k ≠ 0) :
    ∃ ca, ca ≠ 0 ∧
      a = expand k (ringChar k) ca ∧
      a.natDegree = ca.natDegree * ringChar k

Proof state:
case refine_1
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = 0
h : contract (ringChar k) a = 0
⊢ False

Tactic:
exact ha heq

Result:
no goals

Proof state:
case refine_1
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
⊢ contract (ringChar k) a ≠ 0

Tactic:
intro h

Result:
case refine_1
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
h : contract (ringChar k) a = 0
⊢ False

Proof state:
case refine_1
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
h : contract (ringChar k) a = 0
⊢ False

Tactic:
rw [h, map_zero] at heq

Result:
case refine_1
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = 0
h : contract (ringChar k) a = 0
⊢ False

Proof state:
case refine_2
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
⊢ a.natDegree = (contract (ringChar k) a).natDegree * ringChar k

Tactic:
rw [← natDegree_expand, ← heq]

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
⊢ ∃ ca, ca ≠ 0 ∧ a = (expand k (ringChar k)) ca ∧ a.natDegree = ca.natDegree * ringChar k

Tactic:
refine ⟨contract (ringChar k) a, ?_, heq, ?_⟩

Result:
case refine_1
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
⊢ contract (ringChar k) a ≠ 0

case refine_2
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
⊢ a.natDegree = (contract (ringChar k) a).natDegree * ringChar k

Proof state:
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
⊢ ∃ ca, ca ≠ 0 ∧ a = (expand k (ringChar k)) ca ∧ a.natDegree = ca.natDegree * ringChar k

Tactic:
have heq := (expand_contract (ringChar k) hda chn0).symm

Result:
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
⊢ ∃ ca, ca ≠ 0 ∧ a = (expand k (ringChar k)) ca ∧ a.natDegree = ca.natDegree * ringChar k
-- Mathlib/LinearAlgebra/Prod.lean
theorem fst_comp_prodComm :
    (LinearMap.fst R M₂ M).comp (prodComm R M M₂).toLinearMap = (LinearMap.snd R M M₂)

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ LinearMap.fst R M₂ M ∘ₗ ↑(prodComm R M M₂) = LinearMap.snd R M M₂

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem coordChange_linear_comp (i j k : ι) :
    ∀ x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet k,
      (Z.coordChange j k x).comp (Z.coordChange i j x) = Z.coordChange i k x :=
  fun x hx => by
  ext v
  exact Z.coordChange_comp i j k x hx v

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j k : ι
x : B
hx : x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet k
⊢ (Z.coordChange j k x).comp (Z.coordChange i j x) = Z.coordChange i k x

Tactic:
ext v

Result:
case h
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j k : ι
x : B
hx : x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet k
v : F
⊢ ((Z.coordChange j k x).comp (Z.coordChange i j x)) v = (Z.coordChange i k x) v

Proof state:
case h
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j k : ι
x : B
hx : x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet k
v : F
⊢ ((Z.coordChange j k x).comp (Z.coordChange i j x)) v = (Z.coordChange i k x) v

Tactic:
exact Z.coordChange_comp i j k x hx v

Result:
no goals
-- Mathlib/Data/Sym/Card.lean
theorem card_sym_fin_eq_multichoose : ∀ n k : ℕ, card (Sym (Fin n) k) = multichoose n k
  | n, 0 => by simp
  | 0, k + 1 => by rw [multichoose_zero_succ]; exact card_eq_zero
  | 1, k + 1 => by simp
  | n + 2, k + 1 => by
    rw [multichoose_succ_succ, ← card_sym_fin_eq_multichoose (n + 1) (k + 1),
      ← card_sym_fin_eq_multichoose (n + 2) k, add_comm (Fintype.card _), ← card_sum]
    refine Fintype.card_congr (Equiv.symm ?_)
    apply (Sym.e1.symm.sumCongr Sym.e2.symm).trans
    apply Equiv.sumCompl

Proof state:
n k : ℕ
⊢ Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1) ≃ Sym (Fin (n + 2)) (k + 1)

Tactic:
apply (Sym.e1.symm.sumCongr Sym.e2.symm).trans

Result:
n k : ℕ
⊢ { s // 0 ∈ s } ⊕ { s // 0 ∉ s } ≃ Sym (Fin (n + 2)) (k + 1)

Proof state:
n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = (n + 2).multichoose (k + 1)

Tactic:
rw [multichoose_succ_succ, ← card_sym_fin_eq_multichoose (n + 1) (k + 1),
  ← card_sym_fin_eq_multichoose (n + 2) k, add_comm (Fintype.card _), ← card_sum]

Result:
n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))

Proof state:
n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))

Tactic:
refine Fintype.card_congr (Equiv.symm ?_)

Result:
n k : ℕ
⊢ Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1) ≃ Sym (Fin (n + 2)) (k + 1)

Proof state:
n : ℕ
⊢ Fintype.card (Sym (Fin n) 0) = n.multichoose 0

Tactic:
simp

Result:
no goals

Proof state:
k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = multichoose 0 (k + 1)

Tactic:
rw [multichoose_zero_succ]

Result:
k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = 0

Proof state:
n k : ℕ
⊢ { s // 0 ∈ s } ⊕ { s // 0 ∉ s } ≃ Sym (Fin (n + 2)) (k + 1)

Tactic:
apply Equiv.sumCompl

Result:
no goals

Proof state:
k : ℕ
⊢ Fintype.card (Sym (Fin 1) (k + 1)) = multichoose 1 (k + 1)

Tactic:
simp

Result:
no goals

Proof state:
k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = 0

Tactic:
exact card_eq_zero

Result:
no goals
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.even_odd₇ (a b c : ℕ) (r : ℤ) (ha : a % 2 = 0) (hb : b % 8 = 7)
    (hc : a / 2 = c) (hr : jacobiSymNat c b = r) : jacobiSymNat a b = r

Proof state:
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8

Tactic:
norm_num

Result:
no goals

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Tactic:
rw [← Nat.mod_mod_of_dvd, hb]

Result:
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ¬(b % 8 = 3 ∨ b % 8 = 5)

Tactic:
simp [hb]

Result:
no goals

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r

Tactic:
simp only [jacobiSymNat, ← hr, ← hc, Int.ofNat_ediv, Nat.cast_ofNat]

Result:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a) b = jacobiSym (↑a / 2) b

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a) b = jacobiSym (↑a / 2) b

Tactic:
rw [← jacobiSym.even_odd (mod_cast ha), if_neg (by simp [hb])]

Result:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
-- Mathlib/Analysis/Convolution.lean
theorem integrable_posConvolution {f : ℝ → E} {g : ℝ → E'} {μ ν : Measure ℝ} [SFinite μ]
    [SFinite ν] [IsAddRightInvariant μ] [NoAtoms ν] (hf : IntegrableOn f (Ioi 0) ν)
    (hg : IntegrableOn g (Ioi 0) μ) (L : E →L[ℝ] E' →L[ℝ] F) :
    Integrable (posConvolution f g L ν) μ

Proof state:
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
μ ν : Measure ℝ
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : μ.IsAddRightInvariant
inst✝ : NoAtoms ν
hf : Integrable ((Ioi 0).indicator f) ν
hg : Integrable ((Ioi 0).indicator g) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Integrable ((Ioi 0).indicator f ⋆[L, ν] (Ioi 0).indicator g) μ

Tactic:
exact (hf.convolution_integrand L hg).integral_prod_left

Result:
no goals

Proof state:
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
μ ν : Measure ℝ
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : μ.IsAddRightInvariant
inst✝ : NoAtoms ν
hf : Integrable ((Ioi 0).indicator f) ν
hg : Integrable ((Ioi 0).indicator g) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Integrable (posConvolution f g L ν) μ

Tactic:
rw [posConvolution_eq_convolution_indicator f g L ν]

Result:
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
μ ν : Measure ℝ
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : μ.IsAddRightInvariant
inst✝ : NoAtoms ν
hf : Integrable ((Ioi 0).indicator f) ν
hg : Integrable ((Ioi 0).indicator g) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Integrable ((Ioi 0).indicator f ⋆[L, ν] (Ioi 0).indicator g) μ

Proof state:
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
μ ν : Measure ℝ
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : μ.IsAddRightInvariant
inst✝ : NoAtoms ν
hf : IntegrableOn f (Ioi 0) ν
hg : IntegrableOn g (Ioi 0) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Integrable (posConvolution f g L ν) μ

Tactic:
rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))] at hf hg

Result:
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
μ ν : Measure ℝ
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : μ.IsAddRightInvariant
inst✝ : NoAtoms ν
hf : Integrable ((Ioi 0).indicator f) ν
hg : Integrable ((Ioi 0).indicator g) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Integrable (posConvolution f g L ν) μ
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast!_insertList_of_mem [BEq α] [LawfulBEq α]
    {l toInsert : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k') (v : β k) [Inhabited (β k')]
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ toInsert) :
    getValueCast! k' (insertList l toInsert) =
    cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
γ : α → Type w
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ k = k'

Proof state:
case e_a
α : Type u
β : α → Type v
γ : α → Type w
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ k = k'

Tactic:
exact LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ getValueCast! k' (insertList l toInsert) = cast ⋯ v

Tactic:
rw [getValueCast!_eq_getValueCast?,
  getValueCast?_insertList_of_mem k_beq distinct_l distinct_toInsert mem, Option.get!_some]

Result:
no goals
-- Mathlib/Data/Tree/Basic.lean
theorem id_map (t : Tree α) : t.map id = t

Proof state:
α : Type u
t : Tree α
⊢ map id t = t

Tactic:
induction t with
| nil => rw [map]
| node v l r hl hr => rw [map, hl, hr, id_eq]

Result:
no goals

Proof state:
case node
α : Type u
v : α
l r : Tree α
hl : map id l = l
hr : map id r = r
⊢ map id (node v l r) = node v l r

Tactic:
rw [map, hl, hr, id_eq]

Result:
no goals

Proof state:
case nil
α : Type u
⊢ map id nil = nil

Tactic:
rw [map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulOperator.lean
theorem le_size_of_le_aig_size (aig : AIG α) (input : β aig) (h : x ≤ aig.decls.size) :
    x ≤ (f aig input).aig.decls.size

Proof state:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ x ≤ ?m

Tactic:
exact h

Result:
no goals

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ x ≤ (f aig input).aig.decls.size

Tactic:
apply Nat.le_trans

Result:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ x ≤ ?m

case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ Nat

Proof state:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size

Tactic:
exact le_size aig input

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem IsClosed.frontier_eq (hs : IsClosed s) : frontier s = s \ interior s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
hs : IsClosed s
⊢ frontier s = s \ interior s

Tactic:
rw [frontier, hs.closure_eq]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_le_norm_add_norm_div' (u v : E) : ‖u‖ ≤ ‖v‖ + ‖u / v‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖u / v‖ + ‖v‖

Tactic:
refine (norm_mul_le' _ _).trans_eq' ?_

Result:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ = ‖u / v * v‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖v‖ + ‖u / v‖

Tactic:
rw [add_comm]

Result:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖u / v‖ + ‖v‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ = ‖u / v * v‖

Tactic:
rw [div_mul_cancel]

Result:
no goals