harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem neg_neg {x : BitVec w} : - - x = x

Proof state:
case pos
w : Nat
x : BitVec w
h : x = 0#w
⊢ - -x = x

Tactic:
simp [h]

Result:
no goals

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

Tactic:
by_cases h : x = 0#w

Result:
case pos
w : Nat
x : BitVec w
h : x = 0#w
⊢ - -x = x

case neg
w : Nat
x : BitVec w
h : ¬x = 0#w
⊢ - -x = x

Proof state:
case neg
w : Nat
x : BitVec w
h : ¬x = 0#w
⊢ - -x = x

Tactic:
simp [bv_toNat, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sub_max_sub_left (a b c : Nat) : max (a - b) (a - c) = a - min b c

Proof state:
a b c : Nat
⊢ max (a - b) (a - c) = a - min b c

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@[to_additive]
lemma _root_.Cardinal.mk_mul_le : #(s * t) ≤ #s * #t

Proof state:
M : Type u_2
inst✝ : Mul M
s t : Set M
⊢ #↑(image2 (fun x1 x2 => x1 * x2) s t) ≤ #↑s * #↑t

Tactic:
exact Cardinal.mk_image2_le

Result:
no goals

Proof state:
M : Type u_2
inst✝ : Mul M
s t : Set M
⊢ #↑(s * t) ≤ #↑s * #↑t

Tactic:
rw [← image2_mul]

Result:
M : Type u_2
inst✝ : Mul M
s t : Set M
⊢ #↑(image2 (fun x1 x2 => x1 * x2) s t) ≤ #↑s * #↑t
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem isPrefixOf?_eq_some_iff_append_eq [BEq α] [LawfulBEq α] {xs ys zs : List α} :
    xs.isPrefixOf? ys = some zs ↔ xs ++ zs = ys

Proof state:
case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
zs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {ys : List α}, tail✝.isPrefixOf? ys = some zs ↔ tail✝ ++ zs = ys
ys : List α
⊢ (head✝ :: tail✝).isPrefixOf? ys = some zs ↔ head✝ :: tail✝ ++ zs = ys

Tactic:
cases ys <;> simp [isPrefixOf?, *]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
⊢ xs.isPrefixOf? ys = some zs ↔ xs ++ zs = ys

Tactic:
induction xs generalizing ys with
| nil => simp [isPrefixOf?, Eq.comm]
| cons => cases ys <;> simp [isPrefixOf?, *]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
zs ys : List α
⊢ [].isPrefixOf? ys = some zs ↔ [] ++ zs = ys

Tactic:
simp [isPrefixOf?, Eq.comm]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma ofHoms_comp (φ : ∀ (p : ℤ), F.X p ⟶ G.X p) (ψ : ∀ (p : ℤ), G.X p ⟶ K.X p) :
    (ofHoms φ).comp (ofHoms ψ) (zero_add 0) = ofHoms (fun p => φ p ≫ ψ p)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
φ : (p : ℤ) → F.X p ⟶ G.X p
ψ : (p : ℤ) → G.X p ⟶ K.X p
⊢ (ofHoms φ).comp (ofHoms ψ) ⋯ = ofHoms fun p => φ p ≫ ψ p

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean
theorem leftUnitor_naturality {X₁ X₂ : C} (f : X₁ ⟶ X₂) :
    tensorHom ℬ (𝟙 𝒯.cone.pt) f ≫ (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₂).isLimit).hom =
      (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₁).isLimit).hom ≫ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ (ℬ 𝒯.cone.pt X₂).isLimit.lift
        (BinaryFan.mk (BinaryFan.fst (ℬ 𝒯.cone.pt X₁).cone ≫ 𝟙 𝒯.cone.pt) (BinaryFan.snd (ℬ 𝒯.cone.pt X₁).cone ≫ f)) ≫
      BinaryFan.snd (ℬ 𝒯.cone.pt X₂).cone =
    BinaryFan.snd (ℬ 𝒯.cone.pt X₁).cone ≫ f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ tensorHom ℬ (𝟙 𝒯.cone.pt) f ≫ (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₂).isLimit).hom =
    (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₁).isLimit).hom ≫ f

Tactic:
dsimp [tensorHom]

Result:
C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ (ℬ 𝒯.cone.pt X₂).isLimit.lift
        (BinaryFan.mk (BinaryFan.fst (ℬ 𝒯.cone.pt X₁).cone ≫ 𝟙 𝒯.cone.pt) (BinaryFan.snd (ℬ 𝒯.cone.pt X₁).cone ≫ f)) ≫
      BinaryFan.snd (ℬ 𝒯.cone.pt X₂).cone =
    BinaryFan.snd (ℬ 𝒯.cone.pt X₁).cone ≫ f
-- Mathlib/Computability/TMToPartrec.lean
theorem K'.elim_update_main {a b c d a'} : update (K'.elim a b c d) main a' = K'.elim a' b c d

Proof state:
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' = elim a' b c d

Tactic:
funext x

Result:
case h
a b c d a' : List Γ'
x : K'
⊢ update (elim a b c d) main a' x = elim a' b c d x

Proof state:
case h
a b c d a' : List Γ'
x : K'
⊢ update (elim a b c d) main a' x = elim a' b c d x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem ext_inner_right {x y : E} (h : ∀ v, ⟪x, v⟫ = ⟪y, v⟫) : x = y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ∀ (v : E), inner x v = inner y v
⊢ x = y

Tactic:
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_left, sub_eq_zero, h (x - y)]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal (hf : Summable f) (hg : Summable g)
    (hfg : Summable fun x : A × A ↦ f x.1 * g x.2) :
    ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Proof state:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.1 * g x.2
⊢ (∑' (n : A), f n) * ∑' (n : A), g n = ∑' (n : A), ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Tactic:
conv_rhs => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]

Result:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.1 * g x.2
⊢ (∑' (n : A), f n) * ∑' (n : A), g n = ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2

Proof state:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.1 * g x.2
⊢ (∑' (n : A), f n) * ∑' (n : A), g n = ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2

Tactic:
rw [tsum_mul_tsum hf hg hfg, ← sigmaAntidiagonalEquivProd.tsum_eq (_ : A × A → α)]

Result:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.1 * g x.2
⊢ ∑' (c : (n : A) × { x // x ∈ antidiagonal n }),
      f (sigmaAntidiagonalEquivProd c).1 * g (sigmaAntidiagonalEquivProd c).2 =
    ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2

Proof state:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.1 * g x.2
⊢ ∑' (c : (n : A) × { x // x ∈ antidiagonal n }),
      f (sigmaAntidiagonalEquivProd c).1 * g (sigmaAntidiagonalEquivProd c).2 =
    ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2

Tactic:
exact
  tsum_sigma' (fun n ↦ (hasSum_fintype _).summable)
    (summable_mul_prod_iff_summable_mul_sigma_antidiagonal.mp hfg)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
lemma exp_sub_sum_range_isBigO_pow (n : ℕ) :
    (fun x ↦ exp x - ∑ i ∈ Finset.range n, x ^ i / i !) =O[𝓝 0] (· ^ n)

Proof state:
n : ℕ
this : (fun x => Complex.exp ↑x - ∑ i ∈ Finset.range n, ↑x ^ i / ↑i !) =O[𝓝 0] fun x => ↑x ^ n
⊢ (fun x => rexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n

Tactic:
norm_cast at this

Result:
no goals

Proof state:
n : ℕ
this :
  ((fun x => Complex.exp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) ∘ Complex.ofReal) =O[𝓝 0]
    ((fun x => x ^ n) ∘ Complex.ofReal)
⊢ (fun x => rexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n

Tactic:
simp only [Function.comp_def] at this

Result:
n : ℕ
this : (fun x => Complex.exp ↑x - ∑ i ∈ Finset.range n, ↑x ^ i / ↑i !) =O[𝓝 0] fun x => ↑x ^ n
⊢ (fun x => rexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n

Proof state:
n : ℕ
⊢ (fun x => rexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n

Tactic:
have := (Complex.exp_sub_sum_range_isBigO_pow n).comp_tendsto
  (Complex.continuous_ofReal.tendsto' 0 0 rfl)

Result:
n : ℕ
this :
  ((fun x => Complex.exp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) ∘ Complex.ofReal) =O[𝓝 0]
    ((fun x => x ^ n) ∘ Complex.ofReal)
⊢ (fun x => rexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem aeval_algHom (f : A →ₐ[R] B) (x : A) : aeval (f x) = f.comp (aeval x) :=
  algHom_ext <| by simp only [aeval_X, AlgHom.comp_apply]

Proof state:
R : Type u
A : Type z
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A
⊢ (aeval (f x)) X = (f.comp (aeval x)) X

Tactic:
simp only [aeval_X, AlgHom.comp_apply]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem compl_le_self : xᶜ ≤ x ↔ x = ⊤

Proof state:
α : Type u
x : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ≤ x ↔ x = ⊤

Tactic:
simpa using le_compl_self (a := xᶜ)

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem target_inter_preimage_symm_source_eq (e f : Pretrivialization F proj) :
    f.target ∩ f.toPartialEquiv.symm ⁻¹' e.source = (e.baseSet ∩ f.baseSet) ×ˢ univ

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e f : Pretrivialization F proj
⊢ f.target ∩ ↑f.symm ⁻¹' e.source = (e.baseSet ∩ f.baseSet) ×ˢ univ

Tactic:
rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_modify [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.1)
    {a : α} {f : β a → β a} :
    Perm (toListModel (m.modify a f).1.2) (modifyKey a f (toListModel m.1.2))

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : β a → β a
⊢ toListModel (m.modify a f).val.buckets ~ modifyKey a f (toListModel m.val.buckets)

Tactic:
rw [modify_eq_alter, modifyKey_eq_alterKey]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : β a → β a
⊢ toListModel (m.alter a fun x => Option.map f x).val.buckets ~
    alterKey a (fun x => Option.map f x) (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : β a → β a
⊢ toListModel (m.alter a fun x => Option.map f x).val.buckets ~
    alterKey a (fun x => Option.map f x) (toListModel m.val.buckets)

Tactic:
exact toListModel_alter h

Result:
no goals
-- Mathlib/Topology/UniformSpace/CompactConvergence.lean
theorem uniformSpace_eq_iInf_precomp_of_cover {δ : ι → Type*} [∀ i, TopologicalSpace (δ i)]
    (φ : Π i, C(δ i, α)) (h_proper : ∀ i, IsProperMap (φ i))
    (h_lf : LocallyFinite fun i ↦ range (φ i)) (h_cover : ⋃ i, range (φ i) = univ) :
    (inferInstanceAs <| UniformSpace C(α, β)) = ⨅ i, .comap (comp · (φ i)) inferInstance

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i => range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i => {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
⊢ (⋃ i ∈ {i | (range ⇑(φ i) ∩ S).Nonempty}, range ⇑(φ i)) ∩ S = S

Tactic:
simp_rw [iUnion₂_inter, mem_setOf, iUnion_nonempty_self, ← iUnion_inter, h_cover, univ_inter]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem eq_of_smul_eq_smul_left {a : ℤ} {b c : ℤ√d} (ha : a ≠ 0) (h : ↑a * b = a * c) :
    b = c

Proof state:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ b.re = c.re ∧ b.im = c.im

Tactic:
apply And.imp _ _ h <;> simpa only [smul_re, smul_im] using mul_left_cancel₀ ha

Result:
no goals

Proof state:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : ↑a * b = ↑a * c
⊢ b = c

Tactic:
rw [Zsqrtd.ext_iff] at h ⊢

Result:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ b.re = c.re ∧ b.im = c.im
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma nnnorm_le_one_iff_of_nonneg (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ ↑‖a‖₊ ≤ ↑1 ↔ a ≤ 1

Tactic:
exact norm_le_one_iff_of_nonneg a

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖a‖₊ ≤ 1 ↔ a ≤ 1

Tactic:
rw [← NNReal.coe_le_coe]

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ ↑‖a‖₊ ≤ ↑1 ↔ a ≤ 1
-- Mathlib/Analysis/Normed/Order/UpperLower.lean
theorem IsUpperSet.thickening' (hs : IsUpperSet s) (ε : ℝ) :
    IsUpperSet (thickening ε s)

Proof state:
α : Type u_1
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (thickening ε s)

Tactic:
rw [← ball_mul_one]

Result:
α : Type u_1
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (ball 1 ε * s)

Proof state:
α : Type u_1
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (ball 1 ε * s)

Tactic:
exact hs.mul_left

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem uniformContinuous_sInf_dom {f : α → β} {u₁ : Set (UniformSpace α)} {u₂ : UniformSpace β}
    {u : UniformSpace α} (h₁ : u ∈ u₁) (hf : UniformContinuous[u, u₂] f) :
    UniformContinuous[sInf u₁, u₂] f

Proof state:
α : Type ua
β : Type ub
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
rw [sInf_eq_iInf', iInf_uniformity]

Result:
α : Type ua
β : Type ub
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.1, f x.2)) (⨅ i, 𝓤 α) (𝓤 β)

Proof state:
α : Type ua
β : Type ub
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.1, f x.2)) (⨅ i, 𝓤 α) (𝓤 β)

Tactic:
exact tendsto_iInf' ⟨u, h₁⟩ hf

Result:
no goals

Proof state:
α : Type ua
β : Type ub
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ UniformContinuous f

Tactic:
delta UniformContinuous

Result:
α : Type ua
β : Type ub
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β)
-- Mathlib/LinearAlgebra/Dual.lean
theorem toDual_eq_equivFun [Finite ι] (m : M) (i : ι) : b.toDual m (b i) = b.equivFun m i

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
m : M
i : ι
⊢ (b.toDual m) (b i) = b.equivFun m i

Tactic:
rw [b.equivFun_apply, toDual_eq_repr]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem natDegree_prod_of_monic (h : ∀ i ∈ s, (f i).Monic) :
    (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∀ i ∈ s, (f i).Monic
⊢ ∀ f_1 ∈ Multiset.map f s.val, f_1.Monic

Tactic:
simpa using h

Result:
no goals

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∀ i ∈ s, (f i).Monic
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Tactic:
simpa using natDegree_multiset_prod_of_monic (s.1.map f) (by simpa using h)

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem mem_ideal_smul_span_iff_exists_sum' {ι : Type*} (s : Set ι) (f : ι → M) (x : M) :
    x ∈ I • span R (f '' s) ↔
    ∃ (a : s →₀ R) (_ : ∀ i, a i ∈ I), (a.sum fun i c => c • f i) = x

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
s : Set ι
f : ι → M
x : M
⊢ x ∈ I • span R (f '' s) ↔ ∃ a, ∃ (_ : ∀ (i : ↑s), a i ∈ I), (a.sum fun i c => c • f ↑i) = x

Tactic:
rw [← Submodule.mem_ideal_smul_span_iff_exists_sum, ← Set.image_eq_range]

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_right [NeBot f] : map₂ (fun _ y => y) f g = g

Proof state:
α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst✝ : f.NeBot
⊢ map₂ (fun x y => y) f g = g

Tactic:
rw [map₂_swap, map₂_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem replaceEntry_append_of_containsKey_right_eq_false [BEq α] {l l' : List ((a : α) × β a)}
    {k : α} {v : β k} (h : containsKey k l' = false) :
    replaceEntry k v (l ++ l') = replaceEntry k v l ++ l'

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l' = false
h' : containsKey k l = false
⊢ containsKey k (l ++ l') = false

Tactic:
simpa using ⟨h', h⟩

Result:
no goals

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l' = false
h' : containsKey k l = false
⊢ replaceEntry k v (l ++ l') = replaceEntry k v l ++ l'

Tactic:
rw [replaceEntry_of_containsKey_eq_false, replaceEntry_of_containsKey_eq_false h']

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l' = false
h' : containsKey k l = false
⊢ containsKey k (l ++ l') = false

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l' = false
⊢ replaceEntry k v (l ++ l') = replaceEntry k v l ++ l'

Tactic:
cases h' : containsKey k l

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l' = false
h' : containsKey k l = false
⊢ replaceEntry k v (l ++ l') = replaceEntry k v l ++ l'

case true
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l' = false
h' : containsKey k l = true
⊢ replaceEntry k v (l ++ l') = replaceEntry k v l ++ l'

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l' = false
h' : containsKey k l = true
⊢ replaceEntry k v (l ++ l') = replaceEntry k v l ++ l'

Tactic:
rw [replaceEntry_append_of_containsKey_left h']

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrixAlgEquiv_toLinAlgEquiv (M : Matrix n n R) :
    LinearMap.toMatrixAlgEquiv v₁ (Matrix.toLinAlgEquiv v₁ M) = M

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
⊢ (toMatrixAlgEquiv v₁) ((toLinAlgEquiv v₁) M) = M

Tactic:
rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.symm_apply_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem tendsto_atTop_intervalIntegral_of_pos (h₀ : 0 < ∫ x in (0)..T, g x) (hT : 0 < T) :
    Tendsto (fun t => ∫ x in (0)..t, g x) atTop atTop

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
⊢ Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) atTop atTop

Tactic:
have h_int := intervalIntegrable_of_integral_ne_zero h₀.ne'

Result:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) atTop atTop

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun x => ⌊x / T⌋) atTop atTop

Tactic:
exact tendsto_floor_atTop.comp (tendsto_id.atTop_mul_const (inv_pos.mpr hT))

Result:
no goals

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) atTop atTop

Tactic:
apply tendsto_atTop_mono (hg.sInf_add_zsmul_le_integral_of_pos h_int hT)

Result:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun n => sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊n / T⌋ • ∫ (x : ℝ) in 0 ..T, g x) atTop
    atTop

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun x => ⌊x / T⌋ • ∫ (x : ℝ) in 0 ..T, g x) atTop atTop

Tactic:
apply Tendsto.atTop_zsmul_const h₀

Result:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun x => ⌊x / T⌋) atTop atTop

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun n => sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊n / T⌋ • ∫ (x : ℝ) in 0 ..T, g x) atTop
    atTop

Tactic:
apply atTop.tendsto_atTop_add_const_left (sInf <| (fun t => ∫ x in (0)..t, g x) '' Icc 0 T)

Result:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun x => ⌊x / T⌋ • ∫ (x : ℝ) in 0 ..T, g x) atTop atTop