harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigOWith_pi {ι : Type*} [Fintype ι] {E' : ι → Type*} [∀ i, NormedAddCommGroup (E' i)]
    {f : α → ∀ i, E' i} {C : ℝ} (hC : 0 ≤ C) :
    IsBigOWith C l f g' ↔ ∀ i, IsBigOWith C l (fun x => f x i) g'

Proof state:
α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → NormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
C : ℝ
hC : 0 ≤ C
this : ∀ (x : α), 0 ≤ C * ‖g' x‖
⊢ IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith C l (fun x => f x i) g'

Tactic:
simp only [isBigOWith_iff, pi_norm_le_iff_of_nonneg (this _), eventually_all]

Result:
no goals

Proof state:
α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → NormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
C : ℝ
hC : 0 ≤ C
⊢ IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith C l (fun x => f x i) g'

Tactic:
have : ∀ x, 0 ≤ C * ‖g' x‖ := fun x => mul_nonneg hC (norm_nonneg _)

Result:
α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → NormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
C : ℝ
hC : 0 ≤ C
this : ∀ (x : α), 0 ≤ C * ‖g' x‖
⊢ IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith C l (fun x => f x i) g'
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_extend_one {f : α → M'} {g : α → N} (hf : f.Injective) :
    mulSupport (f.extend g 1) = f '' mulSupport g :=
  mulSupport_extend_one_subset.antisymm <| by
    rintro _ ⟨x, hx, rfl⟩; rwa [mem_mulSupport, hf.extend_apply]

Proof state:
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
hf : Injective f
⊢ f '' mulSupport g ⊆ mulSupport (extend f g 1)

Tactic:
rintro _ ⟨x, hx, rfl⟩

Result:
case intro.intro
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
hf : Injective f
x : α
hx : x ∈ mulSupport g
⊢ f x ∈ mulSupport (extend f g 1)

Proof state:
case intro.intro
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
hf : Injective f
x : α
hx : x ∈ mulSupport g
⊢ f x ∈ mulSupport (extend f g 1)

Tactic:
rwa [mem_mulSupport, hf.extend_apply]

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem last_ofFn {n : ℕ} (f : Fin n → α) (h : ofFn f ≠ [])
    (hn : n - 1 < n := Nat.pred_lt <| ofFn_eq_nil_iff.not.mp h) :
    getLast (ofFn f) h = f ⟨n - 1, hn⟩

Proof state:
α : Type u
n : ℕ
f : Fin n → α
h : ofFn f ≠ []
hn : optParam (n - 1 < n) ⋯
⊢ (ofFn f).getLast h = f ⟨n - 1, hn⟩

Tactic:
simp [getLast_eq_getElem]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffOn_nat_iff_continuousOn_differentiableOn {n : ℕ} (hs : UniqueDiffOn 𝕜 s) :
    ContDiffOn 𝕜 n f s ↔
      (∀ m : ℕ, m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ∧
        ∀ m : ℕ, m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s

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
n : ℕ
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (↑n) f s ↔
    (∀ m ≤ n, ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ∧
      ∀ m < n, DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s

Tactic:
rw [← WithTop.coe_natCast, contDiffOn_iff_continuousOn_differentiableOn hs]

Result:
𝕜 : 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
n : ℕ
hs : UniqueDiffOn 𝕜 s
⊢ ((∀ (m : ℕ), ↑m ≤ ↑n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ∧
      ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ↔
    (∀ m ≤ n, ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ∧
      ∀ m < n, DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s

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
n : ℕ
hs : UniqueDiffOn 𝕜 s
⊢ ((∀ (m : ℕ), ↑m ≤ ↑n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ∧
      ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ↔
    (∀ m ≤ n, ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ∧
      ∀ m < n, DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toMeasure_apply_eq_zero_iff (hs : MeasurableSet s) :
    p.toMeasure s = 0 ↔ Disjoint p.support s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
p : PMF α
s : Set α
hs : MeasurableSet s
⊢ p.toMeasure s = 0 ↔ Disjoint p.support s

Tactic:
rw [toMeasure_apply_eq_toOuterMeasure_apply p s hs, toOuterMeasure_apply_eq_zero_iff]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_pow_id (a : A) (n : ℕ) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
n : ℕ
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => x ^ n) a = a ^ n

Tactic:
rw [cfc_pow .., cfc_id' ..]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma isReal_comp_iff {f : k ≃+* K} {φ : K →+* ℂ} :
    IsReal (φ.comp (f : k →+* K)) ↔ IsReal φ :=
  ⟨fun H ↦ by convert H.comp f.symm.toRingHom; ext1; simp, IsReal.comp _⟩

Proof state:
K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp ↑f)
⊢ IsReal φ

Tactic:
convert H.comp f.symm.toRingHom

Result:
case h.e'_3
K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp ↑f)
⊢ φ = (φ.comp ↑f).comp f.symm.toRingHom

Proof state:
case h.e'_3
K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp ↑f)
⊢ φ = (φ.comp ↑f).comp f.symm.toRingHom

Tactic:
ext1

Result:
case h.e'_3.a
K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp ↑f)
x✝ : K
⊢ φ x✝ = ((φ.comp ↑f).comp f.symm.toRingHom) x✝

Proof state:
case h.e'_3.a
K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp ↑f)
x✝ : K
⊢ φ x✝ = ((φ.comp ↑f).comp f.symm.toRingHom) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Part.lean
theorem some_mul_some [Mul α] (a b : α) : some a * some b = some (a * b)

Proof state:
α : Type u_1
inst✝ : Mul α
a b : α
⊢ some a * some b = some (a * b)

Tactic:
simp [mul_def]

Result:
no goals
-- Mathlib/Data/List/ProdSigma.lean
theorem length_product (l₁ : List α) (l₂ : List β) :
    length (l₁ ×ˢ l₂) = length l₁ * length l₂

Proof state:
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
⊢ (l₁ ×ˢ l₂).length = l₁.length * l₂.length

Tactic:
induction' l₁ with x l₁ IH

Result:
case nil
α : Type u_1
β : Type u_2
l₂ : List β
⊢ ([] ×ˢ l₂).length = [].length * l₂.length

case cons
α : Type u_1
β : Type u_2
l₂ : List β
x : α
l₁ : List α
IH : (l₁ ×ˢ l₂).length = l₁.length * l₂.length
⊢ ((x :: l₁) ×ˢ l₂).length = (x :: l₁).length * l₂.length

Proof state:
case nil
α : Type u_1
β : Type u_2
l₂ : List β
⊢ ([] ×ˢ l₂).length = [].length * l₂.length

Tactic:
exact (Nat.zero_mul _).symm

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
l₂ : List β
x : α
l₁ : List α
IH : (l₁ ×ˢ l₂).length = l₁.length * l₂.length
⊢ ((x :: l₁) ×ˢ l₂).length = (x :: l₁).length * l₂.length

Tactic:
simp only [length, product_cons, length_append, IH, Nat.add_mul, Nat.one_mul, length_map,
  Nat.add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insert [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {k a : α}
    {v : β k} :
    (m.insert k v).getKey! a = if k == a then k else m.getKey! a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
k a : α
v : β k
⊢ (m.insert k v).getKey! a = if (k == a) = true then k else m.getKey! a

Tactic:
simp_to_model [insert] using List.getKey!_insertEntry

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UInt.lean
theorem USize.toUInt64_toNat (x : USize) : x.toUInt64.toNat = x.toNat

Proof state:
x : USize
⊢ x.toUInt64.toNat = x.toNat

Tactic:
simp only [USize.toUInt64, UInt64.toNat]

Result:
x : USize
⊢ (UInt64.ofNatCore x.toBitVec.toNat ⋯).toBitVec.toNat = x.toNat

Proof state:
x : USize
⊢ (UInt64.ofNatCore x.toBitVec.toNat ⋯).toBitVec.toNat = x.toNat

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem inl_mul [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
    (r₁ r₂ : R) : (inl (r₁ * r₂) : tsze R M) = inl r₁ * inl r₂ :=
  ext rfl <| show (0 : M) = r₁ •> (0 : M) + (0 : M) <• r₂ by rw [smul_zero, zero_add, smul_zero]

Proof state:
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r₁ r₂ : R
⊢ 0 = r₁ •> 0 + 0 <• r₂

Tactic:
rw [smul_zero, zero_add, smul_zero]

Result:
no goals
-- Mathlib/RingTheory/Localization/Away/Basic.lean
theorem selfZPow_sub_natCast {n m : ℕ} :
    selfZPow x B (n - m) = mk' _ (x ^ n) (Submonoid.pow x m)

Proof state:
case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : ¬m ≤ n
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

Tactic:
rw [← neg_sub, ← Int.ofNat_sub (le_of_not_le h), selfZPow_neg_natCast,
  IsLocalization.mk'_eq_iff_eq]

Result:
case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : ¬m ≤ n
⊢ (algebraMap R B) (↑(Submonoid.pow x m) * 1) = (algebraMap R B) (↑(Submonoid.pow x (m - n)) * x ^ n)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

Tactic:
by_cases h : m ≤ n

Result:
case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : m ≤ n
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : ¬m ≤ n
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

Proof state:
case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : m ≤ n
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

Tactic:
rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
  selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel h]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : ¬m ≤ n
⊢ (algebraMap R B) (↑(Submonoid.pow x m) * 1) = (algebraMap R B) (↑(Submonoid.pow x (m - n)) * x ^ n)

Tactic:
simp [Submonoid.pow_apply, ← pow_add, Nat.sub_add_cancel (le_of_not_le h)]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma XIsoOfEq_inv_comp_XIsoOfEq_hom (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
    (h₂₁ : p₂ = p₁) (h₂₃ : p₂ = p₃) :
    (K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq (h₂₁.symm.trans h₂₃)).hom

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₂₃ : p₂ = p₃
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp only [eqToHom_trans]

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₂₃ : p₂ = p₃
⊢ (K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom

Tactic:
dsimp [XIsoOfEq]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₂₃ : p₂ = p₃
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯
-- Mathlib/Data/Nat/Size.lean
theorem lt_size {m n : ℕ} : m < size n ↔ 2 ^ m ≤ n

Proof state:
m n : ℕ
⊢ m < n.size ↔ 2 ^ m ≤ n

Tactic:
rw [← not_lt, Decidable.iff_not_comm, not_lt, size_le]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Internal.lean
theorem SetLike.natCast_mem_graded [Zero ι] [AddMonoidWithOne R] [SetLike σ R]
    [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedOne A] (n : ℕ) : (n : R) ∈ A 0

Proof state:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n : ℕ
⊢ ↑n ∈ A 0

Tactic:
induction n with
| zero =>
  rw [Nat.cast_zero]
  exact zero_mem (A 0)
| succ _ n_ih =>
  rw [Nat.cast_succ]
  exact add_mem n_ih (SetLike.one_mem_graded _)

Result:
no goals

Proof state:
case zero
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
⊢ ↑0 ∈ A 0

Tactic:
rw [Nat.cast_zero]

Result:
case zero
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
⊢ 0 ∈ A 0

Proof state:
case succ
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n✝ : ℕ
n_ih : ↑n✝ ∈ A 0
⊢ ↑n✝ + 1 ∈ A 0

Tactic:
exact add_mem n_ih (SetLike.one_mem_graded _)

Result:
no goals

Proof state:
case zero
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
⊢ 0 ∈ A 0

Tactic:
exact zero_mem (A 0)

Result:
no goals

Proof state:
case succ
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n✝ : ℕ
n_ih : ↑n✝ ∈ A 0
⊢ ↑(n✝ + 1) ∈ A 0

Tactic:
rw [Nat.cast_succ]

Result:
case succ
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n✝ : ℕ
n_ih : ↑n✝ ∈ A 0
⊢ ↑n✝ + 1 ∈ A 0
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_const_mul_atTop_of_neg (hr : r < 0) :
    Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atBot

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atBot

Tactic:
simpa only [neg_mul, tendsto_neg_atBot_iff] using tendsto_const_mul_atBot_of_pos (neg_pos.2 hr)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_map {f : α → β} {g : β → γ} {as : Vector α n} :
    (as.map f).map g = as.map (g ∘ f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β
g : β → γ
as : Vector α n
⊢ map g (map f as) = map (g ∘ f) as

Tactic:
cases as

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β
g : β → γ
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map g (map f { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    map (g ∘ f) { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β
g : β → γ
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map g (map f { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    map (g ∘ f) { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Order/UpperLower.lean
lemma dist_anti_left_pi : AntitoneOn (dist · y) (Iic y)

Proof state:
ι : Type u_2
inst✝ : Fintype ι
y : ι → ℝ
⊢ AntitoneOn (fun x => dist x y) (Iic y)

Tactic:
refine fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ ?_)

Result:
ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Iic y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Iic y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ nndist (y₂ i) (y i) ≤ nndist (y₁ i) (y i)

Proof state:
ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Iic y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Iic y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ nndist (y₂ i) (y i) ≤ nndist (y₁ i) (y i)

Tactic:
rw [Real.nndist_eq', Real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₂ i ≤ y i)),
  Real.nndist_eq', Real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₁ i ≤ y i))]

Result:
ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Iic y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Iic y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ (y i - y₂ i).toNNReal ≤ (y i - y₁ i).toNNReal

Proof state:
ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Iic y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Iic y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ (y i - y₂ i).toNNReal ≤ (y i - y₁ i).toNNReal

Tactic:
exact Real.toNNReal_mono (sub_le_sub_left (hy _) _)

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem le_sum_condensed (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) (n : ℕ) :
    (∑ k ∈ range (2 ^ n), f k) ≤ f 0 + ∑ k ∈ range n, 2 ^ k • f (2 ^ k)

Proof state:
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range (2 ^ n), f k ≤ f 0 + ∑ k ∈ range n, 2 ^ k • f (2 ^ k)

Tactic:
convert add_le_add_left (le_sum_condensed' hf n) (f 0)

Result:
case h.e'_3
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range (2 ^ n), f k = f 0 + ∑ k ∈ Ico 1 (2 ^ n), f k

Proof state:
case h.e'_3
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range (2 ^ n), f k = f 0 + ∑ k ∈ Ico 1 (2 ^ n), f k

Tactic:
rw [← sum_range_add_sum_Ico _ n.one_le_two_pow, sum_range_succ, sum_range_zero, zero_add]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
lemma inner_eq_zero_of_right (x : E) {y : E} (h : ‖y‖ = 0) : ⟪x, y⟫_𝕜 = 0

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

Tactic:
rw [inner_eq_zero_symm, inner_eq_zero_of_left _ h]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem tendsto_nat_floor_div_atTop : Tendsto (fun x ↦ (⌊x⌋₊ : R) / x) atTop (𝓝 1)

Proof state:
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
⊢ Tendsto (fun x => ↑⌊x⌋₊ / x) atTop (𝓝 1)

Tactic:
simpa using tendsto_nat_floor_mul_div_atTop (zero_le_one' R)

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Defs.lean
lemma one_sub_le_one_sub_mul_one_add (h : b + b * c ≤ a + c) : 1 - a ≤ (1 - b) * (1 + c)

Proof state:
α : Type u
inst✝ : OrderedRing α
a b c : α
h : b + b * c ≤ a + c
⊢ 1 + (b + b * c) ≤ 1 + (a + c)

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u
inst✝ : OrderedRing α
a b c : α
h : b + b * c ≤ a + c
⊢ 1 - a ≤ (1 - b) * (1 + c)

Tactic:
rw [one_sub_mul, mul_one_add, sub_le_sub_iff, add_assoc, add_comm c]

Result:
α : Type u
inst✝ : OrderedRing α
a b c : α
h : b + b * c ≤ a + c
⊢ 1 + (b + b * c) ≤ 1 + (a + c)
-- Mathlib/Topology/Order/LowerUpperTopology.lean
lemma isTopologicalBasis_insert_univ_subbasis :
    IsTopologicalBasis (insert univ {s : Set α | ∃ a, (Ici a)ᶜ = s}) :=
  isTopologicalBasis_of_subbasis_of_inter (by rw [topology_eq α, lower]) (by
    rintro _ ⟨b, rfl⟩ _ ⟨c, rfl⟩
    use b ⊓ c
    rw [compl_Ici, compl_Ici, compl_Ici, Iio_inter_Iio])

Proof state:
case intro.intro
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
b c : α
⊢ (Ici b)ᶜ ∩ (Ici c)ᶜ ∈ {s | ∃ a, (Ici a)ᶜ = s}

Tactic:
use b ⊓ c

Result:
case h
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
b c : α
⊢ (Ici (b ⊓ c))ᶜ = (Ici b)ᶜ ∩ (Ici c)ᶜ

Proof state:
case h
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
b c : α
⊢ (Ici (b ⊓ c))ᶜ = (Ici b)ᶜ ∩ (Ici c)ᶜ

Tactic:
rw [compl_Ici, compl_Ici, compl_Ici, Iio_inter_Iio]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ inst✝¹ = generateFrom {s | ∃ a, (Ici a)ᶜ = s}

Tactic:
rw [topology_eq α, lower]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ ∀ ⦃s : Set α⦄,
    s ∈ {s | ∃ a, (Ici a)ᶜ = s} → ∀ ⦃t : Set α⦄, t ∈ {s | ∃ a, (Ici a)ᶜ = s} → s ∩ t ∈ {s | ∃ a, (Ici a)ᶜ = s}

Tactic:
rintro _ ⟨b, rfl⟩ _ ⟨c, rfl⟩

Result:
case intro.intro
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
b c : α
⊢ (Ici b)ᶜ ∩ (Ici c)ᶜ ∈ {s | ∃ a, (Ici a)ᶜ = s}
-- Mathlib/Topology/Constructible.lean
lemma IsRetrocompact.finsetInf' {ι : Type*} {s : Finset ι} {hs} {t : ι → Set X}
    (ht : ∀ i ∈ s, IsRetrocompact (t i)) : IsRetrocompact (s.inf' hs t)

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.inf' hs t)

Tactic:
rw [Finset.inf'_eq_inf]

Result:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.inf t)

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.inf t)

Tactic:
exact .finsetInf ht

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
/-- A small set of games is bounded above. -/
lemma bddAbove_of_small (s : Set Game.{u}) [Small.{u} s] : BddAbove s

Proof state:
s : Set Game
inst✝ : Small.{u, u + 1} ↑s
⊢ BddAbove s

Tactic:
simpa using bddAbove_range_of_small (Subtype.val : s → Game.{u})

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
theorem swap_mul_eq_iff {i j : α} {σ : Perm α} : swap i j * σ = σ ↔ i = j

Proof state:
α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ swap i j * σ = σ ↔ i = j

Tactic:
rw [mul_left_eq_self, swap_eq_one_iff]

Result:
no goals
-- Mathlib/Data/Vector/Defs.lean
theorem cons_head_tail : ∀ v : Vector α (succ n), cons (head v) (tail v) = v
  | ⟨[], h⟩ => by contradiction
  | ⟨_ :: _, _⟩ => rfl

Proof state:
α : Type u_1
n : ℕ
h : [].length = n.succ
⊢ cons (head ⟨[], h⟩) (tail ⟨[], h⟩) = ⟨[], h⟩

Tactic:
contradiction

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_star : -star = star

Proof state:
⊢ -star = star

Tactic:
simp [star]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem liftRel_think_right (R : α → β → Prop) (ca : Computation α) (cb : Computation β) :
    LiftRel R ca (think cb) ↔ LiftRel R ca cb

Proof state:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel (swap R) cb.think ca ↔ LiftRel (swap R) cb ca

Tactic:
apply liftRel_think_left

Result:
no goals

Proof state:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel R ca cb.think ↔ LiftRel R ca cb

Tactic:
rw [← LiftRel.swap R, ← LiftRel.swap R]

Result:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel (swap R) cb.think ca ↔ LiftRel (swap R) cb ca