harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convolution.lean
theorem convolution_mono_right {f g g' : G → ℝ} (hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ)
    (hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ) (hf : ∀ x, 0 ≤ f x) (hg : ∀ x, g x ≤ g' x) :
    (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Proof state:
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
⊢ (fun t => ((lsmul ℝ ℝ) (f t)) (g (x - t))) ≤ fun t => ((lsmul ℝ ℝ) (f t)) (g' (x - t))

Tactic:
simp only [lsmul_apply, Algebra.id.smul_eq_mul]

Result:
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
⊢ (fun t => f t * g (x - t)) ≤ fun t => f t * g' (x - t)

Proof state:
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
apply integral_mono hfg hfg'

Result:
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
⊢ (fun t => ((lsmul ℝ ℝ) (f t)) (g (x - t))) ≤ fun t => ((lsmul ℝ ℝ) (f t)) (g' (x - t))

Proof state:
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
t : G
⊢ (fun t => f t * g (x - t)) t ≤ (fun t => f t * g' (x - t)) t

Tactic:
apply mul_le_mul_of_nonneg_left (hg _) (hf _)

Result:
no goals

Proof state:
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
⊢ (fun t => f t * g (x - t)) ≤ fun t => f t * g' (x - t)

Tactic:
intro t

Result:
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
t : G
⊢ (fun t => f t * g (x - t)) t ≤ (fun t => f t * g' (x - t)) t
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_erase_self [LawfulBEq α] (h : m.WF) {k : α} : (m.erase k).get? k = none

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k : α
⊢ (m.erase k).get? k = none

Tactic:
simp_to_raw using Raw₀.get?_erase_self

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_or {x y : BitVec w} :
    (x ||| y).setWidth k = x.setWidth k ||| y.setWidth k

Proof state:
w k : Nat
x y : BitVec w
⊢ setWidth k (x ||| y) = setWidth k x ||| setWidth k y

Tactic:
ext i h

Result:
case pred
w k : Nat
x y : BitVec w
i : Nat
h : i < k
⊢ (setWidth k (x ||| y)).getLsbD i = (setWidth k x ||| setWidth k y).getLsbD i

Proof state:
case pred
w k : Nat
x y : BitVec w
i : Nat
h : i < k
⊢ (setWidth k (x ||| y)).getLsbD i = (setWidth k x ||| setWidth k y).getLsbD i

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem _root_.CompleteLatticeHom.apply_limsup_iterate (f : CompleteLatticeHom α α) (a : α) :
    f (limsup (fun n => f^[n] a) atTop) = limsup (fun n => f^[n] a) atTop

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ i, f (⨆ i_1, (⇑f)^[i_1 + i] a) = ⨅ n, ⨆ i, (⇑f)^[i + n] a

Tactic:
simp_rw [_root_.map_iSup, ← Function.comp_apply (f := f), ← Function.iterate_succ' f,
  ← Nat.add_succ]

Result:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ i, ⨆ i_1, (⇑f)^[i_1 + i.succ] a = ⨅ n, ⨆ i, (⇑f)^[i + n] a

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ f (limsup (fun n => (⇑f)^[n] a) atTop) = limsup (fun n => (⇑f)^[n] a) atTop

Tactic:
rw [limsup_eq_iInf_iSup_of_nat', map_iInf]

Result:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ i, f (⨆ i_1, (⇑f)^[i_1 + i] a) = ⨅ n, ⨆ i, (⇑f)^[i + n] a

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ i, ⨆ i_1, (⇑f)^[i_1 + i.succ] a =
    (⨅ i, ⨅ (_ : 0 < i), ⨆ i_1, (⇑f)^[i_1 + i] a) ⊓ ⨅ i, ⨅ (_ : ¬0 < i), ⨆ i_1, (⇑f)^[i_1 + i] a

Tactic:
simp only [not_lt, Nat.le_zero, iInf_iInf_eq_left, add_zero, iInf_nat_gt_zero_eq, left_eq_inf]

Result:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ i, ⨆ i_1, (⇑f)^[i_1 + i.succ] a ≤ ⨆ i, (⇑f)^[i] a

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨆ j, (⇑f)^[j + (0 + 1)] a ≤ ⨆ i, (⇑f)^[i] a

Tactic:
simp only [zero_add, Function.comp_apply, iSup_le_iff]

Result:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ∀ (i : ℕ), (⇑f)^[i + 1] a ≤ ⨆ i, (⇑f)^[i] a

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ∀ (i : ℕ), (⇑f)^[i + 1] a ≤ ⨆ i, (⇑f)^[i] a

Tactic:
exact fun i => le_iSup (fun i => f^[i] a) (i + 1)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ i, ⨆ i_1, (⇑f)^[i_1 + i.succ] a ≤ ⨆ i, (⇑f)^[i] a

Tactic:
refine (iInf_le (fun i => ⨆ j, f^[j + (i + 1)] a) 0).trans ?_

Result:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨆ j, (⇑f)^[j + (0 + 1)] a ≤ ⨆ i, (⇑f)^[i] a
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem epi_of_epi_image {X Y : C} (f : X ⟶ Y) [HasImage f] [Epi (image.ι f)]
    [Epi (factorThruImage f)] : Epi f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : Epi (image.ι f)
inst✝ : Epi (factorThruImage f)
⊢ Epi f

Tactic:
rw [← image.fac f]

Result:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : Epi (image.ι f)
inst✝ : Epi (factorThruImage f)
⊢ Epi (factorThruImage f ≫ image.ι f)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : Epi (image.ι f)
inst✝ : Epi (factorThruImage f)
⊢ Epi (factorThruImage f ≫ image.ι f)

Tactic:
apply epi_comp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toArray_ofFn (f : Fin n → α) : (ofFn f).toArray = Array.ofFn f

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
⊢ (ofFn f).toArray = Array.ofFn f

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem Filter.Tendsto.finInsertNth
    (i : Fin (n + 1)) {f : Y → π i} {g : Y → ∀ j : Fin n, π (i.succAbove j)} {l : Filter Y}
    {x : π i} {y : ∀ j, π (i.succAbove j)} (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
    Tendsto (fun a => i.insertNth (f a) (g a)) l (𝓝 <| i.insertNth x y) :=
  tendsto_pi_nhds.2 fun j => Fin.succAboveCases i (by simpa) (by simpa using tendsto_pi_nhds.1 hg) j

Proof state:
Y : Type v
n : ℕ
π : Fin (n + 1) → Type u_8
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (π i)
i : Fin (n + 1)
f : Y → π i
g : Y → (j : Fin n) → π (i.succAbove j)
l : Filter Y
x : π i
y : (j : Fin n) → π (i.succAbove j)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ Tendsto (fun i_1 => i.insertNth (f i_1) (g i_1) i) l (𝓝 (i.insertNth x y i))

Tactic:
simpa

Result:
no goals

Proof state:
Y : Type v
n : ℕ
π : Fin (n + 1) → Type u_8
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (π i)
i : Fin (n + 1)
f : Y → π i
g : Y → (j : Fin n) → π (i.succAbove j)
l : Filter Y
x : π i
y : (j : Fin n) → π (i.succAbove j)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (j : Fin n),
    Tendsto (fun i_1 => i.insertNth (f i_1) (g i_1) (i.succAbove j)) l (𝓝 (i.insertNth x y (i.succAbove j)))

Tactic:
simpa using tendsto_pi_nhds.1 hg

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem coeff_contract {p : ℕ} (hp : p ≠ 0) (f : R[X]) (n : ℕ) :
    (contract p f).coeff n = f.coeff (n * p)

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ f.natDegree + 1 ≤ n * 1

Tactic:
simpa only [mul_one] using hn

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ (contract p f).coeff n = f.coeff (n * p)

Tactic:
simp only [contract, coeff_monomial, sum_ite_eq', finset_sum_coeff, mem_range, not_lt,
  ite_eq_left_iff]

Result:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ f.natDegree + 1 ≤ n → 0 = f.coeff (n * p)

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ f.natDegree + 1 ≤ n → 0 = f.coeff (n * p)

Tactic:
intro hn

Result:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ 0 = f.coeff (n * p)

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ f.natDegree < n * p

Tactic:
calc
  f.natDegree < f.natDegree + 1 := Nat.lt_succ_self _
  _ ≤ n * 1 := by simpa only [mul_one] using hn
  _ ≤ n * p := mul_le_mul_of_nonneg_left (show 1 ≤ p from hp.bot_lt) (zero_le n)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ 0 = f.coeff (n * p)

Tactic:
apply (coeff_eq_zero_of_natDegree_lt _).symm

Result:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ f.natDegree < n * p
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem exists_not_mem_null_integral_le (hf : Integrable f μ) (hN : μ N = 0) :
    ∃ x, x ∉ N ∧ ∫ a, f a ∂μ ≤ f x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
hN : μ N = 0
⊢ ∃ x ∉ N, ∫ (a : α), f a ∂μ ≤ f x

Tactic:
simpa only [average_eq_integral] using
  exists_not_mem_null_average_le (IsProbabilityMeasure.ne_zero μ) hf hN

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Bounded.lean
lemma Continuous.bounded_above_of_compact_support (hf : Continuous f) (h : HasCompactSupport f) :
    ∃ C, ∀ x, ‖f x‖ ≤ C

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup E
inst✝ : TopologicalSpace α
f : α → E
hf : Continuous f
h : HasCompactSupport f
⊢ ∃ C, ∀ (x : α), ‖f x‖ ≤ C

Tactic:
simpa [bddAbove_def] using hf.norm.bddAbove_range_of_hasCompactSupport h.norm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast?

Proof state:
α : Type u_1
l : List α
⊢ l.toArray.back? = l.getLast?

Tactic:
simp [back?, List.getLast?_eq_getElem?]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m

Proof state:
case isTrue
m n : Nat
h : 0 < n ∧ n ≤ m
⊢ n * ite (0 < n ∧ n ≤ m) ((m - n) / n + 1) 0 + ite (0 < n ∧ n ≤ m) ((m - n) % n) m = m

Tactic:
simp [h]

Result:
case isTrue
m n : Nat
h : 0 < n ∧ n ≤ m
⊢ n * ((m - n) / n + 1) + (m - n) % n = m

Proof state:
case isTrue
m n : Nat
h : 0 < n ∧ n ≤ m
⊢ n * ((m - n) / n + 1) + (m - n) % n = m

Tactic:
have ih := div_add_mod (m - n) n

Result:
case isTrue
m n : Nat
h : 0 < n ∧ n ≤ m
ih : n * ((m - n) / n) + (m - n) % n = m - n
⊢ n * ((m - n) / n + 1) + (m - n) % n = m

Proof state:
m n : Nat
⊢ n * ite (0 < n ∧ n ≤ m) ((m - n) / n + 1) 0 + ite (0 < n ∧ n ≤ m) ((m - n) % n) m = m

Tactic:
have h : Decidable (0 < n ∧ n ≤ m) := inferInstance

Result:
m n : Nat
h : Decidable (0 < n ∧ n ≤ m)
⊢ n * ite (0 < n ∧ n ≤ m) ((m - n) / n + 1) 0 + ite (0 < n ∧ n ≤ m) ((m - n) % n) m = m

Proof state:
m n : Nat
⊢ n * (m / n) + m % n = m

Tactic:
rw [div_eq, mod_eq]

Result:
m n : Nat
⊢ n * ite (0 < n ∧ n ≤ m) ((m - n) / n + 1) 0 + ite (0 < n ∧ n ≤ m) ((m - n) % n) m = m

Proof state:
case isTrue
m n : Nat
h : 0 < n ∧ n ≤ m
ih : n * ((m - n) / n) + (m - n) % n = m - n
⊢ n * ((m - n) / n + 1) + (m - n) % n = m

Tactic:
rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2]

Result:
no goals

Proof state:
case isFalse
m n : Nat
h : ¬(0 < n ∧ n ≤ m)
⊢ n * ite (0 < n ∧ n ≤ m) ((m - n) / n + 1) 0 + ite (0 < n ∧ n ≤ m) ((m - n) % n) m = m

Tactic:
simp [h]

Result:
no goals

Proof state:
m n : Nat
h : Decidable (0 < n ∧ n ≤ m)
⊢ n * ite (0 < n ∧ n ≤ m) ((m - n) / n + 1) 0 + ite (0 < n ∧ n ≤ m) ((m - n) % n) m = m

Tactic:
cases h with
| isFalse h => simp [h]
| isTrue h =>
  simp [h]
  have ih := div_add_mod (m - n) n
  rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2]

Result:
no goals

Proof state:
case a
m n : Nat
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h✝¹ : Decidable (0 < n ∧ n ≤ m)
h : 0 < n ∧ n ≤ m
h✝ : h✝¹ = isTrue h
⊢ 0 < n ∧ n ≤ m

Tactic:
assumption

Result:
no goals

Proof state:
m n : Nat
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h✝¹ : Decidable (0 < n ∧ n ≤ m)
h : 0 < n ∧ n ≤ m
h✝ : h✝¹ = isTrue h
⊢ m - n < m

Tactic:
apply div_rec_lemma

Result:
case a
m n : Nat
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h✝¹ : Decidable (0 < n ∧ n ≤ m)
h : 0 < n ∧ n ≤ m
h✝ : h✝¹ = isTrue h
⊢ 0 < n ∧ n ≤ m
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem eq_one_of_mul_right (h : a * b = 1) : a = 1 :=
  congr_arg Units.inv <| Subsingleton.elim (Units.mk _ _ (by
    rw [← mul_right_cancel_iff (a := b), mul_assoc, h, one_mul, mul_one]) h) 1

Proof state:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1

Tactic:
rw [← mul_right_cancel_iff (a := b), mul_assoc, h, one_mul, mul_one]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.of_mul_right_right (H : IsCoprime x (y * z)) : IsCoprime x z

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime x (y * z)
⊢ IsCoprime x z

Tactic:
rw [mul_comm] at H

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime x (z * y)
⊢ IsCoprime x z

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime x (z * y)
⊢ IsCoprime x z

Tactic:
exact H.of_mul_right_left

Result:
no goals
-- Mathlib/Topology/GDelta/Basic.lean
theorem IsGδ.union {s t : Set X} (hs : IsGδ s) (ht : IsGδ t) : IsGδ (s ∪ t)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (s ∪ t)

Tactic:
rcases hs with ⟨S, Sopen, Scount, rfl⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
t : Set X
ht : IsGδ t
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen t
Scount : S.Countable
⊢ IsGδ (⋂₀ S ∪ t)

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen t
Tcount : T.Countable
⊢ IsGδ (⋂ p ∈ S ×ˢ T, p.1 ∪ p.2)

Tactic:
refine .biInter_of_isOpen (Scount.prod Tcount) ?_

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen t
Tcount : T.Countable
⊢ ∀ i ∈ S ×ˢ T, IsOpen (i.1 ∪ i.2)

Proof state:
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
t : Set X
ht : IsGδ t
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen t
Scount : S.Countable
⊢ IsGδ (⋂₀ S ∪ t)

Tactic:
rcases ht with ⟨T, Topen, Tcount, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen t
Tcount : T.Countable
⊢ IsGδ (⋂₀ S ∪ ⋂₀ T)

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen t
Tcount : T.Countable
⊢ ∀ i ∈ S ×ˢ T, IsOpen (i.1 ∪ i.2)

Tactic:
rintro ⟨a, b⟩ ⟨ha, hb⟩

Result:
case intro.intro.intro.intro.intro.intro.mk.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen t
Tcount : T.Countable
a b : Set X
ha : (a, b).1 ∈ S
hb : (a, b).2 ∈ T
⊢ IsOpen ((a, b).1 ∪ (a, b).2)

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen t
Tcount : T.Countable
⊢ IsGδ (⋂₀ S ∪ ⋂₀ T)

Tactic:
rw [sInter_union_sInter]

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen t
Tcount : T.Countable
⊢ IsGδ (⋂ p ∈ S ×ˢ T, p.1 ∪ p.2)

Proof state:
case intro.intro.intro.intro.intro.intro.mk.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen t
Tcount : T.Countable
a b : Set X
ha : (a, b).1 ∈ S
hb : (a, b).2 ∈ T
⊢ IsOpen ((a, b).1 ∪ (a, b).2)

Tactic:
exact (Sopen a ha).union (Topen b hb)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_zero_left {hT : DominatedFinMeasAdditive μ (0 : Set α → E →L[ℝ] F) C} :
    setToFun μ 0 hT f = 0

Proof state:
case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ 0 C
hf : ¬Integrable f μ
⊢ setToFun μ 0 hT f = 0

Tactic:
exact setToFun_undef hT hf

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ 0 C
hf : Integrable f μ
⊢ setToFun μ 0 hT f = 0

Tactic:
rw [setToFun_eq hT hf]

Result:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ 0 C
hf : Integrable f μ
⊢ (L1.setToL1 hT) (Integrable.toL1 f hf) = 0

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ 0 C
⊢ setToFun μ 0 hT f = 0

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ 0 C
hf : Integrable f μ
⊢ setToFun μ 0 hT f = 0

case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ 0 C
hf : ¬Integrable f μ
⊢ setToFun μ 0 hT f = 0

Proof state:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ 0 C
hf : Integrable f μ
⊢ (L1.setToL1 hT) (Integrable.toL1 f hf) = 0

Tactic:
exact L1.setToL1_zero_left hT _

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
@[simp]
lemma ι_appLE (V W e) :
    U.ι.appLE V W e =
      X.presheaf.map (homOfLE (x := U.ι ''ᵁ W) (Set.image_subset_iff.mpr ‹_›)).op

Proof state:
X : Scheme
U V : X.Opens
W : (↑U).Opens
e : W ≤ U.ι ⁻¹ᵁ V
⊢ X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) = X.presheaf.map (homOfLE ⋯).op

Tactic:
rfl

Result:
no goals

Proof state:
X : Scheme
U V : X.Opens
W : (↑U).Opens
e : W ≤ U.ι ⁻¹ᵁ V
⊢ Hom.appLE U.ι V W e = X.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [Hom.appLE, ι_app, Functor.op_obj, Opens.carrier_eq_coe, toScheme_presheaf_map,
  Quiver.Hom.unop_op, Hom.opensFunctor_map_homOfLE, Opens.coe_inclusion', ← Functor.map_comp]

Result:
X : Scheme
U V : X.Opens
W : (↑U).Opens
e : W ≤ U.ι ⁻¹ᵁ V
⊢ X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) = X.presheaf.map (homOfLE ⋯).op
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem natCast [StarOrderedRing R] [DecidableEq n] (d : ℕ) :
    PosSemidef (d : Matrix n n R) :=
  ⟨isHermitian_natCast _, fun x => by
    simp only [natCast_mulVec, dotProduct_smul]
    rw [Nat.cast_smul_eq_nsmul]
    exact nsmul_nonneg (dotProduct_star_self_nonneg _) _⟩

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℕ
x : n → R
⊢ 0 ≤ d • (star x ⬝ᵥ x)

Tactic:
exact nsmul_nonneg (dotProduct_star_self_nonneg _) _

Result:
no goals

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℕ
x : n → R
⊢ 0 ≤ ↑d • (star x ⬝ᵥ x)

Tactic:
rw [Nat.cast_smul_eq_nsmul]

Result:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℕ
x : n → R
⊢ 0 ≤ d • (star x ⬝ᵥ x)

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℕ
x : n → R
⊢ 0 ≤ star x ⬝ᵥ ↑d *ᵥ x

Tactic:
simp only [natCast_mulVec, dotProduct_smul]

Result:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℕ
x : n → R
⊢ 0 ≤ ↑d • (star x ⬝ᵥ x)
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem sumIDeriv_derivative (p : R[X]) : sumIDeriv (derivative p) = derivative (sumIDeriv p)

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] (derivative p) =
    ∑ b ∈ range (p.natDegree + 1), derivative ((⇑derivative)^[b] p)

Tactic:
simp_rw [← Function.iterate_succ_apply, Function.iterate_succ_apply']

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ sumIDeriv (derivative p) = derivative (sumIDeriv p)

Tactic:
rw [sumIDeriv_apply_of_le ((natDegree_derivative_le p).trans tsub_le_self), sumIDeriv_apply,
  derivative_sum]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] (derivative p) =
    ∑ b ∈ range (p.natDegree + 1), derivative ((⇑derivative)^[b] p)
-- Mathlib/Order/Basic.lean
theorem lt_update_self_iff : x < update x i a ↔ x i < a

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a : π i
⊢ x < update x i a ↔ x i < a

Tactic:
simp [lt_iff_le_not_le]

Result:
no goals