harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SetFamily/Intersecting.lean
theorem Intersecting.insert (hs : s.Intersecting) (ha : a ≠ ⊥)
    (h : ∀ b ∈ s, ¬Disjoint a b) : (insert a s).Intersecting

Proof state:
case inr.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
a : α
hs : s.Intersecting
ha : a ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
⊢ ¬Disjoint b c

Tactic:
exact hs hb hc

Result:
no goals

Proof state:
case inl.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
⊢ ¬Disjoint c c

Tactic:
rwa [disjoint_self]

Result:
no goals

Proof state:
case inl.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
b : α
ha : b ≠ ⊥
h : ∀ b_1 ∈ s, ¬Disjoint b b_1
c : α
hc : c ∈ s
⊢ ¬Disjoint b c

Tactic:
exact h _ hc

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
b : α
hb : b ∈ s
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
⊢ ¬Disjoint b c

Tactic:
exact fun H => h _ hb H.symm

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
a : α
hs : s.Intersecting
ha : a ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint a b
⊢ (insert a s).Intersecting

Tactic:
rintro b (rfl | hb) c (rfl | hc)

Result:
case inl.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
⊢ ¬Disjoint c c

case inl.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
b : α
ha : b ≠ ⊥
h : ∀ b_1 ∈ s, ¬Disjoint b b_1
c : α
hc : c ∈ s
⊢ ¬Disjoint b c

case inr.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
b : α
hb : b ∈ s
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
⊢ ¬Disjoint b c

case inr.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
a : α
hs : s.Intersecting
ha : a ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
⊢ ¬Disjoint b c
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem neg_inj {x y : BitVec w} : -x = -y ↔ x = y :=
  ⟨fun h => by rw [← @neg_neg w x, ← @neg_neg w y, h], congrArg _⟩

Proof state:
w : Nat
x y : BitVec w
h : -x = -y
⊢ x = y

Tactic:
rw [← @neg_neg w x, ← @neg_neg w y, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SizeOfLemmas.lean
theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1

Proof state:
α : Sort u_1
p : α → Prop
s : Subtype p
⊢ sizeOf s = sizeOf s.val + 1

Tactic:
cases s

Result:
case mk
α : Sort u_1
p : α → Prop
val✝ : α
property✝ : p val✝
⊢ sizeOf ⟨val✝, property✝⟩ = sizeOf ⟨val✝, property✝⟩.val + 1

Proof state:
case mk
α : Sort u_1
p : α → Prop
val✝ : α
property✝ : p val✝
⊢ sizeOf ⟨val✝, property✝⟩ = sizeOf ⟨val✝, property✝⟩.val + 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_sub_left_of_add_lt {a b c : Int} (h : a + b < c) : b < c - a

Proof state:
a b c : Int
h : a + b < c
⊢ b < c - a

Tactic:
have h := Int.add_lt_add_right h (-a)

Result:
a b c : Int
h✝ : a + b < c
h : a + b + -a < c + -a
⊢ b < c - a

Proof state:
a b c : Int
h✝ : a + b < c
h : a + b + -a < c + -a
⊢ b < c - a

Tactic:
rwa [Int.add_comm a b, Int.add_neg_cancel_right] at h

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg {f : α → F} {g : α → G} {c : ℝ}
    (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ c * ‖g x‖) (hc : c < 0) (p : ℝ≥0∞) :
    eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0

Proof state:
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖
hc : c < 0
p : ℝ≥0∞
⊢ eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0

Tactic:
simp_rw [le_mul_iff_eq_zero_of_nonneg_of_neg_of_nonneg (norm_nonneg _) hc (norm_nonneg _),
  norm_eq_zero, eventually_and] at h

Result:
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
hc : c < 0
p : ℝ≥0∞
h : (∀ᵐ (x : α) ∂μ, f x = 0) ∧ ∀ᵐ (x : α) ∂μ, g x = 0
⊢ eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0

Proof state:
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
hc : c < 0
p : ℝ≥0∞
h : (∀ᵐ (x : α) ∂μ, f x = 0) ∧ ∀ᵐ (x : α) ∂μ, g x = 0
⊢ eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0

Tactic:
change f =ᵐ[μ] 0 ∧ g =ᵐ[μ] 0 at h

Result:
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
hc : c < 0
p : ℝ≥0∞
h : f =ᶠ[ae μ] 0 ∧ g =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0

Proof state:
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
hc : c < 0
p : ℝ≥0∞
h : f =ᶠ[ae μ] 0 ∧ g =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0

Tactic:
simp [eLpNorm_congr_ae h.1, eLpNorm_congr_ae h.2]

Result:
no goals
-- Mathlib/NumberTheory/BernoulliPolynomials.lean
theorem derivative_bernoulli (k : ℕ) :
    Polynomial.derivative (bernoulli k) = k * bernoulli (k - 1)

Proof state:
case succ
k : ℕ
⊢ derivative (bernoulli (k + 1)) = ↑(k + 1) * bernoulli (k + 1 - 1)

Tactic:
exact mod_cast derivative_bernoulli_add_one k

Result:
no goals

Proof state:
k : ℕ
⊢ derivative (bernoulli k) = ↑k * bernoulli (k - 1)

Tactic:
cases k with
| zero => rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
| succ k => exact mod_cast derivative_bernoulli_add_one k

Result:
no goals

Proof state:
case zero

⊢ derivative (bernoulli 0) = ↑0 * bernoulli (0 - 1)

Tactic:
rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma even_iff_two_dvd : Even a ↔ 2 ∣ a

Proof state:
α : Type u_2
inst✝ : Semiring α
a : α
⊢ Even a ↔ 2 ∣ a

Tactic:
simp [Even, Dvd.dvd, two_mul]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean
theorem ae_finite_setOf_mem {s : ι → Set α} (h : ∑' i, μ (s i) ≠ ∞) :
    ∀ᵐ x ∂μ, {i | x ∈ s i}.Finite

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
h : ∑' (i : ι), μ (s i) ≠ ⊤
⊢ μ {a | ¬{i | a ∈ s i}.Finite} = μ (limsup s cofinite)

Tactic:
congr 1 with x

Result:
case h.e_6.h.h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
h : ∑' (i : ι), μ (s i) ≠ ⊤
x : α
⊢ x ∈ {a | ¬{i | a ∈ s i}.Finite} ↔ x ∈ limsup s cofinite

Proof state:
case h.e_6.h.h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
h : ∑' (i : ι), μ (s i) ≠ ⊤
x : α
⊢ x ∈ {a | ¬{i | a ∈ s i}.Finite} ↔ x ∈ limsup s cofinite

Tactic:
simp [mem_limsup_iff_frequently_mem, Filter.Frequently]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
h : ∑' (i : ι), μ (s i) ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, {i | x ∈ s i}.Finite

Tactic:
rw [ae_iff, ← measure_limsup_cofinite_eq_zero h]

Result:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
h : ∑' (i : ι), μ (s i) ≠ ⊤
⊢ μ {a | ¬{i | a ∈ s i}.Finite} = μ (limsup s cofinite)
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem coeFn_univ_ne_zero (ν : ProbabilityMeasure Ω) : ν univ ≠ 0

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
⊢ ν univ ≠ 0

Tactic:
simp only [coeFn_univ, Ne, one_ne_zero, not_false_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem mem_append_right {b : α} {bs : List α} (as : List α) : b ∈ bs → b ∈ as ++ bs

Proof state:
case cons
α : Type u
b : α
bs : List α
h : b ∈ bs
head✝ : α
tail✝ : List α
tail_ih✝ : b ∈ tail✝ ++ bs
⊢ b ∈ head✝ :: tail✝ ++ bs

Tactic:
apply Mem.tail

Result:
case cons.a
α : Type u
b : α
bs : List α
h : b ∈ bs
head✝ : α
tail✝ : List α
tail_ih✝ : b ∈ tail✝ ++ bs
⊢ Mem b (tail✝.append bs)

Proof state:
case nil
α : Type u
b : α
bs : List α
h : b ∈ bs
⊢ b ∈ nil ++ bs

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u
b : α
bs as : List α
h : b ∈ bs
⊢ b ∈ as ++ bs

Tactic:
induction as with
| nil  => simp [h]
| cons => apply Mem.tail; assumption

Result:
no goals

Proof state:
case cons.a
α : Type u
b : α
bs : List α
h : b ∈ bs
head✝ : α
tail✝ : List α
tail_ih✝ : b ∈ tail✝ ++ bs
⊢ Mem b (tail✝.append bs)

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u
b : α
bs as : List α
⊢ b ∈ bs → b ∈ as ++ bs

Tactic:
intro h

Result:
α : Type u
b : α
bs as : List α
h : b ∈ bs
⊢ b ∈ as ++ bs
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_foldr_inf (l : List (L.BoundedFormula α n)) (v : α → M) (xs : Fin n → M) :
    (l.foldr (· ⊓ ·) ⊤).Realize v xs ↔ ∀ φ ∈ l, BoundedFormula.Realize φ v xs

Proof state:
case cons
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih : (List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ l).Realize v xs ↔ ∀ φ ∈ l, φ.Realize v xs
⊢ (List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ (φ :: l)).Realize v xs ↔ ∀ φ_1 ∈ φ :: l, φ_1.Realize v xs

Tactic:
simp [ih]

Result:
no goals

Proof state:
case nil
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ []).Realize v xs ↔ ∀ φ ∈ [], φ.Realize v xs

Tactic:
simp

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
l : List (L.BoundedFormula α n)
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ l).Realize v xs ↔ ∀ φ ∈ l, φ.Realize v xs

Tactic:
induction' l with φ l ih

Result:
case nil
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ []).Realize v xs ↔ ∀ φ ∈ [], φ.Realize v xs

case cons
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih : (List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ l).Realize v xs ↔ ∀ φ ∈ l, φ.Realize v xs
⊢ (List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ (φ :: l)).Realize v xs ↔ ∀ φ_1 ∈ φ :: l, φ_1.Realize v xs
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
theorem map_neg (a : R) : abv (-a) = abv a

Proof state:
case pos
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : a = 0
⊢ abv (-a) = abv a

Tactic:
simp [ha]

Result:
no goals

Proof state:
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv (-a) * abv (-a) = abv a * abv a

Tactic:
rw [← abv.map_mul, neg_mul_neg, abv.map_mul]

Result:
no goals

Proof state:
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
⊢ abv (-a) = abv a

Tactic:
by_cases ha : a = 0

Result:
case pos
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : a = 0
⊢ abv (-a) = abv a

case neg
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv (-a) = abv a

Proof state:
case neg
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ¬abv (-a) = -abv a

Tactic:
exact ((neg_lt_zero.mpr (abv.pos ha)).trans (abv.pos (neg_ne_zero.mpr ha))).ne'

Result:
no goals

Proof state:
case neg
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv (-a) = abv a

Tactic:
refine
  (mul_self_eq_mul_self_iff.mp (by rw [← abv.map_mul, neg_mul_neg, abv.map_mul])).resolve_right ?_

Result:
case neg
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ¬abv (-a) = -abv a
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem prehaar_sup_le {K₀ : PositiveCompacts G} {U : Set G} (K₁ K₂ : Compacts G)
    (hU : (interior U).Nonempty) :
    prehaar (K₀ : Set G) U (K₁ ⊔ K₂) ≤ prehaar (K₀ : Set G) U K₁ + prehaar (K₀ : Set G) U K₂

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ prehaar (↑K₀) U (K₁ ⊔ K₂) ≤ prehaar (↑K₀) U K₁ + prehaar (↑K₀) U K₂

Tactic:
simp only [prehaar]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) ≤ ↑(index (↑K₁) U) / ↑(index (↑K₀) U) + ↑(index (↑K₂) U) / ↑(index (↑K₀) U)

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) ≤ ↑(index (↑K₁) U) + ↑(index (↑K₂) U)

Tactic:
exact mod_cast index_union_le K₁ K₂ hU

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) ≤ ↑(index (↑K₁) U) / ↑(index (↑K₀) U) + ↑(index (↑K₂) U) / ↑(index (↑K₀) U)

Tactic:
rw [div_add_div_same, div_le_div_iff_of_pos_right]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) ≤ ↑(index (↑K₁) U) + ↑(index (↑K₂) U)

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ 0 < ↑(index (↑K₀) U)

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ 0 < ↑(index (↑K₀) U)

Tactic:
exact mod_cast index_pos K₀ hU

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem IsCompact.nhdsSet_inter_eq [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) :
    𝓝ˢ (s ∩ t) = 𝓝ˢ s ⊓ 𝓝ˢ t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ s ⊓ 𝓝ˢ t ≤ 𝓝ˢ (s ∩ t)

Tactic:
simp_rw [hs.nhdsSet_inf_eq_biSup, ht.inf_nhdsSet_eq_biSup, nhdsSet, sSup_image]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ ⨆ x ∈ s, ⨆ x_2 ∈ t, 𝓝 x ⊓ 𝓝 x_2 ≤ ⨆ a ∈ s ∩ t, 𝓝 a

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ ⨆ x ∈ s, ⨆ x_2 ∈ t, 𝓝 x ⊓ 𝓝 x_2 ≤ ⨆ a ∈ s ∩ t, 𝓝 a

Tactic:
refine iSup₂_le fun x hxs ↦ iSup₂_le fun y hyt ↦ ?_

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
x : X
hxs : x ∈ s
y : X
hyt : y ∈ t
⊢ 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a

Proof state:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
x : X
hxs : x ∈ s
hyt : x ∈ t
⊢ 𝓝 x ⊓ 𝓝 x ≤ ⨆ a ∈ s ∩ t, 𝓝 a

Tactic:
exact le_iSup₂_of_le x ⟨hxs, hyt⟩ (inf_idem _).le

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
x : X
hxs : x ∈ s
y : X
hyt : y ∈ t
⊢ 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a

Tactic:
rcases eq_or_ne x y with (rfl|hne)

Result:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
x : X
hxs : x ∈ s
hyt : x ∈ t
⊢ 𝓝 x ⊓ 𝓝 x ≤ ⨆ a ∈ s ∩ t, 𝓝 a

case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
x : X
hxs : x ∈ s
y : X
hyt : y ∈ t
hne : x ≠ y
⊢ 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a

Proof state:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
x : X
hxs : x ∈ s
y : X
hyt : y ∈ t
hne : x ≠ y
⊢ 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a

Tactic:
exact (disjoint_nhds_nhds.mpr hne).eq_bot ▸ bot_le

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ (s ∩ t) = 𝓝ˢ s ⊓ 𝓝ˢ t

Tactic:
refine le_antisymm (nhdsSet_inter_le _ _) ?_

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ s ⊓ 𝓝ˢ t ≤ 𝓝ˢ (s ∩ t)
-- Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
theorem ContMDiffAt.div {f g : M → G} {x₀ : M} (hf : ContMDiffAt I' I n f x₀)
    (hg : ContMDiffAt I' I n g x₀) : ContMDiffAt I' I n (fun x => f x / g x) x₀

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : WithTop ℕ∞
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : LieGroup I n G
f g : M → G
x₀ : M
hf : ContMDiffAt I' I n f x₀
hg : ContMDiffAt I' I n g x₀
⊢ ContMDiffAt I' I n (fun x => f x / g x) x₀

Tactic:
simp_rw [div_eq_mul_inv]

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : WithTop ℕ∞
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : LieGroup I n G
f g : M → G
x₀ : M
hf : ContMDiffAt I' I n f x₀
hg : ContMDiffAt I' I n g x₀
⊢ ContMDiffAt I' I n (fun x => f x * (g x)⁻¹) x₀

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : WithTop ℕ∞
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : LieGroup I n G
f g : M → G
x₀ : M
hf : ContMDiffAt I' I n f x₀
hg : ContMDiffAt I' I n g x₀
⊢ ContMDiffAt I' I n (fun x => f x * (g x)⁻¹) x₀

Tactic:
exact hf.mul hg.inv

Result:
no goals
-- Mathlib/Probability/Martingale/Convergence.lean
theorem Submartingale.upcrossings_ae_lt_top [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)
    (hbdd : ∀ n, eLpNorm (f n) 1 μ ≤ R) : ∀ᵐ ω ∂μ, ∀ a b : ℚ, a < b → upcrossings a b f ω < ∞

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤

Tactic:
simp only [ae_all_iff, eventually_imp_distrib_left]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
⊢ ∀ (i i_1 : ℚ), i < i_1 → ∀ᵐ (x : Ω) ∂μ, upcrossings (↑i) (↑i_1) f x < ⊤

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
a b : ℚ
hab : a < b
⊢ ∀ᵐ (x : Ω) ∂μ, upcrossings (↑a) (↑b) f x < ⊤

Tactic:
exact hf.upcrossings_ae_lt_top' hbdd (Rat.cast_lt.2 hab)

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
⊢ ∀ (i i_1 : ℚ), i < i_1 → ∀ᵐ (x : Ω) ∂μ, upcrossings (↑i) (↑i_1) f x < ⊤

Tactic:
rintro a b hab

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
a b : ℚ
hab : a < b
⊢ ∀ᵐ (x : Ω) ∂μ, upcrossings (↑a) (↑b) f x < ⊤
-- Mathlib/Algebra/Order/Ring/Canonical.lean
theorem mul_self_tsub_one (a : α) : a * a - 1 = (a + 1) * (a - 1)

Proof state:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : CanonicallyOrderedAdd α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : AddLeftReflectLE α
a : α
⊢ a * a - 1 = (a + 1) * (a - 1)

Tactic:
rw [← mul_self_tsub_mul_self, mul_one]

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive] lemma oneLePart_mul_leOnePart (a : α) : a⁺ᵐ * a⁻ᵐ = |a|ₘ

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁺ᵐ * a⁻ᵐ = mabs a

Tactic:
rw [oneLePart_def, sup_mul, one_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel, sup_assoc,
  ← sup_assoc a, sup_eq_right.2 le_sup_right]

Result:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a ⊔ a⁻¹ ⊔ 1 = mabs a

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a ⊔ a⁻¹ ⊔ 1 = mabs a

Tactic:
exact sup_eq_left.2 <| one_le_mabs a

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_ofNNReal {M : ℝ≥0} {P : ℝ} (hP : 0 ≤ P) : (M : ℝ≥0∞) ^ P = ↑(M ^ P)

Proof state:
M : ℝ≥0
P : ℝ
hP : 0 ≤ P
⊢ ↑M ^ P = ↑(M ^ P)

Tactic:
rw [ENNReal.coe_rpow_of_nonneg _ hP, ← ENNReal.rpow_eq_pow]

Result:
no goals