harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.inter_iInter_nonempty {ι : Type v} (hs : IsCompact s) (t : ι → Set X)
    (htc : ∀ i, IsClosed (t i)) (hst : ∀ u : Finset ι, (s ∩ ⋂ i ∈ u, t i).Nonempty) :
    (s ∩ ⋂ i, t i).Nonempty

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : s ∩ ⋂ i, t i = ∅
⊢ ∃ u, s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
exact hs.elim_finite_subfamily_closed t htc hst

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : ∀ (u : Finset ι), (s ∩ ⋂ i ∈ u, t i).Nonempty
⊢ (s ∩ ⋂ i, t i).Nonempty

Tactic:
contrapose! hst

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : s ∩ ⋂ i, t i = ∅
⊢ ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem Function.Surjective.mul_comm [Mul M] [Mul N] {f : M →ₙ* N}
    (is_surj : Function.Surjective f) (is_comm : Std.Commutative (· * · : M → M → M)) :
    Std.Commutative (· * · : N → N → N) where
  comm := fun a b ↦ by
    obtain ⟨a', ha'⟩ := is_surj a
    obtain ⟨b', hb'⟩ := is_surj b
    simp only [← ha', ← hb', ← map_mul]
    rw [is_comm.comm]

Proof state:
case intro.intro
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
is_surj : Surjective ⇑f
is_comm : Std.Commutative fun x1 x2 => x1 * x2
a b : N
a' : M
ha' : f a' = a
b' : M
hb' : f b' = b
⊢ a * b = b * a

Tactic:
simp only [← ha', ← hb', ← map_mul]

Result:
case intro.intro
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
is_surj : Surjective ⇑f
is_comm : Std.Commutative fun x1 x2 => x1 * x2
a b : N
a' : M
ha' : f a' = a
b' : M
hb' : f b' = b
⊢ f (a' * b') = f (b' * a')

Proof state:
case intro.intro
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
is_surj : Surjective ⇑f
is_comm : Std.Commutative fun x1 x2 => x1 * x2
a b : N
a' : M
ha' : f a' = a
b' : M
hb' : f b' = b
⊢ f (a' * b') = f (b' * a')

Tactic:
rw [is_comm.comm]

Result:
no goals

Proof state:
case intro
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
is_surj : Surjective ⇑f
is_comm : Std.Commutative fun x1 x2 => x1 * x2
a b : N
a' : M
ha' : f a' = a
⊢ a * b = b * a

Tactic:
obtain ⟨b', hb'⟩ := is_surj b

Result:
case intro.intro
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
is_surj : Surjective ⇑f
is_comm : Std.Commutative fun x1 x2 => x1 * x2
a b : N
a' : M
ha' : f a' = a
b' : M
hb' : f b' = b
⊢ a * b = b * a

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
is_surj : Surjective ⇑f
is_comm : Std.Commutative fun x1 x2 => x1 * x2
a b : N
⊢ a * b = b * a

Tactic:
obtain ⟨a', ha'⟩ := is_surj a

Result:
case intro
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
is_surj : Surjective ⇑f
is_comm : Std.Commutative fun x1 x2 => x1 * x2
a b : N
a' : M
ha' : f a' = a
⊢ a * b = b * a
-- Mathlib/Data/Set/Basic.lean
theorem sep_ext_iff : { x ∈ s | p x } = { x ∈ s | q x } ↔ ∀ x ∈ s, p x ↔ q x

Proof state:
α : Type u
s : Set α
p q : α → Prop
⊢ {x | x ∈ s ∧ p x} = {x | x ∈ s ∧ q x} ↔ ∀ x ∈ s, p x ↔ q x

Tactic:
simp_rw [Set.ext_iff, mem_sep_iff, and_congr_right_iff]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
lemma mFourier_add {m : d → ℤ} : mFourier (m + n) x = mFourier m x * mFourier n x

Proof state:
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
x : UnitAddTorus d
m : d → ℤ
⊢ (mFourier (m + n)) x = (mFourier m) x * (mFourier n) x

Tactic:
simp only [mFourier, Pi.add_apply, fourier_add, ContinuousMap.coe_mk, ← Finset.prod_mul_distrib]

Result:
no goals
-- Mathlib/FieldTheory/Normal/Closure.lean
lemma normal_iff_forall_map_le' : Normal F K ↔ ∀ σ : L ≃ₐ[F] L, K.map ↑σ ≤ K

Proof state:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ Normal F ↥K ↔ ∀ (σ : L ≃ₐ[F] L), map (↑σ) K ≤ K

Tactic:
rw [normal_iff_normalClosure_le, normalClosure_def'', iSup_le_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem existsUnique_sub_zpow_mem_Ioc {a : α} (ha : 1 < a) (b c : α) :
    ∃! m : ℤ, b / a ^ m ∈ Set.Ioc c (c * a) :=
  (Equiv.neg ℤ).bijective.existsUnique_iff.2 <| by
    simpa only [Equiv.neg_apply, zpow_neg, div_inv_eq_mul] using
      existsUnique_add_zpow_mem_Ioc ha b c

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedCommGroup α
inst✝ : MulArchimedean α
a : α
ha : 1 < a
b c : α
⊢ ∃! x, b / a ^ (Equiv.neg ℤ) x ∈ Ioc c (c * a)

Tactic:
simpa only [Equiv.neg_apply, zpow_neg, div_inv_eq_mul] using
  existsUnique_add_zpow_mem_Ioc ha b c

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem hom_eq_iff {X Y : StructuredArrow S T} (f g : X ⟶ Y) : f = g ↔ f.right = g.right :=
  ⟨fun h ↦ by rw [h], hom_ext _ _⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
X Y : StructuredArrow S T
f g : X ⟶ Y
h : f = g
⊢ f.right = g.right

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Data/Finset/Grade.lean
lemma covBy_iff : s ⋖ t ↔ ∃ a, a ::ₘ s = t :=
  ⟨CovBy.exists_multiset_cons, by rintro ⟨a, rfl⟩; exact covBy_cons _ _⟩

Proof state:
α : Type u_1
s t : Multiset α
⊢ (∃ a, a ::ₘ s = t) → s ⋖ t

Tactic:
rintro ⟨a, rfl⟩

Result:
case intro
α : Type u_1
s : Multiset α
a : α
⊢ s ⋖ a ::ₘ s

Proof state:
case intro
α : Type u_1
s : Multiset α
a : α
⊢ s ⋖ a ::ₘ s

Tactic:
exact covBy_cons _ _

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
@[to_additive existing (attr := simp) pow_addRight]
lemma pow_mulRight (n : ℕ) : Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)

Proof state:
case H
α : Type u_4
inst✝ : Group α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.mulRight a ^ n) x✝ = (Equiv.mulRight (a ^ n)) x✝

Tactic:
simp [Perm.coe_pow]

Result:
no goals

Proof state:
α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)

Tactic:
ext

Result:
case H
α : Type u_4
inst✝ : Group α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.mulRight a ^ n) x✝ = (Equiv.mulRight (a ^ n)) x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem length_zipWith (f : α → β → γ) (l₁ l₂) :
    length (zipWith f l₁ l₂) = min (length l₁) (length l₂)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁ : List α
l₂ : List β
⊢ (zipWith f l₁ l₂).length = min l₁.length l₂.length

Tactic:
induction l₁ generalizing l₂ <;> cases l₂ <;>
  simp_all [succ_min_succ, Nat.zero_min, Nat.min_zero]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem logMap_apply_of_norm_one (hx : mixedEmbedding.norm x = 1)
    (w : {w : InfinitePlace K // w ≠ w₀}) :
    logMap x w = mult w.val * Real.log (normAtPlace w x)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x = 1
w : { w // w ≠ w₀ }
⊢ logMap x w = ↑(↑w).mult * Real.log ((normAtPlace ↑w) x)

Tactic:
rw [logMap_apply, hx, Real.log_one, zero_mul, sub_zero]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem w_nonneg (D : ℝ) (x : E) : 0 ≤ w D x

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ 0 ≤ w D x

Tactic:
apply mul_nonneg _ (u_nonneg _)

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ 0 ≤ ((∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E)⁻¹

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ 0 ≤ ((∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E)⁻¹

Tactic:
apply inv_nonneg.2

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ 0 ≤ (∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ 0 ≤ |D| ^ finrank ℝ E

Tactic:
apply pow_nonneg (abs_nonneg D)

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ 0 ≤ (∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E

Tactic:
apply mul_nonneg (u_int_pos E).le

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ 0 ≤ |D| ^ finrank ℝ E
-- Mathlib/Combinatorics/Pigeonhole.lean
theorem exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Nonempty)
    (hb : #t • b ≤ ∑ x ∈ s, w x) : ∃ y ∈ t, b ≤ ∑ x ∈ s with f x = y, w x :=
  exists_le_of_sum_le ht <| by simpa only [sum_fiberwise_of_maps_to hf, sum_const]

Proof state:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
inst✝ : LinearOrderedCancelAddCommMonoid M
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ ∑ x ∈ s, w x
⊢ ∑ i ∈ t, b ≤ ∑ i ∈ t, ∑ x ∈ filter (fun x => f x = i) s, w x

Tactic:
simpa only [sum_fiberwise_of_maps_to hf, sum_const]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_neg_Ici : Neg.neg '' Ici a = Iic (-a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a : α
⊢ Neg.neg '' Ici a = Iic (-a)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioo_subset_Ioi_self : Ioo a b ⊆ Ioi a

Proof state:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ioi a

Tactic:
simpa [← coe_subset] using Set.Ioo_subset_Ioi_self

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem bind₂_map (f : S →+* MvPolynomial σ T) (g : R →+* S) (φ : MvPolynomial σ R) :
    bind₂ f (map g φ) = bind₂ (f.comp g) φ

Proof state:
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : S →+* MvPolynomial σ T
g : R →+* S
φ : MvPolynomial σ R
⊢ (bind₂ f) ((map g) φ) = (bind₂ (f.comp g)) φ

Tactic:
simp [bind₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natAbs

Proof state:
n : Nat
z : Int
⊢ ↑n ∣ z ↔ n ∣ z.natAbs

Tactic:
rw [← natAbs_dvd_natAbs, natAbs_ofNat]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem le_radius_of_eventually_le (C) (h : ∀ᶠ n in atTop, ‖p n‖ * (r : ℝ) ^ n ≤ C) :
    ↑r ≤ p.radius :=
  p.le_radius_of_isBigO <| IsBigO.of_bound C <| h.mono fun n hn => by simpa

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
C : ℝ
h : ∀ᶠ (n : ℕ) in atTop, ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
hn : ‖p n‖ * ↑r ^ n ≤ C
⊢ ‖‖p n‖ * ↑r ^ n‖ ≤ C * ‖1‖

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem length_mapFinIdx {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} :
    (as.mapFinIdx f).length = as.length

Proof state:
α : Type u_1
β : Type u_2
as : List α
f : (i : Nat) → α → i < as.length → β
⊢ (as.mapFinIdx f).length = as.length

Tactic:
simp [mapFinIdx, length_mapFinIdx_go]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_mul {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : √(x * y) = √x * √y

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √(x * y) = √x * √y

Tactic:
simp_rw [Real.sqrt, ← NNReal.coe_mul, NNReal.coe_inj, Real.toNNReal_mul hx, NNReal.sqrt_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_neg {b : Bool} {a a' : α} (h : b = false) : (bif b then a else a') = a'

Proof state:
α : Type u_1
b : Bool
a a' : α
h : b = false
⊢ (bif b then a else a') = a'

Tactic:
rw [h, cond_false]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Basic.lean
@[to_additive]
lemma hom_inv_apply {X Y : CommGrp} (e : X ≅ Y) (s : Y) : e.hom (e.inv s) = s

Proof state:
X Y : CommGrp
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
/-- This holds true for all `x : ℝ` because of the junk values `0 / 0 = 0` and `log 0 = 0`. -/
@[simp] lemma log_div_self (x : ℝ) : log (x / x) = 0

Proof state:
x : ℝ
⊢ log (x / x) = 0

Tactic:
obtain rfl | hx := eq_or_ne x 0 <;> simp [*]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem ComponentCompl.supp_injective :
    Function.Injective (ComponentCompl.supp : G.ComponentCompl K → Set V)

Proof state:
V : Type u
G : SimpleGraph V
K : Set V
⊢ ∀ (v w : ↑Kᶜ),
    supp ((induce Kᶜ G).connectedComponentMk v) = supp ((induce Kᶜ G).connectedComponentMk w) →
      (induce Kᶜ G).connectedComponentMk v = (induce Kᶜ G).connectedComponentMk w

Tactic:
rintro ⟨v, hv⟩ ⟨w, hw⟩ h

Result:
case mk.mk
V : Type u
G : SimpleGraph V
K : Set V
v : V
hv : v ∈ Kᶜ
w : V
hw : w ∈ Kᶜ
h : supp ((induce Kᶜ G).connectedComponentMk ⟨v, hv⟩) = supp ((induce Kᶜ G).connectedComponentMk ⟨w, hw⟩)
⊢ (induce Kᶜ G).connectedComponentMk ⟨v, hv⟩ = (induce Kᶜ G).connectedComponentMk ⟨w, hw⟩

Proof state:
case mk.mk
V : Type u
G : SimpleGraph V
K : Set V
v : V
hv : v ∈ Kᶜ
w : V
hw : w ∈ Kᶜ
h : supp ((induce Kᶜ G).connectedComponentMk ⟨v, hv⟩) = supp ((induce Kᶜ G).connectedComponentMk ⟨w, hw⟩)
⊢ (induce Kᶜ G).connectedComponentMk ⟨v, hv⟩ = (induce Kᶜ G).connectedComponentMk ⟨w, hw⟩

Tactic:
simp only [Set.ext_iff, ConnectedComponent.eq, Set.mem_setOf_eq, ComponentCompl.supp] at h ⊢

Result:
case mk.mk
V : Type u
G : SimpleGraph V
K : Set V
v : V
hv : v ∈ Kᶜ
w : V
hw : w ∈ Kᶜ
h :
  ∀ (x : V),
    (∃ (h : x ∉ K), (induce Kᶜ G).Reachable ⟨x, ⋯⟩ ⟨v, hv⟩) ↔ ∃ (h : x ∉ K), (induce Kᶜ G).Reachable ⟨x, ⋯⟩ ⟨w, hw⟩
⊢ (induce Kᶜ G).Reachable ⟨v, hv⟩ ⟨w, hw⟩

Proof state:
case mk.mk
V : Type u
G : SimpleGraph V
K : Set V
v : V
hv : v ∈ Kᶜ
w : V
hw : w ∈ Kᶜ
h :
  ∀ (x : V),
    (∃ (h : x ∉ K), (induce Kᶜ G).Reachable ⟨x, ⋯⟩ ⟨v, hv⟩) ↔ ∃ (h : x ∉ K), (induce Kᶜ G).Reachable ⟨x, ⋯⟩ ⟨w, hw⟩
⊢ (induce Kᶜ G).Reachable ⟨v, hv⟩ ⟨w, hw⟩

Tactic:
exact ((h v).mp ⟨hv, Reachable.refl _⟩).choose_spec

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
K : Set V
⊢ Function.Injective supp

Tactic:
refine ConnectedComponent.ind₂ ?_

Result:
V : Type u
G : SimpleGraph V
K : Set V
⊢ ∀ (v w : ↑Kᶜ),
    supp ((induce Kᶜ G).connectedComponentMk v) = supp ((induce Kᶜ G).connectedComponentMk w) →
      (induce Kᶜ G).connectedComponentMk v = (induce Kᶜ G).connectedComponentMk w
-- Mathlib/Topology/Partial.lean
theorem rtendsto'_nhds {r : Rel Y X} {l : Filter Y} {x : X} :
    RTendsto' r l (𝓝 x) ↔ ∀ s, IsOpen s → x ∈ s → r.preimage s ∈ l

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
r : Rel Y X
l : Filter Y
x : X
⊢ RTendsto' r l (𝓝 x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → r.preimage s ∈ l

Tactic:
rw [rtendsto'_def]

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
r : Rel Y X
l : Filter Y
x : X
⊢ (∀ s ∈ 𝓝 x, r.preimage s ∈ l) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → r.preimage s ∈ l

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
r : Rel Y X
l : Filter Y
x : X
⊢ (∀ s ∈ 𝓝 x, r.preimage s ∈ l) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → r.preimage s ∈ l

Tactic:
apply all_mem_nhds_filter

Result:
case hf
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
r : Rel Y X
l : Filter Y
x : X
⊢ ∀ (s t : Set X), s ⊆ t → r.preimage s ⊆ r.preimage t

Proof state:
case hf
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
r : Rel Y X
l : Filter Y
x : X
⊢ ∀ (s t : Set X), s ⊆ t → r.preimage s ⊆ r.preimage t

Tactic:
apply Rel.preimage_mono

Result:
no goals
-- Mathlib/Data/Matrix/Diagonal.lean
theorem diagonal_smul [Zero α] [SMulZeroClass R α] (r : R) (d : n → α) :
    diagonal (r • d) = r • diagonal d

Proof state:
case a
n : Type u_3
R : Type u_7
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
d : n → α
i j : n
⊢ diagonal (r • d) i j = (r • diagonal d) i j

Tactic:
by_cases h : i = j <;> simp [h]

Result:
no goals

Proof state:
n : Type u_3
R : Type u_7
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
d : n → α
⊢ diagonal (r • d) = r • diagonal d

Tactic:
ext i j

Result:
case a
n : Type u_3
R : Type u_7
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
d : n → α
i j : n
⊢ diagonal (r • d) i j = (r • diagonal d) i j
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
theorem sat_and {x y : BoolExpr α} {a : α → Bool} (hx : Sat a x) (hy : Sat a y) :
    Sat a (BoolExpr.gate .and x y)

Proof state:
α : Type
x y : BoolExpr α
a : α → Bool
hx : eval a x = true
hy : eval a y = true
⊢ eval a (gate Gate.and x y) = true

Tactic:
simp [hx, hy, Gate.eval]

Result:
no goals

Proof state:
α : Type
x y : BoolExpr α
a : α → Bool
hx : Sat a x
hy : Sat a y
⊢ Sat a (gate Gate.and x y)

Tactic:
simp only [Sat] at *

Result:
α : Type
x y : BoolExpr α
a : α → Bool
hx : eval a x = true
hy : eval a y = true
⊢ eval a (gate Gate.and x y) = true
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem isOpenEmbedding_of_pullback {X Y S : TopCat} {f : X ⟶ S} {g : Y ⟶ S}
    (H₁ : IsOpenEmbedding f) (H₂ : IsOpenEmbedding g) :
    IsOpenEmbedding (limit.π (cospan f g) WalkingCospan.one)

Proof state:
case h.e'_5.h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S
⊢ ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr)) =
    ⇑(ConcreteCategory.hom (pullback.snd f g ≫ g))

Tactic:
rfl

Result:
no goals

Proof state:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.one))

Tactic:
convert H₂.comp (snd_isOpenEmbedding_of_left H₁ g)

Result:
case h.e'_5.h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S
⊢ ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.one)) =
    ⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom (pullback.snd f g))

Proof state:
case h.e'_5.h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S
⊢ ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.one)) =
    ⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
rw [← coe_comp, ← limit.w _ WalkingCospan.Hom.inr]

Result:
case h.e'_5.h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S
⊢ ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr)) =
    ⇑(ConcreteCategory.hom (pullback.snd f g ≫ g))
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem tendsto_mod_div_atTop_nhds_zero_nat {m : ℕ} (hm : 0 < m) :
    Tendsto (fun n : ℕ => ((n % m : ℕ) : ℝ) / (n : ℝ)) atTop (𝓝 0)

Proof state:
m : ℕ
hm : 0 < m
⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ (fun n => ↑(n % m)) n

Tactic:
aesop

Result:
no goals

Proof state:
m : ℕ
hm : 0 < m
⊢ Tendsto (fun n => ↑(n % m) / ↑n) atTop (𝓝 0)

Tactic:
have h0 : ∀ᶠ n : ℕ in atTop, 0 ≤ (fun n : ℕ => ((n % m : ℕ) : ℝ)) n := by aesop

Result:
m : ℕ
hm : 0 < m
h0 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (fun n => ↑(n % m)) n
⊢ Tendsto (fun n => ↑(n % m) / ↑n) atTop (𝓝 0)

Proof state:
m : ℕ
hm : 0 < m
h0 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (fun n => ↑(n % m)) n
⊢ Tendsto (fun n => ↑(n % m) / ↑n) atTop (𝓝 0)

Tactic:
exact tendsto_bdd_div_atTop_nhds_zero h0
  (.of_forall (fun n ↦  cast_le.mpr (mod_lt n hm).le)) tendsto_natCast_atTop_atTop

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_swap (s : Set α) (t : Set β) : image2 f s t = image2 (fun a b => f b a) t s

Proof state:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ image2 (fun a b => f b a) t s

Tactic:
constructor <;> rintro ⟨a, ha, b, hb, rfl⟩ <;> exact ⟨b, hb, a, ha, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = image2 (fun a b => f b a) t s

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ image2 (fun a b => f b a) t s
-- Mathlib/RingTheory/Perfection.lean
theorem frobenius_pthRoot : (frobenius _ p).comp (pthRoot R p) = RingHom.id _ :=
  RingHom.ext fun x =>
    ext fun n => by
      rw [RingHom.comp_apply, RingHom.id_apply, RingHom.map_frobenius, coeff_pthRoot,
        ← @RingHom.map_frobenius (Ring.Perfection R p) _ R, coeff_frobenius]

Proof state:
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x : Ring.Perfection R p
n : ℕ
⊢ (coeff R p n) (((frobenius (Ring.Perfection R p) p).comp (pthRoot R p)) x) =
    (coeff R p n) ((RingHom.id (Ring.Perfection R p)) x)

Tactic:
rw [RingHom.comp_apply, RingHom.id_apply, RingHom.map_frobenius, coeff_pthRoot,
  ← @RingHom.map_frobenius (Ring.Perfection R p) _ R, coeff_frobenius]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem memLp_zero_iff_aestronglyMeasurable [TopologicalSpace ε] {f : α → ε} :
    MemLp f 0 μ ↔ AEStronglyMeasurable f μ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : TopologicalSpace ε
f : α → ε
⊢ MemLp f 0 μ ↔ AEStronglyMeasurable f μ

Tactic:
simp [MemLp, eLpNorm_exponent_zero]

Result:
no goals
-- Mathlib/Topology/Algebra/Polynomial.lean
theorem continuous_eval₂ [Semiring S] (p : S[X]) (f : S →+* R) :
    Continuous fun x => p.eval₂ f x

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous fun x => p.sum fun e a => f a * x ^ e

Tactic:
exact continuous_finset_sum _ fun c _ => continuous_const.mul (continuous_pow _)

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous fun x => eval₂ f x p

Tactic:
simp only [eval₂_eq_sum, Finsupp.sum]

Result:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous fun x => p.sum fun e a => f a * x ^ e
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.eq_biInf (h : l.HasBasis p s) : l = ⨅ (i) (_ : p i), 𝓟 (s i) :=
  eq_biInf_of_mem_iff_exists_mem fun {_} => by simp only [h.mem_iff, mem_principal, exists_prop]

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x✝ : Set α
⊢ x✝ ∈ l ↔ ∃ i, p i ∧ x✝ ∈ 𝓟 (s i)

Tactic:
simp only [h.mem_iff, mem_principal, exists_prop]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
@[reassoc (attr := simp)]
lemma stalkMap_hom_inv (e : X ≅ Y) (y : Y) :
    e.hom.stalkMap (e.inv.base y) ≫ e.inv.stalkMap y =
      (Y.presheaf.stalkCongr (.of_eq (by simp))).hom :=
  LocallyRingedSpace.stalkMap_hom_inv (forgetToLocallyRingedSpace.mapIso e) y

Proof state:
X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
y : ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y) = y

Tactic:
simp

Result:
no goals