harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem deriv_eq_enumOrd (H : IsNormal f) : deriv f = enumOrd (Function.fixedPoints f)

Proof state:
case h.e'_3.h.e'_1
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ fixedPoints f = ⋂ i, fixedPoints f

Tactic:
exact (Set.iInter_const _).symm

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ deriv f = enumOrd (fixedPoints f)

Tactic:
convert derivFamily_eq_enumOrd fun _ : Unit => H

Result:
case h.e'_3.h.e'_1
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ fixedPoints f = ⋂ i, fixedPoints f
-- Mathlib/Algebra/Ring/Units.lean
theorem divp_sub_divp [CommRing α] (a b : α) (u₁ u₂ : αˣ) :
    a /ₚ u₁ - b /ₚ u₂ = (a * u₂ - u₁ * b) /ₚ (u₁ * u₂)

Proof state:
α : Type u
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b) /ₚ (u₁ * u₂)

Tactic:
simp only [sub_eq_add_neg, neg_divp, divp_add_divp, mul_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobjectIsoComp_hom_arrow {X' : C} (f : X' ⟶ X) [IsIso f] (g : X ⟶ Y) [HasKernel g] :
    (kernelSubobjectIsoComp f g).hom ≫ (kernelSubobject g).arrow =
      (kernelSubobject (f ≫ g)).arrow ≫ f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasZeroMorphisms C
X' : C
f : X' ⟶ X
inst✝¹ : IsIso f
g : X ⟶ Y
inst✝ : HasKernel g
⊢ (kernelSubobjectIsoComp f g).hom ≫ (kernelSubobject g).arrow = (kernelSubobject (f ≫ g)).arrow ≫ f

Tactic:
simp [kernelSubobjectIsoComp]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem mem_map_of_injective {f : α → β} (H : Function.Injective f) {a : α} {o : Option α} :
    f a ∈ o.map f ↔ a ∈ o

Proof state:
α : Type u_1
β : Type u_2
f : α → β
H : Function.Injective f
a : α
o : Option α
⊢ f a ∈ Option.map f o ↔ a ∈ o

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem foldTR_loop_congr {α : Type u} {n m : Nat} (w : n = m)
     (f : (i : Nat) → i < n → α → α) (j : Nat) (h : j ≤ n) (init : α) :
     foldTR.loop n f j h init = foldTR.loop m (fun i h => f i (by omega)) j (by omega) init

Proof state:
α : Type u
n m : Nat
w : n = m
f : (i : Nat) → i < n → α → α
j : Nat
h : j ≤ n
init : α
⊢ j ≤ m

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
n m : Nat
w : n = m
f : (i : Nat) → i < n → α → α
j : Nat
h : j ≤ n
init : α
⊢ foldTR.loop n f j h init = foldTR.loop m (fun i h => f i ⋯) j ⋯ init

Tactic:
subst m

Result:
α : Type u
n : Nat
f : (i : Nat) → i < n → α → α
j : Nat
h : j ≤ n
init : α
⊢ foldTR.loop n f j h init = foldTR.loop n (fun i h => f i ⋯) j ⋯ init

Proof state:
α : Type u
n m : Nat
w : n = m
f : (i : Nat) → i < n → α → α
j : Nat
h✝ : j ≤ n
init : α
i : Nat
h : i < m
⊢ i < n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
n : Nat
f : (i : Nat) → i < n → α → α
j : Nat
h : j ≤ n
init : α
⊢ foldTR.loop n f j h init = foldTR.loop n (fun i h => f i ⋯) j ⋯ init

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Int/Lemmas.lean
theorem succ_natCast_pos (n : ℕ) : 0 < (n : ℤ) + 1 :=
  lt_add_one_iff.mpr (by simp)

Proof state:
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Hopf_.lean
theorem mul_antipode₁ (A : Hopf_ C) :
    (A.X.comul.hom ⊗ A.X.comul.hom) ≫
      (α_ A.X.X.X A.X.X.X (A.X.X.X ⊗ A.X.X.X)).hom ≫
      A.X.X.X ◁ (α_ A.X.X.X A.X.X.X A.X.X.X).inv ≫
      A.X.X.X ◁ (β_ A.X.X.X A.X.X.X).hom ▷ A.X.X.X ≫
      (α_ A.X.X.X (A.X.X.X ⊗ A.X.X.X) A.X.X.X).inv ≫
      (α_ A.X.X.X A.X.X.X A.X.X.X).inv ▷ A.X.X.X ≫
      A.X.X.mul ▷ A.X.X.X ▷ A.X.X.X ≫
      A.antipode ▷ A.X.X.X ▷ A.X.X.X ≫
      (α_ A.X.X.X A.X.X.X A.X.X.X).hom ≫
      A.X.X.X ◁ A.X.X.mul ≫
      A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ (A.X.comul.hom ⊗ A.X.comul.hom) ≫
      (α_ A.X.X.X A.X.X.X (A.X.X.X ⊗ A.X.X.X)).hom ≫
        A.X.X.X ◁ (α_ A.X.X.X A.X.X.X A.X.X.X).inv ≫
          A.X.X.X ◁ (β_ A.X.X.X A.X.X.X).hom ▷ A.X.X.X ≫
            (α_ A.X.X.X (A.X.X.X ⊗ A.X.X.X) A.X.X.X).inv ≫
              (α_ A.X.X.X A.X.X.X A.X.X.X).inv ▷ A.X.X.X ≫
                A.X.X.mul ▷ A.X.X.X ▷ A.X.X.X ≫
                  (α_ A.X.X.X A.X.X.X A.X.X.X).hom ≫ (A.X.X.X ◁ A.X.X.mul ≫ A.antipode ▷ A.X.X.X) ≫ A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Tactic:
slice_lhs 7 8 =>
  rw [associator_naturality_left]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ (A.X.comul.hom ⊗ A.X.comul.hom) ≫
      (α_ A.X.X.X A.X.X.X (A.X.X.X ⊗ A.X.X.X)).hom ≫
        A.X.X.X ◁ (α_ A.X.X.X A.X.X.X A.X.X.X).inv ≫
          A.X.X.X ◁ (β_ A.X.X.X A.X.X.X).hom ▷ A.X.X.X ≫
            (α_ A.X.X.X (A.X.X.X ⊗ A.X.X.X) A.X.X.X).inv ≫
              (α_ A.X.X.X A.X.X.X A.X.X.X).inv ▷ A.X.X.X ≫
                ((((α_ (A.X.X.X ⊗ A.X.X.X) A.X.X.X A.X.X.X).hom ≫ A.X.X.mul ▷ (A.X.X.X ⊗ A.X.X.X)) ≫
                      A.X.X.X ◁ A.X.X.mul) ≫
                    A.antipode ▷ A.X.X.X) ≫
                  A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one
-- Mathlib/Geometry/RingedSpace/Basic.lean
lemma zeroLocus_isClosed {U : Opens X} (s : Set (X.presheaf.obj (op U))) :
    IsClosed (X.zeroLocus s)

Proof state:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
i : ↑(X.presheaf.obj (op U))
a✝ : i ∈ s
⊢ IsClosed (↑(X.basicOpen i))ᶜ

Tactic:
simp only [isClosed_compl_iff]

Result:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
i : ↑(X.presheaf.obj (op U))
a✝ : i ∈ s
⊢ IsOpen ↑(X.basicOpen i)

Proof state:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
⊢ ∀ i ∈ s, IsClosed (↑(X.basicOpen i))ᶜ

Tactic:
intro i _

Result:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
i : ↑(X.presheaf.obj (op U))
a✝ : i ∈ s
⊢ IsClosed (↑(X.basicOpen i))ᶜ

Proof state:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
i : ↑(X.presheaf.obj (op U))
a✝ : i ∈ s
⊢ IsOpen ↑(X.basicOpen i)

Tactic:
exact Opens.isOpen (X.basicOpen i)

Result:
no goals

Proof state:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
⊢ IsClosed (X.zeroLocus s)

Tactic:
apply isClosed_biInter

Result:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
⊢ ∀ i ∈ s, IsClosed (↑(X.basicOpen i))ᶜ
-- Mathlib/Probability/Moments/ComplexMGF.lean
lemma complexMGF_undef (hX : AEMeasurable X μ) (h : ¬ Integrable (fun ω ↦ rexp (z.re * X ω)) μ) :
    complexMGF X μ z = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (fun ω => rexp (z.re * X ω)) μ
⊢ complexMGF X μ z = 0

Tactic:
rw [complexMGF, integral_undef]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (fun ω => rexp (z.re * X ω)) μ
⊢ ¬Integrable (fun ω => cexp (z * ↑(X ω))) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (fun ω => rexp (z.re * X ω)) μ
⊢ ¬Integrable (fun a => ‖cexp (z * ↑(X a))‖) μ

Tactic:
simpa [Complex.norm_exp] using h

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (fun ω => rexp (z.re * X ω)) μ
⊢ AEMeasurable (fun ω => cexp (z * ↑(X ω))) μ

Tactic:
fun_prop

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (fun ω => rexp (z.re * X ω)) μ
⊢ ¬Integrable (fun ω => cexp (z * ↑(X ω))) μ

Tactic:
rw [← integrable_norm_iff (AEMeasurable.aestronglyMeasurable <| by fun_prop)]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (fun ω => rexp (z.re * X ω)) μ
⊢ ¬Integrable (fun a => ‖cexp (z * ↑(X a))‖) μ
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem intCast_dvd (z : ℤ) (a : ℤ√d) : ↑z ∣ a ↔ z ∣ a.re ∧ z ∣ a.im

Proof state:
case h
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a.re = { re := z * r, im := z * i }.re ∧ a.im = { re := z * r, im := z * i }.im

Tactic:
exact ⟨hr, hi⟩

Result:
no goals

Proof state:
case mpr.intro.intro.intro
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ ↑z ∣ a

Tactic:
use ⟨r, i⟩

Result:
case h
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a = ↑z * { re := r, im := i }

Proof state:
case mp
d z : ℤ
a : ℤ√d
⊢ ↑z ∣ a → z ∣ a.re ∧ z ∣ a.im

Tactic:
rintro ⟨x, rfl⟩

Result:
case mp.intro
d z : ℤ
x : ℤ√d
⊢ z ∣ (↑z * x).re ∧ z ∣ (↑z * x).im

Proof state:
d z : ℤ
a : ℤ√d
⊢ ↑z ∣ a ↔ z ∣ a.re ∧ z ∣ a.im

Tactic:
constructor

Result:
case mp
d z : ℤ
a : ℤ√d
⊢ ↑z ∣ a → z ∣ a.re ∧ z ∣ a.im

case mpr
d z : ℤ
a : ℤ√d
⊢ z ∣ a.re ∧ z ∣ a.im → ↑z ∣ a

Proof state:
case mpr
d z : ℤ
a : ℤ√d
⊢ z ∣ a.re ∧ z ∣ a.im → ↑z ∣ a

Tactic:
rintro ⟨⟨r, hr⟩, ⟨i, hi⟩⟩

Result:
case mpr.intro.intro.intro
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ ↑z ∣ a

Proof state:
case h
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a = ↑z * { re := r, im := i }

Tactic:
rw [smul_val, Zsqrtd.ext_iff]

Result:
case h
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a.re = { re := z * r, im := z * i }.re ∧ a.im = { re := z * r, im := z * i }.im

Proof state:
case mp.intro
d z : ℤ
x : ℤ√d
⊢ z ∣ (↑z * x).re ∧ z ∣ (↑z * x).im

Tactic:
simp only [add_zero, intCast_re, zero_mul, mul_im, dvd_mul_right, and_self_iff,
  mul_re, mul_zero, intCast_im]

Result:
no goals
-- Mathlib/ModelTheory/Complexity.lean
theorem not_ex_isQF (φ : L.BoundedFormula α (n + 1)) : ¬φ.ex.IsQF := fun con => by
  obtain - | con | con := con
  · exact φ.not_ex_isAtomic con
  · exact not_all_isQF _ con

Proof state:
case of_isAtomic
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∃'φ).IsAtomic
⊢ False

Tactic:
exact φ.not_ex_isAtomic con

Result:
no goals

Proof state:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∃'φ).IsQF
⊢ False

Tactic:
obtain - | con | con := con

Result:
case of_isAtomic
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∃'φ).IsAtomic
⊢ False

case imp
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀'∼φ).IsQF
h₂✝ : ⊥.IsQF
⊢ False

Proof state:
case imp
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀'∼φ).IsQF
h₂✝ : ⊥.IsQF
⊢ False

Tactic:
exact not_all_isQF _ con

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem isImage_preimage_prod (e : Trivialization F proj) (s : Set B) :
    e.toPartialHomeomorph.IsImage (proj ⁻¹' s) (s ×ˢ univ) := fun x hx => by simp [e.coe_fst', hx]

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
s : Set B
x : Z
hx : x ∈ e.source
⊢ ↑e.toPartialHomeomorph x ∈ s ×ˢ univ ↔ x ∈ proj ⁻¹' s

Tactic:
simp [e.coe_fst', hx]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToHom_iso_inv_naturality {f g : β → C} (z : ∀ b, f b ≅ g b) {j j' : β} (w : j = j') :
    (z j).inv ≫ eqToHom (by simp [w]) = eqToHom (by simp [w]) ≫ (z j').inv

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ g j = g j'

Tactic:
simp [w]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ (z j).inv ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j').inv

Tactic:
cases w

Result:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j : β
⊢ (z j).inv ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j).inv

Proof state:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j : β
⊢ (z j).inv ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j).inv

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
lemma ball_eq_openSegment (hε : 0 < ε) : ball r ε = openSegment ℝ (r - ε) (r + ε)

Proof state:
r ε : ℝ
hε : 0 < ε
⊢ ball r ε = openSegment ℝ (r - ε) (r + ε)

Tactic:
rw [ball_eq_Ioo, openSegment_eq_Ioo ((sub_lt_self _ hε).trans <| lt_add_of_pos_right _ hε)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem setIfInBounds_append {s t : Array α} {i : Nat} {x : α} :
    (s ++ t).setIfInBounds i x =
      if i < s.size then
        s.setIfInBounds i x ++ t
      else
        s ++ t.setIfInBounds (i - s.size) x

Proof state:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : List α
⊢ (if i < s.length then s.set i x ++ t else s ++ t.set (i - s.length) x).toArray =
    if i < { toList := s }.size then (s.set i x ++ t).toArray else (s ++ t.set (i - { toList := s }.size) x).toArray

Tactic:
split <;> simp

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : List α
⊢ ({ toList := s } ++ { toList := t }).setIfInBounds i x =
    if i < { toList := s }.size then { toList := s }.setIfInBounds i x ++ { toList := t }
    else { toList := s } ++ { toList := t }.setIfInBounds (i - { toList := s }.size) x

Tactic:
simp only [List.append_toArray, List.setIfInBounds_toArray, List.set_append]

Result:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : List α
⊢ (if i < s.length then s.set i x ++ t else s ++ t.set (i - s.length) x).toArray =
    if i < { toList := s }.size then (s.set i x ++ t).toArray else (s ++ t.set (i - { toList := s }.size) x).toArray

Proof state:
case mk
α : Type u_1
t : Array α
i : Nat
x : α
s : List α
⊢ ({ toList := s } ++ t).setIfInBounds i x =
    if i < { toList := s }.size then { toList := s }.setIfInBounds i x ++ t
    else { toList := s } ++ t.setIfInBounds (i - { toList := s }.size) x

Tactic:
rcases t with ⟨t⟩

Result:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : List α
⊢ ({ toList := s } ++ { toList := t }).setIfInBounds i x =
    if i < { toList := s }.size then { toList := s }.setIfInBounds i x ++ { toList := t }
    else { toList := s } ++ { toList := t }.setIfInBounds (i - { toList := s }.size) x

Proof state:
α : Type u_1
s t : Array α
i : Nat
x : α
⊢ (s ++ t).setIfInBounds i x = if i < s.size then s.setIfInBounds i x ++ t else s ++ t.setIfInBounds (i - s.size) x

Tactic:
rcases s with ⟨s⟩

Result:
case mk
α : Type u_1
t : Array α
i : Nat
x : α
s : List α
⊢ ({ toList := s } ++ t).setIfInBounds i x =
    if i < { toList := s }.size then { toList := s }.setIfInBounds i x ++ t
    else { toList := s } ++ t.setIfInBounds (i - { toList := s }.size) x
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integrableOn_Ioi_exp_neg_mul_sq_iff {b : ℝ} :
    IntegrableOn (fun x : ℝ => exp (-b * x ^ 2)) (Ioi 0) ↔ 0 < b

Proof state:
b : ℝ
h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume
hb : b ≤ 0
⊢ ∫⁻ (x : ℝ) in Ioi 0, 1 ≤ ∫⁻ (x : ℝ) in Ioi 0, ↑‖rexp (-b * x ^ 2)‖₊

Tactic:
apply lintegral_mono (fun x ↦ _)

Result:
b : ℝ
h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume
hb : b ≤ 0
⊢ ∀ (x : ℝ), 1 ≤ ↑‖rexp (-b * x ^ 2)‖₊

Proof state:
b : ℝ
⊢ IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume ↔ 0 < b

Tactic:
refine ⟨fun h => ?_, fun h => (integrable_exp_neg_mul_sq h).integrableOn⟩

Result:
b : ℝ
h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume
⊢ 0 < b

Proof state:
b : ℝ
h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume
⊢ 0 < b

Tactic:
by_contra! hb

Result:
b : ℝ
h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume
hb : b ≤ 0
⊢ False

Proof state:
b : ℝ
h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume
hb : b ≤ 0
⊢ ∀ (x : ℝ), b * x ^ 2 ≤ 0

Tactic:
exact fun x ↦ mul_nonpos_of_nonpos_of_nonneg hb (sq_nonneg x)

Result:
no goals

Proof state:
b : ℝ
h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume
hb : b ≤ 0
⊢ False

Tactic:
have : ∫⁻ _ : ℝ in Ioi 0, 1 ≤ ∫⁻ x : ℝ in Ioi 0, ‖exp (-b * x ^ 2)‖₊ := by
  apply lintegral_mono (fun x ↦ _)
  simp only [neg_mul, ENNReal.one_le_coe_iff, ← toNNReal_one, toNNReal_le_iff_le_coe,
    Real.norm_of_nonneg (exp_pos _).le, coe_nnnorm, one_le_exp_iff, Right.nonneg_neg_iff]
  exact fun x ↦ mul_nonpos_of_nonpos_of_nonneg hb (sq_nonneg x)

Result:
b : ℝ
h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume
hb : b ≤ 0
this : ∫⁻ (x : ℝ) in Ioi 0, 1 ≤ ∫⁻ (x : ℝ) in Ioi 0, ↑‖rexp (-b * x ^ 2)‖₊
⊢ False

Proof state:
b : ℝ
h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume
hb : b ≤ 0
this : ∫⁻ (x : ℝ) in Ioi 0, 1 ≤ ∫⁻ (x : ℝ) in Ioi 0, ↑‖rexp (-b * x ^ 2)‖₊
⊢ False

Tactic:
simpa using this.trans_lt h.2

Result:
no goals

Proof state:
b : ℝ
h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume
hb : b ≤ 0
⊢ ∀ (x : ℝ), 1 ≤ ↑‖rexp (-b * x ^ 2)‖₊

Tactic:
simp only [neg_mul, ENNReal.one_le_coe_iff, ← toNNReal_one, toNNReal_le_iff_le_coe,
  Real.norm_of_nonneg (exp_pos _).le, coe_nnnorm, one_le_exp_iff, Right.nonneg_neg_iff]

Result:
b : ℝ
h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume
hb : b ≤ 0
⊢ ∀ (x : ℝ), b * x ^ 2 ≤ 0
-- Mathlib/Data/Complex/Basic.lean
theorem inv_I : I⁻¹ = -I

Proof state:
⊢ I⁻¹ = -I

Tactic:
rw [inv_eq_one_div, div_I, one_mul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arctan_inv_2_add_arctan_inv_3 : arctan 2⁻¹ + arctan 3⁻¹ = π / 4

Proof state:
⊢ arctan 2⁻¹ + arctan 3⁻¹ = π / 4

Tactic:
rw [arctan_add] <;> norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem insert_of_mem {l : List α} (h : a ∈ l) : l.insert a = l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ List.insert a l = l

Tactic:
simp [List.insert, h]

Result:
no goals
-- Mathlib/RingTheory/Invariant.lean
theorem fixed_of_fixed2 (f : L ≃ₐ[K] L) (x : L)
    (hx : ∀ g : MulAction.stabilizer G Q, IsFractionRing.stabilizerHom G P Q K L g x = x) :
    f x = x

Proof state:
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Group G
inst✝¹⁵ : Finite G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹² : Q.IsPrime
inst✝¹¹ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra (A ⧸ P) K
inst✝⁷ : Algebra (B ⧸ Q) L
inst✝⁶ : Algebra (A ⧸ P) L
inst✝⁵ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower (A ⧸ P) K L
inst✝² : Algebra.IsInvariant A B G
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : L ≃ₐ[K] L
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
ha : a ≠ 0
h : a • x = y * b
⊢ (algebraMap (A ⧸ P) L) a ≠ 0

Tactic:
rwa [Ne, algebraMap_apply (A ⧸ P) K L, algebraMap_eq_zero_iff, algebraMap_eq_zero_iff]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Group G
inst✝¹⁵ : Finite G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹² : Q.IsPrime
inst✝¹¹ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra (A ⧸ P) K
inst✝⁷ : Algebra (B ⧸ Q) L
inst✝⁶ : Algebra (A ⧸ P) L
inst✝⁵ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower (A ⧸ P) K L
inst✝² : Algebra.IsInvariant A B G
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : L ≃ₐ[K] L
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y b : B ⧸ Q
a : A ⧸ P
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
h : (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y = (algebraMap (B ⧸ Q) L) b / (algebraMap (A ⧸ P) L) a
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) b) = (algebraMap (B ⧸ Q) L) b
⊢ f ((algebraMap (B ⧸ Q) L) b) = (algebraMap (B ⧸ Q) L) b

Tactic:
exact fixed_of_fixed1 G P Q K L f b (fun g ↦ IsFractionRing.injective (B ⧸ Q) L
  ((IsFractionRing.fieldEquivOfAlgEquiv_algebraMap K L L
    (Ideal.Quotient.stabilizerHom Q P G g) b).symm.trans (hx g)))

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem IsLocal.mem_jacobson_or_exists_inv {I : Ideal R} (hi : IsLocal I) (x : R) :
    x ∈ jacobson I ∨ ∃ y, y * x - 1 ∈ I :=
  by_cases
    (fun h : I ⊔ span {x} = ⊤ =>
      let ⟨p, hpi, q, hq, hpq⟩ := Submodule.mem_sup.1 ((eq_top_iff_one _).1 h)
      let ⟨r, hr⟩ := mem_span_singleton.1 hq
      Or.inr ⟨r, by
        rw [← hpq, mul_comm, ← hr, ← neg_sub, add_sub_cancel_right]; exact I.neg_mem hpi⟩)
    fun h : I ⊔ span {x} ≠ ⊤ =>
    Or.inl <|
      le_trans le_sup_right (hi.le_jacobson le_sup_left h) <| mem_span_singleton.2 <| dvd_refl x

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
hi : I.IsLocal
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {x}
hpq : p + q = 1
r : R
hr : q = x * r
⊢ -p ∈ I

Tactic:
exact I.neg_mem hpi

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
hi : I.IsLocal
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {x}
hpq : p + q = 1
r : R
hr : q = x * r
⊢ r * x - 1 ∈ I

Tactic:
rw [← hpq, mul_comm, ← hr, ← neg_sub, add_sub_cancel_right]

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
hi : I.IsLocal
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {x}
hpq : p + q = 1
r : R
hr : q = x * r
⊢ -p ∈ I
-- Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
/-- If we take the path along the spine of a face of a `spineToSimplex`, the
arrows not contained in the original path can be recovered as the diagonal edge
of the `spineToSimplex` that "composes" arrows `i` and `i + 1`. -/
lemma spine_δ_arrow_eq (f : Path X (n + 1)) {i : Fin n} {j : Fin (n + 2)}
    (h : j = i.succ.castSucc) :
    (X.spine n (X.δ j (spineToSimplex f))).arrow i =
      spineToDiagonal (Path.interval f i 2 (by omega))

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ (X.spine n (SimplicialObject.δ X j (spineToSimplex f))).arrow i = spineToDiagonal (f.interval (↑i) 2 ⋯)

Tactic:
simp only [SimplicialObject.δ, spine_arrow]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ X.map (mkOfSucc i).op (X.map (SimplexCategory.δ j).op (spineToSimplex f)) = spineToDiagonal (f.interval (↑i) 2 ⋯)

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ X.map (mkOfSucc i).op (X.map (SimplexCategory.δ j).op (spineToSimplex f)) = spineToDiagonal (f.interval (↑i) 2 ⋯)

Tactic:
rw [← FunctorToTypes.map_comp_apply, ← op_comp]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ X.map (mkOfSucc i ≫ SimplexCategory.δ j).op (spineToSimplex f) = spineToDiagonal (f.interval (↑i) 2 ⋯)

Proof state:
X✝ X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ ↑i + 2 ≤ n + 1

Tactic:
omega

Result:
no goals

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ X.map (mkOfSucc i ≫ SimplexCategory.δ j).op (spineToSimplex f) = spineToDiagonal (f.interval (↑i) 2 ⋯)

Tactic:
rw [mkOfSucc_δ_eq h, spineToSimplex_edge]

Result:
no goals