harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProd_eq_tsum_compProd (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ)
    [IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) :
    (κ ⊗ₖ η) a s = ∑' (n : ℕ) (m : ℕ), (seq κ n ⊗ₖ seq η m) a s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ κ.compProdFun η a s = ∑' (n : ℕ) (m : ℕ), (κ.seq n).compProdFun (η.seq m) a s

Tactic:
exact compProdFun_eq_tsum κ η a hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = ∑' (n : ℕ) (m : ℕ), ((κ.seq n ⊗ₖ η.seq m) a) s

Tactic:
simp_rw [compProd_apply_eq_compProdFun _ _ _ hs]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ κ.compProdFun η a s = ∑' (n : ℕ) (m : ℕ), (κ.seq n).compProdFun (η.seq m) a s
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem add_tsub_add_le_tsub_right : a + c - (b + c) ≤ a - b

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + c - (b + c) ≤ a - b

Tactic:
rw [tsub_le_iff_left, add_right_comm]

Result:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + c ≤ b + (a - b) + c

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + c ≤ b + (a - b) + c

Tactic:
exact add_le_add_right le_add_tsub c

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem removePos_addPos_cancel {assignment : Assignment} (h : ¬(hasPosAssignment assignment)) :
  removePosAssignment (addPosAssignment assignment) = assignment

Proof state:
assignment : Assignment
h : ¬assignment.hasPosAssignment = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment

Tactic:
cases assignment <;> simp_all [removePosAssignment, addPosAssignment, hasPosAssignment]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem semiconj_of_isUnit_of_translationNumber_eq {f₁ f₂ : CircleDeg1Lift} (h₁ : IsUnit f₁)
    (h₂ : IsUnit f₂) (h : τ f₁ = τ f₂) : ∃ F : CircleDeg1Lift, Semiconj F f₁ f₂

Proof state:
case intro.intro
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
⊢ ∃ F, Semiconj ⇑F ⇑↑f₁ ⇑↑f₂

Tactic:
exact units_semiconj_of_translationNumber_eq h

Result:
no goals

Proof state:
f₁ f₂ : CircleDeg1Lift
h₁ : IsUnit f₁
h₂ : IsUnit f₂
h : τ f₁ = τ f₂
⊢ ∃ F, Semiconj ⇑F ⇑f₁ ⇑f₂

Tactic:
rcases h₁, h₂ with ⟨⟨f₁, rfl⟩, ⟨f₂, rfl⟩⟩

Result:
case intro.intro
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
⊢ ∃ F, Semiconj ⇑F ⇑↑f₁ ⇑↑f₂
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} : getKey? a (insertEntry k v l) = if k == a then some k else getKey? a l

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = true
⊢ (if true = true ∧ (k == a) = true then some k else getKey? a l) = if (k == a) = true then some k else getKey? a l

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = false
⊢ getKey? a (insertEntry k v l) = if (k == a) = true then some k else getKey? a l

Tactic:
simp [insertEntry_of_containsKey_eq_false hl]

Result:
no goals

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = true
⊢ getKey? a (insertEntry k v l) = if (k == a) = true then some k else getKey? a l

Tactic:
rw [insertEntry_of_containsKey hl, getKey?_replaceEntry, hl]

Result:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = true
⊢ (if true = true ∧ (k == a) = true then some k else getKey? a l) = if (k == a) = true then some k else getKey? a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ getKey? a (insertEntry k v l) = if (k == a) = true then some k else getKey? a l

Tactic:
cases hl : containsKey k l

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = false
⊢ getKey? a (insertEntry k v l) = if (k == a) = true then some k else getKey? a l

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = true
⊢ getKey? a (insertEntry k v l) = if (k == a) = true then some k else getKey? a l
-- Mathlib/Data/Erased.lean
theorem map_out {α β} {f : α → β} (a : Erased α) : (a.map f).out = f a.out

Proof state:
α : Sort u_1
β : Sort u_2
f : α → β
a : Erased α
⊢ (map f a).out = f a.out

Tactic:
simp [map]

Result:
no goals
-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_atTop (hff' : ∀ᶠ x in atTop, HasDerivAt f (f' x) x)
    (hgg' : ∀ᶠ x in atTop, HasDerivAt g (g' x) x) (hg' : ∀ᶠ x in atTop, g' x ≠ 0)
    (hftop : Tendsto f atTop (𝓝 0)) (hgtop : Tendsto g atTop (𝓝 0))
    (hdiv : Tendsto (fun x => f' x / g' x) atTop l) : Tendsto (fun x => f x / g x) atTop l

Proof state:
case intro.intro.intro.intro
l : Filter ℝ
f f' g g' : ℝ → ℝ
hg' : ∃ v ∈ atTop, ∀ y ∈ v, g' y ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
⊢ Tendsto (fun x => f x / g x) atTop l

Tactic:
rcases hg' with ⟨s₃, hs₃, hg'⟩

Result:
case intro.intro.intro.intro.intro.intro
l : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ y ∈ s₃, g' y ≠ 0
⊢ Tendsto (fun x => f x / g x) atTop l

Proof state:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∃ v ∈ atTop, ∀ y ∈ v, HasDerivAt f (f' y) y
hgg' : ∃ v ∈ atTop, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ atTop, ∀ y ∈ v, g' y ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
⊢ Tendsto (fun x => f x / g x) atTop l

Tactic:
rcases hff' with ⟨s₁, hs₁, hff'⟩

Result:
case intro.intro
l : Filter ℝ
f f' g g' : ℝ → ℝ
hgg' : ∃ v ∈ atTop, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ atTop, ∀ y ∈ v, g' y ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
⊢ Tendsto (fun x => f x / g x) atTop l

Proof state:
case intro.intro.intro.intro.intro.intro.intro.refine_1.a
l✝ : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l✝
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ b ≥ l, b ∈ s
hl' : Ioi l ⊆ s
x : ℝ
hx : x ∈ Ioi l
⊢ x ∈ s₁

Tactic:
exact (hl' hx).1.1

Result:
no goals

Proof state:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atTop, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
⊢ Tendsto (fun x => f x / g x) atTop l

Tactic:
rw [eventually_iff_exists_mem] at *

Result:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∃ v ∈ atTop, ∀ y ∈ v, HasDerivAt f (f' y) y
hgg' : ∃ v ∈ atTop, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ atTop, ∀ y ∈ v, g' y ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
⊢ Tendsto (fun x => f x / g x) atTop l
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobject_comp_le {X' : C} (h : X' ⟶ X) (f : X ⟶ Y) [HasImage f] [HasImage (h ≫ f)] :
    imageSubobject (h ≫ f) ≤ imageSubobject f :=
  Subobject.mk_le_mk_of_comm (image.preComp h f) (by simp)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y X' : C
h : X' ⟶ X
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage (h ≫ f)
⊢ image.preComp h f ≫ image.ι f = image.ι (h ≫ f)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem uniformity_eq_comap_inv_mul_nhds_one :
    𝓤 α = comap (fun x : α × α => x.1⁻¹ * x.2) (𝓝 (1 : α))

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ comap (unop ∘ (fun x => x.2 / x.1) ∘ fun p => (op p.1, op p.2)) (𝓝 1) = comap (fun x => x.1⁻¹ * x.2) (𝓝 1)

Tactic:
simp [Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ 𝓤 α = comap (fun x => x.1⁻¹ * x.2) (𝓝 1)

Tactic:
rw [← comap_uniformity_mulOpposite, uniformity_eq_comap_nhds_one, ← op_one, ← comap_unop_nhds,
  comap_comap, comap_comap]

Result:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ comap (unop ∘ (fun x => x.2 / x.1) ∘ fun p => (op p.1, op p.2)) (𝓝 1) = comap (fun x => x.1⁻¹ * x.2) (𝓝 1)
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContinuousLinearEquiv.iteratedFDerivWithin_comp_right (g : G ≃L[𝕜] E) (f : E → F)
    (hs : UniqueDiffOn 𝕜 s) {x : G} (hx : g x ∈ s) (i : ℕ) :
    iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s) x =
      (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun _ => g

Proof state:
case succ.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G},
    g x ∈ s →
      iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
        (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x => ↑g
x : G
hx : g x ∈ s
m : Fin (i + 1) → G
this :
  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s)) (⇑g ⁻¹' s) x =
    fderivWithin 𝕜
      (⇑(ContinuousMultilinearMap.compContinuousLinearMapEquivL F fun _x => g) ∘ iteratedFDerivWithin 𝕜 i f s ∘ ⇑g)
      (⇑g ⁻¹' s) x
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s)) (⇑g ⁻¹' s) x) (m 0)) (tail m) =
    ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s (g x)) (g (m 0))) (tail fun i => g (m i))

Tactic:
rw [this, ContinuousLinearEquiv.comp_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx)]

Result:
case succ.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G},
    g x ∈ s →
      iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
        (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x => ↑g
x : G
hx : g x ∈ s
m : Fin (i + 1) → G
this :
  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s)) (⇑g ⁻¹' s) x =
    fderivWithin 𝕜
      (⇑(ContinuousMultilinearMap.compContinuousLinearMapEquivL F fun _x => g) ∘ iteratedFDerivWithin 𝕜 i f s ∘ ⇑g)
      (⇑g ⁻¹' s) x
⊢ (((↑(ContinuousMultilinearMap.compContinuousLinearMapEquivL F fun _x => g)).comp
          (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s ∘ ⇑g) (⇑g ⁻¹' s) x))
        (m 0))
      (tail m) =
    ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s (g x)) (g (m 0))) (tail fun i => g (m i))
-- Mathlib/CategoryTheory/Sites/PreservesSheafification.lean
@[reassoc (attr := simp)]
lemma sheafComposeIso_inv_fac :
    whiskerRight (toSheafify J P) F ≫ (sheafifyComposeIso J F P).inv =
      toSheafify J (P ⋙ F)

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝⁵ : Category.{u_4, u_1} A
inst✝⁴ : Category.{u_3, u_2} B
F : A ⥤ B
inst✝³ : HasWeakSheafify J A
inst✝² : HasWeakSheafify J B
inst✝¹ : J.HasSheafCompose F
inst✝ : J.PreservesSheafification F
P : Cᵒᵖ ⥤ A
⊢ whiskerRight (toSheafify J P) F ≫ (sheafifyComposeIso J F P).inv = toSheafify J (P ⋙ F)

Tactic:
rw [← sheafComposeIso_hom_fac, assoc, Iso.hom_inv_id, comp_id]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma toAffineLift_neg (P : W.Point) : (-P).toAffineLift = -P.toAffineLift

Proof state:
case mk.mk
F : Type u
inst✝ : Field F
W : Projective F
point✝ : PointClass F
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ (-mk hP).toAffineLift = -(mk hP).toAffineLift

Tactic:
exact toAffine_neg hP

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : W.Point
⊢ (-P).toAffineLift = -P.toAffineLift

Tactic:
rcases P with @⟨⟨_⟩, hP⟩

Result:
case mk.mk
F : Type u
inst✝ : Field F
W : Projective F
point✝ : PointClass F
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ (-mk hP).toAffineLift = -(mk hP).toAffineLift
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean
theorem tendsto_norm_tan_of_cos_eq_zero {x : ℂ} (hx : cos x = 0) :
    Tendsto (fun x => ‖tan x‖) (𝓝[≠] x) atTop

Proof state:
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0)
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop

Tactic:
exact continuous_sin.continuousWithinAt.norm.mul_atTop (norm_pos_iff.2 A)
  (tendsto_norm_nhdsNE_zero.comp B).inv_tendsto_nhdsGT_zero

Result:
no goals

Proof state:
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop

Tactic:
have B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0) :=
  hx ▸ (hasDerivAt_cos x).tendsto_punctured_nhds (neg_ne_zero.2 A)

Result:
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0)
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop

Proof state:
x : ℂ
hx : cos x = 0
⊢ Tendsto (fun x => ‖tan x‖) (𝓝[≠] x) atTop

Tactic:
simp only [tan_eq_sin_div_cos, norm_div]

Result:
x : ℂ
hx : cos x = 0
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop

Proof state:
x : ℂ
hx : cos x = 0
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop

Tactic:
have A : sin x ≠ 0 := fun h => by simpa [*, sq] using sin_sq_add_cos_sq x

Result:
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop

Proof state:
x : ℂ
hx : cos x = 0
h : sin x = 0
⊢ False

Tactic:
simpa [*, sq] using sin_sq_add_cos_sq x

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem nat_eq_toNat {x : BitVec w} {y : Nat}
  : (y = x.toNat) ↔ (y < 2^w ∧ (x = BitVec.ofNat w y))

Proof state:
w : Nat
x : BitVec w
y : Nat
⊢ y = x.toNat ↔ y < 2 ^ w ∧ x = BitVec.ofNat w y

Tactic:
rw [@eq_comm _ _ x.toNat]

Result:
w : Nat
x : BitVec w
y : Nat
⊢ x.toNat = y ↔ y < 2 ^ w ∧ x = BitVec.ofNat w y

Proof state:
w : Nat
x : BitVec w
y : Nat
⊢ x.toNat = y ↔ y < 2 ^ w ∧ x = BitVec.ofNat w y

Tactic:
apply toNat_eq_nat

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem loopyOn_restrict (E R : Set α) : (loopyOn E) ↾ R = loopyOn R

Proof state:
α : Type u_1
E R : Set α
⊢ ∀ ⦃I : Set α⦄, I ⊆ R → I = ∅ → I ⊆ R

Tactic:
exact fun _ h _ ↦ h

Result:
no goals

Proof state:
α : Type u_1
E R : Set α
⊢ loopyOn E ↾ R = loopyOn R

Tactic:
refine ext_indep rfl ?_

Result:
α : Type u_1
E R : Set α
⊢ ∀ ⦃I : Set α⦄, I ⊆ (loopyOn E ↾ R).E → ((loopyOn E ↾ R).Indep I ↔ (loopyOn R).Indep I)

Proof state:
α : Type u_1
E R : Set α
⊢ ∀ ⦃I : Set α⦄, I ⊆ (loopyOn E ↾ R).E → ((loopyOn E ↾ R).Indep I ↔ (loopyOn R).Indep I)

Tactic:
simp only [restrict_ground_eq, restrict_indep_iff, loopyOn_indep_iff, and_iff_left_iff_imp]

Result:
α : Type u_1
E R : Set α
⊢ ∀ ⦃I : Set α⦄, I ⊆ R → I = ∅ → I ⊆ R
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma le_pushouts : P ≤ P.pushouts

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P ≤ P.pushouts

Tactic:
intro X Y p hp

Result:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
p : X ⟶ Y
hp : P p
⊢ P.pushouts p

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
p : X ⟶ Y
hp : P p
⊢ P.pushouts p

Tactic:
exact P.pushouts_mk IsPushout.of_id_fst hp

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem not_irreducible_C (x : R) : ¬Irreducible (C x)

Proof state:
R : Type u
inst✝ : Field R
x : R
⊢ ¬Irreducible (C x)

Tactic:
by_cases H : x = 0

Result:
case pos
R : Type u
inst✝ : Field R
x : R
H : x = 0
⊢ ¬Irreducible (C x)

case neg
R : Type u
inst✝ : Field R
x : R
H : ¬x = 0
⊢ ¬Irreducible (C x)

Proof state:
case pos
R : Type u
inst✝ : Field R
x : R
H : x = 0
⊢ ¬Irreducible 0

Tactic:
exact not_irreducible_zero

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Field R
x : R
H : ¬x = 0
⊢ ¬Irreducible (C x)

Tactic:
exact fun hx => Irreducible.not_unit hx <| isUnit_C.2 <| isUnit_iff_ne_zero.2 H

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Field R
x : R
H : x = 0
⊢ ¬Irreducible (C x)

Tactic:
rw [H, C_0]

Result:
case pos
R : Type u
inst✝ : Field R
x : R
H : x = 0
⊢ ¬Irreducible 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_eq_some_getKey [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l) :
    getKey? a l = some (getKey a l h)

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
a : α
h : containsKey a l = true
⊢ getKey? a l = some (getKey a l h)

Tactic:
simp [getKey]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_alter (h : m.1.WF) {k : α} {f : Option β → Option β} :
    (Const.alter m k f).1.size =
      if m.contains k && (f (Const.get? m k)).isNone then
        m.1.size - 1
      else if !m.contains k && (f (Const.get? m k)).isSome then
        m.1.size + 1
      else
        m.1.size

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
f : Option β → Option β
⊢ (alter m k f).val.size =
    if (m.contains k && (f (get? m k)).isNone) = true then m.val.size - 1
    else if (!m.contains k && (f (get? m k)).isSome) = true then m.val.size + 1 else m.val.size

Tactic:
simp_to_model [Const.alter] using List.Const.length_alterKey'

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem norm_fderiv_norm [Nontrivial E] (h : DifferentiableAt ℝ (‖·‖) x) :
    ‖fderiv ℝ (‖·‖) x‖ = 1

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
x : E
inst✝ : Nontrivial E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : x ≠ 0
⊢ 1 * ‖x‖ = (fderiv ℝ (fun x => ‖x‖) x) x

Tactic:
rw [one_mul, h.fderiv_norm_self]

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
x : E
inst✝ : Nontrivial E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : x ≠ 0
⊢ 1 ≤ ‖fderiv ℝ (fun x => ‖x‖) x‖

Tactic:
apply le_of_mul_le_mul_right _ (norm_pos_iff.2 this)

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
x : E
inst✝ : Nontrivial E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : x ≠ 0
⊢ 1 * ‖x‖ ≤ ‖fderiv ℝ (fun x => ‖x‖) x‖ * ‖x‖

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
x : E
inst✝ : Nontrivial E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ ‖fderiv ℝ (fun x => ‖x‖) x‖ = 1

Tactic:
have : x ≠ 0 := fun hx ↦ not_differentiableAt_norm_zero E (hx ▸ h)

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
x : E
inst✝ : Nontrivial E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : x ≠ 0
⊢ ‖fderiv ℝ (fun x => ‖x‖) x‖ = 1

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
x : E
inst✝ : Nontrivial E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : x ≠ 0
⊢ ‖fderiv ℝ (fun x => ‖x‖) x‖ = 1

Tactic:
refine le_antisymm (NNReal.coe_one ▸ norm_fderiv_le_of_lipschitz ℝ lipschitzWith_one_norm) ?_

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
x : E
inst✝ : Nontrivial E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : x ≠ 0
⊢ 1 ≤ ‖fderiv ℝ (fun x => ‖x‖) x‖
-- Mathlib/Topology/Sequences.lean
theorem FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto
    (h : ∀ (f : X → Prop) (a : X),
      (∀ u : ℕ → X, Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a) :
    FrechetUrysohnSpace X

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
⊢ FrechetUrysohnSpace X

Tactic:
refine ⟨fun s x hcx => ?_⟩

Result:
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
⊢ x ∈ seqClosure s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
⊢ x ∈ seqClosure s

Tactic:
by_cases hx : x ∈ s

Result:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : x ∈ s
⊢ x ∈ seqClosure s

case neg
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : x ∉ s
⊢ x ∈ seqClosure s

Proof state:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : x ∈ s
⊢ x ∈ seqClosure s

Tactic:
exact subset_seqClosure hx

Result:
no goals

Proof state:
case neg.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : x ∉ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφ : ∀ (n : ℕ), u (φ n) ∈ s
⊢ x ∈ seqClosure s

Tactic:
exact ⟨u ∘ φ, hφ, hux.comp φ_mono.tendsto_atTop⟩

Result:
no goals

Proof state:
case neg.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : x ∉ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
⊢ x ∈ seqClosure s

Tactic:
rcases extraction_of_frequently_atTop hus with ⟨φ, φ_mono, hφ⟩

Result:
case neg.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : x ∉ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφ : ∀ (n : ℕ), u (φ n) ∈ s
⊢ x ∈ seqClosure s