harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_pos (x : ℝ) : 0 < exp x :=
  (le_total 0 x).elim (lt_of_lt_of_le zero_lt_one ∘ one_le_exp) fun h => by
    rw [← neg_neg x, Real.exp_neg]
    exact inv_pos.2 (lt_of_lt_of_le zero_lt_one (one_le_exp (neg_nonneg.2 h)))

Proof state:
x : ℝ
h : x ≤ 0
⊢ 0 < (rexp (-x))⁻¹

Tactic:
exact inv_pos.2 (lt_of_lt_of_le zero_lt_one (one_le_exp (neg_nonneg.2 h)))

Result:
no goals

Proof state:
x : ℝ
h : x ≤ 0
⊢ 0 < rexp x

Tactic:
rw [← neg_neg x, Real.exp_neg]

Result:
x : ℝ
h : x ≤ 0
⊢ 0 < (rexp (-x))⁻¹
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem natTrailingDegree_intCast (n : ℤ) : natTrailingDegree (n : R[X]) = 0

Proof state:
R : Type u
inst✝ : Ring R
n : ℤ
⊢ (↑n).natTrailingDegree = 0

Tactic:
simp only [← C_eq_intCast, natTrailingDegree_C]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coverage.lean
theorem isSheaf_coverage (K : Coverage C) (P : Cᵒᵖ ⥤ Type*) :
    Presieve.IsSheaf (toGrothendieck _ K) P ↔
    (∀ {X : C} (R : Presieve X), R ∈ K X → Presieve.IsSheafFor P R)

Proof state:
case mpr.transitive.refine_1
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : K.Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C},
    ∀ R ∈ K.covering X, IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
⊢ P.map g.op t₁ = P.map g.op t₂

Tactic:
refine (H2 hg (𝟙 _)).ext (fun ZZ gg hgg => ?_)

Result:
case mpr.transitive.refine_1
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : K.Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C},
    ∀ R ∈ K.covering X, IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows gg
⊢ P.map gg.op (P.map g.op t₁) = P.map gg.op (P.map g.op t₂)

Proof state:
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R
X : C
S : Sieve X
hS : S ∈ (toGrothendieck C K) X
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f S).arrows
⊢ IsSheafFor P S.arrows

Tactic:
simpa using this (f := 𝟙 _)

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coverage.lean
theorem isSheaf_coverage (K : Coverage C) (P : Cᵒᵖ ⥤ Type*) :
    Presieve.IsSheaf (toGrothendieck _ K) P ↔
    (∀ {X : C} (R : Presieve X), R ∈ K X → Presieve.IsSheafFor P R)

Proof state:
case e_f
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : K.Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C},
    ∀ R ∈ K.covering X, IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), (y g).IsAmalgamation (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback g₁ (Sieve.pullback (f₁ ≫ f) S)).arrows gg
⊢ (gg ≫ g₁) ≫ f₁ = (gg ≫ g₂) ≫ f₂

Tactic:
simp only [Category.assoc, h]

Result:
no goals

Proof state:
case mpr.top
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R
X : C
S : Sieve X
X✝ Y✝ : C
f✝ : Y✝ ⟶ X✝
⊢ IsSheafFor P (Sieve.pullback f✝ ⊤).arrows

Tactic:
simpa using Presieve.isSheafFor_top_sieve _

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Ring/Multiset.lean
@[simp]
lemma CanonicallyOrderedAdd.multiset_prod_pos {R : Type*}
    [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [NoZeroDivisors R] [Nontrivial R]
    {m : Multiset R} : 0 < m.prod ↔ ∀ x ∈ m, 0 < x

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
m : Multiset R
⊢ 0 < m.prod ↔ ∀ x ∈ m, 0 < x

Tactic:
rcases m with ⟨l⟩

Result:
case mk
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < Multiset.prod (Quot.mk (⇑(List.isSetoid R)) l) ↔ ∀ x ∈ Quot.mk (⇑(List.isSetoid R)) l, 0 < x

Proof state:
case mk
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < Multiset.prod (Quot.mk (⇑(List.isSetoid R)) l) ↔ ∀ x ∈ Quot.mk (⇑(List.isSetoid R)) l, 0 < x

Tactic:
rw [Multiset.quot_mk_to_coe'', Multiset.prod_coe]

Result:
case mk
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < l.prod ↔ ∀ x ∈ ↑l, 0 < x

Proof state:
case mk
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < l.prod ↔ ∀ x ∈ ↑l, 0 < x

Tactic:
exact CanonicallyOrderedAdd.list_prod_pos

Result:
no goals
-- Mathlib/ModelTheory/Definability.lean
theorem Definable.inter {f g : Set (α → M)} (hf : A.Definable L f) (hg : A.Definable L g) :
    A.Definable L (f ∩ g)

Proof state:
case intro.intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ θ : L[[↑A]].Formula α
x✝ : α → M
⊢ x✝ ∈ setOf φ.Realize ∩ setOf θ.Realize ↔ x✝ ∈ setOf (φ ⊓ θ).Realize

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ θ : L[[↑A]].Formula α
⊢ A.Definable L (setOf φ.Realize ∩ setOf θ.Realize)

Tactic:
refine ⟨φ ⊓ θ, ?_⟩

Result:
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ θ : L[[↑A]].Formula α
⊢ setOf φ.Realize ∩ setOf θ.Realize = setOf (φ ⊓ θ).Realize

Proof state:
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ θ : L[[↑A]].Formula α
⊢ setOf φ.Realize ∩ setOf θ.Realize = setOf (φ ⊓ θ).Realize

Tactic:
ext

Result:
case intro.intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ θ : L[[↑A]].Formula α
x✝ : α → M
⊢ x✝ ∈ setOf φ.Realize ∩ setOf θ.Realize ↔ x✝ ∈ setOf (φ ⊓ θ).Realize

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
hf : A.Definable L f
hg : A.Definable L g
⊢ A.Definable L (f ∩ g)

Tactic:
rcases hf with ⟨φ, rfl⟩

Result:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
g : Set (α → M)
hg : A.Definable L g
φ : L[[↑A]].Formula α
⊢ A.Definable L (setOf φ.Realize ∩ g)

Proof state:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
g : Set (α → M)
hg : A.Definable L g
φ : L[[↑A]].Formula α
⊢ A.Definable L (setOf φ.Realize ∩ g)

Tactic:
rcases hg with ⟨θ, rfl⟩

Result:
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ θ : L[[↑A]].Formula α
⊢ A.Definable L (setOf φ.Realize ∩ setOf θ.Realize)
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem IsUniformInducing.equicontinuousAt_iff {F : ι → X → α} {x₀ : X} {u : α → β}
    (hu : IsUniformInducing u) : EquicontinuousAt F x₀ ↔ EquicontinuousAt ((u ∘ ·) ∘ F) x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x => u ∘ x) ∘ F) x₀

Tactic:
rw [equicontinuousAt_iff_continuousAt, equicontinuousAt_iff_continuousAt, this.continuousAt_iff]

Result:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ ContinuousAt ((⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun) ∘ ⇑ofFun ∘ swap F) x₀ ↔
    ContinuousAt (⇑ofFun ∘ swap ((fun x => u ∘ x) ∘ F)) x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ ContinuousAt ((⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun) ∘ ⇑ofFun ∘ swap F) x₀ ↔
    ContinuousAt (⇑ofFun ∘ swap ((fun x => u ∘ x) ∘ F)) x₀

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x => u ∘ x) ∘ F) x₀

Tactic:
have := (UniformFun.postcomp_isUniformInducing (α := ι) hu).isInducing

Result:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x => u ∘ x) ∘ F) x₀
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsRestriction.base_iff (hMN : N ≤r M) {B : Set α} : N.IsBase B ↔ M.IsBasis B N.E :=
  ⟨fun h ↦ IsBase.isBasis_of_isRestriction h hMN,
    fun h ↦ by simpa [hMN.eq_restrict] using h.restrict_isBase⟩

Proof state:
α : Type u_1
M N : Matroid α
hMN : N ≤r M
B : Set α
h : M.IsBasis B N.E
⊢ N.IsBase B

Tactic:
simpa [hMN.eq_restrict] using h.restrict_isBase

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem getElem_congr_idx [GetElem coll idx elem valid] {c : coll} {i j : idx} {w : valid c i}
    (h' : i = j) : c[i] = c[j]'(h' ▸ w)

Proof state:
case refl
coll : Type u_1
idx : Type u_2
elem : Type u_3
valid : coll → idx → Prop
inst✝ : GetElem coll idx elem valid
c : coll
i : idx
w : valid c i
⊢ getElem c i w = getElem c i ⋯

Tactic:
rfl

Result:
no goals

Proof state:
coll : Type u_1
idx : Type u_2
elem : Type u_3
valid : coll → idx → Prop
inst✝ : GetElem coll idx elem valid
c : coll
i j : idx
w : valid c i
h' : i = j
⊢ getElem c i w = getElem c j ⋯

Tactic:
cases h'

Result:
case refl
coll : Type u_1
idx : Type u_2
elem : Type u_3
valid : coll → idx → Prop
inst✝ : GetElem coll idx elem valid
c : coll
i : idx
w : valid c i
⊢ getElem c i w = getElem c i ⋯
-- Mathlib/Control/Traversable/Equiv.lean
theorem traverse_eq_map_id (f : α → β) (x : t' α) :
    Equiv.traverse eqv ((pure : β → Id β) ∘ f) x = pure (Equiv.map eqv f x)

Proof state:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α β : Type u
f : α → β
x : t' α
⊢ Equiv.traverse eqv (pure ∘ f) x = pure (Equiv.map eqv f x)

Tactic:
simp only [Equiv.traverse, traverse_eq_map_id, Id.map_eq, Id.pure_eq]

Result:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α β : Type u
f : α → β
x : t' α
⊢ (eqv β) (id.mk (f <$> (eqv α).symm x)) = Equiv.map eqv f x

Proof state:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α β : Type u
f : α → β
x : t' α
⊢ (eqv β) (id.mk (f <$> (eqv α).symm x)) = Equiv.map eqv f x

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem erase_zero (a : α) : erase a (0 : α →₀ M) = 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
⊢ erase a 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem inv_intCast_den (a : ℤ) : (a : ℚ)⁻¹.den = if a = 0 then 1 else a.natAbs

Proof state:
case inl
a : ℤ
lt : a < 0
⊢ ↑(↑a)⁻¹.den = ↑(if a = 0 then 1 else a.natAbs)

Tactic:
obtain ⟨a, rfl⟩ : ∃ b, -b = a := ⟨-a, a.neg_neg⟩

Result:
case inl.intro
a : ℤ
lt : -a < 0
⊢ ↑(↑(-a))⁻¹.den = ↑(if -a = 0 then 1 else (-a).natAbs)

Proof state:
a : ℤ
gt : 0 < a
⊢ ¬a = 0

Tactic:
omega

Result:
no goals

Proof state:
a : ℤ
⊢ (↑a)⁻¹.den = if a = 0 then 1 else a.natAbs

Tactic:
rw [← Int.ofNat_inj]

Result:
a : ℤ
⊢ ↑(↑a)⁻¹.den = ↑(if a = 0 then 1 else a.natAbs)

Proof state:
case inr.inr
a : ℤ
gt : 0 < a
⊢ a = ↑a.natAbs

Tactic:
exact Int.eq_natAbs_of_zero_le (by omega)

Result:
no goals

Proof state:
case inl.intro
a : ℤ
lt : 0 < a
⊢ ↑(↑(-a))⁻¹.den = ↑(if -a = 0 then 1 else (-a).natAbs)

Tactic:
rw [if_neg (by omega)]

Result:
case inl.intro
a : ℤ
lt : 0 < a
⊢ ↑(↑(-a))⁻¹.den = ↑(-a).natAbs

Proof state:
a : ℤ
lt : 0 < a
⊢ 0 ≤ a

Tactic:
omega

Result:
no goals

Proof state:
a : ℤ
lt : 0 < a
⊢ ¬-a = 0

Tactic:
omega

Result:
no goals

Proof state:
case inl.intro
a : ℤ
lt : -a < 0
⊢ ↑(↑(-a))⁻¹.den = ↑(if -a = 0 then 1 else (-a).natAbs)

Tactic:
simp at lt

Result:
case inl.intro
a : ℤ
lt : 0 < a
⊢ ↑(↑(-a))⁻¹.den = ↑(if -a = 0 then 1 else (-a).natAbs)

Proof state:
a : ℤ
⊢ ↑(↑a)⁻¹.den = ↑(if a = 0 then 1 else a.natAbs)

Tactic:
rcases lt_trichotomy a 0 with lt | rfl | gt

Result:
case inl
a : ℤ
lt : a < 0
⊢ ↑(↑a)⁻¹.den = ↑(if a = 0 then 1 else a.natAbs)

case inr.inl

⊢ ↑(↑0)⁻¹.den = ↑(if 0 = 0 then 1 else Int.natAbs 0)

case inr.inr
a : ℤ
gt : 0 < a
⊢ ↑(↑a)⁻¹.den = ↑(if a = 0 then 1 else a.natAbs)

Proof state:
case inl.intro
a : ℤ
lt : 0 < a
⊢ a = ↑a.natAbs

Tactic:
exact Int.eq_natAbs_of_zero_le (by omega)

Result:
no goals

Proof state:
case inr.inr
a : ℤ
gt : 0 < a
⊢ ↑(↑a)⁻¹.den = ↑a.natAbs

Tactic:
simp only [inv_intCast_den_of_pos gt]

Result:
case inr.inr
a : ℤ
gt : 0 < a
⊢ a = ↑a.natAbs

Proof state:
case inr.inr
a : ℤ
gt : 0 < a
⊢ ↑(↑a)⁻¹.den = ↑(if a = 0 then 1 else a.natAbs)

Tactic:
rw [if_neg (by omega)]

Result:
case inr.inr
a : ℤ
gt : 0 < a
⊢ ↑(↑a)⁻¹.den = ↑a.natAbs

Proof state:
case inr.inl

⊢ ↑(↑0)⁻¹.den = ↑(if 0 = 0 then 1 else Int.natAbs 0)

Tactic:
simp

Result:
no goals

Proof state:
a : ℤ
gt : 0 < a
⊢ 0 ≤ a

Tactic:
omega

Result:
no goals

Proof state:
case inl.intro
a : ℤ
lt : 0 < a
⊢ ↑(↑(-a))⁻¹.den = ↑(-a).natAbs

Tactic:
simp only [Int.cast_neg, Rat.inv_neg, neg_den, inv_intCast_den_of_pos lt, Int.natAbs_neg]

Result:
case inl.intro
a : ℤ
lt : 0 < a
⊢ a = ↑a.natAbs
-- Mathlib/Data/NNReal/Defs.lean
theorem coe_sSup (s : Set ℝ≥0) : (↑(sSup s) : ℝ) = sSup (((↑) : ℝ≥0 → ℝ) '' s)

Proof state:
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ ¬BddAbove (toReal '' s)

Tactic:
contrapose! H

Result:
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove (toReal '' s)
⊢ BddAbove s

Proof state:
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove (toReal '' s)
⊢ BddAbove s

Tactic:
exact bddAbove_coe.1 H

Result:
no goals

Proof state:
s : Set ℝ≥0
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
rcases Set.eq_empty_or_nonempty s with rfl|hs

Result:
case inl

⊢ ↑(sSup ∅) = sSup (toReal '' ∅)

case inr
s : Set ℝ≥0
hs : s.Nonempty
⊢ ↑(sSup s) = sSup (toReal '' s)

Proof state:
case hs
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
⊢ ∀ x ∈ Subtype.val '' s, 0 ≤ x

Tactic:
rintro - ⟨y, -, rfl⟩

Result:
case hs.intro.intro
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
y : { r // 0 ≤ r }
⊢ 0 ≤ ↑y

Proof state:
case inl

⊢ ↑(sSup ∅) = sSup (toReal '' ∅)

Tactic:
simp

Result:
no goals

Proof state:
case pos
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
have A : sSup (Subtype.val '' s) ∈ Set.Ici 0 := by
  apply Real.sSup_nonneg
  rintro - ⟨y, -, rfl⟩
  exact y.2

Result:
case pos
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
A : sSup (Subtype.val '' s) ∈ Set.Ici 0
⊢ ↑(sSup s) = sSup (toReal '' s)

Proof state:
case neg
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
simp only [csSup_of_not_bddAbove H, csSup_empty, bot_eq_zero', NNReal.coe_zero]

Result:
case neg
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ 0 = sSup (toReal '' s)

Proof state:
case pos
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
A : sSup (Subtype.val '' s) ∈ Set.Ici 0
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
exact (@subset_sSup_of_within ℝ (Set.Ici (0 : ℝ)) _ _ (_) s hs H A).symm

Result:
no goals

Proof state:
case neg
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ 0 = sSup (toReal '' s)

Tactic:
apply (Real.sSup_of_not_bddAbove ?_).symm

Result:
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ ¬BddAbove (toReal '' s)

Proof state:
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
⊢ sSup (Subtype.val '' s) ∈ Set.Ici 0

Tactic:
apply Real.sSup_nonneg

Result:
case hs
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
⊢ ∀ x ∈ Subtype.val '' s, 0 ≤ x

Proof state:
case inr
s : Set ℝ≥0
hs : s.Nonempty
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
by_cases H : BddAbove s

Result:
case pos
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
⊢ ↑(sSup s) = sSup (toReal '' s)

case neg
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ ↑(sSup s) = sSup (toReal '' s)

Proof state:
case hs.intro.intro
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
y : { r // 0 ≤ r }
⊢ 0 ≤ ↑y

Tactic:
exact y.2

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma stabilizer_inf_stabilizer_le_stabilizer_apply₂ {f : Set α → Set α → Set α}
    (hf : ∀ a : G, a • f s t = f (a • s) (a • t)) :
    stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (f s t)

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
f : Set α → Set α → Set α
hf : ∀ (a : G), a • f s t = f (a • s) (a • t)
⊢ stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (f s t)

Tactic:
aesop (add simp [SetLike.le_def])

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Positivity.lean
/-- If all values of `a : ℕ → ℂ` are nonnegative reals and `a 1` is positive,
then `L a x` is positive real for all real `x` larger than `abscissaOfAbsConv a`. -/
lemma positive {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {x : ℝ} (hx : abscissaOfAbsConv a < x) :
    0 < LSeries a x

Proof state:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < ↑x
⊢ abscissaOfAbsConv a < ↑(↑x).re

Tactic:
simpa only [ofReal_re] using hx

Result:
no goals

Proof state:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < ↑x
⊢ Summable (term a ↑x)

Tactic:
exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <| by simpa only [ofReal_re] using hx

Result:
no goals

Proof state:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < ↑x
⊢ 0 < ∑' (n : ℕ), term a (↑x) n

Tactic:
refine tsum_pos ?_ (fun n ↦ term_nonneg (ha₀ n) x) 1 <| term_pos one_ne_zero ha₁ x

Result:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < ↑x
⊢ Summable (term a ↑x)

Proof state:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < ↑x
⊢ 0 < LSeries a ↑x

Tactic:
rw [LSeries]

Result:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < ↑x
⊢ 0 < ∑' (n : ℕ), term a (↑x) n
-- Mathlib/Computability/Primrec.lean
theorem list_get? : Primrec₂ (@List.get? α) :=
  let F (l : List α) (n : ℕ) :=
    l.foldl
      (fun (s : ℕ ⊕ α) (a : α) =>
        Sum.casesOn s (@Nat.casesOn (fun _ => ℕ ⊕ α) · (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n)
  have hF : Primrec₂ F :=
    (list_foldl fst (sumInl.comp snd)
      ((sumCasesOn fst (nat_casesOn snd (sumInr.comp <| snd.comp fst) (sumInl.comp snd).to₂).to₂
              (sumInr.comp snd).to₂).comp
          snd).to₂).to₂
  have :
    @Primrec _ (Option α) _ _ fun p : List α × ℕ => Sum.casesOn (F p.1 p.2) (fun _ => none) some :=
    sumCasesOn hF (const none).to₂ (option_some.comp snd).to₂
  this.to₂.of_eq fun l n => by
    dsimp; symm
    induction' l with a l IH generalizing n; · rfl
    rcases n with - | n
    · dsimp [F]
      clear IH
      induction' l with _ l IH <;> simp [*]
    · apply IH

Proof state:
case cons.zero
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
a : α
l : List α
IH : ∀ (n : ℕ), l.get? n = Sum.rec (fun val => none) (fun val => some val) (F l n)
⊢ some a =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inr a) l)

Tactic:
clear IH

Result:
case cons.zero
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.1 p.2) (fun x => none) some
a : α
l : List α
⊢ some a =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inr a) l)