harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma appLE_eq_away_map {X Y : Scheme.{u}} (f : X ⟶ Y) {U : Y.Opens} (hU : IsAffineOpen U)
    {V : X.Opens} (hV : IsAffineOpen V) (e) (r : Γ(Y, U)) :
    letI := hU.isLocalization_basicOpen r
    letI := hV.isLocalization_basicOpen (f.appLE U V e r)
    f.appLE (Y.basicOpen r) (X.basicOpen (f.appLE U V e r)) (by simp [Scheme.Hom.appLE]) =
        CommRingCat.ofHom (IsLocalization.Away.map _ _ (f.appLE U V e).hom r)

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
⊢ Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯ =
    CommRingCat.ofHom
      (IsLocalization.Away.map (↑(Y.presheaf.toPrefunctor.1 (op (Y.basicOpen r))))
        (↑(X.presheaf.toPrefunctor.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)))))
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r)

Tactic:
letI := hU.isLocalization_basicOpen r

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
⊢ Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯ =
    CommRingCat.ofHom
      (IsLocalization.Away.map (↑(Y.presheaf.toPrefunctor.1 (op (Y.basicOpen r))))
        (↑(X.presheaf.toPrefunctor.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)))))
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r)
-- Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
theorem continuous_C [Semiring R] :
    Continuous (C σ R)

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
⊢ Tendsto (fun i => if d = 0 then i else 0) (nhds r) (nhds (if d = 0 then r else 0))

Tactic:
split_ifs

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
h✝ : d = 0
⊢ Tendsto (fun i => i) (nhds r) (nhds r)

case neg
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
h✝ : ¬d = 0
⊢ Tendsto (fun i => 0) (nhds r) (nhds 0)

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
⊢ ∀ (x : R), ContinuousAt (⇑(C σ R)) x

Tactic:
refine fun r ↦ (tendsto_iff_coeff_tendsto _ _ _).mpr fun d ↦ ?_

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
⊢ Tendsto (fun i => (coeff R d) ((C σ R) i)) (nhds r) (nhds ((coeff R d) ((C σ R) r)))

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
⊢ Tendsto (fun i => (coeff R d) ((C σ R) i)) (nhds r) (nhds ((coeff R d) ((C σ R) r)))

Tactic:
simp only [coeff_C]

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
⊢ Tendsto (fun i => if d = 0 then i else 0) (nhds r) (nhds (if d = 0 then r else 0))

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
h✝ : d = 0
⊢ Tendsto (fun i => i) (nhds r) (nhds r)

Tactic:
exact tendsto_id

Result:
no goals

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
h✝ : ¬d = 0
⊢ Tendsto (fun i => 0) (nhds r) (nhds 0)

Tactic:
exact tendsto_const_nhds

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
⊢ Continuous ⇑(C σ R)

Tactic:
simp only [continuous_iff_continuousAt]

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
⊢ ∀ (x : R), ContinuousAt (⇑(C σ R)) x
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
lemma cfcₙ_nnreal_eq_real {a : A} (f : ℝ≥0 → ℝ≥0) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : SMulCommClass ℝ A A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
f : ℝ≥0 → ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
⊢ cfcₙ f a = cfcₙ (fun x => ↑(f x.toNNReal)) a

Tactic:
replace ha : 0 ≤ a := ha

Result:
A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : SMulCommClass ℝ A A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
⊢ cfcₙ f a = cfcₙ (fun x => ↑(f x.toNNReal)) a

Proof state:
A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : SMulCommClass ℝ A A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
⊢ cfcₙ f a = cfcₙ (fun x => ↑(f x.toNNReal)) a

Tactic:
apply (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙ_eq_restrict _
  isUniformEmbedding_subtype_val ha (.of_nonneg ha)

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem add_succ : ∀ m n : PosNum, m + succ n = succ (m + n)
  | 1, b => by simp [one_add]
  | bit0 a, 1 => congr_arg bit0 (add_one a)
  | bit1 a, 1 => congr_arg bit1 (add_one a)
  | bit0 _, bit0 _ => rfl
  | bit0 a, bit1 b => congr_arg bit0 (add_succ a b)
  | bit1 _, bit0 _ => rfl
  | bit1 a, bit1 b => congr_arg bit1 (add_succ a b)

Proof state:
b : PosNum
⊢ 1 + b.succ = (1 + b).succ

Tactic:
simp [one_add]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem coeff_coe_trunc_of_lt {n m} {f : R⟦X⟧} (h : n < m) :
    coeff R n (trunc m f) = coeff R n f

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
h : n < m
⊢ (coeff R n) ↑(trunc m f) = (coeff R n) f

Tactic:
rwa [coeff_coe, coeff_trunc, if_pos]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean
lemma Exact.moduleCat_of_range_eq_ker {X₁ X₂ X₃ : ModuleCat.{v} R}
    (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (hfg : LinearMap.range f.hom = LinearMap.ker g.hom) :
    (moduleCatMkOfKerLERange f g (by rw [hfg])).Exact

Proof state:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
X₁ X₂ X₃ : ModuleCat R
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
hfg : LinearMap.range (ModuleCat.Hom.hom f) = LinearMap.ker (ModuleCat.Hom.hom g)
⊢ LinearMap.range (ModuleCat.Hom.hom f) ≤ LinearMap.ker (ModuleCat.Hom.hom g)

Tactic:
rw [hfg]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
X₁ X₂ X₃ : ModuleCat R
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
hfg : LinearMap.range (ModuleCat.Hom.hom f) = LinearMap.ker (ModuleCat.Hom.hom g)
⊢ (moduleCatMkOfKerLERange f g ⋯).Exact

Tactic:
simpa only [moduleCat_exact_iff_range_eq_ker] using hfg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mk_eq : Vector.mk a h = v ↔ a = v.toArray

Proof state:
α✝ : Type u_1
a : Array α✝
a✝ : Nat
h : a.size = a✝
v : Vector α✝ a✝
⊢ { toArray := a, size_toArray := h } = v ↔ a = v.toArray

Tactic:
cases v

Result:
case mk
α✝ : Type u_1
a : Array α✝
a✝ : Nat
h : a.size = a✝
toArray✝ : Array α✝
size_toArray✝ : toArray✝.size = a✝
⊢ { toArray := a, size_toArray := h } = { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    a = { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray

Proof state:
case mk
α✝ : Type u_1
a : Array α✝
a✝ : Nat
h : a.size = a✝
toArray✝ : Array α✝
size_toArray✝ : toArray✝.size = a✝
⊢ { toArray := a, size_toArray := h } = { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    a = { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem measurable_ereal_toReal : Measurable EReal.toReal :=
  EReal.measurable_of_measurable_real (by simpa using measurable_id)

Proof state:
⊢ Measurable fun p => (↑p).toReal

Tactic:
simpa using measurable_id

Result:
no goals
-- Mathlib/Analysis/Calculus/LogDeriv.lean
theorem logDeriv_div {f g : 𝕜 → 𝕜'} (x : 𝕜) (hf : f x ≠ 0) (hg : g x ≠ 0)
    (hdf : DifferentiableAt 𝕜 f x) (hdg : DifferentiableAt 𝕜 g x) :
    logDeriv (fun z => f z / g z) x = logDeriv f x - logDeriv g x

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
x : 𝕜
hf : f x ≠ 0
hg : g x ≠ 0
hdf : DifferentiableAt 𝕜 f x
hdg : DifferentiableAt 𝕜 g x
⊢ logDeriv (fun z => f z / g z) x = logDeriv f x - logDeriv g x

Tactic:
simp only [logDeriv_apply, deriv_div hdf hdg]

Result:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
x : 𝕜
hf : f x ≠ 0
hg : g x ≠ 0
hdf : DifferentiableAt 𝕜 f x
hdg : DifferentiableAt 𝕜 g x
⊢ deriv (fun z => f z / g z) x / (f x / g x) = deriv f x / f x - deriv g x / g x

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
x : 𝕜
hf : f x ≠ 0
hg : g x ≠ 0
hdf : DifferentiableAt 𝕜 f x
hdg : DifferentiableAt 𝕜 g x
⊢ f x * g x * (g x * (g x * deriv f x - f x * deriv g x)) = (g x * deriv f x - f x * deriv g x) * (f x * g x ^ 2)

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
x : 𝕜
hf : f x ≠ 0
hg : g x ≠ 0
hdf : DifferentiableAt 𝕜 f x
hdg : DifferentiableAt 𝕜 g x
⊢ deriv (fun z => f z / g z) x / (f x / g x) = deriv f x / f x - deriv g x / g x

Tactic:
field_simp [mul_comm]

Result:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
x : 𝕜
hf : f x ≠ 0
hg : g x ≠ 0
hdf : DifferentiableAt 𝕜 f x
hdg : DifferentiableAt 𝕜 g x
⊢ f x * g x * (g x * (g x * deriv f x - f x * deriv g x)) = (g x * deriv f x - f x * deriv g x) * (f x * g x ^ 2)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem add_both_eq_both (b : Bool) : addAssignment b both = both

Proof state:
b : Bool
⊢ (if b = true then addPosAssignment else addNegAssignment) both = both

Tactic:
split <;> decide

Result:
no goals

Proof state:
b : Bool
⊢ addAssignment b both = both

Tactic:
rw [addAssignment]

Result:
b : Bool
⊢ (if b = true then addPosAssignment else addNegAssignment) both = both
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma even_sub' : Even (m - n) ↔ (Odd m ↔ Odd n)

Proof state:
m n : ℤ
⊢ Even (m - n) ↔ (Odd m ↔ Odd n)

Tactic:
rw [even_sub, ← not_odd_iff_even, ← not_odd_iff_even, not_iff_not]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem thickening_ball [PseudoMetricSpace α] (x : α) (ε δ : ℝ) :
    thickening ε (ball x δ) ⊆ ball x (ε + δ)

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε δ : ℝ
⊢ thickening ε (thickening δ {x}) ⊆ thickening (ε + δ) {x}

Tactic:
apply thickening_thickening_subset

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε δ : ℝ
⊢ thickening ε (ball x δ) ⊆ ball x (ε + δ)

Tactic:
rw [← thickening_singleton, ← thickening_singleton]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε δ : ℝ
⊢ thickening ε (thickening δ {x}) ⊆ thickening (ε + δ) {x}
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_modify (h : m.1.WF) {k : α} {f : β → β} :
    (Const.modify m k f).1.size = 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 : β → β
⊢ (modify m k f).val.size = m.val.size

Tactic:
simp_to_model [Const.modify] using List.Const.length_modifyKey

Result:
no goals
-- Mathlib/Order/Filter/Cofinite.lean
theorem univ_pi_mem_pi {α : ι → Type*} {s : ∀ i, Set (α i)} {l : ∀ i, Filter (α i)}
    (h : ∀ i, s i ∈ l i) (hfin : ∀ᶠ i in cofinite, s i = univ) : univ.pi s ∈ pi l

Proof state:
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ {x | s x = univ}ᶜ.pi s
i : ι
a✝ : i ∈ univ
hi : ¬s i = univ
⊢ a i ∈ s i

Tactic:
exact ha i hi

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
⊢ univ.pi s ∈ pi l

Tactic:
filter_upwards [pi_mem_pi hfin fun i _ ↦ h i] with a ha i _

Result:
case h
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ {x | s x = univ}ᶜ.pi s
i : ι
a✝ : i ∈ univ
⊢ a i ∈ s i

Proof state:
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ {x | s x = univ}ᶜ.pi s
i : ι
a✝ : i ∈ univ
hi : s i = univ
⊢ a i ∈ s i

Tactic:
simp [hi]

Result:
no goals

Proof state:
case h
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ {x | s x = univ}ᶜ.pi s
i : ι
a✝ : i ∈ univ
⊢ a i ∈ s i

Tactic:
if hi : s i = univ then
  simp [hi]
else
  exact ha i hi

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Univ.lean
@[simp]
lemma univ_map_eval₂Hom (M : n × n → S) :
    (univ R n).map (eval₂Hom f M) = charpoly (Matrix.of M.curry)

Proof state:
R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
M : n × n → S
⊢ ((mvPolynomialX n n R).map (eval₂ f M)).charpoly =
    ((mvPolynomialX n n R).map (eval₂ f fun p => of (Function.curry M) p.1 p.2)).charpoly

Tactic:
simp only [of_apply, Function.curry_apply, Prod.mk.eta]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
M : n × n → S
⊢ Polynomial.map (eval₂Hom f M) (univ R n) = (of (Function.curry M)).charpoly

Tactic:
rw [univ, ← charpoly_map, coe_eval₂Hom, ← mvPolynomialX_map_eval₂ f (Matrix.of M.curry)]

Result:
R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
M : n × n → S
⊢ ((mvPolynomialX n n R).map (eval₂ f M)).charpoly =
    ((mvPolynomialX n n R).map (eval₂ f fun p => of (Function.curry M) p.1 p.2)).charpoly
-- Mathlib/Topology/Order/IsLUB.lean
theorem IsLUB.exists_seq_strictMono_tendsto_of_not_mem {t : Set α} {x : α}
    [IsCountablyGenerated (𝓝 x)] (htx : IsLUB t x) (not_mem : x ∉ t) (ht : t.Nonempty) :
    ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t

Proof state:
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
not_mem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
choose N hN hvN using fun k => ((eventually_gt_atTop k).and (this k)).exists

Result:
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
not_mem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Proof state:
case intro.intro.refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
not_mem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ N^[x✝] 0 < N (N^[x✝] 0)

Tactic:
exact hN _

Result:
no goals
-- Mathlib/Topology/AlexandrovDiscrete.lean
lemma Topology.IsInducing.alexandrovDiscrete [AlexandrovDiscrete α] {f : β → α} (h : IsInducing f) :
    AlexandrovDiscrete β where
  isOpen_sInter S hS

Proof state:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
U : (s : Set β) → s ∈ S → Set α
hU : ∀ (s : Set β) (a : s ∈ S), IsOpen (U s a)
htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s
⊢ f ⁻¹' ⋂ i, ⋂ (j : i ∈ S), U i j = ⋂₀ S

Tactic:
simp_rw [preimage_iInter, htU, sInter_eq_biInter]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
U : (s : Set β) → s ∈ S → Set α
hU : ∀ (s : Set β) (a : s ∈ S), IsOpen (U s a)
htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s
⊢ ∃ t, IsOpen t ∧ f ⁻¹' t = ⋂₀ S

Tactic:
refine ⟨_, isOpen_iInter₂ hU, ?_⟩

Result:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
U : (s : Set β) → s ∈ S → Set α
hU : ∀ (s : Set β) (a : s ∈ S), IsOpen (U s a)
htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s
⊢ f ⁻¹' ⋂ i, ⋂ (j : i ∈ S), U i j = ⋂₀ S

Proof state:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen s
⊢ IsOpen (⋂₀ S)

Tactic:
simp_rw [h.isOpen_iff] at hS ⊢

Result:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
hS : ∀ s ∈ S, ∃ t, IsOpen t ∧ f ⁻¹' t = s
⊢ ∃ t, IsOpen t ∧ f ⁻¹' t = ⋂₀ S

Proof state:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
hS : ∀ s ∈ S, ∃ t, IsOpen t ∧ f ⁻¹' t = s
⊢ ∃ t, IsOpen t ∧ f ⁻¹' t = ⋂₀ S

Tactic:
choose U hU htU using hS

Result:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
U : (s : Set β) → s ∈ S → Set α
hU : ∀ (s : Set β) (a : s ∈ S), IsOpen (U s a)
htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s
⊢ ∃ t, IsOpen t ∧ f ⁻¹' t = ⋂₀ S
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem map_zip_eq_zipWith (f : α × β → γ) (l : List α) (l' : List β) :
    map f (l.zip l') = zipWith (Function.curry f) l l'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
l : List α
l' : List β
⊢ map f (l.zip l') = zipWith (Function.curry f) l l'

Tactic:
rw [zip]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
l : List α
l' : List β
⊢ map f (zipWith Prod.mk l l') = zipWith (Function.curry f) l l'

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
l' : List β
⊢ map f (zipWith Prod.mk [] l') = zipWith (Function.curry f) [] l'

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
hl : α
tl : List α
ih : ∀ (l' : List β), map f (zipWith Prod.mk tl l') = zipWith (Function.curry f) tl l'
l' : List β
⊢ map f (zipWith Prod.mk (hl :: tl) l') = zipWith (Function.curry f) (hl :: tl) l'

Tactic:
cases l' <;> simp [ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
l : List α
l' : List β
⊢ map f (zipWith Prod.mk l l') = zipWith (Function.curry f) l l'

Tactic:
induction l generalizing l' with
| nil => simp
| cons hl tl ih =>
  cases l' <;> simp [ih]

Result:
no goals
-- Mathlib/Data/Set/Accumulate.lean
theorem disjoint_accumulate [Preorder α] (hs : Pairwise (Disjoint on s)) {i j : α} (hij : i < j) :
    Disjoint (Accumulate s i) (s j)

Proof state:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
⊢ Disjoint (Accumulate s i) (s j)

Tactic:
apply disjoint_left.2 (fun x hx ↦ ?_)

Result:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
hx : x ∈ Accumulate s i
⊢ x ∉ s j

Proof state:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
hx : x ∈ Accumulate s i
⊢ x ∉ s j

Tactic:
simp only [Accumulate, mem_iUnion, exists_prop] at hx

Result:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
hx : ∃ i_1 ≤ i, x ∈ s i_1
⊢ x ∉ s j

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
k : α
hk : k ≤ i
hx : x ∈ s k
⊢ x ∉ s j

Tactic:
exact disjoint_left.1 (hs (hk.trans_lt hij).ne) hx

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
hx : ∃ i_1 ≤ i, x ∈ s i_1
⊢ x ∉ s j

Tactic:
rcases hx with ⟨k, hk, hx⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
k : α
hk : k ≤ i
hx : x ∈ s k
⊢ x ∉ s j
-- Mathlib/Logic/Unique.lean
theorem Unique.bijective {A B} [Unique A] [Unique B] {f : A → B} : Function.Bijective f

Proof state:
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.Bijective f

Tactic:
rw [Function.bijective_iff_has_inverse]

Result:
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f

Proof state:
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f

Tactic:
refine ⟨default, ?_, ?_⟩ <;> intro x <;> simp

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem support_mapRange_of_injective {e : M → N} (he0 : e 0 = 0) (f : ι →₀ M)
    (he : Function.Injective e) : (Finsupp.mapRange e he0 f).support = f.support

Proof state:
case h
ι : Type u_4
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he0 : e 0 = 0
f : ι →₀ M
he : Injective e
a✝ : ι
⊢ ¬e (f a✝) = 0 ↔ ¬f a✝ = 0

Tactic:
exact he.ne_iff' he0

Result:
no goals

Proof state:
case h
ι : Type u_4
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he0 : e 0 = 0
f : ι →₀ M
he : Injective e
a✝ : ι
⊢ a✝ ∈ (mapRange e he0 f).support ↔ a✝ ∈ f.support

Tactic:
simp only [Finsupp.mem_support_iff, Ne, Finsupp.mapRange_apply]

Result:
case h
ι : Type u_4
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he0 : e 0 = 0
f : ι →₀ M
he : Injective e
a✝ : ι
⊢ ¬e (f a✝) = 0 ↔ ¬f a✝ = 0

Proof state:
ι : Type u_4
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he0 : e 0 = 0
f : ι →₀ M
he : Injective e
⊢ (mapRange e he0 f).support = f.support

Tactic:
ext

Result:
case h
ι : Type u_4
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he0 : e 0 = 0
f : ι →₀ M
he : Injective e
a✝ : ι
⊢ a✝ ∈ (mapRange e he0 f).support ↔ a✝ ∈ f.support