harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.Tendsto.continuousAt_of_equicontinuousAt {l : Filter ι} [l.NeBot] {F : ι → X → α}
    {f : X → α} {x₀ : X} (h₁ : Tendsto F l (𝓝 f)) (h₂ : EquicontinuousAt F x₀) :
    ContinuousAt f x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
x₀ : X
h₁ : Tendsto F l (𝓝 f)
h₂ : EquicontinuousAt F x₀
⊢ ContinuousAt f x₀

Tactic:
rw [← continuousWithinAt_univ, ← equicontinuousWithinAt_univ, tendsto_pi_nhds] at *

Result:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
x₀ : X
h₁ : ∀ (x : X), Tendsto (fun i => F i x) l (𝓝 (f x))
h₂ : EquicontinuousWithinAt F univ x₀
⊢ ContinuousWithinAt f univ x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
x₀ : X
h₁ : ∀ (x : X), Tendsto (fun i => F i x) l (𝓝 (f x))
h₂ : EquicontinuousWithinAt F univ x₀
⊢ ContinuousWithinAt f univ x₀

Tactic:
exact continuousWithinAt_of_equicontinuousWithinAt (fun x _ ↦ h₁ x) (h₁ x₀) h₂

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem zero : IsBoundedLinearMap 𝕜 fun _ : E => (0 : F) :=
  (0 : E →ₗ[𝕜] F).isLinear.with_bound 0 <| by simp [le_refl]

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ ∀ (x : E), ‖0 x‖ ≤ 0 * ‖x‖

Tactic:
simp [le_refl]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem clusterPt_iff_not_disjoint {F : Filter X} :
    ClusterPt x F ↔ ¬Disjoint (𝓝 x) F

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
⊢ ClusterPt x F ↔ ¬Disjoint (𝓝 x) F

Tactic:
rw [disjoint_iff, ClusterPt, neBot_iff]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
@[simp] lemma toFinset_Icc (a b : α) [Fintype (Icc a b)] : (Icc a b).toFinset = Finset.Icc a b

Proof state:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Icc a b)
a✝ : α
⊢ a✝ ∈ (Icc a b).toFinset ↔ a✝ ∈ Finset.Icc a b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Icc a b)
⊢ (Icc a b).toFinset = Finset.Icc a b

Tactic:
ext

Result:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Icc a b)
a✝ : α
⊢ a✝ ∈ (Icc a b).toFinset ↔ a✝ ∈ Finset.Icc a b
-- Mathlib/CategoryTheory/LiftingProperties/Basic.lean
theorem of_arrow_iso_left {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'}
    (e : Arrow.mk i ≅ Arrow.mk i') (p : X ⟶ Y) [hip : HasLiftingProperty i p] :
    HasLiftingProperty i' p

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i' p

Tactic:
rw [Arrow.iso_w' e]

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
⊢ HasLiftingProperty (e.inv.left ≫ i ≫ e.hom.right) p

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
⊢ HasLiftingProperty (e.inv.left ≫ i ≫ e.hom.right) p

Tactic:
infer_instance

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem cocycle_fst_snd (i j k : 𝒰.J) :
    t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.fst _ _ ≫ pullback.snd _ _ =
      pullback.fst _ _ ≫ pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ t' 𝒰 f g i j k ≫
      t' 𝒰 f g j k i ≫
        t' 𝒰 f g k i j ≫
          pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)

Tactic:
simp only [t'_fst_snd, t'_snd_snd, t'_fst_fst_fst]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean
theorem pullbackLeftPullbackSndIso_inv_fst_snd :
    (pullbackLeftPullbackSndIso f g g').inv ≫ pullback.fst _ _ ≫ pullback.snd _ _ =
      pullback.snd _ _ ≫ g'

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst✝¹ : HasPullback f g
inst✝ : HasPullback (pullback.snd f g) g'
⊢ (pullbackLeftPullbackSndIso f g g').inv ≫ pullback.snd (pullback.snd f g) g' ≫ g' = pullback.snd f (g' ≫ g) ≫ g'

Tactic:
exact pullbackLeftPullbackSndIso_inv_snd_snd_assoc f g g' g'

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst✝¹ : HasPullback f g
inst✝ : HasPullback (pullback.snd f g) g'
⊢ (pullbackLeftPullbackSndIso f g g').inv ≫ pullback.fst (pullback.snd f g) g' ≫ pullback.snd f g =
    pullback.snd f (g' ≫ g) ≫ g'

Tactic:
rw [pullback.condition]

Result:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst✝¹ : HasPullback f g
inst✝ : HasPullback (pullback.snd f g) g'
⊢ (pullbackLeftPullbackSndIso f g g').inv ≫ pullback.snd (pullback.snd f g) g' ≫ g' = pullback.snd f (g' ≫ g) ≫ g'
-- Mathlib/Order/Interval/Finset/Box.lean
lemma box_succ_eq_sdiff (n : ℕ) :
    box (n + 1) = Icc (-n.succ : α) n.succ \ Icc (-n) n

Proof state:
α : Type u_1
inst✝² : OrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ Icc (-↑(n + 1)) ↑(n + 1) \ Icc (-↑n) ↑n = Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n

Tactic:
simp only [Nat.cast_add_one, Nat.succ_eq_add_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : OrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ box (n + 1) = Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n

Tactic:
rw [box, Icc_neg_mono.disjointed_add_one]

Result:
α : Type u_1
inst✝² : OrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ Icc (-↑(n + 1)) ↑(n + 1) \ Icc (-↑n) ↑n = Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem Squarefree.pow_dvd_of_pow_dvd [Monoid R] {x y : R} {n : ℕ}
    (hx : Squarefree y) (h : x ^ n ∣ y) : x ^ n ∣ x

Proof state:
R : Type u_1
inst✝ : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
⊢ x ^ n ∣ x

Tactic:
by_cases hu : IsUnit x

Result:
case pos
R : Type u_1
inst✝ : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
hu : IsUnit x
⊢ x ^ n ∣ x

case neg
R : Type u_1
inst✝ : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
hu : ¬IsUnit x
⊢ x ^ n ∣ x

Proof state:
case neg
R : Type u_1
inst✝ : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
hu : ¬IsUnit x
⊢ x ^ n ∣ x

Tactic:
rcases (hx.squarefree_of_dvd h).eq_zero_or_one_of_pow_of_not_isUnit hu with rfl | rfl <;> simp

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
hu : IsUnit x
⊢ x ^ n ∣ x

Tactic:
exact (hu.pow n).dvd

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem isCompact_range [CompactSpace X] {f : X → Y} (hf : Continuous f) : IsCompact (range f)

Proof state:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
hf : Continuous f
⊢ IsCompact (f '' univ)

Tactic:
exact isCompact_univ.image hf

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
hf : Continuous f
⊢ IsCompact (range f)

Tactic:
rw [← image_univ]

Result:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
hf : Continuous f
⊢ IsCompact (f '' univ)
-- Mathlib/NumberTheory/Cyclotomic/Three.lean
/-- We have that `η ^ 2 = -η - 1`. -/
lemma eta_sq : (η ^ 2 : 𝓞 K) = - η - 1

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ 0 < ↑3

Tactic:
decide

Result:
no goals

Proof state:
case h
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ ↑(↑η ^ 2 + ↑η + 1) = ↑0

Tactic:
simpa using hζ.isRoot_cyclotomic (by decide)

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ ↑η ^ 2 + ↑η + 1 = 0

Tactic:
ext

Result:
case h
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ ↑(↑η ^ 2 + ↑η + 1) = ↑0

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ ↑η ^ 2 = -↑η - 1

Tactic:
rw [← neg_add', ← add_eq_zero_iff_eq_neg, ← add_assoc]

Result:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ ↑η ^ 2 + ↑η + 1 = 0
-- Mathlib/Algebra/Module/Presentation/Finite.lean
lemma finitePresentation [Finite pres.G] [Finite pres.R] :
    Module.FinitePresentation A M :=
  Module.finitePresentation_of_surjective _ pres.surjective_π (by
    rw [pres.ker_π]
    exact Submodule.fg_span (Set.finite_range _))

Proof state:
A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
pres : Presentation A M
inst✝¹ : Finite pres.G
inst✝ : Finite pres.R
⊢ (Submodule.span A (Set.range pres.relation)).FG

Tactic:
exact Submodule.fg_span (Set.finite_range _)

Result:
no goals

Proof state:
A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
pres : Presentation A M
inst✝¹ : Finite pres.G
inst✝ : Finite pres.R
⊢ (LinearMap.ker pres.π).FG

Tactic:
rw [pres.ker_π]

Result:
A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
pres : Presentation A M
inst✝¹ : Finite pres.G
inst✝ : Finite pres.R
⊢ (Submodule.span A (Set.range pres.relation)).FG
-- Mathlib/RingTheory/RingHom/StandardSmooth.lean
lemma isStandardSmoothOfRelativeDimension_holdsForLocalizationAway :
    HoldsForLocalizationAway (IsStandardSmoothOfRelativeDimension.{0, 0} 0)

Proof state:
⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => IsStandardSmoothOfRelativeDimension 0

Tactic:
introv R h

Result:
R S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ IsStandardSmoothOfRelativeDimension 0 (algebraMap R S)

Proof state:
R S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ IsStandardSmoothOfRelativeDimension 0 (algebraMap R S)

Tactic:
exact IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway r

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
lemma toNerve₂.mk_naturality_δ0i (i : Fin 2) : toNerve₂.mk.naturalityProperty F (δ₂ i)

Proof state:
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
i : Fin 2
⊢ mk.naturalityProperty F (δ₂ i ⋯ ⋯)

Tactic:
ext x

Result:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
i : Fin 2
x : X.obj (op { obj := [0 + 1], property := ⋯ })
⊢ (X.map (δ₂ i ⋯ ⋯).op ≫ (fun n => mk.app F (unop n)) (op { obj := [0], property := ⋯ })) x =
    ((fun n => mk.app F (unop n)) (op { obj := [0 + 1], property := ⋯ }) ≫
        (nerveFunctor₂.obj (Cat.of C)).map (δ₂ i ⋯ ⋯).op)
      x

Proof state:
case h.h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
i : Fin 2
x : X.obj (op { obj := [0 + 1], property := ⋯ })
⊢ ComposableArrows.obj' ((X.map (δ₂ i ⋯ ⋯).op ≫ (fun n => mk.app F (unop n)) (op { obj := [0], property := ⋯ })) x) 0
      ⋯ =
    (((fun n => mk.app F (unop n)) (op { obj := [0 + 1], property := ⋯ }) ≫
            (nerveFunctor₂.obj (Cat.of C)).map (δ₂ i ⋯ ⋯).op)
          x).obj
      0

Tactic:
fin_cases i <;> rfl

Result:
no goals

Proof state:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
i : Fin 2
x : X.obj (op { obj := [0 + 1], property := ⋯ })
⊢ (X.map (δ₂ i ⋯ ⋯).op ≫ (fun n => mk.app F (unop n)) (op { obj := [0], property := ⋯ })) x =
    ((fun n => mk.app F (unop n)) (op { obj := [0 + 1], property := ⋯ }) ≫
        (nerveFunctor₂.obj (Cat.of C)).map (δ₂ i ⋯ ⋯).op)
      x

Tactic:
apply ComposableArrows.ext₀

Result:
case h.h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
i : Fin 2
x : X.obj (op { obj := [0 + 1], property := ⋯ })
⊢ ComposableArrows.obj' ((X.map (δ₂ i ⋯ ⋯).op ≫ (fun n => mk.app F (unop n)) (op { obj := [0], property := ⋯ })) x) 0
      ⋯ =
    (((fun n => mk.app F (unop n)) (op { obj := [0 + 1], property := ⋯ }) ≫
            (nerveFunctor₂.obj (Cat.of C)).map (δ₂ i ⋯ ⋯).op)
          x).obj
      0
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
lemma mk'_homEquiv (adj : CoreHomEquivUnitCounit F G) : (mk' adj).homEquiv = adj.homEquiv

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquivUnitCounit F G
⊢ (mk' adj).homEquiv = adj.homEquiv

Tactic:
ext

Result:
case h.h.H
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquivUnitCounit F G
x✝² : C
x✝¹ : D
x✝ : F.obj x✝² ⟶ x✝¹
⊢ ((mk' adj).homEquiv x✝² x✝¹) x✝ = (adj.homEquiv x✝² x✝¹) x✝

Proof state:
case h.h.H
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquivUnitCounit F G
x✝² : C
x✝¹ : D
x✝ : F.obj x✝² ⟶ x✝¹
⊢ ((mk' adj).homEquiv x✝² x✝¹) x✝ = (adj.homEquiv x✝² x✝¹) x✝

Tactic:
rw [homEquiv_unit, adj.homEquiv_unit, mk'_unit]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
@[simp]
lemma reflexiveCoforkEquivCofork_functor_obj_π (G : ReflexiveCofork F) :
    ((reflexiveCoforkEquivCofork F).functor.obj G).π = G.π

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ ((reflexiveCoforkEquivCofork F).functor.obj G).π = G.π

Tactic:
dsimp [reflexiveCoforkEquivCofork]

Result:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ ((Cocones.precompose (diagramIsoParallelPair (WalkingParallelPair.inclusionWalkingReflexivePair ⋙ F)).inv).obj
        (Cocone.whisker WalkingParallelPair.inclusionWalkingReflexivePair G)).π =
    G.π

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ ((Cocones.precompose (diagramIsoParallelPair (WalkingParallelPair.inclusionWalkingReflexivePair ⋙ F)).inv).obj
            (Cocone.whisker WalkingParallelPair.inclusionWalkingReflexivePair G)).ι.app
      WalkingParallelPair.one =
    G.ι.app zero

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ ((Cocones.precompose (diagramIsoParallelPair (WalkingParallelPair.inclusionWalkingReflexivePair ⋙ F)).inv).obj
        (Cocone.whisker WalkingParallelPair.inclusionWalkingReflexivePair G)).π =
    G.π

Tactic:
rw [ReflexiveCofork.π, Cofork.π]

Result:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ ((Cocones.precompose (diagramIsoParallelPair (WalkingParallelPair.inclusionWalkingReflexivePair ⋙ F)).inv).obj
            (Cocone.whisker WalkingParallelPair.inclusionWalkingReflexivePair G)).ι.app
      WalkingParallelPair.one =
    G.ι.app zero
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem hasFDerivAtFilter_const_add_iff (c : F) :
    HasFDerivAtFilter (c + f ·) f' x L ↔ HasFDerivAtFilter f f' x L

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
L : Filter E
c : F
⊢ HasFDerivAtFilter (fun x => c + f x) f' x L ↔ HasFDerivAtFilter f f' x L

Tactic:
simpa only [add_comm] using hasFDerivAtFilter_add_const_iff c

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
/-- Sanity check: `isoFunctorOfIsoInverse (isoInverseOfIsoFunctor i)` is just `i`. -/
@[simp]
lemma isoFunctorOfIsoInverse_isoInverseOfIsoFunctor {G G' : C ≌ D} (i : G.functor ≅ G'.functor) :
    isoFunctorOfIsoInverse (isoInverseOfIsoFunctor i) = i

Proof state:
case w.w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G G' : C ≌ D
i : G.functor ≅ G'.functor
X : C
⊢ i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse.hom.app X = i.hom.app X

Tactic:
simp [← NatTrans.naturality]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G G' : C ≌ D
i : G.functor ≅ G'.functor
⊢ i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse = i

Tactic:
ext X

Result:
case w.w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G G' : C ≌ D
i : G.functor ≅ G'.functor
X : C
⊢ i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse.hom.app X = i.hom.app X
-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma Opens.isDominant_homOfLE {U V : X.Opens} (hU : Dense (X := X) U) (hU' : U ≤ V) :
    IsDominant (X.homOfLE hU') :=
  have : IsDominant (X.homOfLE hU' ≫ Opens.ι _)

Proof state:
X : Scheme
U V : X.Opens
hU : Dense ↑U
hU' : U ≤ V
⊢ IsDominant (X.homOfLE hU' ≫ V.ι)

Tactic:
simpa using Opens.isDominant_ι hU

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem add (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a + c ≡ b + d [ZMOD n] :=
  modEq_iff_dvd.2 <| by convert Int.dvd_add h₁.dvd h₂.dvd using 1; omega

Proof state:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ n ∣ b + d - (a + c)

Tactic:
convert Int.dvd_add h₁.dvd h₂.dvd using 1

Result:
case h.e'_4
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ b + d - (a + c) = b - a + (d - c)

Proof state:
case h.e'_4
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ b + d - (a + c) = b - a + (d - c)

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem ae_le_set : s ≤ᵐ[μ] t ↔ μ (s \ t) = 0 :=
  calc
    s ≤ᵐ[μ] t ↔ ∀ᵐ x ∂μ, x ∈ s → x ∈ t := Iff.rfl
    _ ↔ μ (s \ t) = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ μ {a | a ∈ s ∧ a ∉ t} = 0 ↔ μ (s \ t) = 0

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → x ∈ t) ↔ μ (s \ t) = 0

Tactic:
simp [ae_iff]

Result:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ μ {a | a ∈ s ∧ a ∉ t} = 0 ↔ μ (s \ t) = 0
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem preimage_mul_left_one' : preimage 1 (a⁻¹ * ·) (mul_right_injective _).injOn = {a}

Proof state:
α : Type u_2
inst✝ : Group α
a : α
⊢ preimage 1 (fun x => a⁻¹ * x) ⋯ = {a}

Tactic:
rw [preimage_mul_left_one, inv_inv]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem idealSetEquiv_symm_apply
    (a : {a : integerSet K // (preimageOfMemIntegerSet a : 𝓞 K) ∈ (J : Set (𝓞 K)) }) :
    ((idealSetEquiv K J).symm a : mixedSpace K) = a

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : { a // ↑(preimageOfMemIntegerSet a) ∈ ↑↑J }
⊢ ↑((idealSetEquiv K J).symm a) = ↑↑a

Tactic:
rw [← (idealSetEquiv_apply ((idealSetEquiv K J).symm a)), Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma IsAffineOpen.fromSpec_preimage_zeroLocus {X : Scheme.{u}} {U : X.Opens}
    (hU : IsAffineOpen U) (s : Set Γ(X, U)) :
    hU.fromSpec.base ⁻¹' X.zeroLocus s = PrimeSpectrum.zeroLocus s

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' X.zeroLocus s = PrimeSpectrum.zeroLocus s

Tactic:
ext x

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↑↑(Spec Γ(X, U)).toPresheafedSpace
⊢ x ∈ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' X.zeroLocus s ↔ x ∈ PrimeSpectrum.zeroLocus s

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↑↑(Spec Γ(X, U)).toPresheafedSpace
⊢ x ∈ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' X.zeroLocus s ↔ x ∈ PrimeSpectrum.zeroLocus s

Tactic:
suffices (∀ f ∈ s, ¬¬ f ∈ x.asIdeal) ↔ s ⊆ x.asIdeal by
  simpa [← hU.fromSpec_image_basicOpen, -not_not] using this

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↑↑(Spec Γ(X, U)).toPresheafedSpace
⊢ (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ ↑x.asIdeal

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↑↑(Spec Γ(X, U)).toPresheafedSpace
⊢ (∀ f ∈ s, f ∈ x.asIdeal) ↔ s ⊆ ↑x.asIdeal

Tactic:
rfl

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↑↑(Spec Γ(X, U)).toPresheafedSpace
this : (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ ↑x.asIdeal
⊢ x ∈ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' X.zeroLocus s ↔ x ∈ PrimeSpectrum.zeroLocus s

Tactic:
simpa [← hU.fromSpec_image_basicOpen, -not_not] using this

Result:
no goals

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↑↑(Spec Γ(X, U)).toPresheafedSpace
⊢ (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ ↑x.asIdeal

Tactic:
simp_rw [not_not]

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↑↑(Spec Γ(X, U)).toPresheafedSpace
⊢ (∀ f ∈ s, f ∈ x.asIdeal) ↔ s ⊆ ↑x.asIdeal
-- Mathlib/Algebra/Module/Submodule/Invariant.lean
protected lemma disjoint_iff {p q : f.invtSubmodule} :
    Disjoint p q ↔ Disjoint (p : Submodule R M) (q : Submodule R M)

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
q : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ Disjoint ⟨p, hp⟩ q ↔ Disjoint ↑⟨p, hp⟩ ↑q

Tactic:
obtain ⟨q, hq⟩ := q

Result:
case mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ Disjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Disjoint ↑⟨p, hp⟩ ↑⟨q, hq⟩

Proof state:
case mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ Disjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Disjoint ↑⟨p, hp⟩ ↑⟨q, hq⟩

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : ↥f.invtSubmodule
⊢ Disjoint p q ↔ Disjoint ↑p ↑q

Tactic:
obtain ⟨p, hp⟩ := p

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
q : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ Disjoint ⟨p, hp⟩ q ↔ Disjoint ↑⟨p, hp⟩ ↑q