harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_eq_iInf_iSup {f : Filter β} {u : β → α} : limsup u f = ⨅ s ∈ f, ⨆ a ∈ s, u a :=
  (f.basis_sets.map u).limsSup_eq_iInf_sSup.trans <| by simp only [sSup_image, id]

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ ⨅ i ∈ f, sSup (u '' id i) = ⨅ s ∈ f, ⨆ a ∈ s, u a

Tactic:
simp only [sSup_image, id]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem Basis.ofEquivFun_equivFun [Finite ι] (v : Basis ι R M) :
    Basis.ofEquivFun v.equivFun = v :=
  Basis.repr_injective <| by ext; rfl

Proof state:
case h.h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
v : Basis ι R M
x✝ : M
a✝ : ι
⊢ ((ofEquivFun v.equivFun).repr x✝) a✝ = (v.repr x✝) a✝

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
v : Basis ι R M
⊢ (ofEquivFun v.equivFun).repr = v.repr

Tactic:
ext

Result:
case h.h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
v : Basis ι R M
x✝ : M
a✝ : ι
⊢ ((ofEquivFun v.equivFun).repr x✝) a✝ = (v.repr x✝) a✝
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDeriv_const_add (hn : 0 < n) (c : F) :
    iteratedDeriv n (fun z => c + f z) x = iteratedDeriv n f x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
f : 𝕜 → F
hn : 0 < n
c : F
⊢ iteratedDeriv n (fun z => c + f z) x = iteratedDeriv n f x

Tactic:
simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_const_add hn c

Result:
no goals
-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem matPolyEquiv_map_C (M : Matrix n n R) : matPolyEquiv (M.map C) = C M

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ matPolyEquiv (M.map ⇑C) = C M

Tactic:
rw [← matPolyEquiv_symm_C, AlgEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Data/NNRat/BigOperators.lean
theorem toNNRat_sum_of_nonneg {s : Finset α} {f : α → ℚ} (hf : ∀ a, a ∈ s → 0 ≤ f a) :
    (∑ a ∈ s, f a).toNNRat = ∑ a ∈ s, (f a).toNNRat

Proof state:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ (∑ a ∈ s, f a).toNNRat = ∑ a ∈ s, (f a).toNNRat

Tactic:
rw [← coe_inj, coe_sum, Rat.coe_toNNRat _ (Finset.sum_nonneg hf)]

Result:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ∑ i ∈ s, f i = ∑ a ∈ s, ↑(f a).toNNRat

Proof state:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ∑ i ∈ s, f i = ∑ a ∈ s, ↑(f a).toNNRat

Tactic:
exact Finset.sum_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(f x).toNNRat

Tactic:
rw [Rat.coe_toNNRat _ (hf x hxs)]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Subcategory.lean
lemma W.shift {X₁ X₂ : C} {f : X₁ ⟶ X₂} (hf : S.W f) (n : ℤ) : S.W (f⟦n⟧')

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : S.W f
n : ℤ
⊢ S.W ((shiftFunctor C n).map f)

Tactic:
rw [← smul_mem_W_iff _ _ (n.negOnePow)]

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : S.W f
n : ℤ
⊢ S.W (n.negOnePow • (shiftFunctor C n).map f)

Proof state:
case intro.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
X₁ X₂ : C
f : X₁ ⟶ X₂
n : ℤ
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
mem : S.P X₃
⊢ S.W (n.negOnePow • (shiftFunctor C n).map f)

Tactic:
exact ⟨_, _, _, Pretriangulated.Triangle.shift_distinguished _ hT n, S.shift _ _ mem⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : S.W f
n : ℤ
⊢ S.W (n.negOnePow • (shiftFunctor C n).map f)

Tactic:
obtain ⟨X₃, g, h, hT, mem⟩ := hf

Result:
case intro.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
X₁ X₂ : C
f : X₁ ⟶ X₂
n : ℤ
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
mem : S.P X₃
⊢ S.W (n.negOnePow • (shiftFunctor C n).map f)
-- Mathlib/Data/Set/Function.lean
theorem imageFactorization_injective_iff : Injective (s.imageFactorization f) ↔ InjOn f s :=
  ⟨fun h x hx y hy _ ↦ by simpa using @h ⟨x, hx⟩ ⟨y, hy⟩ (by simpa [imageFactorization]),
    InjOn.imageFactorization_injective⟩

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : Injective (imageFactorization f s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
x✝ : f x = f y
⊢ x = y

Tactic:
simpa using @h ⟨x, hx⟩ ⟨y, hy⟩ (by simpa [imageFactorization])

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : Injective (imageFactorization f s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
x✝ : f x = f y
⊢ imageFactorization f s ⟨x, hx⟩ = imageFactorization f s ⟨y, hy⟩

Tactic:
simpa [imageFactorization]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean
theorem postComp_φ : (f.postComp h).φ = f.φ ≫ h

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
h : Z ⟶ Z'
⊢ (f.postComp h).φ = f.φ ≫ h

Tactic:
unfold φ postComp

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
h : Z ⟶ Z'
⊢ PInfty.f (n + 1) ≫ { a := f.a ≫ h, b := fun i => f.b i ≫ h }.a +
      ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ { a := f.a ≫ h, b := fun i => f.b i ≫ h }.b i.rev =
    (PInfty.f (n + 1) ≫ f.a + ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev) ≫ h

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
h : Z ⟶ Z'
⊢ PInfty.f (n + 1) ≫ { a := f.a ≫ h, b := fun i => f.b i ≫ h }.a +
      ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ { a := f.a ≫ h, b := fun i => f.b i ≫ h }.b i.rev =
    (PInfty.f (n + 1) ≫ f.a + ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev) ≫ h

Tactic:
simp only [add_comp, sum_comp, assoc]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem zeroLocus_subset_zeroLocus_singleton_iff (f g : R) :
    zeroLocus ({f} : Set R) ⊆ zeroLocus {g} ↔ g ∈ (Ideal.span ({f} : Set R)).radical

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ zeroLocus {f} ⊆ zeroLocus {g} ↔ g ∈ (Ideal.span {f}).radical

Tactic:
rw [← zeroLocus_span {f}, ← zeroLocus_span {g}, zeroLocus_subset_zeroLocus_iff, Ideal.span_le,
  Set.singleton_subset_iff, SetLike.mem_coe]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem tendsto_intCast_atBot_iff [StrictOrderedRing R] [Archimedean R] {f : α → ℤ}
    {l : Filter α} : Tendsto (fun n => (f n : R)) l atBot ↔ Tendsto f l atBot

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto (Int.cast ∘ f) l atBot

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto f l atBot

Tactic:
rw [← @Int.comap_cast_atBot R, tendsto_comap_iff]

Result:
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto (Int.cast ∘ f) l atBot
-- Mathlib/Data/List/EditDistance/Defs.lean
theorem suffixLevenshtein_eq_tails_map (xs ys) :
    (suffixLevenshtein C xs ys).1 = xs.tails.map fun xs' => levenshtein C xs' ys

Proof state:
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
ys : List β
⊢ (suffixLevenshtein C [] ys).val = List.map (fun xs' => levenshtein C xs' ys) [].tails

Tactic:
simp only [suffixLevenshtein_nil', List.tails, List.map_cons, List.map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
ys : List β
⊢ (suffixLevenshtein C xs ys).val = List.map (fun xs' => levenshtein C xs' ys) xs.tails

Tactic:
induction xs with
| nil =>
  simp only [suffixLevenshtein_nil', List.tails, List.map_cons, List.map]
| cons x xs ih =>
  simp only [suffixLevenshtein_cons₁, ih, List.tails, List.map_cons]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
ys : List β
x : α
xs : List α
ih : (suffixLevenshtein C xs ys).val = List.map (fun xs' => levenshtein C xs' ys) xs.tails
⊢ (suffixLevenshtein C (x :: xs) ys).val = List.map (fun xs' => levenshtein C xs' ys) (x :: xs).tails

Tactic:
simp only [suffixLevenshtein_cons₁, ih, List.tails, List.map_cons]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem ContDiffAt.rpow_const_of_le (hf : ContDiffAt ℝ m f x) (h : ↑m ≤ p) :
    ContDiffAt ℝ m (fun x => f x ^ p) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x : E
p : ℝ
m : ℕ
hf : ContDiffWithinAt ℝ (↑m) f Set.univ x
h : ↑m ≤ p
⊢ ContDiffWithinAt ℝ (↑m) (fun x => f x ^ p) Set.univ x

Tactic:
exact hf.rpow_const_of_le h

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x : E
p : ℝ
m : ℕ
hf : ContDiffAt ℝ (↑m) f x
h : ↑m ≤ p
⊢ ContDiffAt ℝ (↑m) (fun x => f x ^ p) x

Tactic:
rw [← contDiffWithinAt_univ] at *

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x : E
p : ℝ
m : ℕ
hf : ContDiffWithinAt ℝ (↑m) f Set.univ x
h : ↑m ≤ p
⊢ ContDiffWithinAt ℝ (↑m) (fun x => f x ^ p) Set.univ x
-- Mathlib/Analysis/InnerProductSpace/NormPow.lean
theorem hasDerivAt_abs_rpow (x : ℝ) {p : ℝ} (hp : 1 < p) :
    HasDerivAt (fun x : ℝ ↦ |x| ^ p) (p * |x| ^ (p - 2) * x) x

Proof state:
x p : ℝ
hp : 1 < p
⊢ HasDerivAt (fun x => |x| ^ p) (p * |x| ^ (p - 2) * x) x

Tactic:
simpa using hasDerivAt_norm_rpow x hp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthSup_biSup {α : Type*} (u : α → ℕ → ℝ≥0∞) {s : Set α} (hs : s.Finite) :
    expGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Proof state:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
⊢ expGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Tactic:
have := map_finset_sup expGrowthSupBotHom hs.toFinset u

Result:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
this : expGrowthSupBotHom (hs.toFinset.sup u) = hs.toFinset.sup (⇑expGrowthSupBotHom ∘ u)
⊢ expGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Proof state:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
this : expGrowthSupBotHom (hs.toFinset.sup u) = hs.toFinset.sup (⇑expGrowthSupBotHom ∘ u)
⊢ expGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Tactic:
simpa only [expGrowthSupBotHom, SupBotHom.coe_mk, SupHom.coe_mk, Finset.sup_eq_iSup,
  hs.mem_toFinset, comp_apply]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem bihimp_eq_inf_himp_inf : a ⇔ b = a ⊔ b ⇨ a ⊓ b

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⇔ b = a ⊔ b ⇨ a ⊓ b

Tactic:
simp [himp_inf_distrib, bihimp]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_le_inv_mul_iff [MulRightMono α] :
    a / b ≤ a⁻¹ * b ↔ a ≤ b

Proof state:
α : Type u
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a * a ≤ b * b ↔ a ≤ b

Tactic:
exact
  ⟨fun h => not_lt.mp fun k => not_lt.mpr h (mul_lt_mul_of_lt_of_lt k k), fun h =>
    mul_le_mul' h h⟩

Result:
no goals

Proof state:
α : Type u
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a / b ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
rw [div_eq_mul_inv, mul_inv_le_inv_mul_iff]

Result:
α : Type u
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a * a ≤ b * b ↔ a ≤ b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_insertEntry [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a fallback : α}
    {v : β k} : getKeyD a (insertEntry k v l) fallback =
      if k == a then k else getKeyD a l fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
k a fallback : α
v : β k
⊢ getKeyD a (insertEntry k v l) fallback = if (k == a) = true then k else getKeyD a l fallback

Tactic:
simp [getKeyD_eq_getKey?, getKey?_insertEntry, apply_ite (fun x => Option.getD x fallback)]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem Submodule.finrank_add_finrank_orthogonal [FiniteDimensional 𝕜 E] (K : Submodule 𝕜 E) :
    finrank 𝕜 K + finrank 𝕜 Kᗮ = finrank 𝕜 E

Proof state:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 E = finrank 𝕜 ↥⊤

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 ↥K + finrank 𝕜 ↥Kᗮ = finrank 𝕜 E

Tactic:
convert Submodule.finrank_add_inf_finrank_orthogonal (le_top : K ≤ ⊤) using 1

Result:
case h.e'_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 ↥K + finrank 𝕜 ↥Kᗮ = finrank 𝕜 ↥K + finrank 𝕜 ↥(Kᗮ ⊓ ⊤)

case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 E = finrank 𝕜 ↥⊤

Proof state:
case h.e'_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 ↥K + finrank 𝕜 ↥Kᗮ = finrank 𝕜 ↥K + finrank 𝕜 ↥(Kᗮ ⊓ ⊤)

Tactic:
rw [inf_top_eq]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem tendsto_card_div_pow₅ :
    (fun x ↦ (Nat.card ↑(s ∩ (⌊x⌋₊ : ℝ)⁻¹ • L) : ℝ) / ⌊x⌋₊ ^ card ι * (⌊x⌋₊ / x) ^ card ι)
      =ᶠ[atTop] (fun x ↦ (Nat.card ↑(s ∩ (⌊x⌋₊ : ℝ)⁻¹ • L) : ℝ) / x ^ card ι)

Proof state:
case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ℝ
hx : 1 ≤ x
⊢ ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌊x⌋₊ ^ card ι * (↑⌊x⌋₊ / x) ^ card ι =
    ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
have : 0 < ⌊x⌋₊ := Nat.floor_pos.mpr hx

Result:
case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ℝ
hx : 1 ≤ x
this : 0 < ⌊x⌋₊
⊢ ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌊x⌋₊ ^ card ι * (↑⌊x⌋₊ / x) ^ card ι =
    ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Proof state:
case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ℝ
hx : 1 ≤ x
this : 0 < ⌊x⌋₊
⊢ ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌊x⌋₊ ^ card ι * (↑⌊x⌋₊ / x) ^ card ι =
    ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
rw [div_pow, mul_div, div_mul_cancel₀ _ (by positivity)]

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
⊢ (fun x =>
      ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌊x⌋₊ ^ card ι *
        (↑⌊x⌋₊ / x) ^ card ι) =ᶠ[atTop]
    fun x => ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx

Result:
case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ℝ
hx : 1 ≤ x
⊢ ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌊x⌋₊ ^ card ι * (↑⌊x⌋₊ / x) ^ card ι =
    ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ℝ
hx : 1 ≤ x
this : 0 < ⌊x⌋₊
⊢ ↑⌊x⌋₊ ^ card ι ≠ 0

Tactic:
positivity

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem dist_inv (x y : E) : dist x⁻¹ y = dist x y⁻¹

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
x y : E
⊢ dist x⁻¹ y = dist x y⁻¹

Tactic:
simp_rw [dist_eq_norm_div, ← norm_inv' (x⁻¹ / y), inv_div, div_inv_eq_mul, mul_comm]

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
lemma card_mul_cast_subConst (A B : Finset G') : (#A * δ[A, B] : 𝕜) = #(A - B)

Proof state:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ ↑(#A) * ↑δ[A, B] = ↑(#(A - B))

Tactic:
norm_cast

Result:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ ↑(#A) * δ[A, B] = ↑(#(A - B))

Proof state:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ ↑(#A) * δ[A, B] = ↑(#(A - B))

Tactic:
exact card_mul_subConst _ _

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffWithinAt.contDiffAt (h : ContDiffWithinAt 𝕜 n f s x) (hx : s ∈ 𝓝 x) :
    ContDiffAt 𝕜 n f x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
hx : s ∈ 𝓝 x
⊢ ContDiffAt 𝕜 n f x

Tactic:
rwa [ContDiffAt, ← contDiffWithinAt_inter hx, univ_inter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem le_sub_of_add_le {a b c : Nat} (h : a + b ≤ c) : a ≤ c - b

Proof state:
a b c : Nat
h : a + b ≤ c
d : Nat
hd✝ : a + b + d = c
hd : a + d + b = c
⊢ a + d = c - b

Tactic:
have hd := Nat.sub_eq_of_eq_add hd.symm

Result:
a b c : Nat
h : a + b ≤ c
d : Nat
hd✝¹ : a + b + d = c
hd✝ : a + d + b = c
hd : c - b = a + d
⊢ a + d = c - b

Proof state:
a b c : Nat
h : a + b ≤ c
d : Nat
hd : a + b + d = c
⊢ a + d + b = c

Tactic:
simp [← hd, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]

Result:
no goals

Proof state:
a b c : Nat
h : a + b ≤ c
d : Nat
hd : a + b + d = c
⊢ a ≤ c - b

Tactic:
apply @le.intro _ _ d

Result:
a b c : Nat
h : a + b ≤ c
d : Nat
hd : a + b + d = c
⊢ a + d = c - b

Proof state:
a b c : Nat
h : a + b ≤ c
d : Nat
hd : a + b + d = c
⊢ a + d = c - b

Tactic:
have hd : a + d + b = c := by simp [← hd, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]

Result:
a b c : Nat
h : a + b ≤ c
d : Nat
hd✝ : a + b + d = c
hd : a + d + b = c
⊢ a + d = c - b

Proof state:
a b c : Nat
h : a + b ≤ c
d : Nat
hd✝¹ : a + b + d = c
hd✝ : a + d + b = c
hd : c - b = a + d
⊢ a + d = c - b

Tactic:
exact hd.symm

Result:
no goals

Proof state:
a b c : Nat
h : a + b ≤ c
⊢ a ≤ c - b

Tactic:
match le.dest h with
| ⟨d, hd⟩ =>
  apply @le.intro _ _ d
  have hd : a + d + b = c := by simp [← hd, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]
  have hd := Nat.sub_eq_of_eq_add hd.symm
  exact hd.symm

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem neg_eq_self_iff {θ : Angle} : -θ = θ ↔ θ = 0 ∨ θ = π

Proof state:
θ : Angle
⊢ -θ = θ ↔ θ = 0 ∨ θ = ↑π

Tactic:
rw [eq_comm, eq_neg_self_iff]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem not_mem_setOfIdeal {I : Ideal C(X, R)} {x : X} :
    x ∉ setOfIdeal I ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → f x = 0

Proof state:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ x ∉ setOfIdeal I ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → f x = 0

Tactic:
rw [← Set.mem_compl_iff, setOfIdeal, compl_compl, Set.mem_setOf]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem cons_subset_cons {hs ht} : s.cons a hs ⊆ t.cons a ht ↔ s ⊆ t

Proof state:
α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ cons a s hs ⊆ cons a t ht ↔ s ⊆ t

Tactic:
rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_left_eq_self : a * b = b ↔ a = 1 := calc
  a * b = b ↔ a * b = 1 * b

Proof state:
M : Type u_4
inst✝ : RightCancelMonoid M
a b : M
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_biUnion_congr {s : Set ι} {t : ι → Set α} (hc : s.Countable) :
    μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔
      ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Set ι
t : ι → Set α
hc : s.Countable
this : Encodable ↑s
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)

Tactic:
simp only [biUnion_eq_iUnion, SetCoe.forall', restrict_iUnion_congr]

Result:
no goals

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Set ι
t : ι → Set α
hc : s.Countable
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)

Tactic:
haveI := hc.toEncodable

Result:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Set ι
t : ι → Set α
hc : s.Countable
this : Encodable ↑s
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
-- Mathlib/CategoryTheory/Abelian/RightDerived.lean
theorem NatTrans.rightDerived_id (F : C ⥤ D) [F.Additive] (n : ℕ) :
    NatTrans.rightDerived (𝟙 F) n = 𝟙 (F.rightDerived n)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ whiskerRight (rightDerivedToHomotopyCategory (𝟙 F)) (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) =
    𝟙 (F.rightDerived n)

Tactic:
simp only [rightDerivedToHomotopyCategory_id, whiskerRight_id']

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ 𝟙 (F.rightDerivedToHomotopyCategory ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) = 𝟙 (F.rightDerived n)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ rightDerived (𝟙 F) n = 𝟙 (F.rightDerived n)

Tactic:
dsimp only [rightDerived]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ whiskerRight (rightDerivedToHomotopyCategory (𝟙 F)) (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) =
    𝟙 (F.rightDerived n)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ 𝟙 (F.rightDerivedToHomotopyCategory ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) = 𝟙 (F.rightDerived n)

Tactic:
rfl

Result:
no goals