harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Image.lean
theorem image_eq_image {f : α → β} (hf : Injective f) : f '' s = f '' t ↔ s = t :=
  Iff.symm <|
    (Iff.intro fun eq => eq ▸ rfl) fun eq => by
      rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, eq]

Proof state:
α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
eq : f '' s = f '' t
⊢ s = t

Tactic:
rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, eq]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem exists_length_eq_zero_iff {u v : V} : (∃ p : G.Walk u v, p.length = 0) ↔ u = v

Proof state:
case mp
V : Type u
G : SimpleGraph V
u v : V
⊢ (∃ p, p.length = 0) → u = v

Tactic:
rintro ⟨p, hp⟩

Result:
case mp.intro
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = 0
⊢ u = v

Proof state:
case mp.intro
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = 0
⊢ u = v

Tactic:
exact eq_of_length_eq_zero hp

Result:
no goals

Proof state:
case mpr
V : Type u
G : SimpleGraph V
u : V
⊢ ∃ p, p.length = 0

Tactic:
exact ⟨nil, rfl⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
⊢ (∃ p, p.length = 0) ↔ u = v

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
u v : V
⊢ (∃ p, p.length = 0) → u = v

case mpr
V : Type u
G : SimpleGraph V
u v : V
⊢ u = v → ∃ p, p.length = 0

Proof state:
case mpr
V : Type u
G : SimpleGraph V
u v : V
⊢ u = v → ∃ p, p.length = 0

Tactic:
rintro rfl

Result:
case mpr
V : Type u
G : SimpleGraph V
u : V
⊢ ∃ p, p.length = 0
-- Mathlib/AlgebraicTopology/TopologicalSimplex.lean
lemma toTopObj_one_add_eq_one (f : ⦋1⦌.toTopObj) : f 0 + f 1 = 1

Proof state:
f : ↑⦋1⦌.toTopObj
⊢ ↑f 0 + ↑f 1 = 1

Tactic:
simpa [toType_apply, Finset.sum] using show ∑ _, _ = _ from f.2

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem submatrix_id_mul_right [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type*}
    (M : Matrix m n α) (N : Matrix o p α) (e₁ : l → p) (e₂ : o ≃ n) :
    M.submatrix id e₂ * N.submatrix id e₁ = M * N.submatrix e₂.symm e₁

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → p
e₂ : o ≃ n
i✝ : m
j✝ : l
⊢ (M.submatrix id ⇑e₂ * N.submatrix id e₁) i✝ j✝ = (M * N.submatrix (⇑e₂.symm) e₁) i✝ j✝

Tactic:
simp [mul_apply, ← e₂.bijective.sum_comp]

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → p
e₂ : o ≃ n
⊢ M.submatrix id ⇑e₂ * N.submatrix id e₁ = M * N.submatrix (⇑e₂.symm) e₁

Tactic:
ext

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → p
e₂ : o ≃ n
i✝ : m
j✝ : l
⊢ (M.submatrix id ⇑e₂ * N.submatrix id e₁) i✝ j✝ = (M * N.submatrix (⇑e₂.symm) e₁) i✝ j✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.ro_eq_true_of_le (u v k : Nat) : u ≤ v → (u ≤ v + k) = True :=
  by simp; omega

Proof state:
u v k : Nat
⊢ u ≤ v → (u ≤ v + k) = True

Tactic:
simp

Result:
u v k : Nat
⊢ u ≤ v → u ≤ v + k

Proof state:
u v k : Nat
⊢ u ≤ v → u ≤ v + k

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
theorem nth_eq_sInf (p : ℕ → Prop) (n : ℕ) : nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Proof state:
case neg.intro
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #⋯.toFinset ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
rw [nth_of_card_le _ hn]

Result:
case neg.intro
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #⋯.toFinset ≤ n
⊢ 0 = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Proof state:
case neg
p : ℕ → Prop
n : ℕ
hn : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
rcases hn with ⟨hf, hn⟩

Result:
case neg.intro
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #⋯.toFinset ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Proof state:
case neg
p : ℕ → Prop
n : ℕ
hn : ¬∀ (hf : (setOf p).Finite), n < #hf.toFinset
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
push_neg at hn

Result:
case neg
p : ℕ → Prop
n : ℕ
hn : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Proof state:
case neg.intro.intro.intro
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #⋯.toFinset ≤ n
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k < #hf.toFinset
hk : nth p k ∈ {x | p x ∧ ∀ k < n, nth p k < x}
⊢ False

Tactic:
exact (hk.2 _ ((hlt hf).trans_le hn)).false

Result:
no goals

Proof state:
case neg.intro
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #⋯.toFinset ≤ n
⊢ 0 = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
refine ((congr_arg sInf <| Set.eq_empty_of_forall_not_mem fun k hk => ?_).trans sInf_empty).symm

Result:
case neg.intro
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #⋯.toFinset ≤ n
k : ℕ
hk : k ∈ {x | p x ∧ ∀ k < n, nth p k < x}
⊢ False

Proof state:
case neg.intro
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #⋯.toFinset ≤ n
k : ℕ
hk : k ∈ {x | p x ∧ ∀ k < n, nth p k < x}
⊢ False

Tactic:
rcases exists_lt_card_nth_eq hk.1 with ⟨k, hlt, rfl⟩

Result:
case neg.intro.intro.intro
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #⋯.toFinset ≤ n
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k < #hf.toFinset
hk : nth p k ∈ {x | p x ∧ ∀ k < n, nth p k < x}
⊢ False

Proof state:
p : ℕ → Prop
n : ℕ
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
by_cases hn : ∀ hf : (setOf p).Finite, n < #hf.toFinset

Result:
case pos
p : ℕ → Prop
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #hf.toFinset
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

case neg
p : ℕ → Prop
n : ℕ
hn : ¬∀ (hf : (setOf p).Finite), n < #hf.toFinset
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Proof state:
case pos
p : ℕ → Prop
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #hf.toFinset
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
exact (isLeast_nth hn).csInf_eq.symm

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem IsSt.map {x : ℝ*} {r : ℝ} (hxr : IsSt x r) {f : ℝ → ℝ} (hf : ContinuousAt f r) :
    IsSt (x.map f) (f r)

Proof state:
x : ℝ*
r : ℝ
hxr : x.IsSt r
f : ℝ → ℝ
hf : ContinuousAt f r
⊢ IsSt (Germ.map f x) (f r)

Tactic:
rcases ofSeq_surjective x with ⟨g, rfl⟩

Result:
case intro
r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
g : ℕ → ℝ
hxr : (ofSeq g).IsSt r
⊢ IsSt (Germ.map f (ofSeq g)) (f r)

Proof state:
case intro
r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
g : ℕ → ℝ
hxr : (ofSeq g).IsSt r
⊢ IsSt (Germ.map f (ofSeq g)) (f r)

Tactic:
exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (isSt_ofSeq_iff_tendsto.1 hxr)

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_inter_Ico : Ico a b ∩ Ico c d = Ico (max a c) (min b d)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Ico a b ∩ Ico c d = Ico (a ⊔ c) (b ⊓ d)

Tactic:
rw [Ico, Ico, Ico, ← Finset.inter_val, Finset.Ico_inter_Ico]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Cones.lean
theorem cocone_iso_of_hom_iso {K : J ⥤ C} {c d : Cocone K} (f : c ⟶ d) [i : IsIso f.hom] :
    IsIso f :=
  ⟨⟨{ hom := inv f.hom
      w := fun j => (asIso f.hom).comp_inv_eq.2 (f.w j).symm }, by aesop_cat⟩⟩

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
K : J ⥤ C
c d : Cocone K
f : c ⟶ d
i : IsIso f.hom
⊢ f ≫ { hom := inv f.hom, w := ⋯ } = 𝟙 c ∧ { hom := inv f.hom, w := ⋯ } ≫ f = 𝟙 d

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem toOuterMeasure_bind_apply :
    (p.bind f).toOuterMeasure s = ∑' a, p a * (f a).toOuterMeasure s

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
⊢ (if b ∈ s then (f a) b else 0) = if b ∈ s then (f a) b else 0

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
⊢ (p.bind f).toOuterMeasure s = ∑' (b : β), if b ∈ s then ∑' (a : α), p a * (f a) b else 0

Tactic:
simp [toOuterMeasure_apply, Set.indicator_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
⊢ (p a * ∑' (b : β), if b ∈ s then (f a) b else 0) = p a * (f a).toOuterMeasure s

Tactic:
simp only [toOuterMeasure_apply, Set.indicator_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
b : β
⊢ (if b ∈ s then ∑' (a : α), p a * (f a) b else 0) = ∑' (a : α), p a * if b ∈ s then (f a) b else 0

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
⊢ (p.bind f).toOuterMeasure s = ∑' (a : α), p a * (f a).toOuterMeasure s

Tactic:
classical
calc
  (p.bind f).toOuterMeasure s = ∑' b, if b ∈ s then ∑' a, p a * f a b else 0 := by
    simp [toOuterMeasure_apply, Set.indicator_apply]
  _ = ∑' (b) (a), p a * if b ∈ s then f a b else 0 := tsum_congr fun b => by split_ifs <;> simp
  _ = ∑' (a) (b), p a * if b ∈ s then f a b else 0 :=
    (tsum_comm' ENNReal.summable (fun _ => ENNReal.summable) fun _ => ENNReal.summable)
  _ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 := tsum_congr fun _ => ENNReal.tsum_mul_left
  _ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 :=
    (tsum_congr fun a => (congr_arg fun x => p a * x) <| tsum_congr fun b => by split_ifs <;> rfl)
  _ = ∑' a, p a * (f a).toOuterMeasure s :=
    tsum_congr fun a => by simp only [toOuterMeasure_apply, Set.indicator_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
⊢ (p.bind f).toOuterMeasure s = ∑' (a : α), p a * (f a).toOuterMeasure s

Tactic:
calc
  (p.bind f).toOuterMeasure s = ∑' b, if b ∈ s then ∑' a, p a * f a b else 0 := by
    simp [toOuterMeasure_apply, Set.indicator_apply]
  _ = ∑' (b) (a), p a * if b ∈ s then f a b else 0 := tsum_congr fun b => by split_ifs <;> simp
  _ = ∑' (a) (b), p a * if b ∈ s then f a b else 0 :=
    (tsum_comm' ENNReal.summable (fun _ => ENNReal.summable) fun _ => ENNReal.summable)
  _ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 := tsum_congr fun _ => ENNReal.tsum_mul_left
  _ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 :=
    (tsum_congr fun a => (congr_arg fun x => p a * x) <| tsum_congr fun b => by split_ifs <;> rfl)
  _ = ∑' a, p a * (f a).toOuterMeasure s :=
    tsum_congr fun a => by simp only [toOuterMeasure_apply, Set.indicator_apply]

Result:
no goals
-- Mathlib/Tactic/Peel.lean
theorem eventually_congr {α : Type*} {p q : α → Prop} {f : Filter α}
    (hq : ∀ (x : α), p x ↔ q x) : (∀ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, q x

Proof state:
case a.h.e'_2.h.a
α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x ↔ q x
x✝ : α
⊢ p x✝ ↔ q x✝

Tactic:
exact hq _

Result:
no goals

Proof state:
α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x ↔ q x
⊢ (∀ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, q x

Tactic:
congr! 2

Result:
case a.h.e'_2.h.a
α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x ↔ q x
x✝ : α
⊢ p x✝ ↔ q x✝
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem tendsto_Ioo_atBot {f : β → Ioo a b} :
    Tendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l (𝓝[>] a)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
l : Filter β
f : β → ↑(Ioo a b)
⊢ Tendsto f l atBot ↔ Tendsto (fun x => ↑(f x)) l (𝓝[>] a)

Tactic:
rw [← comap_coe_Ioo_nhdsGT, tendsto_comap_iff]

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
l : Filter β
f : β → ↑(Ioo a b)
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[>] a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[>] a)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
l : Filter β
f : β → ↑(Ioo a b)
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[>] a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[>] a)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (l : Vector α n) (l' : Vector β n) :
    map (Function.uncurry f) (l.zip l') = zipWith f l l'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β → γ
l : Vector α n
l' : Vector β n
⊢ map (Function.uncurry f) (l.zip l') = zipWith f l l'

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : Array α
l' : Vector β l.size
⊢ map (Function.uncurry f) ({ toArray := l, size_toArray := ⋯ }.zip l') =
    zipWith f { toArray := l, size_toArray := ⋯ } l'

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : Array α
l' : Vector β l.size
⊢ map (Function.uncurry f) ({ toArray := l, size_toArray := ⋯ }.zip l') =
    zipWith f { toArray := l, size_toArray := ⋯ } l'

Tactic:
rcases l' with ⟨l', h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : Array α
l' : Array β
h : l'.size = l.size
⊢ map (Function.uncurry f) ({ toArray := l, size_toArray := ⋯ }.zip { toArray := l', size_toArray := h }) =
    zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : Array α
l' : Array β
h : l'.size = l.size
⊢ map (Function.uncurry f) ({ toArray := l, size_toArray := ⋯ }.zip { toArray := l', size_toArray := h }) =
    zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }

Tactic:
simp [Array.map_uncurry_zip_eq_zipWith]

Result:
no goals
-- Mathlib/RingTheory/IsTensorProduct.lean
theorem Algebra.pushoutDesc_left [Algebra.IsPushout R S R' S'] {A : Type*} [Semiring A]
    [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H) (x : S) :
    Algebra.pushoutDesc S' f g H (algebraMap S S' x) = f x

Proof state:
R : Type u_1
S : Type v₃
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝¹⁰ : CommSemiring R'
inst✝⁹ : CommSemiring S'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra R' S'
inst✝⁵ : Algebra R S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsScalarTower R S S'
inst✝² : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : S →ₐ[R] A
g : R' →ₐ[R] A
H : ∀ (x : S) (y : R'), f x * g y = g y * f x
x : S
⊢ (pushoutDesc S' f g H) ((algebraMap S S') x) = f x

Tactic:
simp [Algebra.pushoutDesc_apply]

Result:
no goals
-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_atTop_on_Ioi (hdf : DifferentiableOn ℝ f (Ioi a))
    (hg' : ∀ x ∈ Ioi a, (deriv g) x ≠ 0) (hftop : Tendsto f atTop (𝓝 0))
    (hgtop : Tendsto g atTop (𝓝 0)) (hdiv : Tendsto (fun x => (deriv f) x / (deriv g) x) atTop l) :
    Tendsto (fun x => f x / g x) atTop l

Proof state:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Ioi a)
hg' : ∀ x ∈ Ioi a, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l
hdf : ∀ x ∈ Ioi a, DifferentiableAt ℝ f x
⊢ Tendsto (fun x => f x / g x) atTop l

Tactic:
have hdg : ∀ x ∈ Ioi a, DifferentiableAt ℝ g x := fun x hx =>
  by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)

Result:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Ioi a)
hg' : ∀ x ∈ Ioi a, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l
hdf : ∀ x ∈ Ioi a, DifferentiableAt ℝ f x
hdg : ∀ x ∈ Ioi a, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) atTop l

Proof state:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Ioi a)
hg' : ∀ x ∈ Ioi a, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l
hdf : ∀ x ∈ Ioi a, DifferentiableAt ℝ f x
hdg : ∀ x ∈ Ioi a, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) atTop l

Tactic:
exact HasDerivAt.lhopital_zero_atTop_on_Ioi (fun x hx => (hdf x hx).hasDerivAt)
  (fun x hx => (hdg x hx).hasDerivAt) hg' hftop hgtop hdiv

Result:
no goals

Proof state:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Ioi a)
hg' : ∀ x ∈ Ioi a, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l
⊢ Tendsto (fun x => f x / g x) atTop l

Tactic:
have hdf : ∀ x ∈ Ioi a, DifferentiableAt ℝ f x := fun x hx =>
  (hdf x hx).differentiableAt (Ioi_mem_nhds hx)

Result:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Ioi a)
hg' : ∀ x ∈ Ioi a, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l
hdf : ∀ x ∈ Ioi a, DifferentiableAt ℝ f x
⊢ Tendsto (fun x => f x / g x) atTop l
-- Mathlib/Analysis/Calculus/MeanValue.lean
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is strictly positive,
then `f` is a strictly monotone function on `D`. -/
lemma strictAntiOn_of_hasDerivWithinAt_neg {D : Set ℝ} (hD : Convex ℝ D) {f f' : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x)
    (hf'₀ : ∀ x ∈ interior D, f' x < 0) : StrictAntiOn f D :=
  strictAntiOn_of_deriv_neg hD hf fun x hx ↦ by
    rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx

Proof state:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x < 0
x : ℝ
hx : x ∈ interior D
⊢ deriv f x < 0

Tactic:
rw [deriv_eqOn isOpen_interior hf' hx]

Result:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x < 0
x : ℝ
hx : x ∈ interior D
⊢ f' x < 0

Proof state:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x < 0
x : ℝ
hx : x ∈ interior D
⊢ f' x < 0

Tactic:
exact hf'₀ _ hx

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
lemma d₂_eq_zero (h : ¬ c₂.Rel i₂ (c₂.next i₂)) :
    K.d₂ c₁₂ i₁ i₂ i₁₂ = 0

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ = 0

Tactic:
dsimp [d₂]

Result:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
      (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂ =
    0

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
      (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂ =
    0

Tactic:
rw [HomologicalComplex.shape _ _ _ h, zero_comp, smul_zero]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullback_smul_apply :
    mpullback I I' f (c • V) x = c • mpullback I I' f V x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
V : (x : M') → TangentSpace I' x
c : 𝕜
⊢ mpullback I I' f (c • V) x = c • mpullback I I' f V x

Tactic:
simp [mpullback]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem mirror_leadingCoeff : p.mirror.leadingCoeff = p.trailingCoeff

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.mirror.leadingCoeff = p.trailingCoeff

Tactic:
rw [← p.mirror_mirror, mirror_trailingCoeff, p.mirror_mirror]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem one_right (a : ℤ) : J(a | 1) = 1

Proof state:
a : ℤ
⊢ J(a | 1) = 1

Tactic:
simp only [jacobiSym, primeFactorsList_one, List.prod_nil, List.pmap]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma Sigma.map'_comp_map {f : α → C} {g h : β → C} [HasCoproduct f] [HasCoproduct g]
    [HasCoproduct h] (p : α → β) (q : ∀ (a : α), f a ⟶ g (p a)) (q' : ∀ (b : β), g b ⟶ h b) :
    Sigma.map' p q ≫ Sigma.map q' = Sigma.map' p (fun a => q a ≫ q' (p a))

Proof state:
case h
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h b
b✝ : α
⊢ ι f b✝ ≫ map' p q ≫ map q' = ι f b✝ ≫ map' p fun a => q a ≫ q' (p a)

Tactic:
simp

Result:
no goals

Proof state:
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h b
⊢ map' p q ≫ map q' = map' p fun a => q a ≫ q' (p a)

Tactic:
ext

Result:
case h
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h b
b✝ : α
⊢ ι f b✝ ≫ map' p q ≫ map q' = ι f b✝ ≫ map' p fun a => q a ≫ q' (p a)
-- Mathlib/Order/Cover.lean
@[simp, norm_cast] lemma coe_wcovBy_coe : (a : WithBot α) ⩿ b ↔ a ⩿ b :=
  Set.OrdConnected.apply_wcovBy_apply_iff OrderEmbedding.withBotCoe <| by
    simp [WithBot.range_coe, ordConnected_Ioi]

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (range ⇑OrderEmbedding.withBotCoe).OrdConnected

Tactic:
simp [WithBot.range_coe, ordConnected_Ioi]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertManyIfNewUnit_nil :
    insertManyIfNewUnit m [] = m

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
⊢ (insertManyIfNewUnit m []).val = m

Tactic:
simp [insertManyIfNewUnit, Id.run]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem castSucc_pos_iff [NeZero n] {i : Fin n} : 0 < castSucc i ↔ 0 < i

Proof state:
n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ 0 < i.castSucc ↔ 0 < i

Tactic:
simp [← val_pos_iff]

Result:
no goals