harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Bounds/Image.lean
theorem BddAbove.bddAbove_image2_of_bddBelow :
    BddAbove s → BddBelow t → BddAbove (Set.image2 f s t)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddAbove s → BddBelow t → BddAbove (image2 f s t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Result:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (image2 f s t)

Proof state:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (image2 f s t)

Tactic:
exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Elements.lean
@[simp]
lemma map_π_liftedConeElement (i : I) :
    A.map (limit.π (F ⋙ π A) i) (liftedConeElement F) = (F.obj i).snd

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
i : I
⊢ A.map (limit.π (F ⋙ π A) i) (liftedConeElement F) = (F.obj i).snd

Tactic:
have := congrFun
  (preservesLimitIso_inv_π A (F ⋙ π A) i) (liftedConeElement' F)

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
i : I
this :
  ((preservesLimitIso A (F ⋙ π A)).inv ≫ A.map (limit.π (F ⋙ π A) i)) (liftedConeElement' F) =
    limit.π ((F ⋙ π A) ⋙ A) i (liftedConeElement' F)
⊢ A.map (limit.π (F ⋙ π A) i) (liftedConeElement F) = (F.obj i).snd

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
i : I
this :
  ((preservesLimitIso A (F ⋙ π A)).inv ≫ A.map (limit.π (F ⋙ π A) i)) (liftedConeElement' F) =
    limit.π ((F ⋙ π A) ⋙ A) i (liftedConeElement' F)
⊢ A.map (limit.π (F ⋙ π A) i) (liftedConeElement F) = (F.obj i).snd

Tactic:
simp_all [liftedConeElement]

Result:
no goals
-- Mathlib/Probability/Moments/ComplexMGF.lean
lemma complexMGF_id_map (hX : AEMeasurable X μ) : complexMGF id (μ.map X) = complexMGF X μ

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℂ
⊢ complexMGF id (Measure.map X μ) t = complexMGF X μ t

Tactic:
rw [complexMGF, integral_map hX]

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℂ
⊢ ∫ (x : Ω), cexp (t * ↑(id (X x))) ∂μ = complexMGF X μ t

case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℂ
⊢ AEStronglyMeasurable (fun ω => cexp (t * ↑(id ω))) (Measure.map X μ)

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℂ
⊢ ∫ (x : Ω), cexp (t * ↑(id (X x))) ∂μ = complexMGF X μ t

Tactic:
rfl

Result:
no goals

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℂ
⊢ AEStronglyMeasurable (fun ω => cexp (t * ↑(id ω))) (Measure.map X μ)

Tactic:
exact AEMeasurable.aestronglyMeasurable <| by fun_prop

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
⊢ complexMGF id (Measure.map X μ) = complexMGF X μ

Tactic:
ext t

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℂ
⊢ complexMGF id (Measure.map X μ) t = complexMGF X μ t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℂ
⊢ AEMeasurable (fun ω => cexp (t * ↑(id ω))) (Measure.map X μ)

Tactic:
fun_prop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_consₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β)
    (h : Raw.WFImp m.1) (a : α) (b : β a) (hc : m.containsₘ a = false) :
    Raw.WFImp (m.consₘ a b).1 where
  buckets_hash_self := isHashSelf_consₘ m h a b
  size_eq

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
hc : m.containsₘ a = false
⊢ (m.consₘ a b).val.size = (⟨a, b⟩ :: toListModel m.val.buckets).length

Tactic:
simpa [consₘ] using h.size_eq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
hc : m.containsₘ a = false
⊢ containsKey a (toListModel m.val.buckets) = false

Tactic:
rwa [← containsₘ_eq_containsKey h]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
hc : m.containsₘ a = false
⊢ DistinctKeys (toListModel (m.consₘ a b).val.buckets)

Tactic:
refine (h.distinct.cons ?_).perm (toListModel_consₘ _ h _ _)

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
hc : m.containsₘ a = false
⊢ containsKey a (toListModel m.val.buckets) = false

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
hc : m.containsₘ a = false
⊢ (m.consₘ a b).val.size = (toListModel (m.consₘ a b).val.buckets).length

Tactic:
refine Eq.trans ?_ (toListModel_consₘ _ h _ _).length_eq.symm

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
hc : m.containsₘ a = false
⊢ (m.consₘ a b).val.size = (⟨a, b⟩ :: toListModel m.val.buckets).length
-- Mathlib/Topology/LocallyClosed.lean
lemma IsOpenMap.coborder_preimage_subset (hf : IsOpenMap f) (s : Set Y) :
    coborder (f ⁻¹' s) ⊆ f ⁻¹' (coborder s)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' closure s \ f ⁻¹' s ⊆ closure (f ⁻¹' s) \ f ⁻¹' s

Tactic:
apply diff_subset_diff_left

Result:
case h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' closure s ⊆ closure (f ⁻¹' s)

Proof state:
case h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' closure s ⊆ closure (f ⁻¹' s)

Tactic:
exact hf.preimage_closure_subset_closure_preimage

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set Y
⊢ coborder (f ⁻¹' s) ⊆ f ⁻¹' coborder s

Tactic:
rw [coborder, coborder, preimage_compl, preimage_diff, compl_subset_compl]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' closure s \ f ⁻¹' s ⊆ closure (f ⁻¹' s) \ f ⁻¹' s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_of_add_le_add_left {a b c : Int} (h : a + b ≤ a + c) : b ≤ c

Proof state:
a b c : Int
h : a + b ≤ a + c
⊢ b ≤ c

Tactic:
have : -a + (a + b) ≤ -a + (a + c) := Int.add_le_add_left h _

Result:
a b c : Int
h : a + b ≤ a + c
this : -a + (a + b) ≤ -a + (a + c)
⊢ b ≤ c

Proof state:
a b c : Int
h : a + b ≤ a + c
this : -a + (a + b) ≤ -a + (a + c)
⊢ b ≤ c

Tactic:
simp [Int.neg_add_cancel_left] at this

Result:
a b c : Int
h : a + b ≤ a + c
this : b ≤ c
⊢ b ≤ c

Proof state:
a b c : Int
h : a + b ≤ a + c
this : b ≤ c
⊢ b ≤ c

Tactic:
assumption

Result:
no goals
-- Mathlib/Topology/Sheaves/Alexandrov.lean
lemma exists_le_of_le_sup {ι : Type v} {x : X}
    (Us : ι → Opens X) (h : principalOpen x ≤ iSup Us) :
    ∃ i : ι, principalOpen x ≤ Us i

Proof state:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
ι : Type v
x : X
Us : ι → Opens X
h : principalOpen x ≤ iSup Us
⊢ ∃ i, principalOpen x ≤ Us i

Tactic:
have : x ∈ iSup Us := h <| self_mem_principalOpen x

Result:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
ι : Type v
x : X
Us : ι → Opens X
h : principalOpen x ≤ iSup Us
this : x ∈ iSup Us
⊢ ∃ i, principalOpen x ≤ Us i

Proof state:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
ι : Type v
x : X
Us : ι → Opens X
h : principalOpen x ≤ iSup Us
this : ∃ i, x ∈ Us i
⊢ ∃ i, principalOpen x ≤ Us i

Tactic:
obtain ⟨i, hi⟩ := this

Result:
case intro
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
ι : Type v
x : X
Us : ι → Opens X
h : principalOpen x ≤ iSup Us
i : ι
hi : x ∈ Us i
⊢ ∃ i, principalOpen x ≤ Us i

Proof state:
case intro
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
ι : Type v
x : X
Us : ι → Opens X
h : principalOpen x ≤ iSup Us
i : ι
hi : x ∈ Us i
⊢ principalOpen x ≤ Us i

Tactic:
simpa

Result:
no goals

Proof state:
case intro
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
ι : Type v
x : X
Us : ι → Opens X
h : principalOpen x ≤ iSup Us
i : ι
hi : x ∈ Us i
⊢ ∃ i, principalOpen x ≤ Us i

Tactic:
refine ⟨i, ?_⟩

Result:
case intro
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
ι : Type v
x : X
Us : ι → Opens X
h : principalOpen x ≤ iSup Us
i : ι
hi : x ∈ Us i
⊢ principalOpen x ≤ Us i

Proof state:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
ι : Type v
x : X
Us : ι → Opens X
h : principalOpen x ≤ iSup Us
this : x ∈ iSup Us
⊢ ∃ i, principalOpen x ≤ Us i

Tactic:
simp only [Opens.mem_iSup] at this

Result:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
ι : Type v
x : X
Us : ι → Opens X
h : principalOpen x ≤ iSup Us
this : ∃ i, x ∈ Us i
⊢ ∃ i, principalOpen x ≤ Us i
-- Mathlib/Algebra/RingQuot.lean
theorem ringQuot_ext [Semiring T] {r : R → R → Prop} (f g : RingQuot r →+* T)
    (w : f.comp (mkRingHom r) = g.comp (mkRingHom r)) : f = g

Proof state:
case a
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : f.comp (mkRingHom r) = g.comp (mkRingHom r)
x : RingQuot r
⊢ f x = g x

Tactic:
rcases mkRingHom_surjective r x with ⟨x, rfl⟩

Result:
case a.intro
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : f.comp (mkRingHom r) = g.comp (mkRingHom r)
x : R
⊢ f ((mkRingHom r) x) = g ((mkRingHom r) x)

Proof state:
case a.intro
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : f.comp (mkRingHom r) = g.comp (mkRingHom r)
x : R
⊢ f ((mkRingHom r) x) = g ((mkRingHom r) x)

Tactic:
exact (RingHom.congr_fun w x :)

Result:
no goals

Proof state:
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : f.comp (mkRingHom r) = g.comp (mkRingHom r)
⊢ f = g

Tactic:
ext x

Result:
case a
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : f.comp (mkRingHom r) = g.comp (mkRingHom r)
x : RingQuot r
⊢ f x = g x
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem parent_root (self : UnionFind) (x : Fin self.size) :
    (self.arr[(self.root x).1]).parent = self.root x

Proof state:
case isFalse
self : UnionFind
x : Fin self.size
h✝ : ¬self.arr[↑x].parent = ↑x
⊢ self.arr[↑(let_fun this := ⋯;
          self.root ⟨self.arr[↑x].parent, ⋯⟩)].parent =
    ↑(let_fun this := ⋯;
      self.root ⟨self.arr[↑x].parent, ⋯⟩)

Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)

Result:
case isFalse
self : UnionFind
x : Fin self.size
h✝ : ¬self.arr[↑x].parent = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ self.arr[↑(let_fun this := ⋯;
          self.root ⟨self.arr[↑x].parent, ⋯⟩)].parent =
    ↑(let_fun this := ⋯;
      self.root ⟨self.arr[↑x].parent, ⋯⟩)

Proof state:
self : UnionFind
x : Fin self.size
⊢ self.arr[↑(if h : self.arr[↑x].parent = ↑x then x
          else
            let_fun this := ⋯;
            self.root ⟨self.arr[↑x].parent, ⋯⟩)].parent =
    ↑(if h : self.arr[↑x].parent = ↑x then x
      else
        let_fun this := ⋯;
        self.root ⟨self.arr[↑x].parent, ⋯⟩)

Tactic:
split <;> [assumption; skip]

Result:
case isFalse
self : UnionFind
x : Fin self.size
h✝ : ¬self.arr[↑x].parent = ↑x
⊢ self.arr[↑(let_fun this := ⋯;
          self.root ⟨self.arr[↑x].parent, ⋯⟩)].parent =
    ↑(let_fun this := ⋯;
      self.root ⟨self.arr[↑x].parent, ⋯⟩)

Proof state:
case isFalse
self : UnionFind
x : Fin self.size
h✝ : ¬self.arr[↑x].parent = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ self.arr[↑(let_fun this := ⋯;
          self.root ⟨self.arr[↑x].parent, ⋯⟩)].parent =
    ↑(let_fun this := ⋯;
      self.root ⟨self.arr[↑x].parent, ⋯⟩)

Tactic:
apply parent_root

Result:
no goals

Proof state:
self : UnionFind
x : Fin self.size
⊢ self.arr[↑(self.root x)].parent = ↑(self.root x)

Tactic:
rw [root]

Result:
self : UnionFind
x : Fin self.size
⊢ self.arr[↑(if h : self.arr[↑x].parent = ↑x then x
          else
            let_fun this := ⋯;
            self.root ⟨self.arr[↑x].parent, ⋯⟩)].parent =
    ↑(if h : self.arr[↑x].parent = ↑x then x
      else
        let_fun this := ⋯;
        self.root ⟨self.arr[↑x].parent, ⋯⟩)
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integral_gaussian_Ioi (b : ℝ) :
    ∫ x in Ioi (0 : ℝ), exp (-b * x ^ 2) = √(π / b) / 2

Proof state:
b : ℝ
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ 2) = √(π / b) / 2

Tactic:
rcases le_or_lt b 0 with (hb | hb)

Result:
case inl
b : ℝ
hb : b ≤ 0
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ 2) = √(π / b) / 2

case inr
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ 2) = √(π / b) / 2

Proof state:
case inl
b : ℝ
hb : b ≤ 0
⊢ π / b ≤ 0

Tactic:
exact div_nonpos_of_nonneg_of_nonpos pi_pos.le hb

Result:
no goals

Proof state:
case h.e'_3
b : ℝ
hb : 0 < b
⊢ ↑(π / b) ^ ↑(1 / 2) / ↑2 = ↑(π / b) ^ (1 / 2) / 2

Tactic:
norm_num

Result:
no goals

Proof state:
case h.e'_2.h.e'_7.h
b : ℝ
hb : 0 < b
x✝ : ℝ
⊢ ↑(rexp (-b * x✝ ^ 2)) = cexp (-↑b * ↑x✝ ^ 2)

Tactic:
simp

Result:
no goals

Proof state:
case inl
b : ℝ
hb : b ≤ 0
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ 2) = √(π / b) / 2

Tactic:
rw [integral_undef, sqrt_eq_zero_of_nonpos, zero_div]

Result:
case inl
b : ℝ
hb : b ≤ 0
⊢ π / b ≤ 0

case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x => rexp (-b * x ^ 2)) (volume.restrict (Ioi 0))

Proof state:
case inr
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ 2) = √(π / b) / 2

Tactic:
rw [← RCLike.ofReal_inj (K := ℂ), ← integral_ofReal, ← RCLike.algebraMap_eq_ofReal,
  coe_algebraMap]

Result:
case inr
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-b * x ^ 2)) = ↑(√(π / b) / 2)

Proof state:
case h.e'_3.hx
b : ℝ
hb : 0 < b
⊢ 0 ≤ π / b

Tactic:
exact (div_pos pi_pos hb).le

Result:
no goals

Proof state:
case inr
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-b * x ^ 2)) = ↑(√(π / b) / 2)

Tactic:
convert integral_gaussian_complex_Ioi (by rwa [ofReal_re] : 0 < (b : ℂ).re)

Result:
case h.e'_2.h.e'_7.h
b : ℝ
hb : 0 < b
x✝ : ℝ
⊢ ↑(rexp (-b * x✝ ^ 2)) = cexp (-↑b * ↑x✝ ^ 2)

case h.e'_3
b : ℝ
hb : 0 < b
⊢ ↑(√(π / b) / 2) = (↑π / ↑b) ^ (1 / 2) / 2

Proof state:
case h.e'_3
b : ℝ
hb : 0 < b
⊢ ↑(√(π / b) / 2) = (↑π / ↑b) ^ (1 / 2) / 2

Tactic:
rw [sqrt_eq_rpow, ← ofReal_div, ofReal_div, ofReal_cpow]

Result:
case h.e'_3
b : ℝ
hb : 0 < b
⊢ ↑(π / b) ^ ↑(1 / 2) / ↑2 = ↑(π / b) ^ (1 / 2) / 2

case h.e'_3.hx
b : ℝ
hb : 0 < b
⊢ 0 ≤ π / b

Proof state:
case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x => rexp (-b * x ^ 2)) (volume.restrict (Ioi 0))

Tactic:
rwa [← IntegrableOn, integrableOn_Ioi_exp_neg_mul_sq_iff, not_lt]

Result:
no goals

Proof state:
b : ℝ
hb : 0 < b
⊢ 0 < (↑b).re

Tactic:
rwa [ofReal_re]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
theorem dual_ordConnectedComponent :
    ordConnectedComponent (ofDual ⁻¹' s) (toDual x) = ofDual ⁻¹' ordConnectedComponent s x :=
  ext <| (Surjective.forall toDual.surjective).2 fun x => by
    rw [mem_ordConnectedComponent, dual_uIcc]
    rfl

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x✝ x : α
⊢ ⇑ofDual ⁻¹' [[x✝, x]] ⊆ ⇑ofDual ⁻¹' s ↔ toDual x ∈ ⇑ofDual ⁻¹' s.ordConnectedComponent x✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x✝ x : α
⊢ toDual x ∈ (⇑ofDual ⁻¹' s).ordConnectedComponent (toDual x✝) ↔ toDual x ∈ ⇑ofDual ⁻¹' s.ordConnectedComponent x✝

Tactic:
rw [mem_ordConnectedComponent, dual_uIcc]

Result:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x✝ x : α
⊢ ⇑ofDual ⁻¹' [[x✝, x]] ⊆ ⇑ofDual ⁻¹' s ↔ toDual x ∈ ⇑ofDual ⁻¹' s.ordConnectedComponent x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem natAbs_dvd_self {a : Int} : (a.natAbs : Int) ∣ a

Proof state:
a : Int
⊢ ↑a.natAbs ∣ a

Tactic:
rw [Int.natAbs_dvd]

Result:
a : Int
⊢ a ∣ a

Proof state:
a : Int
⊢ a ∣ a

Tactic:
exact Int.dvd_refl a

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem norm_cpow_eq_rpow_re_of_pos {x : ℝ} (hx : 0 < x) (y : ℂ) : ‖(x : ℂ) ^ y‖ = x ^ y.re

Proof state:
x : ℝ
hx : 0 < x
y : ℂ
⊢ ‖↑x ^ y‖ = x ^ y.re

Tactic:
rw [norm_cpow_of_ne_zero (ofReal_ne_zero.mpr hx.ne'), arg_ofReal_of_nonneg hx.le,
  zero_mul, Real.exp_zero, div_one, Complex.norm_of_nonneg hx.le]

Result:
no goals
-- Mathlib/RingTheory/IsTensorProduct.lean
theorem IsBaseChange.iff_lift_unique :
    IsBaseChange S f ↔
      ∀ (Q : Type max v₁ v₂ v₃) [AddCommMonoid Q],
        ∀ [Module R Q] [Module S Q],
          ∀ [IsScalarTower R S Q],
            ∀ g : M →ₗ[R] Q, ∃! g' : N →ₗ[S] Q, (g'.restrictScalars R).comp f = g :=
  ⟨fun h => by
    intros Q _ _ _ _ g
    exact ⟨h.lift g, h.lift_comp g, fun g' e => h.algHom_ext' _ _ (e.trans (h.lift_comp g).symm)⟩,
    IsBaseChange.of_lift_unique f⟩

Proof state:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type (max v₁ v₂ v₃)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module S Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
⊢ ∃! g', ↑R g' ∘ₗ f = g

Tactic:
exact ⟨h.lift g, h.lift_comp g, fun g' e => h.algHom_ext' _ _ (e.trans (h.lift_comp g).symm)⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
⊢ ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g

Tactic:
intros Q _ _ _ _ g

Result:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type (max v₁ v₂ v₃)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module S Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
⊢ ∃! g', ↑R g' ∘ₗ f = g
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma rightShift_rightUnshift {a n' : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn' : n' + a = n) :
    (γ.rightUnshift n hn').rightShift a n' hn' = γ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn' : n' + a = n
⊢ (γ.rightUnshift n hn').rightShift a n' hn' = γ

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
⊢ ((γ.rightUnshift n hn').rightShift a n' hn').v p q hpq = γ.v p q hpq

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
⊢ ((γ.rightUnshift n hn').rightShift a n' hn').v p q hpq = γ.v p q hpq

Tactic:
simp only [(γ.rightUnshift n hn').rightShift_v a n' hn' p q hpq (p + n) rfl,
  γ.rightUnshift_v n hn' p (p + n) rfl q hpq,
  shiftFunctorObjXIso, assoc, Iso.hom_inv_id, comp_id]

Result:
no goals
-- Mathlib/NumberTheory/ADEInequality.lean
theorem lt_six {r : ℕ+} (H : 1 < sumInv {2, 3, r}) : r < 6

Proof state:
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ (↑↑r)⁻¹ ≤ 6⁻¹

Tactic:
rw [inv_le_inv₀ _ h6]

Result:
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 6 ≤ ↑↑r

r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 0 < ↑↑r

Proof state:
r : ℕ+
H : 1 < sumInv {2, 3, r}
⊢ r < 6

Tactic:
have h6 : (0 : ℚ) < 6 := by norm_num

Result:
r : ℕ+
H : 1 < sumInv {2, 3, r}
h6 : 0 < 6
⊢ r < 6

Proof state:
r : ℕ+
H : 1 < sumInv {2, 3, r}
⊢ 0 < 6

Tactic:
norm_num

Result:
no goals

Proof state:
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 6 ≤ ↑↑r

Tactic:
assumption_mod_cast

Result:
no goals

Proof state:
r : ℕ+
H : 1 < sumInv {2, 3, r}
h6 : 0 < 6
⊢ r < 6

Tactic:
contrapose! H

Result:
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ sumInv {2, 3, r} ≤ 1

Proof state:
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ sumInv {2, 3, r} ≤ 1

Tactic:
rw [sumInv_pqr]

Result:
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1

Proof state:
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 0 < ↑↑r

Tactic:
norm_num

Result:
no goals

Proof state:
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
hr : (↑↑r)⁻¹ ≤ 6⁻¹
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1

Tactic:
calc
  (2⁻¹ + 3⁻¹ + (r : ℚ)⁻¹ : ℚ) ≤ 2⁻¹ + 3⁻¹ + 6⁻¹ := add_le_add (add_le_add le_rfl le_rfl) hr
  _ = 1 := by norm_num

Result:
no goals

Proof state:
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
hr : (↑↑r)⁻¹ ≤ 6⁻¹
⊢ 2⁻¹ + 3⁻¹ + 6⁻¹ = 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iInf_false {s : False → α} : iInf s = ⊤

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : False → α
⊢ iInf s = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem map_join (f : α → β) (S : Multiset (Multiset α)) :
    map f (join S) = join (map (map f) S)

Proof state:
case cons
α : Type u_1
β : Type v
f : α → β
a✝ : Multiset α
s✝ : Multiset (Multiset α)
ih : map f s✝.join = (map (map f) s✝).join
⊢ map f (a✝ ::ₘ s✝).join = (map (map f) (a✝ ::ₘ s✝)).join

Tactic:
simp [ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type v
f : α → β
S : Multiset (Multiset α)
⊢ map f S.join = (map (map f) S).join

Tactic:
induction S using Multiset.induction with
| empty => simp
| cons _ _ ih => simp [ih]

Result:
no goals

Proof state:
case empty
α : Type u_1
β : Type v
f : α → β
⊢ map f (join 0) = (map (map f) 0).join

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem single_eq_C_mul_T (r : R) (n : ℤ) :
    (Finsupp.single n r : R[T;T⁻¹]) = (C r * T n : R[T;T⁻¹])

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
n : ℤ
⊢ Finsupp.single n r = C r * T n

Tactic:
simp [C, T, single_mul_single]

Result:
no goals