harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Heyting/Regular.lean
theorem IsRegular.disjoint_compl_right_iff (hb : IsRegular b) :
    Disjoint a bᶜ ↔ a ≤ b

Proof state:
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
hb : IsRegular b
⊢ Disjoint a bᶜ ↔ a ≤ b

Tactic:
rw [← le_compl_iff_disjoint_right, hb.eq]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_smul_left_of_neg (x y : V) {r : ℝ} (hr : r < 0) : angle (r • x) y = angle (-x) y

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : r < 0
⊢ angle (r • x) y = angle (-x) y

Tactic:
rw [angle_comm, angle_smul_right_of_neg y x hr, angle_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem isSome_dite' {p : Prop} [Decidable p] {b : ¬ p → β} :
    (if h : p then none else some (b h)).isSome = true ↔ ¬ p

Proof state:
β : Type u_1
p : Prop
inst✝ : Decidable p
b : ¬p → β
⊢ (if h : p then none else some (b h)).isSome = true ↔ ¬p

Tactic:
split <;> simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_set_self (v : Vector α n) (i : Nat) (hi : i < n) (x : α) :
    (v.set i x hi)[i]? = some x

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
x : α
⊢ (v.set i x hi)[i]? = some x

Tactic:
simp [getElem?_eq_getElem, hi]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean
theorem sSup_unit_ball_eq_norm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E] [SeminormedAddCommGroup F]
    [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E]
    [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
    sSup ((fun x => ‖f x‖) '' ball 0 1) = ‖f‖

Proof state:
𝕜 : Type u_11
𝕜₂ : Type u_12
E : Type u_13
F : Type u_14
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ sSup ((fun x => ‖f x‖) '' ball 0 1) = ‖f‖

Tactic:
simpa only [NNReal.coe_sSup, Set.image_image] using NNReal.coe_inj.2 f.sSup_unit_ball_eq_nnnorm

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem ciSup_add_ciSup (hf : BddAbove (range f)) (g : ι' → Cardinal.{v})
    (hg : BddAbove (range g)) :
    (⨆ i, f i) + (⨆ j, g j) = ⨆ (i) (j), f i + g j

Proof state:
ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
hf : BddAbove (range f)
g : ι' → Cardinal.{v}
hg : BddAbove (range g)
⊢ (⨆ i, f i) + ⨆ j, g j = ⨆ i, ⨆ j, f i + g j

Tactic:
simp_rw [Cardinal.ciSup_add f hf, Cardinal.add_ciSup g hg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem or_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∨ b) = True

Proof state:
a b : Prop
h : a = True
⊢ (a ∨ b) = True

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem join_map_ret (s : Seq α) : Seq.join (Seq.map ret s) = s

Proof state:
case H
α : Type u
s✝ s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct

Tactic:
cases s <;> simp [ret]

Result:
no goals

Proof state:
case H
α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct

Tactic:
intro s

Result:
case H
α : Type u
s✝ s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct

Proof state:
α : Type u
s : Seq α
⊢ (Seq.map ret s).join = s

Tactic:
apply coinduction2 s

Result:
case H
α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma image_add_right_Ico (a b c : α) : (Ico a b).image (· + c) = Ico (a + c) (b + c)

Proof state:
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ico a b) = Ico (a + c) (b + c)

Tactic:
rw [← map_add_right_Ico, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Field.lean
theorem HasProd.norm (hfx : HasProd f x) : HasProd (‖f ·‖) ‖x‖

Proof state:
α : Type u_1
E : Type u_2
inst✝ : NormedField E
f : α → E
x : E
hfx : HasProd f x
⊢ Filter.Tendsto (fun s => ‖∏ b ∈ s, f b‖) Filter.atTop (nhds ‖x‖)

Tactic:
exact hfx.norm

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝ : NormedField E
f : α → E
x : E
hfx : HasProd f x
⊢ HasProd (fun x => ‖f x‖) ‖x‖

Tactic:
simp only [HasProd, ← norm_prod]

Result:
α : Type u_1
E : Type u_2
inst✝ : NormedField E
f : α → E
x : E
hfx : HasProd f x
⊢ Filter.Tendsto (fun s => ‖∏ b ∈ s, f b‖) Filter.atTop (nhds ‖x‖)
-- Mathlib/CategoryTheory/GradedObject.lean
@[reassoc (attr := simp)]
lemma inv_hom_id_eval (e : X ≅ Y) (j : J) :
    e.inv j ≫ e.hom j = 𝟙 _

Proof state:
C : Type u_1
J : Type u_4
inst✝ : Category.{u_5, u_1} C
X Y : GradedObject J C
e : X ≅ Y
j : J
⊢ e.inv j ≫ e.hom j = 𝟙 (Y j)

Tactic:
rw [← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
  GradedObject.categoryOfGradedObjects_id]

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
theorem disjoint_cons_right {a : α} {s t : Multiset α} :
    Disjoint s (a ::ₘ t) ↔ a ∉ s ∧ Disjoint s t

Proof state:
α : Type u_1
a : α
s t : Multiset α
⊢ _root_.Disjoint s (a ::ₘ t) ↔ a ∉ s ∧ _root_.Disjoint s t

Tactic:
rw [_root_.disjoint_comm, disjoint_cons_left]

Result:
α : Type u_1
a : α
s t : Multiset α
⊢ a ∉ s ∧ _root_.Disjoint t s ↔ a ∉ s ∧ _root_.Disjoint s t

Proof state:
α : Type u_1
a : α
s t : Multiset α
⊢ a ∉ s ∧ _root_.Disjoint t s ↔ a ∉ s ∧ _root_.Disjoint s t

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem rename_prod_mk_eval₂ (j : τ) (g : σ → MvPolynomial σ R) :
    rename (Prod.mk j) (p.eval₂ C g) = p.eval₂ C fun x => rename (Prod.mk j) (g x)

Proof state:
case h_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x => (rename (Prod.mk j)) (g x)) p →
      (rename (Prod.mk j)) (eval₂ C g (p * X n)) = eval₂ C (fun x => (rename (Prod.mk j)) (g x)) (p * X n)

Tactic:
intros

Result:
case h_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
p✝ : MvPolynomial σ R
n✝ : σ
a✝ : (rename (Prod.mk j)) (eval₂ C g p✝) = eval₂ C (fun x => (rename (Prod.mk j)) (g x)) p✝
⊢ (rename (Prod.mk j)) (eval₂ C g (p✝ * X n✝)) = eval₂ C (fun x => (rename (Prod.mk j)) (g x)) (p✝ * X n✝)

Proof state:
case h_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
p✝ : MvPolynomial σ R
n✝ : σ
a✝ : (rename (Prod.mk j)) (eval₂ C g p✝) = eval₂ C (fun x => (rename (Prod.mk j)) (g x)) p✝
⊢ (rename (Prod.mk j)) (eval₂ C g (p✝ * X n✝)) = eval₂ C (fun x => (rename (Prod.mk j)) (g x)) (p✝ * X n✝)

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem guard_eq_some' {p : Prop} [Decidable p] (u) : _root_.guard p = some u ↔ p

Proof state:
p : Prop
inst✝ : Decidable p
u : Unit
⊢ _root_.guard p = some u ↔ p

Tactic:
cases u

Result:
case unit
p : Prop
inst✝ : Decidable p
⊢ _root_.guard p = some PUnit.unit ↔ p

Proof state:
case unit
p : Prop
inst✝ : Decidable p
⊢ _root_.guard p = some PUnit.unit ↔ p

Tactic:
by_cases h : p <;> simp [_root_.guard, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isNe_swap {o : Ordering} : o.swap.isNe = o.isNe

Proof state:
o : Ordering
⊢ o.swap.isNe = o.isNe

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_mul_symm_re_eq_norm (x y : E) : re (⟪x, y⟫ * ⟪y, x⟫) = ‖⟪x, y⟫ * ⟪y, x⟫‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re (⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜) = ‖⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜‖

Tactic:
rw [← inner_conj_symm, mul_comm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re (⟪y, x⟫_𝕜 * (starRingEnd 𝕜) ⟪y, x⟫_𝕜) = ‖⟪y, x⟫_𝕜 * (starRingEnd 𝕜) ⟪y, x⟫_𝕜‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re (⟪y, x⟫_𝕜 * (starRingEnd 𝕜) ⟪y, x⟫_𝕜) = ‖⟪y, x⟫_𝕜 * (starRingEnd 𝕜) ⟪y, x⟫_𝕜‖

Tactic:
exact re_eq_norm_of_mul_conj (inner y x)

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem _root_.Continuous.path_trans {f : Y → Path x y} {g : Y → Path y z} :
    Continuous f → Continuous g → Continuous fun t => (f t).trans (g t)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
f : Y → Path x y
g : Y → Path y z
⊢ Continuous f → Continuous g → Continuous fun t => (f t).trans (g t)

Tactic:
intro hf hg

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
f : Y → Path x y
g : Y → Path y z
hf : Continuous f
hg : Continuous g
⊢ Continuous fun t => (f t).trans (g t)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
f : Y → Path x y
g : Y → Path y z
hf : Continuous f
hg : Continuous g
⊢ Continuous ↿fun t => (f t).trans (g t)

Tactic:
exact trans_continuous_family _ (continuous_uncurry_iff.mpr hf) _ (continuous_uncurry_iff.mpr hg)

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
f : Y → Path x y
g : Y → Path y z
hf : Continuous f
hg : Continuous g
⊢ Continuous fun t => (f t).trans (g t)

Tactic:
apply continuous_uncurry_iff.mp

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
f : Y → Path x y
g : Y → Path y z
hf : Continuous f
hg : Continuous g
⊢ Continuous ↿fun t => (f t).trans (g t)
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem associated_one_iff_isUnit [Monoid M] {a : M} : (a : M) ~ᵤ 1 ↔ IsUnit a :=
  Iff.intro
    (fun h =>
      let ⟨c, h⟩ := h.symm
      h ▸ ⟨c, (one_mul _).symm⟩)
    fun ⟨c, h⟩ => Associated.symm ⟨c, by simp [h]⟩

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
x✝ : IsUnit a
c : Mˣ
h : ↑c = a
⊢ 1 * ↑c = a

Tactic:
simp [h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem fst_app_right (a) : K.ι.app (WalkingMultispan.left a) = I.fst a ≫ K.π _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ K.ι.app (WalkingMultispan.left a) = I.fst a ≫ K.π (J.fst a)

Tactic:
rw [← K.w (WalkingMultispan.Hom.fst a)]

Result:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) = I.fst a ≫ K.π (J.fst a)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) = I.fst a ≫ K.π (J.fst a)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Loop.lean
@[simp]
lemma mapEmbedding_isLoop_iff {f : α ↪ β} : (M.mapEmbedding f).IsLoop (f e) ↔ M.IsLoop e

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α ↪ β
⊢ (M.mapEmbedding f).IsLoop (f e) ↔ M.IsLoop e

Tactic:
simp [mapEmbedding, isLoop_iff, isLoop_iff, map_closure_eq, preimage_empty]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean
lemma eisensteinSeries_slash_apply (k : ℤ) (γ : SL(2, ℤ)) :
    eisensteinSeries a k ∣[k] γ = eisensteinSeries (a ᵥ* γ) k

Proof state:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
⊢ eisensteinSeries a k ∣[k] γ = eisensteinSeries (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)) k

Tactic:
ext1 z

Result:
case h
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ (eisensteinSeries a k ∣[k] γ) z = eisensteinSeries (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)) k z

Proof state:
case h
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ (eisensteinSeries a k ∣[k] γ) z = eisensteinSeries (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)) k z

Tactic:
simp_rw [SL_slash, slash_def, slash, ModularGroup.det_coe, ofReal_one, one_zpow, mul_one,
  zpow_neg, mul_inv_eq_iff_eq_mul₀ (zpow_ne_zero _ <| z.denom_ne_zero _), mul_comm,
  eisensteinSeries, ← ModularGroup.sl_moeb, eisSummand_SL2_apply, tsum_mul_left]

Result:
case h
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ denom (↑γ) z ^ k * ∑' (x : ↑(gammaSet N a)), eisSummand k (↑x ᵥ* ↑γ) z =
    denom (↑γ) z ^ k *
      ∑' (x : ↑(gammaSet N (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)))), eisSummand k (↑x) z
-- Mathlib/Topology/Basic.lean
theorem subset_interior_iff_isOpen : s ⊆ interior s ↔ IsOpen s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ s ⊆ interior s ↔ IsOpen s

Tactic:
simp only [interior_eq_iff_isOpen.symm, Subset.antisymm_iff, interior_subset, true_and]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
@[simp, norm_cast]
lemma ofReal_le_ofReal {x y : ℝ} : (x : K) ≤ (y : K) ↔ x ≤ y

Proof state:
K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ re ↑x ≤ re ↑y ∧ im ↑x = im ↑y ↔ x ≤ y

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ ↑x ≤ ↑y ↔ x ≤ y

Tactic:
rw [le_iff_re_im]

Result:
K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ re ↑x ≤ re ↑y ∧ im ↑x = im ↑y ↔ x ≤ y
-- Mathlib/Order/Compare.lean
theorem Compares.eq_lt [Preorder α] : ∀ {o} {a b : α}, Compares o a b → (o = lt ↔ a < b)
  | lt, _, _, h => ⟨fun _ => h, fun _ => rfl⟩
  | eq, a, b, h => ⟨fun h => by injection h, fun h' => (ne_of_lt h' h).elim⟩
  | gt, a, b, h => ⟨fun h => by injection h, fun h' => (lt_asymm h h').elim⟩

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h✝ : gt.Compares a b
h : gt = lt
⊢ a < b

Tactic:
injection h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h✝ : eq.Compares a b
h : eq = lt
⊢ a < b

Tactic:
injection h

Result:
no goals
-- Mathlib/Data/Finset/Dedup.lean
theorem toFinset_subset : s.toFinset ⊆ t.toFinset ↔ s ⊆ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.toFinset ⊆ t.toFinset ↔ s ⊆ t

Tactic:
simp only [Finset.subset_iff, Multiset.subset_iff, Multiset.mem_toFinset]

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem prod_ofNatMultiset (v : Multiset ℕ) (h) :
    ((ofNatMultiset v h).prod : ℕ) = (v.prod : ℕ)

Proof state:
v : Multiset ℕ
h : ∀ p ∈ v, Nat.Prime p
⊢ ↑(ofNatMultiset v h).prod = v.prod

Tactic:
rw [coe_prod, to_ofNatMultiset]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem EqOn.piecewise_ite' {f f' g : α → β} {t t'} (h : EqOn f g (t ∩ s))
    (h' : EqOn f' g (t' ∩ sᶜ)) : EqOn (s.piecewise f f') g (s.ite t t')

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t t' : Set α
h : EqOn f g (t ∩ s)
h' : EqOn f' g (t' ∩ sᶜ)
⊢ EqOn (s.piecewise f f') g (s.ite t t')

Tactic:
simp [eqOn_piecewise, *]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem not_disjoint_coe_iff_nonempty_inter :
    ¬Disjoint (I : WithBot (Box ι)) J ↔ (I ∩ J : Set (ι → ℝ)).Nonempty

Proof state:
ι : Type u_1
I J : Box ι
⊢ ¬Disjoint ↑I ↑J ↔ (↑I ∩ ↑J).Nonempty

Tactic:
rw [disjoint_coe, Set.not_disjoint_iff_nonempty_inter]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
lemma measure_inter_conull' (ht : μ (s \ t) = 0) : μ (s ∩ t) = μ s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : μ (s \ t) = 0
⊢ μ (s ∩ t) = μ s

Tactic:
rw [← diff_compl, measure_diff_null']

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : μ (s \ t) = 0
⊢ μ (s ∩ tᶜ) = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : μ (s \ t) = 0
⊢ μ (s ∩ tᶜ) = 0

Tactic:
rwa [← diff_eq]

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map_map₂ (m : α → β → γ) (n : γ → δ) :
    (map₂ m f g).map n = map₂ (fun a b => n (m a b)) f g

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β → γ
n : γ → δ
⊢ map (n ∘ fun p => m p.1 p.2) (f ×ˢ g) = map (fun p => n (m p.1 p.2)) (f ×ˢ g)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β → γ
n : γ → δ
⊢ map n (map₂ m f g) = map₂ (fun a b => n (m a b)) f g

Tactic:
rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, map_map]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β → γ
n : γ → δ
⊢ map (n ∘ fun p => m p.1 p.2) (f ×ˢ g) = map (fun p => n (m p.1 p.2)) (f ×ˢ g)
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma deriv_negMulLog {x : ℝ} (hx : x ≠ 0) : deriv negMulLog x = - log x - 1

Proof state:
x : ℝ
hx : x ≠ 0
⊢ deriv negMulLog x = -log x - 1

Tactic:
rw [negMulLog_eq_neg, deriv.neg, deriv_mul_log hx]

Result:
x : ℝ
hx : x ≠ 0
⊢ -(log x + 1) = -log x - 1

Proof state:
x : ℝ
hx : x ≠ 0
⊢ -(log x + 1) = -log x - 1

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem not_mem_nil {v : α} : ¬Mem v ([] : CNF α)

Proof state:
α : Type u_1
v : α
⊢ ¬Mem v []

Tactic:
simp [Mem]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma tendsto_densityProcess_atTop_of_antitone (κ : Kernel α (γ × β)) (ν : Kernel α γ)
    [IsFiniteKernel κ] (n : ℕ) (a : α) (x : γ)
    (seq : ℕ → Set β) (hseq : Antitone seq) (hseq_iInter : ⋂ i, seq i = ∅)
    (hseq_meas : ∀ m, MeasurableSet (seq m)) :
    Tendsto (fun m ↦ densityProcess κ ν n a x (seq m)) atTop (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun m => κ.densityProcess ν n a x (seq m)) atTop (𝓝 (κ.densityProcess ν n a x ∅))

Tactic:
exact tendsto_densityProcess_atTop_empty_of_antitone κ ν n a x seq hseq hseq_iInter hseq_meas

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun m => κ.densityProcess ν n a x (seq m)) atTop (𝓝 0)

Tactic:
rw [← densityProcess_empty κ ν n a x]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun m => κ.densityProcess ν n a x (seq m)) atTop (𝓝 (κ.densityProcess ν n a x ∅))
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.qr₃ (a b : ℕ) (r : ℤ) (ha : a % 4 = 3) (hb : b % 4 = 3)
    (hr : jacobiSymNat b a = r) : jacobiSymNat a b = -r

Proof state:
a b : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
hr : jacobiSymNat b a = r
⊢ jacobiSymNat a b = -r

Tactic:
rwa [jacobiSymNat, jacobiSym.quadratic_reciprocity_three_mod_four ha hb, neg_inj]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem vanishingIdeal_zeroLocus_eq_radical (I : Ideal R) :
    vanishingIdeal (zeroLocus (I : Set R)) = I.radical :=
  Ideal.ext fun f => by
    rw [mem_vanishingIdeal, Ideal.radical_eq_sInf, Submodule.mem_sInf]
    exact ⟨fun h x hx => h ⟨x, hx.2⟩ hx.1, fun h x hx => h x.1 ⟨hx, x.2⟩⟩

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R
⊢ (∀ x ∈ zeroLocus ↑I, f ∈ x.asIdeal) ↔ ∀ p ∈ {J | I ≤ J ∧ J.IsPrime}, f ∈ p

Tactic:
exact ⟨fun h x hx => h ⟨x, hx.2⟩ hx.1, fun h x hx => h x.1 ⟨hx, x.2⟩⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R
⊢ f ∈ vanishingIdeal (zeroLocus ↑I) ↔ f ∈ I.radical

Tactic:
rw [mem_vanishingIdeal, Ideal.radical_eq_sInf, Submodule.mem_sInf]

Result:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R
⊢ (∀ x ∈ zeroLocus ↑I, f ∈ x.asIdeal) ↔ ∀ p ∈ {J | I ≤ J ∧ J.IsPrime}, f ∈ p
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
    (not_contains : (toInsert.map Prod.fst).contains k = false) :
    getValue? k (insertListConst l toInsert) = getValue? k l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ getValue? k (insertListConst l toInsert) = getValue? k l

Tactic:
unfold insertListConst

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ getValue? k (insertList l (List.map Prod.toSigma toInsert)) = getValue? k l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ (List.map Sigma.fst (List.map Prod.toSigma toInsert)).contains k = false

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ containsKey k (List.map Prod.toSigma toInsert) = false

Tactic:
rw [containsKey_eq_contains_map_fst]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ (List.map Sigma.fst (List.map Prod.toSigma toInsert)).contains k = false

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ getValue? k (insertList l (List.map Prod.toSigma toInsert)) = getValue? k l

Tactic:
rw [getValue?_eq_getEntry?, getValue?_eq_getEntry?, getEntry?_insertList_of_contains_eq_false]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ containsKey k (List.map Prod.toSigma toInsert) = false
-- Mathlib/Data/Nat/Digits.lean
theorem digits_one (b n) (n0 : 0 < n) (nb : n < b) : Nat.digits b n = [n] ∧ 1 < b ∧ 0 < n

Proof state:
b n : ℕ
n0 : 0 < n
nb : n < b
⊢ b.digits n = [n] ∧ 1 < b ∧ 0 < n

Tactic:
have b2 : 1 < b :=
  lt_iff_add_one_le.mpr (le_trans (add_le_add_right (lt_iff_add_one_le.mp n0) 1) nb)

Result:
b n : ℕ
n0 : 0 < n
nb : n < b
b2 : 1 < b
⊢ b.digits n = [n] ∧ 1 < b ∧ 0 < n

Proof state:
b n : ℕ
n0 : 0 < n
nb : n < b
b2 : 1 < b
⊢ b.digits n = [n] ∧ 1 < b ∧ 0 < n

Tactic:
refine ⟨?_, b2, n0⟩

Result:
b n : ℕ
n0 : 0 < n
nb : n < b
b2 : 1 < b
⊢ b.digits n = [n]

Proof state:
b n : ℕ
n0 : 0 < n
nb : n < b
b2 : 1 < b
⊢ b.digits n = [n]

Tactic:
rw [Nat.digits_def' b2 n0, Nat.mod_eq_of_lt nb, Nat.div_eq_zero_iff.2 <| .inr nb, Nat.digits_zero]

Result:
no goals