harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/ReesAlgebra.lean
theorem reesAlgebra.fg (hI : I.FG) : (reesAlgebra I).FG

Proof state:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Algebra.adjoin R ↑(Finset.image (⇑(monomial 1)) s) = Algebra.adjoin R ↑(Submodule.map (monomial 1) (Ideal.span ↑s))

Tactic:
rw [Finset.coe_image]

Result:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Algebra.adjoin R (⇑(monomial 1) '' ↑s) = Algebra.adjoin R ↑(Submodule.map (monomial 1) (Ideal.span ↑s))

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
hI : I.FG
⊢ (reesAlgebra I).FG

Tactic:
obtain ⟨s, hs⟩ := hI

Result:
case intro
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ (reesAlgebra I).FG

Proof state:
case intro
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ (Algebra.adjoin R ↑(Submodule.map (monomial 1) (Ideal.span ↑s))).FG

Tactic:
use s.image (monomial 1)

Result:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Algebra.adjoin R ↑(Finset.image (⇑(monomial 1)) s) = Algebra.adjoin R ↑(Submodule.map (monomial 1) (Ideal.span ↑s))

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
hI : I.FG
⊢ (reesAlgebra I).FG

Tactic:
classical
  obtain ⟨s, hs⟩ := hI
  rw [← adjoin_monomial_eq_reesAlgebra, ← hs]
  use s.image (monomial 1)
  rw [Finset.coe_image]
  change
    _ =
      Algebra.adjoin R
        (Submodule.map (monomial 1 : R →ₗ[R] R[X]) (Submodule.span R ↑s) : Set R[X])
  rw [Submodule.map_span, Algebra.adjoin_span]

Result:
no goals

Proof state:
case intro
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ (reesAlgebra I).FG

Tactic:
rw [← adjoin_monomial_eq_reesAlgebra, ← hs]

Result:
case intro
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ (Algebra.adjoin R ↑(Submodule.map (monomial 1) (Ideal.span ↑s))).FG

Proof state:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Algebra.adjoin R (⇑(monomial 1) '' ↑s) = Algebra.adjoin R ↑(Submodule.map (monomial 1) (Submodule.span R ↑s))

Tactic:
rw [Submodule.map_span, Algebra.adjoin_span]

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Algebra.adjoin R (⇑(monomial 1) '' ↑s) = Algebra.adjoin R ↑(Submodule.map (monomial 1) (Ideal.span ↑s))

Tactic:
change
  _ =
    Algebra.adjoin R
      (Submodule.map (monomial 1 : R →ₗ[R] R[X]) (Submodule.span R ↑s) : Set R[X])

Result:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Algebra.adjoin R (⇑(monomial 1) '' ↑s) = Algebra.adjoin R ↑(Submodule.map (monomial 1) (Submodule.span R ↑s))
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.sup (hf : ωScottContinuous f) (hg : ωScottContinuous g) :
    ωScottContinuous (f ⊔ g)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous (SupSet.sSup {f, g})

Tactic:
apply ωScottContinuous.sSup

Result:
case hs
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ∀ f_1 ∈ {f, g}, ωScottContinuous f_1

Proof state:
case hs
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ∀ f_1 ∈ {f, g}, ωScottContinuous f_1

Tactic:
rintro f (rfl | rfl | _) <;> assumption

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous (f ⊔ g)

Tactic:
rw [← sSup_pair]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous (SupSet.sSup {f, g})
-- Mathlib/NumberTheory/SumPrimeReciprocals.lean
theorem Nat.Primes.summable_rpow {r : ℝ} :
    Summable (fun p : Nat.Primes ↦ (p : ℝ) ^ r) ↔ r < -1

Proof state:
case neg
r : ℝ
h : ¬r < -1
H : Summable fun p => ↑↑p ^ r
p : Primes
⊢ 1 / ↑↑p ≤ ↑↑p ^ r

Tactic:
rw [one_div, ← Real.rpow_neg_one]

Result:
case neg
r : ℝ
h : ¬r < -1
H : Summable fun p => ↑↑p ^ r
p : Primes
⊢ ↑↑p ^ (-1) ≤ ↑↑p ^ r

Proof state:
case neg
r : ℝ
h : ¬r < -1
H : Summable fun p => ↑↑p ^ r
⊢ ∀ (b : Primes), 1 / ↑↑b ≤ ↑↑b ^ r

Tactic:
intro p

Result:
case neg
r : ℝ
h : ¬r < -1
H : Summable fun p => ↑↑p ^ r
p : Primes
⊢ 1 / ↑↑p ≤ ↑↑p ^ r

Proof state:
case neg
r : ℝ
h : ¬r < -1
⊢ ¬Summable fun p => ↑↑p ^ r

Tactic:
refine fun H ↦ Nat.Primes.not_summable_one_div <| H.of_nonneg_of_le (fun _ ↦ by positivity) ?_

Result:
case neg
r : ℝ
h : ¬r < -1
H : Summable fun p => ↑↑p ^ r
⊢ ∀ (b : Primes), 1 / ↑↑b ≤ ↑↑b ^ r

Proof state:
case pos
r : ℝ
h : r < -1
⊢ (Summable fun p => ↑↑p ^ r) ↔ r < -1

Tactic:
simp only [h, iff_true]

Result:
case pos
r : ℝ
h : r < -1
⊢ Summable fun p => ↑↑p ^ r

Proof state:
r : ℝ
h : ¬r < -1
H : Summable fun p => ↑↑p ^ r
x✝ : Primes
⊢ 0 ≤ 1 / ↑↑x✝

Tactic:
positivity

Result:
no goals

Proof state:
r : ℝ
h : ¬r < -1
H : Summable fun p => ↑↑p ^ r
p : Primes
⊢ 1 ≤ ↑↑p

Tactic:
exact_mod_cast p.prop.one_lt.le

Result:
no goals

Proof state:
case neg
r : ℝ
h : ¬r < -1
⊢ (Summable fun p => ↑↑p ^ r) ↔ r < -1

Tactic:
simp only [h, iff_false]

Result:
case neg
r : ℝ
h : ¬r < -1
⊢ ¬Summable fun p => ↑↑p ^ r

Proof state:
case neg
r : ℝ
h : ¬r < -1
H : Summable fun p => ↑↑p ^ r
p : Primes
⊢ ↑↑p ^ (-1) ≤ ↑↑p ^ r

Tactic:
exact Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast p.prop.one_lt.le) <| not_lt.mp h

Result:
no goals

Proof state:
r : ℝ
⊢ (Summable fun p => ↑↑p ^ r) ↔ r < -1

Tactic:
by_cases h : r < -1

Result:
case pos
r : ℝ
h : r < -1
⊢ (Summable fun p => ↑↑p ^ r) ↔ r < -1

case neg
r : ℝ
h : ¬r < -1
⊢ (Summable fun p => ↑↑p ^ r) ↔ r < -1

Proof state:
case pos
r : ℝ
h : r < -1
⊢ Summable fun p => ↑↑p ^ r

Tactic:
exact (Real.summable_nat_rpow.mpr h).subtype _

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
theorem AEMeasurable.ae_eq_of_forall_setLIntegral_eq {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
    (hg : AEMeasurable g μ) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) (hgi : ∫⁻ x, g x ∂μ ≠ ∞)
    (hfg : ∀ ⦃s⦄, MeasurableSet s → μ s < ∞ → ∫⁻ x in s, f x ∂μ = ∫⁻ x in s, g x ∂μ) :
    f =ᵐ[μ] g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : SigmaFinite (μ.restrict hf'.sigmaFiniteSet)
⊢ f =ᶠ[ae (μ.restrict (s ∪ t))] g

Tactic:
have := hg'.sigmaFinite_restrict

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this✝ : SigmaFinite (μ.restrict hf'.sigmaFiniteSet)
this : SigmaFinite (μ.restrict hg'.sigmaFiniteSet)
⊢ f =ᶠ[ae (μ.restrict (s ∪ t))] g
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem isTheta_bot : f =Θ[⊥] g

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
⊢ f =Θ[⊥] g

Tactic:
simp [IsTheta]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive]
lemma norm_div_eq_norm_left (x : E) {y : E} (h : ‖y‖ = 0) : ‖x / y‖ = ‖x‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x‖ ≤ ‖x / y‖

Tactic:
simpa [h] using norm_sub_norm_le' x y

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x / y‖ = ‖x‖

Tactic:
apply le_antisymm ?_ ?_

Result:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x / y‖ ≤ ‖x‖

E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x‖ ≤ ‖x / y‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x / y‖ ≤ ‖x‖

Tactic:
simpa [h] using norm_div_le x y

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
    (l : List α) (f : (a : α) → a ∈ l → β → β) (init : β) :
    forIn' l init (fun a m b => pure (.yield (f a m b))) =
      pure (f := m) (l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (a : α) → a ∈ l → β → β
init : β
l' : List { x // x ∈ l }
⊢ ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => pure (ForInStep.yield (f x.val ⋯ b))
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l' =
    pure (foldl (fun b x => f x.val ⋯ b) init l')

Tactic:
induction l' generalizing init <;> simp_all

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (a : α) → a ∈ l → β → β
init : β
⊢ ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => pure (ForInStep.yield (f x.val ⋯ b))
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l.attach =
    pure (foldl (fun b x => f x.val ⋯ b) init l.attach)

Tactic:
generalize l.attach = l'

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (a : α) → a ∈ l → β → β
init : β
l' : List { x // x ∈ l }
⊢ ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => pure (ForInStep.yield (f x.val ⋯ b))
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l' =
    pure (foldl (fun b x => f x.val ⋯ b) init l')

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (a : α) → a ∈ l → β → β
init : β
⊢ (forIn' l init fun a m_1 b => pure (ForInStep.yield (f a m_1 b))) =
    pure
      (foldl
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f a h b)
        init l.attach)

Tactic:
simp only [forIn'_eq_foldlM]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (a : α) → a ∈ l → β → β
init : β
⊢ ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => pure (ForInStep.yield (f x.val ⋯ b))
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l.attach =
    pure (foldl (fun b x => f x.val ⋯ b) init l.attach)
-- Mathlib/Data/Set/Function.lean
theorem MapsTo.iterate_restrict {f : α → α} {s : Set α} (h : MapsTo f s s) (n : ℕ) :
    (h.restrict f s s)^[n] = (h.iterate n).restrict _ _ _

Proof state:
case h.zero
α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
x : ↑s
⊢ ↑((restrict f s s h)^[0] x) = f^[0] ↑x

Tactic:
rfl

Result:
no goals

Proof state:
case h
α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
x : ↑s
⊢ (restrict f s s h)^[n] x = restrict f^[n] s s ⋯ x

Tactic:
rw [Subtype.ext_iff, MapsTo.val_restrict_apply]

Result:
case h
α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
x : ↑s
⊢ ↑((restrict f s s h)^[n] x) = f^[n] ↑x

Proof state:
case h.succ
α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
ihn : ∀ (x : ↑s), ↑((restrict f s s h)^[n] x) = f^[n] ↑x
x : ↑s
⊢ ↑((restrict f s s h)^[n + 1] x) = f^[n + 1] ↑x

Tactic:
simp [Nat.iterate, ihn]

Result:
no goals

Proof state:
case h
α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
x : ↑s
⊢ ↑((restrict f s s h)^[n] x) = f^[n] ↑x

Tactic:
induction n generalizing x with
| zero => rfl
| succ n ihn => simp [Nat.iterate, ihn]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
⊢ (restrict f s s h)^[n] = restrict f^[n] s s ⋯

Tactic:
funext x

Result:
case h
α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
x : ↑s
⊢ (restrict f s s h)^[n] x = restrict f^[n] s s ⋯ x
-- Mathlib/Topology/UniformSpace/CompactConvergence.lean
theorem tendsto_of_tendstoLocallyUniformly (h : TendstoLocallyUniformly (fun i a => F i a) f p) :
    Tendsto F p (𝓝 f)

Proof state:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p
⊢ Tendsto F p (𝓝 f)

Tactic:
rw [tendsto_iff_forall_isCompact_tendstoUniformlyOn]

Result:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p
⊢ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K

Proof state:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p
K : Set α
hK : IsCompact K
⊢ TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K

Tactic:
rw [← tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK]

Result:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p
K : Set α
hK : IsCompact K
⊢ TendstoLocallyUniformlyOn (fun i a => (F i) a) (⇑f) p K

Proof state:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p
⊢ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K

Tactic:
intro K hK

Result:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p
K : Set α
hK : IsCompact K
⊢ TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K

Proof state:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p
K : Set α
hK : IsCompact K
⊢ TendstoLocallyUniformlyOn (fun i a => (F i) a) (⇑f) p K

Tactic:
exact h.tendstoLocallyUniformlyOn

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_div_pos_iff : 0 < ‖a / b‖ ↔ a ≠ b

Proof state:
E : Type u_5
inst✝ : NormedGroup E
a b : E
⊢ ‖a / b‖ ≠ 0 ↔ a ≠ b

Tactic:
exact norm_div_eq_zero_iff.not

Result:
no goals

Proof state:
E : Type u_5
inst✝ : NormedGroup E
a b : E
⊢ 0 < ‖a / b‖ ↔ a ≠ b

Tactic:
rw [(norm_nonneg' _).lt_iff_ne, ne_comm]

Result:
E : Type u_5
inst✝ : NormedGroup E
a b : E
⊢ ‖a / b‖ ≠ 0 ↔ a ≠ b
-- Mathlib/AlgebraicTopology/Quasicategory/Basic.lean
lemma Quasicategory.hornFilling {S : SSet} [Quasicategory S] ⦃n : ℕ⦄ ⦃i : Fin (n+1)⦄
    (h0 : 0 < i) (hn : i < Fin.last n)
    (σ₀ : Λ[n, i] ⟶ S) : ∃ σ : Δ[n] ⟶ S, σ₀ = hornInclusion n i ≫ σ

Proof state:
S : SSet
inst✝ : S.Quasicategory
n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
σ₀ : Λ[n, i] ⟶ S
⊢ ∃ σ, σ₀ = hornInclusion n i ≫ σ

Tactic:
cases n using Nat.casesAuxOn with
| zero => simp [Fin.lt_iff_val_lt_val] at hn
| succ n =>
cases n using Nat.casesAuxOn with
| zero =>
  simp only [Fin.lt_iff_val_lt_val, Fin.val_zero, Fin.val_last, zero_add, Nat.lt_one_iff] at h0 hn
  simp [hn] at h0
| succ n => exact Quasicategory.hornFilling' σ₀ h0 hn

Result:
no goals

Proof state:
case succ.zero
S : SSet
inst✝ : S.Quasicategory
i : Fin (0 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (0 + 1)
σ₀ : Λ[0 + 1, i] ⟶ S
⊢ ∃ σ, σ₀ = hornInclusion (0 + 1) i ≫ σ

Tactic:
simp only [Fin.lt_iff_val_lt_val, Fin.val_zero, Fin.val_last, zero_add, Nat.lt_one_iff] at h0 hn

Result:
case succ.zero
S : SSet
inst✝ : S.Quasicategory
i : Fin (0 + 1 + 1)
σ₀ : Λ[0 + 1, i] ⟶ S
h0 : 0 < ↑i
hn : ↑i = 0
⊢ ∃ σ, σ₀ = hornInclusion (0 + 1) i ≫ σ

Proof state:
case succ
S : SSet
inst✝ : S.Quasicategory
n : ℕ
i : Fin (n + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (n + 1)
σ₀ : Λ[n + 1, i] ⟶ S
⊢ ∃ σ, σ₀ = hornInclusion (n + 1) i ≫ σ

Tactic:
cases n using Nat.casesAuxOn with
| zero =>
  simp only [Fin.lt_iff_val_lt_val, Fin.val_zero, Fin.val_last, zero_add, Nat.lt_one_iff] at h0 hn
  simp [hn] at h0
| succ n => exact Quasicategory.hornFilling' σ₀ h0 hn

Result:
no goals

Proof state:
case zero
S : SSet
inst✝ : S.Quasicategory
i : Fin (0 + 1)
h0 : 0 < i
hn : i < Fin.last 0
σ₀ : Λ[0, i] ⟶ S
⊢ ∃ σ, σ₀ = hornInclusion 0 i ≫ σ

Tactic:
simp [Fin.lt_iff_val_lt_val] at hn

Result:
no goals

Proof state:
case succ.zero
S : SSet
inst✝ : S.Quasicategory
i : Fin (0 + 1 + 1)
σ₀ : Λ[0 + 1, i] ⟶ S
h0 : 0 < ↑i
hn : ↑i = 0
⊢ ∃ σ, σ₀ = hornInclusion (0 + 1) i ≫ σ

Tactic:
simp [hn] at h0

Result:
no goals

Proof state:
case succ.succ
S : SSet
inst✝ : S.Quasicategory
n : ℕ
i : Fin (n + 1 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (n + 1 + 1)
σ₀ : Λ[n + 1 + 1, i] ⟶ S
⊢ ∃ σ, σ₀ = hornInclusion (n + 1 + 1) i ≫ σ

Tactic:
exact Quasicategory.hornFilling' σ₀ h0 hn

Result:
no goals
-- Mathlib/Order/Monotone/Odd.lean
theorem monotone_of_odd_of_monotoneOn_nonneg {f : G → H} (h₁ : ∀ x, f (-x) = -f x)
    (h₂ : MonotoneOn f (Ici 0)) : Monotone f

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x ≤ y
⊢ -f y ≤ -f x

Tactic:
rw [← h₁, ← h₁]

Result:
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x ≤ y
⊢ f (-y) ≤ f (-x)

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
⊢ Monotone f

Tactic:
refine MonotoneOn.Iic_union_Ici (fun x hx y hy hxy => neg_le_neg_iff.1 ?_) h₂

Result:
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x ≤ y
⊢ -f y ≤ -f x

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x ≤ y
⊢ f (-y) ≤ f (-x)

Tactic:
exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_le_neg hxy)

Result:
no goals
-- Mathlib/NumberTheory/PrimesCongruentOne.lean
theorem frequently_atTop_modEq_one {k : ℕ} (hk0 : k ≠ 0) :
    ∃ᶠ p in atTop, Nat.Prime p ∧ p ≡ 1 [MOD k]

Proof state:
case intro
k : ℕ
hk0 : k ≠ 0
n p : ℕ
hp : Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
⊢ ∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]

Tactic:
exact ⟨p, ⟨hp.2.1.le, hp.1, hp.2.2⟩⟩

Result:
no goals

Proof state:
k : ℕ
hk0 : k ≠ 0
⊢ ∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ 1 [MOD k]

Tactic:
refine frequently_atTop.2 fun n => ?_

Result:
k : ℕ
hk0 : k ≠ 0
n : ℕ
⊢ ∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]

Proof state:
k : ℕ
hk0 : k ≠ 0
n : ℕ
⊢ ∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]

Tactic:
obtain ⟨p, hp⟩ := exists_prime_gt_modEq_one n hk0

Result:
case intro
k : ℕ
hk0 : k ≠ 0
n p : ℕ
hp : Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
⊢ ∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem ghostFun_natCast (i : ℕ) : ghostFun (i : 𝕎 R) = i :=
  show ghostFun i.unaryCast = _ by
    induction i <;>
      simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add, -Pi.natCast_def]

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
i : ℕ
⊢ WittVector.ghostFun i.unaryCast = ↑i

Tactic:
induction i <;>
  simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add, -Pi.natCast_def]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem zeroLocus_empty_iff_eq_top {I : Ideal R} : zeroLocus (I : Set R) = ∅ ↔ I = ⊤

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
⊢ zeroLocus ↑⊤ = ∅

Tactic:
apply zeroLocus_empty_of_one_mem

Result:
case mpr.h
R : Type u
inst✝ : CommSemiring R
⊢ 1 ∈ ↑⊤

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
⊢ (zeroLocus ↑I).Nonempty

Tactic:
rcases Ideal.exists_le_maximal I h with ⟨M, hM, hIM⟩

Result:
case mp.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hIM : I ≤ M
⊢ (zeroLocus ↑I).Nonempty

Proof state:
case mp.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hIM : I ≤ M
⊢ (zeroLocus ↑I).Nonempty

Tactic:
exact ⟨⟨M, hM.isPrime⟩, hIM⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ zeroLocus ↑I = ∅ ↔ I = ⊤

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ zeroLocus ↑I = ∅ → I = ⊤

case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ I = ⊤ → zeroLocus ↑I = ∅

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ zeroLocus ↑I = ∅ → I = ⊤

Tactic:
contrapose!

Result:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ I ≠ ⊤ → (zeroLocus ↑I).Nonempty

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ I ≠ ⊤ → (zeroLocus ↑I).Nonempty

Tactic:
intro h

Result:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
⊢ (zeroLocus ↑I).Nonempty

Proof state:
case mpr.h
R : Type u
inst✝ : CommSemiring R
⊢ 1 ∈ ↑⊤

Tactic:
trivial

Result:
no goals

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ I = ⊤ → zeroLocus ↑I = ∅

Tactic:
rintro rfl

Result:
case mpr
R : Type u
inst✝ : CommSemiring R
⊢ zeroLocus ↑⊤ = ∅