harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
theorem lintegral_lt_top_of_nnreal (f : X →ᵇ ℝ≥0) : ∫⁻ x, f x ∂μ < ∞

Proof state:
case f_bdd
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
x : X
key : f x ≤ nndist f 0
⊢ ↑(f x) ≤ ↑(nndist f 0)

Tactic:
rwa [ENNReal.coe_le_coe]

Result:
no goals

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
⊢ ∫⁻ (x : X), ↑(f x) ∂μ < ⊤

Tactic:
apply IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal

Result:
case f_bdd
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
⊢ ∃ c, ∀ (x : X), ↑(f x) ≤ ↑c

Proof state:
case f_bdd
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
⊢ ∃ c, ∀ (x : X), ↑(f x) ≤ ↑c

Tactic:
refine ⟨nndist f 0, fun x ↦ ?_⟩

Result:
case f_bdd
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
x : X
⊢ ↑(f x) ≤ ↑(nndist f 0)

Proof state:
case f_bdd
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
x : X
⊢ ↑(f x) ≤ ↑(nndist f 0)

Tactic:
have key := BoundedContinuousFunction.NNReal.upper_bound f x

Result:
case f_bdd
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
x : X
key : f x ≤ nndist f 0
⊢ ↑(f x) ≤ ↑(nndist f 0)
-- Mathlib/Data/Nat/PSub.lean
theorem psub_add (m n k) :
    psub m (n + k) = (do psub (← psub m n) k)

Proof state:
case zero
m n : ℕ
⊢ m.psub (n + 0) = do
    let __do_lift ← m.psub n
    __do_lift.psub 0

Tactic:
simp only [zero_eq, add_zero, psub_zero, Option.bind_eq_bind, Option.bind_some]

Result:
no goals

Proof state:
case succ
m n✝ n : ℕ
ih :
  m.psub (n✝ + n) = do
    let __do_lift ← m.psub n✝
    __do_lift.psub n
⊢ m.psub (n✝ + (n + 1)) = do
    let __do_lift ← m.psub n✝
    __do_lift.psub (n + 1)

Tactic:
simp only [ih, add_succ, psub_succ, bind_assoc]

Result:
no goals

Proof state:
m n k : ℕ
⊢ m.psub (n + k) = do
    let __do_lift ← m.psub n
    __do_lift.psub k

Tactic:
induction k with
| zero => simp only [zero_eq, add_zero, psub_zero, Option.bind_eq_bind, Option.bind_some]
| succ n ih => simp only [ih, add_succ, psub_succ, bind_assoc]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem span_singleton_eq_range (x : M) : (R ∙ x) = range (toSpanSingleton R M x) :=
  Submodule.ext fun y => by
    refine Iff.trans ?_ LinearMap.mem_range.symm
    exact mem_span_singleton

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ y ∈ span R {x} ↔ ∃ y_1, (toSpanSingleton R M x) y_1 = y

Tactic:
exact mem_span_singleton

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ y ∈ span R {x} ↔ y ∈ range (toSpanSingleton R M x)

Tactic:
refine Iff.trans ?_ LinearMap.mem_range.symm

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ y ∈ span R {x} ↔ ∃ y_1, (toSpanSingleton R M x) y_1 = y
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem derivWithin_fderivWithin :
    smulRight (1 : 𝕜 →L[𝕜] 𝕜) (derivWithin f s x) = fderivWithin 𝕜 f s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
⊢ smulRight 1 (derivWithin f s x) = fderivWithin 𝕜 f s x

Tactic:
simp [derivWithin]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem univ_pi_update_univ [DecidableEq ι] (i : ι) (s : Set (α i)) :
    pi univ (update (fun j : ι => (univ : Set (α j))) i s) = eval i ⁻¹' s

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
⊢ univ.pi (update (fun j => univ) i s) = eval i ⁻¹' s

Tactic:
rw [univ_pi_update i (fun j => (univ : Set (α j))) s fun j t => t, pi_univ, inter_univ, preimage]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem integral_univ_inv_one_add_sq : ∫ (x : ℝ), (1 + x ^ 2)⁻¹ = π :=
  (by ring : π = (π / 2) - (-(π / 2))) ▸ integral_of_hasDerivAt_of_tendsto hasDerivAt_arctan'
    integrable_inv_one_add_sq (tendsto_nhds_of_tendsto_nhdsWithin tendsto_arctan_atBot)
    (tendsto_nhds_of_tendsto_nhdsWithin tendsto_arctan_atTop)

Proof state:
⊢ π = π / 2 - -(π / 2)

Tactic:
ring

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infDist_le_infDist_add_hausdorffDist (fin : hausdorffEdist s t ≠ ⊤) :
    infDist x t ≤ infDist x s + hausdorffDist s t

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEdist s t ≠ ⊤
h : ¬s.Nonempty
⊢ ¬t.Nonempty

Tactic:
rw [hausdorffEdist_comm] at fin

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEdist t s ≠ ⊤
h : ¬s.Nonempty
⊢ ¬t.Nonempty

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEdist s t ≠ ⊤
⊢ infDist x t ≤ infDist x s + hausdorffDist s t

Tactic:
refine toReal_le_add' infEdist_le_infEdist_add_hausdorffEdist (fun h ↦ ?_) (flip absurd fin)

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEdist s t ≠ ⊤
h : infEdist x s = ⊤
⊢ infEdist x t = ⊤

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEdist s t ≠ ⊤
h : infEdist x s = ⊤
⊢ infEdist x t = ⊤

Tactic:
rw [infEdist_eq_top_iff, ← not_nonempty_iff_eq_empty] at h ⊢

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEdist s t ≠ ⊤
h : ¬s.Nonempty
⊢ ¬t.Nonempty
-- Mathlib/Data/Finsupp/Multiset.lean
theorem prod_toMultiset [CommMonoid α] (f : α →₀ ℕ) :
    f.toMultiset.prod = f.prod fun a n => a ^ n

Proof state:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 →
        ((toMultiset f).prod = f.prod fun a n => a ^ n) →
          (toMultiset (single a b + f)).prod = (single a b + f).prod fun a n => a ^ n

Tactic:
intro a n f _ _ ih

Result:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n => a ^ n
⊢ (toMultiset (single a n + f)).prod = (single a n + f).prod fun a n => a ^ n

Proof state:
case refine_1
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ (toMultiset 0).prod = prod 0 fun a n => a ^ n

Tactic:
rw [toMultiset_zero, Multiset.prod_zero, Finsupp.prod_zero_index]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n => a ^ n
⊢ a ^ 0 = 1

Tactic:
exact pow_zero a

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ (toMultiset f).prod = f.prod fun a n => a ^ n

Tactic:
refine f.induction ?_ ?_

Result:
case refine_1
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ (toMultiset 0).prod = prod 0 fun a n => a ^ n

case refine_2
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 →
        ((toMultiset f).prod = f.prod fun a n => a ^ n) →
          (toMultiset (single a b + f)).prod = (single a b + f).prod fun a n => a ^ n

Proof state:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n => a ^ n
⊢ (toMultiset (single a n + f)).prod = (single a n + f).prod fun a n => a ^ n

Tactic:
rw [toMultiset_add, Multiset.prod_add, ih, toMultiset_single, Multiset.prod_nsmul,
  Finsupp.prod_add_index' pow_zero pow_add, Finsupp.prod_single_index, Multiset.prod_singleton]

Result:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n => a ^ n
⊢ a ^ 0 = 1
-- Mathlib/Tactic/CategoryTheory/Bicategory/Datatypes.lean
theorem StructuralOfExpr_bicategoricalComp {f g h i : a ⟶ b} [BicategoricalCoherence g h]
    (η : f ⟶ g) (η' : f ≅ g) (ih_η : η'.hom = η) (θ : h ⟶ i) (θ' : h ≅ i) (ih_θ : θ'.hom = θ) :
    (bicategoricalIsoComp η' θ').hom = η ⊗≫ θ

Proof state:
B : Type u
inst✝¹ : Bicategory B
a b : B
f g h i : a ⟶ b
inst✝ : BicategoricalCoherence g h
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
θ : h ⟶ i
θ' : h ≅ i
ih_θ : θ'.hom = θ
⊢ (η' ≪⊗≫ θ').hom = η ⊗≫ θ

Tactic:
simp [ih_η, ih_θ, bicategoricalIsoComp, bicategoricalComp]

Result:
no goals
-- Mathlib/Data/Seq/Parallel.lean
theorem exists_of_mem_parallel {S : WSeq (Computation α)} {a} (h : a ∈ parallel S) :
    ∃ c ∈ S, a ∈ c

Proof state:
case cons.inr.inr.intro.intro
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ c, c ∈ l ∧ a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
ad : a' ∈ d
dm : d = c' ∨ d ∈ val✝
⊢ ∃ c_1, c_1 ∈ c :: l ∧ a' ∈ c_1

Tactic:
rcases dm with e | dl

Result:
case cons.inr.inr.intro.intro.inl
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ c, c ∈ l ∧ a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
ad : a' ∈ d
e : d = c'
⊢ ∃ c_1, c_1 ∈ c :: l ∧ a' ∈ c_1

case cons.inr.inr.intro.intro.inr
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ c, c ∈ l ∧ a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
ad : a' ∈ d
dl : d ∈ val✝
⊢ ∃ c_1, c_1 ∈ c :: l ∧ a' ∈ c_1
-- Mathlib/Data/Finsupp/Antidiagonal.lean
theorem prod_antidiagonal_swap {M : Type*} [CommMonoid M] (n : α →₀ ℕ)
    (f : (α →₀ ℕ) → (α →₀ ℕ) → M) :
    ∏ p ∈ antidiagonal n, f p.1 p.2 = ∏ p ∈ antidiagonal n, f p.2 p.1 :=
  prod_equiv (Equiv.prodComm _ _) (by simp [add_comm]) (by simp)

Proof state:
α : Type u
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
n : α →₀ ℕ
f : (α →₀ ℕ) → (α →₀ ℕ) → M
⊢ ∀ i ∈ antidiagonal n, f i.1 i.2 = f ((Equiv.prodComm (α →₀ ℕ) (α →₀ ℕ)) i).2 ((Equiv.prodComm (α →₀ ℕ) (α →₀ ℕ)) i).1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
n : α →₀ ℕ
f : (α →₀ ℕ) → (α →₀ ℕ) → M
⊢ ∀ (i : (α →₀ ℕ) × (α →₀ ℕ)), i ∈ antidiagonal n ↔ (Equiv.prodComm (α →₀ ℕ) (α →₀ ℕ)) i ∈ antidiagonal n

Tactic:
simp [add_comm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors
    {p : R[X]} {t : R} (hpt : Polynomial.IsRoot p t)
    (hnzd : (p.rootMultiplicity t : R) ∈ nonZeroDivisors R) :
    (derivative p).rootMultiplicity t = p.rootMultiplicity t - 1

Proof state:
case neg.intro.intro
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd✝ : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬(X - C t) ^ m ∣ derivative p
⊢ rootMultiplicity t (derivative p) = m - 1

Tactic:
have hnezero : derivative p ≠ 0 := fun h ↦ hndvd (by rw [h]; exact dvd_zero _)

Result:
case neg.intro.intro
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd✝ : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬(X - C t) ^ m ∣ derivative p
hnezero : derivative p ≠ 0
⊢ rootMultiplicity t (derivative p) = m - 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem map_add_range' (a) (s n step) : map (a + ·) (range' s n step) = range' (a + s) n step

Proof state:
a s n step : Nat
⊢ map (fun x => a + x) (range' s n step) = range' (a + s) n step

Tactic:
ext <;> simp <;> omega

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem expand_one (f : R[X]) : expand R 1 f = f :=
  Polynomial.induction_on f (fun r => by rw [expand_C])
    (fun f g ihf ihg => by rw [map_add, ihf, ihg]) fun n r _ => by
    rw [map_mul, expand_C, map_pow, expand_X, pow_one]

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R[X]
r : R
⊢ (expand R 1) (C r) = C r

Tactic:
rw [expand_C]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
f✝ f g : R[X]
ihf : (expand R 1) f = f
ihg : (expand R 1) g = g
⊢ (expand R 1) (f + g) = f + g

Tactic:
rw [map_add, ihf, ihg]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
r : R
x✝ : (expand R 1) (C r * X ^ n) = C r * X ^ n
⊢ (expand R 1) (C r * X ^ (n + 1)) = C r * X ^ (n + 1)

Tactic:
rw [map_mul, expand_C, map_pow, expand_X, pow_one]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Bousfield.lean
lemma isLocalization : G.IsLocalization (W (· ∈ Set.range F.obj))

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.IsLocalization (W fun x => x ∈ Set.range F.obj)

Tactic:
rw [W_eq_inverseImage_isomorphisms adj]

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C).inverseImage G)

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C).inverseImage G)

Tactic:
exact adj.isLocalization

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
/-- If a monotone sequence of functions has an upper bound and the sequence of integrals of these
functions tends to the integral of the upper bound, then the sequence of functions converges
almost everywhere to the upper bound. -/
lemma tendsto_of_integral_tendsto_of_monotone {μ : Measure α} {f : ℕ → α → ℝ} {F : α → ℝ}
    (hf_int : ∀ n, Integrable (f n) μ) (hF_int : Integrable F μ)
    (hf_tendsto : Tendsto (fun i ↦ ∫ a, f i a ∂μ) atTop (𝓝 (∫ a, F a ∂μ)))
    (hf_mono : ∀ᵐ a ∂μ, Monotone (fun i ↦ f i a))
    (hf_bound : ∀ᵐ a ∂μ, ∀ i, f i a ≤ F a) :
    ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a => ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a => ENNReal.ofReal (F a - f 0 a)
i : ℕ
a : α
h_mono : Monotone fun i => f i a
⊢ 0 a ≤ f i a - f 0 a

Tactic:
simp [h_mono (zero_le i)]

Result:
no goals
-- Mathlib/RingTheory/RingHom/FiniteType.lean
theorem IsLocalization.exists_smul_mem_of_mem_adjoin [Algebra R S] [Algebra R S']
    [IsScalarTower R S S'] (M : Submonoid S) [IsLocalization M S'] (x : S) (s : Finset S')
    (A : Subalgebra R S) (hA₁ : (IsLocalization.finsetIntegerMultiple M s : Set S) ⊆ A)
    (hA₂ : M ≤ A.toSubmonoid) (hx : algebraMap S S' x ∈ Algebra.adjoin R (s : Set S')) :
    ∃ m : M, m • x ∈ A

Proof state:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := IsLocalization.commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(IsLocalization.finsetIntegerMultiple M s)
⊢ ∃ m, m • x ∈ A

Tactic:
obtain ⟨n, hn⟩ :=
  Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin (y : S) (s : Set S') (A.map g)
    (by rw [hx₁]; exact Set.image_subset _ hA₁) hx (Set.mem_image_of_mem _ (hA₂ y.2))

Result:
case intro
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := IsLocalization.commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(IsLocalization.finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
⊢ ∃ m, m • x ∈ A
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
@[reassoc (attr := simp)]
lemma Scheme.Opens.toSpecΓ_SpecMap_map {X : Scheme} (U V : X.Opens) (h : U ≤ V) :
    U.toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE h).op) = X.homOfLE h ≫ V.toSpecΓ

Proof state:
X : Scheme
U V : X.Opens
h : U ≤ V
⊢ ((↑U).toSpecΓ ≫ Spec.map U.topIso.inv) ≫ Spec.map (X.presheaf.map (homOfLE h).op) =
    X.homOfLE h ≫ (↑V).toSpecΓ ≫ Spec.map V.topIso.inv

Tactic:
simp [← Spec.map_comp, ← X.presheaf.map_comp, toSpecΓ_naturality_assoc]

Result:
no goals

Proof state:
X : Scheme
U V : X.Opens
h : U ≤ V
⊢ U.toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE h).op) = X.homOfLE h ≫ V.toSpecΓ

Tactic:
delta Scheme.Opens.toSpecΓ

Result:
X : Scheme
U V : X.Opens
h : U ≤ V
⊢ ((↑U).toSpecΓ ≫ Spec.map U.topIso.inv) ≫ Spec.map (X.presheaf.map (homOfLE h).op) =
    X.homOfLE h ≫ (↑V).toSpecΓ ≫ Spec.map V.topIso.inv
-- Mathlib/Algebra/Order/Group/Basic.lean
@[to_additive zsmul_mono_right]
lemma zpow_left_mono (hn : 0 ≤ n) : Monotone ((· ^ n) : α → α) := fun a b hab => by
  rw [← one_le_div', ← div_zpow]; exact one_le_zpow (one_le_div'.2 hab) hn

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ (fun x => x ^ n) a ≤ (fun x => x ^ n) b

Tactic:
rw [← one_le_div', ← div_zpow]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ 1 ≤ (b / a) ^ n

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ 1 ≤ (b / a) ^ n

Tactic:
exact one_le_zpow (one_le_div'.2 hab) hn

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem add (hf : UnifIntegrable f p μ) (hg : UnifIntegrable g p μ) (hp : 1 ≤ p)
    (hf_meas : ∀ i, AEStronglyMeasurable (f i) μ) (hg_meas : ∀ i, AEStronglyMeasurable (g i) μ) :
    UnifIntegrable (f + g) p μ

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
δ₁ : ℝ
hδ₁_pos : 0 < δ₁
hfδ₁ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨δ₂, hδ₂_pos, hgδ₂⟩ := hg hε2

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
δ₁ : ℝ
hδ₁_pos : 0 < δ₁
hfδ₁ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
δ₂ : ℝ
hδ₂_pos : 0 < δ₂
hgδ₂ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Iso.lean
theorem pushoutCoconeOfLeftIso_ι_app_none : (pushoutCoconeOfLeftIso f g).ι.app none = g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ (pushoutCoconeOfLeftIso f g).ι.app none = g

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Defs.lean
theorem coe_pow {R} [Semiring R] [SetLike S R] [SubsemiringClass S R] (x : s) (n : ℕ) :
    ((x ^ n : s) : R) = (x : R) ^ n

Proof state:
case succ
S : Type v
s : S
R : Type u_1
inst✝² : Semiring R
inst✝¹ : SetLike S R
inst✝ : SubsemiringClass S R
x : ↥s
n : ℕ
ih : ↑(x ^ n) = ↑x ^ n
⊢ ↑(x ^ (n + 1)) = ↑x ^ (n + 1)

Tactic:
simp [pow_succ, ih]

Result:
no goals

Proof state:
S : Type v
s : S
R : Type u_1
inst✝² : Semiring R
inst✝¹ : SetLike S R
inst✝ : SubsemiringClass S R
x : ↥s
n : ℕ
⊢ ↑(x ^ n) = ↑x ^ n

Tactic:
induction n with
| zero => simp
| succ n ih => simp [pow_succ, ih]

Result:
no goals

Proof state:
case zero
S : Type v
s : S
R : Type u_1
inst✝² : Semiring R
inst✝¹ : SetLike S R
inst✝ : SubsemiringClass S R
x : ↥s
⊢ ↑(x ^ 0) = ↑x ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem subperm_of_subset (d : Nodup l₁) (H : l₁ ⊆ l₂) : l₁ <+~ l₂

Proof state:
case nil
α✝ : Type u_1
l₁ l₂ : List α✝
H : [] ⊆ l₂
⊢ [] <+~ l₂

Tactic:
exact ⟨nil, .nil, nil_sublist _⟩

Result:
no goals

Proof state:
case cons
α✝ : Type u_1
l₁ l₂ : List α✝
a✝¹ : α✝
l✝ : List α✝
h : ∀ (a' : α✝), a' ∈ l✝ → a✝¹ ≠ a'
a✝ : Pairwise (fun x1 x2 => x1 ≠ x2) l✝
IH : l✝ ⊆ l₂ → l✝ <+~ l₂
H : a✝¹ :: l✝ ⊆ l₂
⊢ a✝¹ :: l✝ <+~ l₂

Tactic:
have ⟨H₁, H₂⟩ := forall_mem_cons.1 H

Result:
case cons
α✝ : Type u_1
l₁ l₂ : List α✝
a✝¹ : α✝
l✝ : List α✝
h : ∀ (a' : α✝), a' ∈ l✝ → a✝¹ ≠ a'
a✝ : Pairwise (fun x1 x2 => x1 ≠ x2) l✝
IH : l✝ ⊆ l₂ → l✝ <+~ l₂
H : a✝¹ :: l✝ ⊆ l₂
H₁ : a✝¹ ∈ l₂
H₂ : ∀ (x : α✝), x ∈ l✝ → x ∈ l₂
⊢ a✝¹ :: l✝ <+~ l₂
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem limsup_pow_nnnorm_pow_one_div_le_spectralRadius (a : A) :
    limsup (fun n : ℕ => (‖a ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ)) atTop ≤ spectralRadius ℂ a

Proof state:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
⊢ limsup (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop ≤ spectralRadius ℂ a

Tactic:
refine ENNReal.inv_le_inv.mp (le_of_forall_pos_nnreal_lt fun r r_pos r_lt => ?_)

Result:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
⊢ ↑r ≤ (limsup (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop)⁻¹
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
/-- The sum of two squares is zero iff both elements are zero. -/
lemma mul_self_add_mul_self_eq_zero [IsRightCancelAdd α] [NoZeroDivisors α]
    [ZeroLEOneClass α] [ExistsAddOfLE α] [PosMulMono α]
    [AddLeftMono α] [AddLeftStrictMono α] :
    a * a + b * b = 0 ↔ a = 0 ∧ b = 0

Proof state:
α : Type u
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
a b : α
inst✝⁶ : IsRightCancelAdd α
inst✝⁵ : NoZeroDivisors α
inst✝⁴ : ZeroLEOneClass α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftStrictMono α
⊢ a * a + b * b = 0 ↔ a = 0 ∧ b = 0

Tactic:
rw [add_eq_zero_iff_of_nonneg, mul_self_eq_zero (M₀ := α), mul_self_eq_zero (M₀ := α)] <;>
  apply mul_self_nonneg

Result:
no goals