harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/Ultra/Basic.lean
lemma closedBall_eq_of_mem {x y: X} {r : ℝ} (h : y ∈ closedBall x r) :
    closedBall x r = closedBall y r

Proof state:
case h
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ closedBall x r
x✝ : X
⊢ x✝ ∈ closedBall x r ↔ x✝ ∈ closedBall y r

Tactic:
simp_rw [mem_closedBall] at h ⊢

Result:
case h
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
x✝ : X
h : dist y x ≤ r
⊢ dist x✝ x ≤ r ↔ dist x✝ y ≤ r

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ closedBall x r
⊢ closedBall x r = closedBall y r

Tactic:
ext

Result:
case h
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ closedBall x r
x✝ : X
⊢ x✝ ∈ closedBall x r ↔ x✝ ∈ closedBall y r

Proof state:
case h
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
x✝ : X
h : dist y x ≤ r
⊢ dist x✝ x ≤ r ↔ dist x✝ y ≤ r

Tactic:
constructor <;> intro h' <;>
exact (dist_triangle_max _ _ _).trans (max_le h' (dist_comm x _ ▸ h))

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem mem_closure_singleton {x y : M} : y ∈ closure ({x} : Set M) ↔ ∃ n : ℕ, x ^ n = y

Proof state:
M : Type u_1
inst✝ : Monoid M
x y : M
⊢ y ∈ closure {x} ↔ ∃ n, x ^ n = y

Tactic:
rw [closure_singleton_eq, mem_mrange]

Result:
M : Type u_1
inst✝ : Monoid M
x y : M
⊢ (∃ x_1, ((powersHom M) x) x_1 = y) ↔ ∃ n, x ^ n = y

Proof state:
M : Type u_1
inst✝ : Monoid M
x y : M
⊢ (∃ x_1, ((powersHom M) x) x_1 = y) ↔ ∃ n, x ^ n = y

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem subset_singleton_iff {s : Finset α} {a : α} : s ⊆ {a} ↔ s = ∅ ∨ s = {a}

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ s ⊆ {a} ↔ s = ∅ ∨ s = {a}

Tactic:
rw [← coe_subset, coe_singleton, Set.subset_singleton_iff_eq, coe_eq_empty, coe_eq_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem nil_eq_flatten_iff {L : List (List α)} : [] = L.flatten ↔ ∀ l ∈ L, l = []

Proof state:
α : Type u_1
L : List (List α)
⊢ [] = L.flatten ↔ ∀ (l : List α), l ∈ L → l = []

Tactic:
rw [eq_comm, flatten_eq_nil_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWith_comm_of_comm (f : α → α → β) (comm : ∀ x y : α, f x y = f y x) (l l' : List α) :
    zipWith f l l' = zipWith f l' l

Proof state:
α : Type u_1
β : Type u_2
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : List α
⊢ zipWith (fun b a => f a b) l' l = zipWith f l' l

Tactic:
simp only [comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : List α
⊢ zipWith f l l' = zipWith f l' l

Tactic:
rw [zipWith_comm]

Result:
α : Type u_1
β : Type u_2
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : List α
⊢ zipWith (fun b a => f a b) l' l = zipWith f l' l
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
lemma mem_ker_iff (S : Submonoid R) {g : M →ₗ[R] M'}
    [IsLocalizedModule S g] {m : M} :
    m ∈ LinearMap.ker g ↔ ∃ r ∈ S, r • m = 0

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
m : M
⊢ m ∈ LinearMap.ker g ↔ ∃ r ∈ S, r • m = 0

Tactic:
simpa using IsLocalizedModule.eq_zero_iff S g

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem _root_.Disjoint.of_preimage (hf : Surjective f) {s t : Set β}
    (h : Disjoint (f ⁻¹' s) (f ⁻¹' t)) : Disjoint s t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
⊢ Disjoint s t

Tactic:
rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq,
  image_empty]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem map_add_smul_aux [DecidableEq ι] (i : ι) (x : Π i, s i) (u : s i →ₗ[R] t i) :
    (fun j ↦ update f i u j (x j)) = update (fun j ↦ (f j) (x j)) i (u (x i))

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁵ : CommSemiring R
s : ι → Type u_7
inst✝⁴ : (i : ι) → AddCommMonoid (s i)
inst✝³ : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
inst✝ : DecidableEq ι
i : ι
x : (i : ι) → s i
u : s i →ₗ[R] t i
⊢ (fun j => (update f i u j) (x j)) = update (fun j => (f j) (x j)) i (u (x i))

Tactic:
ext j

Result:
case h
ι : Type u_1
R : Type u_4
inst✝⁵ : CommSemiring R
s : ι → Type u_7
inst✝⁴ : (i : ι) → AddCommMonoid (s i)
inst✝³ : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
inst✝ : DecidableEq ι
i : ι
x : (i : ι) → s i
u : s i →ₗ[R] t i
j : ι
⊢ (update f i u j) (x j) = update (fun j => (f j) (x j)) i (u (x i)) j

Proof state:
case h
ι : Type u_1
R : Type u_4
inst✝⁵ : CommSemiring R
s : ι → Type u_7
inst✝⁴ : (i : ι) → AddCommMonoid (s i)
inst✝³ : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
inst✝ : DecidableEq ι
i : ι
x : (i : ι) → s i
u : s i →ₗ[R] t i
j : ι
⊢ (update f i u j) (x j) = update (fun j => (f j) (x j)) i (u (x i)) j

Tactic:
exact apply_update (fun i F => F (x i)) f i u j

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_right_comm (a m n : Nat) : (a ^ m) ^ n = (a ^ n) ^ m

Proof state:
a m n : Nat
⊢ (a ^ m) ^ n = (a ^ n) ^ m

Tactic:
rw [← Nat.pow_mul, Nat.pow_mul']

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem span_apply [DecidableEq E] {v' : ι' → E} (h : Orthonormal 𝕜 v') (s : Finset ι')
    (i : s) : (OrthonormalBasis.span h s i : E) = v' i

Proof state:
ι' : Type u_2
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
v' : ι' → E
h : Orthonormal 𝕜 v'
s : Finset ι'
i : { x // x ∈ s }
⊢ ↑((OrthonormalBasis.span h s) i) = v' ↑i

Tactic:
simp only [OrthonormalBasis.span, Basis.span_apply, LinearIsometryEquiv.ofEq_symm,
  OrthonormalBasis.map_apply, OrthonormalBasis.coe_mk, LinearIsometryEquiv.coe_ofEq_apply,
  comp_apply]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/ConstructibleSet.lean
lemma map_comp [DecidableEq S] [DecidableEq T] (f : S →+* T) (g : R →+* S)
    (s : ConstructibleSetData R) : s.map (f.comp g) = (s.map g).map f

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : CommSemiring T
inst✝¹ : DecidableEq S
inst✝ : DecidableEq T
f : S →+* T
g : R →+* S
s : ConstructibleSetData R
⊢ map (f.comp g) s = map f (map g s)

Tactic:
simp [map, image_image, Function.comp_def]

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
theorem count_coe_fill_self_of_not_mem [DecidableEq α] {a : α} {i : Fin (n + 1)} {s : Sym α (n - i)}
    (hx : a ∉ s) :
    count a (fill a i s : Multiset α) = i

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : a ∉ s
⊢ count a ↑(fill a i s) = ↑i

Tactic:
simp [coe_fill, coe_replicate, hx]

Result:
no goals
-- Mathlib/Data/Set/BoolIndicator.lean
theorem not_mem_iff_boolIndicator (x : α) : x ∉ s ↔ s.boolIndicator x = false

Proof state:
α : Type u_1
s : Set α
x : α
⊢ x ∉ s ↔ (if x ∈ s then true else false) = false

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
x : α
⊢ x ∉ s ↔ s.boolIndicator x = false

Tactic:
unfold boolIndicator

Result:
α : Type u_1
s : Set α
x : α
⊢ x ∉ s ↔ (if x ∈ s then true else false) = false
-- Mathlib/Analysis/Complex/Isometry.lean
theorem LinearIsometry.re_apply_eq_re_of_add_conj_eq (f : ℂ →ₗᵢ[ℝ] ℂ)
    (h₃ : ∀ z, z + conj z = f z + conj (f z)) (z : ℂ) : (f z).re = z.re

Proof state:
f : ℂ →ₗᵢ[ℝ] ℂ
h₃ : ∀ (z : ℂ), z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
z : ℂ
⊢ (f z).re = z.re

Tactic:
simpa [Complex.ext_iff, add_re, add_im, conj_re, conj_im, ← two_mul,
  show (2 : ℝ) ≠ 0 by simp [two_ne_zero]] using (h₃ z).symm

Result:
no goals

Proof state:
f : ℂ →ₗᵢ[ℝ] ℂ
h₃ : ∀ (z : ℂ), z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
z : ℂ
⊢ 2 ≠ 0

Tactic:
simp [two_ne_zero]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Defs.lean
theorem mk_eq_mk {p q p' q' : K[X]} (hq : q ≠ 0) (hq' : q' ≠ 0) :
    RatFunc.mk p q = RatFunc.mk p' q' ↔ p * q' = p' * q

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
⊢ RatFunc.mk p q = RatFunc.mk p' q' ↔ p * q' = p' * q

Tactic:
rw [mk_def_of_ne _ hq, mk_def_of_ne _ hq', ofFractionRing_injective.eq_iff,
  IsLocalization.mk'_eq_iff_eq',
  (IsFractionRing.injective K[X] (FractionRing K[X])).eq_iff]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem univ_pi_subset_univ_pi_iff :
    pi univ t₁ ⊆ pi univ t₂ ↔ (∀ i, t₁ i ⊆ t₂ i) ∨ ∃ i, t₁ i = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
t₁ t₂ : (i : ι) → Set (α i)
⊢ univ.pi t₁ ⊆ univ.pi t₂ ↔ (∀ (i : ι), t₁ i ⊆ t₂ i) ∨ ∃ i, t₁ i = ∅

Tactic:
simp [pi_subset_pi_iff]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem _root_.Basis.toBasis_toOrthonormalBasis (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
    (v.toOrthonormalBasis hv).toBasis = v

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
⊢ (v.toOrthonormalBasis hv).toBasis = v

Tactic:
simp [Basis.toOrthonormalBasis, OrthonormalBasis.toBasis]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem tendstoUniformly_iff {F : ι → β → α} {f : β → α} {p : Filter ι} :
    TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x, dist (f x) (F n x) < ε

Proof state:
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε

Tactic:
rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff]

Result:
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
⊢ (∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ univ, dist (f x) (F n x) < ε) ↔
    ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε

Proof state:
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
⊢ (∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ univ, dist (f x) (F n x) < ε) ↔
    ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem insert_diff_singleton {a : α} {s : Set α} : insert a (s \ {a}) = insert a s

Proof state:
α : Type u
a : α
s : Set α
⊢ insert a (s \ {a}) = insert a s

Tactic:
simp [insert_eq, union_diff_self, -union_singleton, -singleton_union]

Result:
no goals
-- Mathlib/Order/Sublattice.lean
@[simp] lemma pi_univ_eq_bot_iff {L : ∀ i, Sublattice (π i)} : pi univ L = ⊥ ↔ ∃ i, L i = ⊥

Proof state:
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ ↑(pi univ L) = ↑⊥ ↔ ∃ i, ↑(L i) = ↑⊥

Tactic:
simp

Result:
no goals

Proof state:
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ pi univ L = ⊥ ↔ ∃ i, L i = ⊥

Tactic:
simp_rw [← coe_inj]

Result:
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ ↑(pi univ L) = ↑⊥ ↔ ∃ i, ↑(L i) = ↑⊥
-- Mathlib/Topology/Constructible.lean
@[stacks 0069 "Iff form of (2). Note that Stacks doesn't define quasi-separated spaces."]
lemma _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact_iff_isCompact
    (basis : IsTopologicalBasis (range b)) (isCompact_basis : ∀ i, IsCompact (b i))
    (hU : IsOpen U) : IsRetrocompact U ↔ IsCompact U :=
  basis.isRetrocompact_iff_isCompact' (by simpa using isCompact_basis) hU

Proof state:
ι : Sort u_1
X : Type u_2
inst✝² : TopologicalSpace X
U : Set X
inst✝¹ : CompactSpace X
b : ι → Set X
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
hU : IsOpen U
⊢ ∀ U ∈ range b, IsCompact U

Tactic:
simpa using isCompact_basis

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Module.lean
lemma Module.isClosed_support [Module.Finite R M] :
    IsClosed (Module.support R M)

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
⊢ IsClosed (support R M)

Tactic:
rw [support_eq_zeroLocus]

Result:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
⊢ IsClosed (PrimeSpectrum.zeroLocus ↑(annihilator R M))

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
⊢ IsClosed (PrimeSpectrum.zeroLocus ↑(annihilator R M))

Tactic:
apply PrimeSpectrum.isClosed_zeroLocus

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
lemma measure_Ioi {l : ℝ} (hf : Tendsto f atTop (𝓝 l)) (x : ℝ) :
    f.measure (Ioi x) = ofReal (l - f x)

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ f.measure (Ioi x) = ofReal (l - ↑f x)

Tactic:
rw [← Ici_diff_left, measure_diff _ (nullMeasurableSet_singleton x), measure_singleton,
  f.measure_Ici hf, ← ofReal_sub _ (sub_nonneg.mpr <| Monotone.leftLim_le f.mono' le_rfl)]
  <;> simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
/-- The p-adic valuation of `n` is equal to the logarithm w.r.t `p` iff
    `n` is less than `p` raised to one plus the p-adic valuation of `n`. -/
lemma nat_log_eq_padicValNat_iff {n : ℕ} [hp : Fact (Nat.Prime p)] (hn : 0 < n) :
    Nat.log p n = padicValNat p n ↔ n < p ^ (padicValNat p n + 1)

Proof state:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
⊢ n < p ^ (padicValNat p n + 1) → p ^ padicValNat p n ≤ n

Tactic:
exact fun _ => Nat.le_of_dvd hn pow_padicValNat_dvd

Result:
no goals

Proof state:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
⊢ n ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
⊢ log p n = padicValNat p n ↔ n < p ^ (padicValNat p n + 1)

Tactic:
rw [Nat.log_eq_iff (Or.inr ⟨(Nat.Prime.one_lt' p).out, by omega⟩), and_iff_right_iff_imp]

Result:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
⊢ n < p ^ (padicValNat p n + 1) → p ^ padicValNat p n ≤ n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_append (f : α → β → β) (b) (l l' : List α) :
    (l ++ l').foldr f b = l.foldr f (l'.foldr f b)

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l l' : List α
⊢ foldr f b (l ++ l') = foldr f (foldr f b l') l

Tactic:
simp [foldr_eq_foldrM]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem summable_norm_geometric_of_norm_lt_one {r : R}
    (hr : ‖r‖ < 1) : Summable fun n : ℕ ↦ ‖(r ^ n : R)‖

Proof state:
R : Type u_2
inst✝ : NormedRing R
r : R
hr : ‖r‖ < 1
⊢ Summable fun n => ‖r ^ n‖

Tactic:
simpa using summable_norm_pow_mul_geometric_of_norm_lt_one 0 hr

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem UniformSpace.ball_mem_nhds (x : α) ⦃V : Set (α × α)⦄ (V_in : V ∈ 𝓤 α) : ball x V ∈ 𝓝 x

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ ∃ V_1 ∈ 𝓤 α, ball x V_1 ⊆ ball x V

Tactic:
exact ⟨V, V_in, Subset.rfl⟩

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ ball x V ∈ 𝓝 x

Tactic:
rw [UniformSpace.mem_nhds_iff]

Result:
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ ∃ V_1 ∈ 𝓤 α, ball x V_1 ⊆ ball x V
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem unzip_eq_map : ∀ l : List (α × β), unzip l = (l.map Prod.fst, l.map Prod.snd)
  | [] => rfl
  | (a, b) :: l => by simp only [unzip_cons, map_cons, unzip_eq_map l]

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
l : List (α × β)
⊢ ((a, b) :: l).unzip = (map Prod.fst ((a, b) :: l), map Prod.snd ((a, b) :: l))

Tactic:
simp only [unzip_cons, map_cons, unzip_eq_map l]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_sigma {β : α → Type*} [Fintype α] [∀ a, Finite (β a)] :
    Nat.card (Sigma β) = ∑ a, Nat.card (β a)

Proof state:
α : Type u_1
β : α → Type u_3
inst✝¹ : Fintype α
inst✝ : ∀ (a : α), Finite (β a)
⊢ Nat.card (Sigma β) = ∑ a : α, Nat.card (β a)

Tactic:
letI _ (a : α) : Fintype (β a) := Fintype.ofFinite (β a)

Result:
α : Type u_1
β : α → Type u_3
inst✝¹ : Fintype α
inst✝ : ∀ (a : α), Finite (β a)
x✝ : (a : α) → Fintype (β a) := fun a => Fintype.ofFinite (β a)
⊢ Nat.card (Sigma β) = ∑ a : α, Nat.card (β a)

Proof state:
α : Type u_1
β : α → Type u_3
inst✝¹ : Fintype α
inst✝ : ∀ (a : α), Finite (β a)
x✝ : (a : α) → Fintype (β a) := fun a => Fintype.ofFinite (β a)
⊢ Nat.card (Sigma β) = ∑ a : α, Nat.card (β a)

Tactic:
simp_rw [Nat.card_eq_fintype_card, Fintype.card_sigma]

Result:
no goals
-- Mathlib/Algebra/Module/NatInt.lean
theorem Int.smul_one_eq_cast {R : Type*} [NonAssocRing R] (m : ℤ) : m • (1 : R) = ↑m

Proof state:
R : Type u_5
inst✝ : NonAssocRing R
m : ℤ
⊢ m • 1 = ↑m

Tactic:
rw [zsmul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
lemma ofArrows_mk (i : I) : ofArrows Y f (f i) :=
  ⟨_, 𝟙 _, _, ⟨i⟩, by simp⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
i : I
⊢ 𝟙 (Y i) ≫ f i = f i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@[simp]
lemma fromCols_fromRows_eq_fromBlocks (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R)
    (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
    fromCols (fromRows B₁₁ B₂₁) (fromRows B₁₂ B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

Tactic:
ext (_ | _) (_ | _) <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_lineMap_image (x y : P) (s : Set ℝ) :
    μH[1] (AffineMap.lineMap x y '' s) = nndist x y • μH[1] s

Proof state:
E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
s : Set ℝ
this : μH[1] (⇑(IsometryEquiv.vaddConst x) '' ((fun x_1 => x_1 • (y -ᵥ x)) '' s)) = nndist x y • μH[1] s
⊢ μH[1] (⇑(AffineMap.lineMap x y) '' s) = nndist x y • μH[1] s

Tactic:
simpa only [Set.image_image]

Result:
no goals

Proof state:
E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
s : Set ℝ
⊢ μH[1] (⇑(IsometryEquiv.vaddConst x) '' ((fun x_1 => x_1 • (y -ᵥ x)) '' s)) = nndist x y • μH[1] s

Tactic:
borelize E

Result:
E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
s : Set ℝ
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ μH[1] (⇑(IsometryEquiv.vaddConst x) '' ((fun x_1 => x_1 • (y -ᵥ x)) '' s)) = nndist x y • μH[1] s

Proof state:
E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
s : Set ℝ
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ μH[1] (⇑(IsometryEquiv.vaddConst x) '' ((fun x_1 => x_1 • (y -ᵥ x)) '' s)) = nndist x y • μH[1] s

Tactic:
rw [IsometryEquiv.hausdorffMeasure_image, hausdorffMeasure_smul_right_image,
  nndist_eq_nnnorm_vsub' E]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobject_factors_iff {W : C} (h : W ⟶ X) :
    (kernelSubobject f).Factors h ↔ h ≫ f = 0 :=
  ⟨fun w => by
    rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, kernelSubobject_arrow_comp,
      comp_zero],
    kernelSubobject_factors f h⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : (kernelSubobject f).Factors h
⊢ h ≫ f = 0

Tactic:
rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, kernelSubobject_arrow_comp,
  comp_zero]

Result:
no goals
-- Mathlib/Order/Filter/Finite.lean
theorem sInter_mem {s : Set (Set α)} (hfin : s.Finite) : ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f

Proof state:
α : Type u
f : Filter α
s : Set (Set α)
hfin : s.Finite
⊢ ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f

Tactic:
rw [sInter_eq_biInter, biInter_mem hfin]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_diff (ht : MeasurableSet t) (hfs : IntegrableOn f s μ) (hts : t ⊆ s) :
    ∫ x in s \ t, f x ∂μ = ∫ x in s, f x ∂μ - ∫ x in t, f x ∂μ

Proof state:
case hst
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : MeasurableSet t
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ Disjoint (s \ t) t

case ht
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : MeasurableSet t
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ MeasurableSet t

case hfs
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : MeasurableSet t
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ IntegrableOn f (s \ t) μ

case hft
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : MeasurableSet t
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ IntegrableOn f t μ

Tactic:
exacts [disjoint_sdiff_self_left, ht, hfs.mono_set diff_subset, hfs.mono_set hts]

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : MeasurableSet t
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ - ∫ (x : X) in t, f x ∂μ

Tactic:
rw [eq_sub_iff_add_eq, ← setIntegral_union, diff_union_of_subset hts]

Result:
case hst
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : MeasurableSet t
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ Disjoint (s \ t) t

case ht
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : MeasurableSet t
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ MeasurableSet t

case hfs
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : MeasurableSet t
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ IntegrableOn f (s \ t) μ

case hft
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : MeasurableSet t
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ IntegrableOn f t μ
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_insert [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    (h : Raw.WFImp m.1) {a : α} {b : β a} : Raw.WFImp (m.insert a b).1

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (m.insert a b).val

Tactic:
rw [insert_eq_insertₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (m.insertₘ a b).val

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (m.insertₘ a b).val

Tactic:
exact wfImp_insertₘ h

Result:
no goals