harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/ZMod/Basic.lean
lemma ringEquivCongr_ringEquivCongr_apply {a b c : ℕ} (hab : a = b) (hbc : b = c) (x : ZMod a) :
    ringEquivCongr hbc (ringEquivCongr hab x) = ringEquivCongr (hab.trans hbc) x

Proof state:
a b c : ℕ
hab : a = b
hbc : b = c
x : ZMod a
⊢ (ringEquivCongr hbc) ((ringEquivCongr hab) x) = (ringEquivCongr ⋯) x

Tactic:
rw [← ringEquivCongr_trans hab hbc]

Result:
a b c : ℕ
hab : a = b
hbc : b = c
x : ZMod a
⊢ (ringEquivCongr hbc) ((ringEquivCongr hab) x) = ((ringEquivCongr hab).trans (ringEquivCongr hbc)) x

Proof state:
a b c : ℕ
hab : a = b
hbc : b = c
x : ZMod a
⊢ (ringEquivCongr hbc) ((ringEquivCongr hab) x) = ((ringEquivCongr hab).trans (ringEquivCongr hbc)) x

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
/-- The empty list lifts the element `0` of `⨂[R] i, s i`.
-/
lemma lifts_zero : 0 ∈ lifts (0 : ⨂[R] i, s i)

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
⊢ [].sum = 0

Tactic:
rw [List.sum_nil]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
⊢ (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) 0).sum = 0

Tactic:
erw [List.map_nil]

Result:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
⊢ [].sum = 0

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
⊢ 0 ∈ lifts 0

Tactic:
rw [mem_lifts_iff]

Result:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
⊢ (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) 0).sum = 0
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem ofComapInfPrincipal_eq_of_map (h : m '' s ∈ g) : (ofComapInfPrincipal h).map m = g

Proof state:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : f.NeBot
⊢ map m (ofComapInfPrincipal h) = g

Tactic:
apply eq_of_le

Result:
case h
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : f.NeBot
⊢ ↑(map m (ofComapInfPrincipal h)) ≤ ↑g

Proof state:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ map m (ofComapInfPrincipal h) = g

Tactic:
let f := Filter.comap m g ⊓ 𝓟 s

Result:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ map m (ofComapInfPrincipal h) = g

Proof state:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ map m (ofComapInfPrincipal h) = g

Tactic:
haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h

Result:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : f.NeBot
⊢ map m (ofComapInfPrincipal h) = g

Proof state:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : f.NeBot
⊢ Filter.map m (Filter.comap m ↑g) ⊓ Filter.map m (𝓟 s) = Filter.map m (Filter.comap m ↑g) ⊓ 𝓟 (m '' s)

Tactic:
rw [map_principal]

Result:
no goals

Proof state:
case h
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : f.NeBot
⊢ ↑(map m (ofComapInfPrincipal h)) ≤ ↑g

Tactic:
calc
  Filter.map m (of f) ≤ Filter.map m f := map_mono (of_le _)
  _ ≤ (Filter.map m <| Filter.comap m g) ⊓ Filter.map m (𝓟 s) := map_inf_le
  _ = (Filter.map m <| Filter.comap m g) ⊓ (𝓟 <| m '' s) := by rw [map_principal]
  _ ≤ ↑g ⊓ (𝓟 <| m '' s) := inf_le_inf_right _ map_comap_le
  _ = ↑g := inf_of_le_left (le_principal_iff.mpr h)

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem zipWith_swap_prod_support [Fintype α] (l l' : List α) :
    (zipWith swap l l').prod.support ≤ l.toFinset ⊔ l'.toFinset

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith swap l l').prod.support
hx' : x ∈ {x | (zipWith swap l l').prod x ≠ x}
⊢ x ∈ l.toFinset ⊔ l'.toFinset

Tactic:
simpa using zipWith_swap_prod_support' _ _ hx'

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith swap l l').prod.support
⊢ x ∈ l.toFinset ⊔ l'.toFinset

Tactic:
have hx' : x ∈ { x | (zipWith swap l l').prod x ≠ x } := by simpa using hx

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith swap l l').prod.support
hx' : x ∈ {x | (zipWith swap l l').prod x ≠ x}
⊢ x ∈ l.toFinset ⊔ l'.toFinset

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
⊢ (zipWith swap l l').prod.support ≤ l.toFinset ⊔ l'.toFinset

Tactic:
intro x hx

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith swap l l').prod.support
⊢ x ∈ l.toFinset ⊔ l'.toFinset

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith swap l l').prod.support
⊢ x ∈ {x | (zipWith swap l l').prod x ≠ x}

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem ModifyWF.of_eq {t : RBSet α cmp}
    (H : ∀ {x}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x) : ModifyWF t cut f

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
⊢ (∀ {x : α}, (zoom cut t.val).fst.root? = some x → cmpEq cmp (f x) x) →
    OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val).fst

Tactic:
cases (t.1.zoom cut).1 <;> intro H <;> [trivial; exact H rfl]

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
⊢ (∀ {x : α}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x) →
    OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val).fst

Tactic:
rw [find?_eq_zoom]

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
⊢ (∀ {x : α}, (zoom cut t.val).fst.root? = some x → cmpEq cmp (f x) x) →
    OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val).fst

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
H : ∀ {x : α}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x
⊢ t.ModifyWF cut f

Tactic:
refine ⟨.modify ?_ t.2⟩

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
H : ∀ {x : α}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x
⊢ OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val).fst

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
H : ∀ {x : α}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x
⊢ OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val).fst

Tactic:
revert H

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
⊢ (∀ {x : α}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x) →
    OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val).fst
-- Mathlib/Probability/Kernel/Disintegration/Basic.lean
/-- If the singleton `{x}` has non-zero mass for `ρ.fst`, then for all `s : Set Ω`,
`ρCond x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)` . -/
lemma IsCondKernel.apply_of_ne_zero [MeasurableSingletonClass α] {x : α}
    (hx : ρ.fst {x} ≠ 0) (s : Set Ω) : ρCond x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

Proof state:
case e_a.h
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s✝ s : Set Ω
hs : MeasurableSet s
⊢ (ρCond x) s = (comap (fun y => (x, y)) ((ρ.fst {x})⁻¹ • ρ)) s

Tactic:
simp [IsCondKernel.apply_of_ne_zero_of_measurableSet _ _ hx hs,
  (measurableEmbedding_prod_mk_left x).comap_apply]

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

Tactic:
have : ρCond x s = ((ρ.fst {x})⁻¹ • ρ).comap (fun (y : Ω) ↦ (x, y)) s := by
  congr 2 with s hs
  simp [IsCondKernel.apply_of_ne_zero_of_measurableSet _ _ hx hs,
    (measurableEmbedding_prod_mk_left x).comap_apply]

Result:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
this : (ρCond x) s = (comap (fun y => (x, y)) ((ρ.fst {x})⁻¹ • ρ)) s
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

Proof state:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
⊢ (ρCond x) s = (comap (fun y => (x, y)) ((ρ.fst {x})⁻¹ • ρ)) s

Tactic:
congr 2 with s hs

Result:
case e_a.h
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s✝ s : Set Ω
hs : MeasurableSet s
⊢ (ρCond x) s = (comap (fun y => (x, y)) ((ρ.fst {x})⁻¹ • ρ)) s

Proof state:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
this : (ρCond x) s = (comap (fun y => (x, y)) ((ρ.fst {x})⁻¹ • ρ)) s
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

Tactic:
simp [this, (measurableEmbedding_prod_mk_left x).comap_apply, hx]

Result:
no goals
-- Mathlib/Dynamics/OmegaLimit.lean
theorem eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset' {c : Set β}
    (hc₁ : IsCompact c) (hc₂ : ∃ v ∈ f, closure (image2 ϕ v s) ⊆ c) {n : Set β} (hn₁ : IsOpen n)
    (hn₂ : ω f ϕ s ⊆ n) : ∃ u ∈ f, closure (image2 ϕ u s) ⊆ n

Proof state:
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
⊢ ∃ u ∈ f, closure (image2 ϕ u s) ⊆ n

Tactic:
let w := (⋂ u ∈ g, u) ∩ v

Result:
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
⊢ ∃ u ∈ f, closure (image2 ϕ u s) ⊆ n

Proof state:
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
⊢ ∃ u ∈ f, closure (image2 ϕ u s) ⊆ n

Tactic:
rcases hk.elim_finite_subcover_image hj₁ hj₂ with ⟨g, hg₁ : ∀ u ∈ g, u ∈ f, hg₂, hg₃⟩

Result:
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
⊢ ∃ u ∈ f, closure (image2 ϕ u s) ⊆ n
-- Mathlib/Data/Sum/Order.lean
theorem denselyOrdered_iff [LT α] [LT β] :
    DenselyOrdered (α ⊕ β) ↔ DenselyOrdered α ∧ DenselyOrdered β :=
  ⟨fun _ =>
    ⟨⟨fun a b h => by
        obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inl_lt_inl_iff.2 h)
        · exact ⟨c, inl_lt_inl_iff.1 ha, inl_lt_inl_iff.1 hb⟩
        · exact (not_inl_lt_inr ha).elim⟩,
      ⟨fun a b h => by
        obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inr_lt_inr_iff.2 h)
        · exact (not_inl_lt_inr hb).elim
        · exact ⟨c, inr_lt_inr_iff.1 ha, inr_lt_inr_iff.1 hb⟩⟩⟩,
    fun h => @Sum.denselyOrdered _ _ _ _ h.1 h.2⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inl_lt_inl_iff.2 h)

Result:
case intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : α
ha : inl a < inl c
hb : inl c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : β
ha : inl a < inr c
hb : inr c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Proof state:
case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : β
ha : inr a < inr c
hb : inr c < inr b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
exact ⟨c, inr_lt_inr_iff.1 ha, inr_lt_inr_iff.1 hb⟩

Result:
no goals

Proof state:
case intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : α
ha : inr a < inl c
hb : inl c < inr b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
exact (not_inl_lt_inr hb).elim

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inr_lt_inr_iff.2 h)

Result:
case intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : α
ha : inr a < inl c
hb : inl c < inr b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : β
ha : inr a < inr c
hb : inr c < inr b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Proof state:
case intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : α
ha : inl a < inl c
hb : inl c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
exact ⟨c, inl_lt_inl_iff.1 ha, inl_lt_inl_iff.1 hb⟩

Result:
no goals

Proof state:
case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : β
ha : inl a < inr c
hb : inr c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
exact (not_inl_lt_inr ha).elim

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem log_two_mul_two_le_sqrt_log_eight : log 2 * 2 ≤ √(log 8)

Proof state:
case h
this : 8 = 2 ^ ↑3
⊢ (log 2 * 2) ^ 2 ≤ ↑3 * log 2

Tactic:
rw [mul_pow, sq (log 2), mul_assoc, mul_comm]

Result:
case h
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ^ 2 * log 2 ≤ ↑3 * log 2

Proof state:
case h
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ^ 2 ≤ ↑3

Tactic:
rw [← le_div_iff₀]

Result:
case h
this : 8 = 2 ^ ↑3
⊢ log 2 ≤ ↑3 / 2 ^ 2

case h
this : 8 = 2 ^ ↑3
⊢ 0 < 2 ^ 2

Proof state:
case h
this : 8 = 2 ^ ↑3
⊢ 0.6931471808 ≤ ↑3 / 2 ^ 2

case h
this : 8 = 2 ^ ↑3
⊢ 0 < 2 ^ 2

Tactic:
all_goals norm_num1

Result:
no goals

Proof state:
⊢ 8 = 2 ^ 3

Tactic:
norm_num

Result:
no goals

Proof state:
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ≤ √(log 8)

Tactic:
rw [this, log_rpow zero_lt_two (3 : ℕ)]

Result:
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ≤ √(↑3 * log 2)

Proof state:
case h
this : 8 = 2 ^ ↑3
⊢ log 2 ≤ ↑3 / 2 ^ 2

Tactic:
apply log_two_lt_d9.le.trans

Result:
case h
this : 8 = 2 ^ ↑3
⊢ 0.6931471808 ≤ ↑3 / 2 ^ 2

Proof state:
case h
this : 8 = 2 ^ ↑3
⊢ 0 < 2 ^ 2

Tactic:
norm_num1

Result:
no goals

Proof state:
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ≤ √(↑3 * log 2)

Tactic:
apply le_sqrt_of_sq_le

Result:
case h
this : 8 = 2 ^ ↑3
⊢ (log 2 * 2) ^ 2 ≤ ↑3 * log 2

Proof state:
⊢ log 2 * 2 ≤ √(log 8)

Tactic:
have : (8 : ℝ) = 2 ^ ((3 : ℕ) : ℝ) := by rw [rpow_natCast]; norm_num

Result:
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ≤ √(log 8)

Proof state:
case h
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ^ 2 * log 2 ≤ ↑3 * log 2

Tactic:
refine mul_le_mul_of_nonneg_right ?_ (log_nonneg one_le_two)

Result:
case h
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ^ 2 ≤ ↑3

Proof state:
case h
this : 8 = 2 ^ ↑3
⊢ log 2 ≤ ↑3 / 2 ^ 2

case h
this : 8 = 2 ^ ↑3
⊢ 0 < 2 ^ 2

Tactic:
on_goal 1 => apply log_two_lt_d9.le.trans

Result:
case h
this : 8 = 2 ^ ↑3
⊢ 0.6931471808 ≤ ↑3 / 2 ^ 2

case h
this : 8 = 2 ^ ↑3
⊢ 0 < 2 ^ 2

Proof state:
⊢ 8 = 2 ^ ↑3

Tactic:
rw [rpow_natCast]

Result:
⊢ 8 = 2 ^ 3
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_ite_nil_left {x : α} [Decidable p] {l : List α} :
    (x ∈ if p then [] else l) ↔ ¬ p ∧ x ∈ l

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : List α
⊢ (x ∈ if p then [] else l) ↔ ¬p ∧ x ∈ l

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Probability/Moments/ComplexMGF.lean
/-- For `z : ℂ` with `z.re ∈ interior (integrableExpSet X μ)`, the derivative of the function
`z' ↦ μ[X ^ n * cexp (z' * X)]` at `z` is `μ[X ^ (n + 1) * cexp (z * X)]`. -/
lemma hasDerivAt_integral_pow_mul_exp (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    HasDerivAt (fun z ↦ μ[fun ω ↦ X ω ^ n * cexp (z * X ω)])
        μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] z

Proof state:
case intro.intro.intro.refine_4.h.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
⊢ ε.re * X ω ≤ z.re * X ω + t / 2 * |X ω|

Tactic:
rw [this, add_re, add_mul]

Result:
case intro.intro.intro.refine_4.h.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
⊢ z.re * X ω + (ε - z).re * X ω ≤ z.re * X ω + t / 2 * |X ω|
-- Mathlib/Data/ENNReal/Inv.lean
theorem zpow_le_of_le {x : ℝ≥0∞} (hx : 1 ≤ x) {a b : ℤ} (h : a ≤ b) : x ^ a ≤ x ^ b

Proof state:
case ofNat.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ Int.ofNat a ≤ x ^ Int.ofNat b

Tactic:
simp only [Int.ofNat_eq_coe, zpow_natCast]

Result:
case ofNat.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ a ≤ x ^ b

Proof state:
case negSucc.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ x ^ Int.negSucc a ≤ x ^ Int.ofNat b

Tactic:
simp only [zpow_negSucc, Int.ofNat_eq_coe, zpow_natCast]

Result:
case negSucc.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ (x ^ (a + 1))⁻¹ ≤ x ^ b

Proof state:
case ofNat.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ x ^ Int.ofNat a ≤ x ^ Int.negSucc b

Tactic:
apply absurd h (not_le_of_gt _)

Result:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ Int.ofNat a > Int.negSucc b

Proof state:
case negSucc.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ (x ^ (a + 1))⁻¹ ≤ x ^ b

Tactic:
refine (ENNReal.inv_le_one.2 ?_).trans ?_ <;> exact one_le_pow_of_one_le' hx _

Result:
no goals

Proof state:
case ofNat.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ a ≤ x ^ b

Tactic:
exact pow_right_mono₀ hx (Int.le_of_ofNat_le_ofNat h)

Result:
no goals

Proof state:
case negSucc.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ Int.negSucc a ≤ x ^ Int.negSucc b

Tactic:
simp only [zpow_negSucc, ENNReal.inv_le_inv]

Result:
case negSucc.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ (b + 1) ≤ x ^ (a + 1)

Proof state:
case negSucc.negSucc.a
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ b + 1 ≤ a + 1

Tactic:
simpa only [← Int.ofNat_le, neg_le_neg_iff, Int.ofNat_add, Int.ofNat_one, Int.negSucc_eq] using
  h

Result:
no goals

Proof state:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ Int.ofNat a > Int.negSucc b

Tactic:
exact lt_of_lt_of_le (Int.negSucc_lt_zero _) (Int.ofNat_nonneg _)

Result:
no goals

Proof state:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℤ
h : a ≤ b
⊢ x ^ a ≤ x ^ b

Tactic:
obtain a | a := a <;> obtain b | b := b

Result:
case ofNat.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ Int.ofNat a ≤ x ^ Int.ofNat b

case ofNat.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ x ^ Int.ofNat a ≤ x ^ Int.negSucc b

case negSucc.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ x ^ Int.negSucc a ≤ x ^ Int.ofNat b

case negSucc.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ Int.negSucc a ≤ x ^ Int.negSucc b

Proof state:
case negSucc.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ (b + 1) ≤ x ^ (a + 1)

Tactic:
apply pow_right_mono₀ hx

Result:
case negSucc.negSucc.a
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ b + 1 ≤ a + 1
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_dblX (P : Fin 3 → R) : (W'.map f).toJacobian.dblX (f ∘ P) = f (W'.dblX P)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toJacobian.dblX (⇑f ∘ P) = f (W'.dblX P)

Tactic:
simp only [dblX, map_dblU, map_negY]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ f (W'.dblU P) ^ 2 - (map W' f).toJacobian.a₁ * f (W'.dblU P) * (⇑f ∘ P) z * ((⇑f ∘ P) y - f (W'.negY P)) -
        (map W' f).toJacobian.a₂ * (⇑f ∘ P) z ^ 2 * ((⇑f ∘ P) y - f (W'.negY P)) ^ 2 -
      2 * (⇑f ∘ P) x * ((⇑f ∘ P) y - f (W'.negY P)) ^ 2 =
    f
      (W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) - W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 -
        2 * P x * (P y - W'.negY P) ^ 2)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ f (W'.dblU P) ^ 2 - (map W' f).toJacobian.a₁ * f (W'.dblU P) * (⇑f ∘ P) z * ((⇑f ∘ P) y - f (W'.negY P)) -
        (map W' f).toJacobian.a₂ * (⇑f ∘ P) z ^ 2 * ((⇑f ∘ P) y - f (W'.negY P)) ^ 2 -
      2 * (⇑f ∘ P) x * ((⇑f ∘ P) y - f (W'.negY P)) ^ 2 =
    f
      (W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) - W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 -
        2 * P x * (P y - W'.negY P) ^ 2)

Tactic:
map_simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem aleph_add_aleph (o₁ o₂ : Ordinal) : ℵ_ o₁ + ℵ_ o₂ = ℵ_ (max o₁ o₂)

Proof state:
o₁ o₂ : Ordinal.{u_1}
⊢ ℵ_ o₁ + ℵ_ o₂ = ℵ_ (o₁ ⊔ o₂)

Tactic:
rw [Cardinal.add_eq_max (aleph0_le_aleph o₁), aleph_max]

Result:
no goals