harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/Injectivity.lean
/-- The map `f ↦ LSeries f` is injective on functions `f` such that `f 0 = 0` and the L-series
of `f` converges somewhere. -/
lemma LSeries_injOn : Set.InjOn LSeries {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}

Proof state:
case h.zero
f g : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
⊢ f 0 = g 0

Tactic:
exact hf.1.trans hg.1.symm

Result:
no goals

Proof state:
f g : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
⊢ f = g

Tactic:
ext1 n

Result:
case h
f g : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
n : ℕ
⊢ f n = g n

Proof state:
f : ℕ → ℂ
hf : f ∈ {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}
g : ℕ → ℂ
hg : g ∈ {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}
h : LSeries f = LSeries g
⊢ f = g

Tactic:
simp only [Set.mem_setOf] at hf hg

Result:
f g : ℕ → ℂ
h : LSeries f = LSeries g
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
⊢ f = g

Proof state:
case h.succ
f g : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
n : ℕ
⊢ f (n + 1) = g (n + 1)

Tactic:
exact h _ n.zero_ne_add_one.symm

Result:
no goals

Proof state:
⊢ Set.InjOn LSeries {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}

Tactic:
intro f hf g hg h

Result:
f : ℕ → ℂ
hf : f ∈ {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}
g : ℕ → ℂ
hg : g ∈ {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}
h : LSeries f = LSeries g
⊢ f = g

Proof state:
case h
f g : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
n : ℕ
⊢ f n = g n

Tactic:
cases n with
| zero => exact hf.1.trans hg.1.symm
| succ n => exact h _ n.zero_ne_add_one.symm

Result:
no goals

Proof state:
f g : ℕ → ℂ
h : LSeries f = LSeries g
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
⊢ f = g

Tactic:
replace h := (LSeries_eq_iff_of_abscissaOfAbsConv_lt_top hf.2 hg.2).mp h

Result:
f g : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
⊢ f = g
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma supSum_of_not_univ_mem (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜) :
    supSum 𝒜 = card α * ∑ k ∈ range (card α), (k : ℚ)⁻¹

Proof state:
case ind.inr.succ.intro.intro.intro.intro.h𝒜₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ (image (fun x => s ⊓ x) 𝒜).Nonempty

Tactic:
exact h𝒜.image _

Result:
no goals

Proof state:
case ind.inr.succ.intro.intro.intro.intro.h𝒜
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ #𝒜 < #𝒜 + 1

Tactic:
exact lt_add_one _

Result:
no goals

Proof state:
case ind.inr.succ.intro.intro.intro.intro.h𝒜₂
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ univ ∉ 𝒜

Tactic:
exact fun h ↦ h𝒜₂ (mem_insert_of_mem h)

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem biUnion_pair (a b : α) (s : α → Set β) : ⋃ x ∈ ({a, b} : Set α), s x = s a ∪ s b

Proof state:
α : Type u_1
β : Type u_2
a b : α
s : α → Set β
⊢ ⋃ x ∈ {a, b}, s x = s a ∪ s b

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UInt.lean
theorem USize.size_le : USize.size ≤ 2 ^ 64

Proof state:
⊢ size ≤ 2 ^ 64

Tactic:
rw [size_eq]

Result:
⊢ 2 ^ System.Platform.numBits ≤ 2 ^ 64

Proof state:
⊢ System.Platform.numBits ≤ 64

Tactic:
cases System.Platform.numBits_eq <;> simp_arith [*]

Result:
no goals

Proof state:
⊢ 2 ^ System.Platform.numBits ≤ 2 ^ 64

Tactic:
apply Nat.pow_le_pow_of_le_right (by decide)

Result:
⊢ System.Platform.numBits ≤ 64

Proof state:
⊢ 2 > 0

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[simp] lemma prod'_η_snd : (η (prod' F G)).2 = η G

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod' G)).2 = η G

Tactic:
change G.map (𝟙 _)  ≫ _ = _

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ G.map (𝟙 ((diag C).obj (𝟙_ C)).2) ≫ (η (F.prod G)).2 = η G

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod G)).2 = η G

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ G.map (𝟙 ((diag C).obj (𝟙_ C)).2) ≫ (η (F.prod G)).2 = η G

Tactic:
rw [Functor.map_id, Category.id_comp]

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod G)).2 = η G
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem map_mul_inv [Group α] [DivisionMonoid β] (f : α →* β) (g h : α) :
    f (g * h⁻¹) = f g * (f h)⁻¹

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : DivisionMonoid β
f : α →* β
g h : α
⊢ f (g * h⁻¹) = f g * (f h)⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isClique_map_iff {f : α ↪ β} {t : Set β} :
    (G.map f).IsClique t ↔ t.Subsingleton ∨ ∃ (s : Set α), G.IsClique s ∧ f '' s = t

Proof state:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
⊢ (SimpleGraph.map f G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t

Tactic:
simp [isClique_map_iff_of_nontrivial ht, ht.not_subsingleton]

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Subsingleton
⊢ (SimpleGraph.map f G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t

Tactic:
simp [IsClique.of_subsingleton, ht]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
⊢ (SimpleGraph.map f G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t

Tactic:
obtain (ht | ht) := t.subsingleton_or_nontrivial

Result:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Subsingleton
⊢ (SimpleGraph.map f G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t

case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
⊢ (SimpleGraph.map f G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.mem_smul (hs : StarConvex 𝕜 0 s) (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) :
    x ∈ t • s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ t⁻¹ • x ∈ s

Tactic:
exact hs.smul_mem hx (by positivity) (inv_le_one_of_one_le₀ ht)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ 0 ≤ t⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ x ∈ t • s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ t⁻¹ • x ∈ s
-- Mathlib/Probability/CondVar.lean
lemma condVar_ae_le_condExp_sq (hm : m ≤ m₀) [IsFiniteMeasure μ] (hX : MemLp X 2 μ) :
    Var[X; μ | m] ≤ᵐ[μ] μ[X ^ 2 | m]

Proof state:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
ω : Ω
hω : Var[X; μ | m] ω = (μ[X ^ 2|m]) ω - (μ[X|m]) ω ^ 2
⊢ Var[X; μ | m] ω ≤ (μ[X ^ 2|m]) ω

Tactic:
nlinarith

Result:
no goals

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ Var[X; μ | m] ≤ᶠ[ae μ] μ[X ^ 2|m]

Tactic:
filter_upwards [condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX] with ω hω

Result:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
ω : Ω
hω : Var[X; μ | m] ω = (μ[X ^ 2|m] - μ[X|m] ^ 2) ω
⊢ Var[X; μ | m] ω ≤ (μ[X ^ 2|m]) ω

Proof state:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
ω : Ω
hω : Var[X; μ | m] ω = (μ[X ^ 2|m] - μ[X|m] ^ 2) ω
⊢ Var[X; μ | m] ω ≤ (μ[X ^ 2|m]) ω

Tactic:
dsimp at hω

Result:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
ω : Ω
hω : Var[X; μ | m] ω = (μ[X ^ 2|m]) ω - (μ[X|m]) ω ^ 2
⊢ Var[X; μ | m] ω ≤ (μ[X ^ 2|m]) ω
-- Mathlib/Data/PNat/Xgcd.lean
theorem flip_v : (flip u).v = u.v.swap

Proof state:
u : XgcdType
⊢ (↑u.z * ↑u.b + u.y * ↑u.a, u.x * ↑u.b + ↑u.w * ↑u.a) = (u.y * ↑u.a + ↑u.z * ↑u.b, ↑u.w * ↑u.a + u.x * ↑u.b)

Tactic:
ext

Result:
case fst
u : XgcdType
⊢ (↑u.z * ↑u.b + u.y * ↑u.a, u.x * ↑u.b + ↑u.w * ↑u.a).1 = (u.y * ↑u.a + ↑u.z * ↑u.b, ↑u.w * ↑u.a + u.x * ↑u.b).1

case snd
u : XgcdType
⊢ (↑u.z * ↑u.b + u.y * ↑u.a, u.x * ↑u.b + ↑u.w * ↑u.a).2 = (u.y * ↑u.a + ↑u.z * ↑u.b, ↑u.w * ↑u.a + u.x * ↑u.b).2

Proof state:
case fst
u : XgcdType
⊢ ↑u.z * ↑u.b + u.y * ↑u.a = u.y * ↑u.a + ↑u.z * ↑u.b

Tactic:
ring

Result:
no goals

Proof state:
case snd
u : XgcdType
⊢ (↑u.z * ↑u.b + u.y * ↑u.a, u.x * ↑u.b + ↑u.w * ↑u.a).2 = (u.y * ↑u.a + ↑u.z * ↑u.b, ↑u.w * ↑u.a + u.x * ↑u.b).2

Tactic:
simp only

Result:
case snd
u : XgcdType
⊢ u.x * ↑u.b + ↑u.w * ↑u.a = ↑u.w * ↑u.a + u.x * ↑u.b

Proof state:
case snd
u : XgcdType
⊢ u.x * ↑u.b + ↑u.w * ↑u.a = ↑u.w * ↑u.a + u.x * ↑u.b

Tactic:
ring

Result:
no goals

Proof state:
u : XgcdType
⊢ u.flip.v = u.v.swap

Tactic:
dsimp [v]

Result:
u : XgcdType
⊢ (↑u.z * ↑u.b + u.y * ↑u.a, u.x * ↑u.b + ↑u.w * ↑u.a) = (u.y * ↑u.a + ↑u.z * ↑u.b, ↑u.w * ↑u.a + u.x * ↑u.b)

Proof state:
case fst
u : XgcdType
⊢ (↑u.z * ↑u.b + u.y * ↑u.a, u.x * ↑u.b + ↑u.w * ↑u.a).1 = (u.y * ↑u.a + ↑u.z * ↑u.b, ↑u.w * ↑u.a + u.x * ↑u.b).1

Tactic:
simp only

Result:
case fst
u : XgcdType
⊢ ↑u.z * ↑u.b + u.y * ↑u.a = u.y * ↑u.a + ↑u.z * ↑u.b
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
lemma isClosed_iff_isLower : IsClosed s ↔ IsLowerSet s

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsClosed s ↔ IsLowerSet s

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_isUpperSet,
  isLowerSet_compl.symm, compl_compl]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_mono_measure (f : α → ε) (hμν : ν ≤ μ) (hq : 0 ≤ q) :
    eLpNorm' f q ν ≤ eLpNorm' f q μ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hq : 0 ≤ q
⊢ eLpNorm' f q ν ≤ eLpNorm' f q μ

Tactic:
simp_rw [eLpNorm']

Result:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hq : 0 ≤ q
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂ν) ^ (1 / q) ≤ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)

Proof state:
case h₁
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hq : 0 ≤ q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂ν ≤ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ

Tactic:
exact lintegral_mono' hμν le_rfl

Result:
no goals

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hq : 0 ≤ q
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂ν) ^ (1 / q) ≤ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)

Tactic:
gcongr

Result:
case h₁
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hq : 0 ≤ q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂ν ≤ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
lemma isTheta_deriv_rpow_const_atTop {p : ℝ} (hp : p ≠ 0) :
    deriv (fun (x : ℝ) => x ^ p) =Θ[atTop] fun x => x ^ (p-1)

Proof state:
case h
p : ℝ
hp : p ≠ 0
x : ℝ
hx : x ≠ 0
⊢ deriv (fun x => x ^ p) x = p * x ^ (p - 1)

Tactic:
rw [Real.deriv_rpow_const (Or.inl hx)]

Result:
no goals

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =Θ[atTop] fun x => x ^ (p - 1)

Tactic:
calc deriv (fun (x : ℝ) => x ^ p) =ᶠ[atTop] fun x => p * x ^ (p - 1) := by
            filter_upwards [eventually_ne_atTop 0] with x hx
            rw [Real.deriv_rpow_const (Or.inl hx)]
     _ =Θ[atTop] fun x => x ^ (p-1) :=
            Asymptotics.IsTheta.const_mul_left hp Asymptotics.isTheta_rfl

Result:
no goals

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =ᶠ[atTop] fun x => p * x ^ (p - 1)

Tactic:
filter_upwards [eventually_ne_atTop 0] with x hx

Result:
case h
p : ℝ
hp : p ≠ 0
x : ℝ
hx : x ≠ 0
⊢ deriv (fun x => x ^ p) x = p * x ^ (p - 1)
-- Mathlib/Computability/Partrec.lean
theorem fix_aux {α σ} (f : α →. σ ⊕ α) (a : α) (b : σ) :
    let F : α → ℕ →. σ ⊕ α := fun a n =>
      n.rec (some (Sum.inr a)) fun _ IH => IH.bind fun s => Sum.casesOn s (fun _ => Part.some s) f
    (∃ n : ℕ,
        ((∃ b' : σ, Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b : α, Sum.inr b ∈ F a m) ∧
          Sum.inl b ∈ F a n) ↔
      b ∈ PFun.fix f a

Proof state:
case refine_2.inr.intro.intro.intro.intro
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂ : b ∈ f.fix a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ f.fix a₃
n : ℕ
hn₁ : Sum.inl b ∈ F a n
hn₂ : ∀ m < n, k.succ ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
m : ℕ
mn : m < n
km : k ≤ m
⊢ ∃ a₂, Sum.inr a₂ ∈ F a m

Tactic:
rcases km.lt_or_eq_dec with km | km

Result:
case refine_2.inr.intro.intro.intro.intro.inl
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂ : b ∈ f.fix a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ f.fix a₃
n : ℕ
hn₁ : Sum.inl b ∈ F a n
hn₂ : ∀ m < n, k.succ ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
m : ℕ
mn : m < n
km✝ : k ≤ m
km : k < m
⊢ ∃ a₂, Sum.inr a₂ ∈ F a m

case refine_2.inr.intro.intro.intro.intro.inr
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂ : b ∈ f.fix a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ f.fix a₃
n : ℕ
hn₁ : Sum.inl b ∈ F a n
hn₂ : ∀ m < n, k.succ ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
m : ℕ
mn : m < n
km✝ : k ≤ m
km : k = m
⊢ ∃ a₂, Sum.inr a₂ ∈ F a m

Proof state:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
⊢ let F := fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n;
  (∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n) ↔ b ∈ f.fix a

Tactic:
intro F

Result:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n
⊢ (∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n) ↔ b ∈ f.fix a
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem ruzsa_triangle_inequality_mul_div_div (A B C : Finset G) :
    #(A * C) * #B ≤ #(A / B) * #(B / C)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C) * #B ≤ #(A / B) * #(B / C)

Tactic:
rw [div_eq_mul_inv, ← card_inv B, ← card_inv (B / C), inv_div', div_inv_eq_mul]

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C) * #B⁻¹ ≤ #(A * B⁻¹) * #(B⁻¹ * C)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C) * #B⁻¹ ≤ #(A * B⁻¹) * #(B⁻¹ * C)

Tactic:
exact ruzsa_triangle_inequality_mul_mul_mul _ _ _

Result:
no goals
-- Mathlib/Topology/StoneCech.lean
theorem induced_topology_pure :
    TopologicalSpace.induced (pure : α → Ultrafilter α) Ultrafilter.topologicalSpace = ⊥

Proof state:
case h
α : Type u
⊢ ∀ (x : α), IsOpen {x}

Tactic:
intro x

Result:
case h
α : Type u
x : α
⊢ IsOpen {x}

Proof state:
case right
α : Type u
x : α
⊢ pure ⁻¹' {u | {x} ∈ u} = {x}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
⊢ induced pure Ultrafilter.topologicalSpace = ⊥

Tactic:
apply eq_bot_of_singletons_open

Result:
case h
α : Type u
⊢ ∀ (x : α), IsOpen {x}

Proof state:
case h
α : Type u
x : α
⊢ IsOpen {x}

Tactic:
use { u : Ultrafilter α | {x} ∈ u }, ultrafilter_isOpen_basic _

Result:
case right
α : Type u
x : α
⊢ pure ⁻¹' {u | {x} ∈ u} = {x}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem succ_min_succ (x y) : min (succ x) (succ y) = succ (min x y)

Proof state:
case inl
x y : Nat
h : x ≤ y
⊢ min x.succ y.succ = (min x y).succ

Tactic:
rw [Nat.min_eq_left h, Nat.min_eq_left (Nat.succ_le_succ h)]

Result:
no goals

Proof state:
x y : Nat
⊢ min x.succ y.succ = (min x y).succ

Tactic:
cases Nat.le_total x y with
| inl h => rw [Nat.min_eq_left h, Nat.min_eq_left (Nat.succ_le_succ h)]
| inr h => rw [Nat.min_eq_right h, Nat.min_eq_right (Nat.succ_le_succ h)]

Result:
no goals

Proof state:
case inr
x y : Nat
h : y ≤ x
⊢ min x.succ y.succ = (min x y).succ

Tactic:
rw [Nat.min_eq_right h, Nat.min_eq_right (Nat.succ_le_succ h)]

Result:
no goals
-- Mathlib/Topology/SeparatedMap.lean
theorem discreteTopology_iff_locallyInjective (y : Y) :
    DiscreteTopology X ↔ IsLocallyInjective fun _ : X ↦ y

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
⊢ DiscreteTopology X ↔ IsLocallyInjective fun x => y

Tactic:
rw [discreteTopology_iff_singleton_mem_nhds, isLocallyInjective_iff_nhds]

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
⊢ (∀ (x : X), {x} ∈ 𝓝 x) ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
x : X
x✝ : ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn (fun x => y) U
⊢ {x} ∈ 𝓝 x

Tactic:
convert hU

Result:
case h.e'_5
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
x : X
x✝ : ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn (fun x => y) U
⊢ {x} = U

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
⊢ (∀ (x : X), {x} ∈ 𝓝 x) ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U

Tactic:
refine forall_congr' fun x ↦ ⟨fun h ↦ ⟨{x}, h, Set.injOn_singleton _ _⟩, fun ⟨U, hU, inj⟩ ↦ ?_⟩

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
x : X
x✝ : ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn (fun x => y) U
⊢ {x} ∈ 𝓝 x

Proof state:
case h.e'_5.h
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
x : X
x✝ : ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn (fun x => y) U
x' : X
⊢ x' ∈ {x} ↔ x' ∈ U

Tactic:
refine ⟨?_, fun h ↦ inj h (mem_of_mem_nhds hU) rfl⟩

Result:
case h.e'_5.h
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
x : X
x✝ : ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn (fun x => y) U
x' : X
⊢ x' ∈ {x} → x' ∈ U

Proof state:
case h.e'_5.h
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
x : X
x✝ : ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn (fun x => y) U
x' : X
⊢ x' ∈ {x} → x' ∈ U

Tactic:
rintro rfl

Result:
case h.e'_5.h
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
U : Set X
inj : Set.InjOn (fun x => y) U
x' : X
x✝ : ∃ U ∈ 𝓝 x', Set.InjOn (fun x => y) U
hU : U ∈ 𝓝 x'
⊢ x' ∈ U

Proof state:
case h.e'_5.h
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
U : Set X
inj : Set.InjOn (fun x => y) U
x' : X
x✝ : ∃ U ∈ 𝓝 x', Set.InjOn (fun x => y) U
hU : U ∈ 𝓝 x'
⊢ x' ∈ U

Tactic:
exact mem_of_mem_nhds hU

Result:
no goals

Proof state:
case h.e'_5
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
x : X
x✝ : ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn (fun x => y) U
⊢ {x} = U

Tactic:
ext x'

Result:
case h.e'_5.h
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
x : X
x✝ : ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn (fun x => y) U
x' : X
⊢ x' ∈ {x} ↔ x' ∈ U