harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Ordmap/Ordset.lean
theorem pos_size_of_mem {x : α} {t : Ordset α} (h_mem : x ∈ t) : 0 < size t

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
t : Ordset α
h_mem : x ∈ t
⊢ 0 < t.size

Tactic:
simp only [Membership.mem, mem, Bool.decide_eq_true] at h_mem

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
t : Ordset α
h_mem : Ordnode.mem x ↑t = true
⊢ 0 < t.size

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
t : Ordset α
h_mem : x ∈ t
⊢ 0 < t.size

Tactic:
simp? [Membership.mem, mem] at h_mem says
  simp only [Membership.mem, mem, Bool.decide_eq_true] at h_mem

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
t : Ordset α
h_mem : Ordnode.mem x ↑t = true
⊢ 0 < t.size

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
t : Ordset α
h_mem : Ordnode.mem x ↑t = true
⊢ 0 < t.size

Tactic:
apply Ordnode.pos_size_of_mem t.property.sz h_mem

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean
theorem withDensityᵥ_zero : μ.withDensityᵥ (0 : α → E) = 0

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
⊢ ↑(μ.withDensityᵥ 0) s = ↑0 s

Tactic:
erw [withDensityᵥ_apply (integrable_zero α E μ) hs]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, 0 ∂μ = ↑0 s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ μ.withDensityᵥ 0 = 0

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
⊢ ↑(μ.withDensityᵥ 0) s = ↑0 s

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, 0 ∂μ = ↑0 s

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma image_add_right_Ioo (a b c : α) : (Ioo a b).image (· + c) = Ioo (a + c) (b + c)

Proof state:
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ioo a b) = Ioo (a + c) (b + c)

Tactic:
rw [← map_add_right_Ioo, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
lemma IsTuranMaximal.le_iff_eq (hG : G.IsTuranMaximal r) (hH : H.CliqueFree (r + 1)) :
    G ≤ H ↔ G = H

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
H : SimpleGraph V
hG : G.IsTuranMaximal r
hH : H.CliqueFree (r + 1)
⊢ G ≤ H ↔ G = H

Tactic:
exact ⟨fun hGH ↦ edgeFinset_inj.1 <| eq_of_subset_of_card_le
(edgeFinset_subset_edgeFinset.2 hGH) (hG.2 _ hH), le_of_eq⟩

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
H : SimpleGraph V
hG : G.IsTuranMaximal r
hH : H.CliqueFree (r + 1)
⊢ G ≤ H ↔ G = H

Tactic:
classical exact ⟨fun hGH ↦ edgeFinset_inj.1 <| eq_of_subset_of_card_le
  (edgeFinset_subset_edgeFinset.2 hGH) (hG.2 _ hH), le_of_eq⟩

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
lemma limsup_sub_const (F : Filter ι) (f : ι → ℝ≥0∞) (c : ℝ≥0∞) :
    Filter.limsup (fun i ↦ f i - c) F = Filter.limsup f F - c

Proof state:
case inl
ι : Type u_4
f : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ limsup (fun i => f i - c) ⊥ = limsup f ⊥ - c

Tactic:
simp only [limsup_bot, bot_eq_zero', zero_le, tsub_eq_zero_of_le]

Result:
no goals

Proof state:
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ limsup (fun i => f i - c) F = limsup f F - c

Tactic:
rcases F.eq_or_neBot with rfl | _

Result:
case inl
ι : Type u_4
f : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ limsup (fun i => f i - c) ⊥ = limsup f ⊥ - c

case inr
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
h✝ : F.NeBot
⊢ limsup (fun i => f i - c) F = limsup f F - c

Proof state:
case inr
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
h✝ : F.NeBot
⊢ limsup (fun i => f i - c) F = limsup f F - c

Tactic:
exact (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ x - c)
(fun _ _ h ↦ tsub_le_tsub_right h c) (continuous_sub_right c).continuousAt).symm

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem isSome_isSuffixOf?_eq_isSuffixOf [BEq α] (xs ys : List α) :
    (xs.isSuffixOf? ys).isSome = xs.isSuffixOf ys

Proof state:
α : Type u_1
inst✝ : BEq α
xs ys : List α
⊢ (xs.isSuffixOf? ys).isSome = xs.isSuffixOf ys

Tactic:
simp [List.isSuffixOf?, isSuffixOf]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_indicator {a₁ a₂ a₃ : ℝ} (h : a₂ ∈ Icc a₁ a₃) :
    ∫ x in a₁..a₃, indicator {x | x ≤ a₂} f x ∂μ = ∫ x in a₁..a₂, f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ ∫ (x : ℝ) in a₁..a₃, {x | x ≤ a₂}.indicator f x ∂μ = ∫ (x : ℝ) in a₁..a₂, f x ∂μ

Tactic:
rw [integral_of_le h.1, integral_of_le (h.1.trans h.2), integral_indicator,
  Measure.restrict_restrict, this]

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}

E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}

Tactic:
apply measurableSet_Iic

Result:
no goals

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}

Tactic:
exact measurableSet_Iic

Result:
no goals

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}

Tactic:
all_goals apply measurableSet_Iic

Result:
no goals

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
⊢ ∫ (x : ℝ) in a₁..a₃, {x | x ≤ a₂}.indicator f x ∂μ = ∫ (x : ℝ) in a₁..a₂, f x ∂μ

Tactic:
have : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂ := Iic_inter_Ioc_of_le h.2

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ ∫ (x : ℝ) in a₁..a₃, {x | x ≤ a₂}.indicator f x ∂μ = ∫ (x : ℝ) in a₁..a₂, f x ∂μ
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem card_opow_eq_of_omega0_le_right {a b : Ordinal} (ha : 1 < a) (hb : ω ≤ b) :
    (a ^ b).card = max a.card b.card

Proof state:
case a
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ a ≤ a ^ b

Tactic:
exact left_le_opow a (omega0_pos.trans_le hb)

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ (a ^ b).card = a.card ⊔ b.card

Tactic:
apply (card_opow_le_of_omega0_le_right a hb).antisymm (max_le _ _) <;> apply card_le_card

Result:
case a
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ a ≤ a ^ b

case a
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ b ≤ a ^ b

Proof state:
case a
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ b ≤ a ^ b

Tactic:
exact right_le_opow b ha

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem associator_inv_conjugation {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
    f ⊗ g ⊗ h = (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h) ≫ (α_ X' Y' Z').hom

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ f ⊗ g ⊗ h = (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h) ≫ (α_ X' Y' Z').hom

Tactic:
rw [associator_naturality, inv_hom_id_assoc]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma le_expGrowthInf_iff {u : ℕ → ℝ≥0∞} {a : EReal} :
    a ≤ expGrowthInf u ↔ ∀ b < a, ∀ᶠ n : ℕ in atTop, exp (b * n) < u n

Proof state:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y < (u a).log / ↑a) ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, (b * ↑n).exp < u n

Tactic:
refine forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Result:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ b < (u n).log / ↑n ↔ (b * ↑n).exp < u n

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ 0 < ↑n

Tactic:
norm_cast

Result:
no goals

Proof state:
u : ℕ → ℝ≥0∞
a : EReal
⊢ a ≤ expGrowthInf u ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, (b * ↑n).exp < u n

Tactic:
rw [expGrowthInf, Filter.le_liminf_iff]

Result:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y < (u a).log / ↑a) ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, (b * ↑n).exp < u n

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ b * ↑n < (u n).log ↔ (b * ↑n).exp < u n

Tactic:
nth_rw 1 [← EReal.log_exp (b * n)]

Result:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ (b * ↑n).exp.log < (u n).log ↔ (b * ↑n).exp < u n

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ (b * ↑n).exp.log < (u n).log ↔ (b * ↑n).exp < u n

Tactic:
exact logOrderIso.lt_iff_lt

Result:
no goals

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ b < (u n).log / ↑n ↔ (b * ↑n).exp < u n

Tactic:
rw [EReal.lt_div_iff (by norm_cast) (natCast_ne_top n)]

Result:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ b * ↑n < (u n).log ↔ (b * ↑n).exp < u n
-- Mathlib/CategoryTheory/Triangulated/Basic.lean
lemma Triangle.eqToHom_hom₁ {A B : Triangle C} (h : A = B) :
    (eqToHom h).hom₁ = eqToHom (by subst h; rfl)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A : Triangle C
⊢ A.obj₁ = A.obj₁

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
h : A = B
⊢ (eqToHom h).hom₁ = eqToHom ⋯

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A : Triangle C
⊢ (eqToHom ⋯).hom₁ = eqToHom ⋯

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A B : Triangle C
h : A = B
⊢ A.obj₁ = B.obj₁

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A : Triangle C
⊢ A.obj₁ = A.obj₁

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A : Triangle C
⊢ (eqToHom ⋯).hom₁ = eqToHom ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/QuotientGroup/Defs.lean
theorem congr_refl (he : G'.map (MulEquiv.refl G : G →* G) = G' := Subgroup.map_id G') :
    congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G')

Proof state:
case h.mk
G : Type u
inst✝¹ : Group G
G' : Subgroup G
inst✝ : G'.Normal
he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') ⋯
x✝ : G ⧸ G'
x : G
⊢ (congr G' G' (MulEquiv.refl G) he) (Quot.mk (⇑(leftRel G')) x) = (MulEquiv.refl (G ⧸ G')) (Quot.mk (⇑(leftRel G')) x)

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
G' : Subgroup G
inst✝ : G'.Normal
he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') ⋯
⊢ congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G')

Tactic:
ext ⟨x⟩

Result:
case h.mk
G : Type u
inst✝¹ : Group G
G' : Subgroup G
inst✝ : G'.Normal
he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') ⋯
x✝ : G ⧸ G'
x : G
⊢ (congr G' G' (MulEquiv.refl G) he) (Quot.mk (⇑(leftRel G')) x) = (MulEquiv.refl (G ⧸ G')) (Quot.mk (⇑(leftRel G')) x)
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma strictAntiOn_smoothingFn : StrictAntiOn ε (Set.Ioi 1)

Proof state:
⊢ StrictAntiOn ε (Set.Ioi 1)

Tactic:
show StrictAntiOn (fun x => 1 / log x) (Set.Ioi 1)

Result:
⊢ StrictAntiOn (fun x => 1 / log x) (Set.Ioi 1)

Proof state:
⊢ StrictAntiOn (fun x => (log x)⁻¹) (Set.Ioi 1)

Tactic:
refine StrictAntiOn.comp_strictMonoOn inv_strictAntiOn ?log fun _ hx => log_pos hx

Result:
case log

⊢ StrictMonoOn log (Set.Ioi 1)

Proof state:
case log

⊢ StrictMonoOn log (Set.Ioi 1)

Tactic:
refine StrictMonoOn.mono strictMonoOn_log (fun x hx => ?_)

Result:
case log
x : ℝ
hx : x ∈ Set.Ioi 1
⊢ x ∈ Set.Ioi 0

Proof state:
case log
x : ℝ
hx : x ∈ Set.Ioi 1
⊢ x ∈ Set.Ioi 0

Tactic:
exact Set.Ioi_subset_Ioi zero_le_one hx

Result:
no goals

Proof state:
⊢ StrictAntiOn (fun x => 1 / log x) (Set.Ioi 1)

Tactic:
simp_rw [one_div]

Result:
⊢ StrictAntiOn (fun x => (log x)⁻¹) (Set.Ioi 1)
-- Mathlib/Analysis/Convex/Jensen.lean
/-- **Maximum principle** for convex functions on a segment. If a function `f` is convex on the
segment `[x, y]`, then the eventual maximum of `f` on `[x, y]` is at `x` or `y`. -/
lemma ConvexOn.le_max_of_mem_segment (hf : ConvexOn 𝕜 s f) (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ [x -[𝕜] y]) : f z ≤ max (f x) (f y)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
x y z : E
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ [x-[𝕜]y]
⊢ f z ≤ f x ⊔ f y

Tactic:
rw [← convexHull_pair] at hz

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
x y z : E
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ (convexHull 𝕜) {x, y}
⊢ f z ≤ f x ⊔ f y

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
x y z : E
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ (convexHull 𝕜) {x, y}
⊢ f z ≤ f x ⊔ f y

Tactic:
simpa using hf.exists_ge_of_mem_convexHull (pair_subset hx hy) hz

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
@[to_additive] lemma Right.min_le_max_of_mul_le_mul
    [MulLeftMono α] [MulRightStrictMono α]
    (h : a * b ≤ c * d) : min a b ≤ max c d

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
h : a * b ≤ c * d
⊢ (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d

Tactic:
contrapose! h

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
h : (c < a ∧ d < a) ∧ c < b ∧ d < b
⊢ c * d < a * b

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
h : a * b ≤ c * d
⊢ a ⊓ b ≤ c ⊔ d

Tactic:
simp_rw [min_le_iff, le_max_iff]

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
h : a * b ≤ c * d
⊢ (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
h : (c < a ∧ d < a) ∧ c < b ∧ d < b
⊢ c * d < a * b

Tactic:
exact mul_lt_mul_of_lt_of_le h.1.1 h.2.2.le

Result:
no goals
-- Mathlib/RingTheory/Norm/Transitivity.lean
/-- `aux M k` is lower triangular. -/
lemma auxMat_blockTriangular : (auxMat M k).BlockTriangular (· ≠ k) :=
  fun i j lt ↦ by
    simp_rw [lt_iff_not_le, le_Prop_eq, Classical.not_imp, not_not] at lt
    rw [auxMat, of_apply, if_pos lt.2, if_neg lt.1]

Proof state:
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k i j : m
lt : (fun x => x ≠ k) j < (fun x => x ≠ k) i
⊢ auxMat M k i j = 0

Tactic:
simp_rw [lt_iff_not_le, le_Prop_eq, Classical.not_imp, not_not] at lt

Result:
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k i j : m
lt : i ≠ k ∧ j = k
⊢ auxMat M k i j = 0

Proof state:
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k i j : m
lt : i ≠ k ∧ j = k
⊢ auxMat M k i j = 0

Tactic:
rw [auxMat, of_apply, if_pos lt.2, if_neg lt.1]

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.convex_epigraph (hf : ConvexOn 𝕜 s f) :
    Convex 𝕜 { p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2 }

Proof state:
case mk.intro.mk.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).2
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • (x, r) + b • (y, t)).1 ≤ (a • (x, r) + b • (y, t)).2

Tactic:
calc
  f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx hy ha hb hab
  _ ≤ a • r + b • t := by gcongr

Result:
no goals

Proof state:
case mk.intro.mk.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).2
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (x, r) + b • (y, t) ∈ {p | p.1 ∈ s ∧ f p.1 ≤ p.2}

Tactic:
refine ⟨hf.1 hx hy ha hb hab, ?_⟩

Result:
case mk.intro.mk.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).2
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • (x, r) + b • (y, t)).1 ≤ (a • (x, r) + b • (y, t)).2

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
⊢ Convex 𝕜 {p | p.1 ∈ s ∧ f p.1 ≤ p.2}

Tactic:
rintro ⟨x, r⟩ ⟨hx, hr⟩ ⟨y, t⟩ ⟨hy, ht⟩ a b ha hb hab

Result:
case mk.intro.mk.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).2
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (x, r) + b • (y, t) ∈ {p | p.1 ∈ s ∧ f p.1 ≤ p.2}

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).2
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • r + b • t

Tactic:
gcongr

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem star_fuzzy_up : star ‖ up

Proof state:
⊢ star ⧏ up ∧ up ⧏ star

Tactic:
simp only [← PGame.not_le]

Result:
⊢ ¬up ≤ star ∧ ¬star ≤ up

Proof state:
⊢ ¬up ≤ star ∧ ¬star ≤ up

Tactic:
simp [le_iff_forall_lf]

Result:
no goals

Proof state:
⊢ star ‖ up

Tactic:
unfold Fuzzy

Result:
⊢ star ⧏ up ∧ up ⧏ star
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem any_push' [BEq α] {as : Array α} {a : α} {p : α → Bool} (h : stop = as.size + 1) :
    (as.push a).any p 0 stop = (as.any p || p a)

Proof state:
case mk
α : Type u_1
stop : Nat
inst✝ : BEq α
a : α
p : α → Bool
toList✝ : List α
h : stop = { toList := toList✝ }.size + 1
⊢ ({ toList := toList✝ }.push a).any p 0 stop = ({ toList := toList✝ }.any p || p a)

Tactic:
rw [List.push_toArray]

Result:
case mk
α : Type u_1
stop : Nat
inst✝ : BEq α
a : α
p : α → Bool
toList✝ : List α
h : stop = { toList := toList✝ }.size + 1
⊢ (toList✝ ++ [a]).toArray.any p 0 stop = ({ toList := toList✝ }.any p || p a)

Proof state:
α : Type u_1
stop : Nat
inst✝ : BEq α
as : Array α
a : α
p : α → Bool
h : stop = as.size + 1
⊢ (as.push a).any p 0 stop = (as.any p || p a)

Tactic:
cases as

Result:
case mk
α : Type u_1
stop : Nat
inst✝ : BEq α
a : α
p : α → Bool
toList✝ : List α
h : stop = { toList := toList✝ }.size + 1
⊢ ({ toList := toList✝ }.push a).any p 0 stop = ({ toList := toList✝ }.any p || p a)

Proof state:
case mk
α : Type u_1
stop : Nat
inst✝ : BEq α
a : α
p : α → Bool
toList✝ : List α
h : stop = { toList := toList✝ }.size + 1
⊢ (toList✝ ++ [a]).toArray.any p 0 stop = ({ toList := toList✝ }.any p || p a)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem Ico_subset_closure_interior (a b : α) : Ico a b ⊆ closure (interior (Ico a b))

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ Ico a b ⊆ closure (interior (Ico a b))

Tactic:
simpa only [dual_Ioc] using Ioc_subset_closure_interior (OrderDual.toDual b) (OrderDual.toDual a)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
@[simp]
lemma diam_top [Nontrivial α] : (⊤ : SimpleGraph α).diam = 1

Proof state:
α : Type u_1
inst✝ : Nontrivial α
⊢ ⊤.diam = 1

Tactic:
rw [diam, ediam_top, ENat.toNat_one]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem valuedAdicCompletion_eq_valuation (r : R) :
    Valued.v (r : v.adicCompletion K) = v.valuation K r

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ Valued.v ↑r = (valuation K v) ↑r

Tactic:
convert Valued.valuedCompletion_apply (r : K)

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
/-- Given a measure upstairs (i.e., on `α`), and a choice `s` of fundamental domain, there's always
an artificial way to generate a measure downstairs such that the pair satisfies the
`QuotientMeasureEqMeasurePreimage` typeclass. -/
@[to_additive]
lemma IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure
    {s : Set α} (fund_dom_s : IsFundamentalDomain G s ν) :
    QuotientMeasureEqMeasurePreimage ν ((ν.restrict s).map π) where
  projection_respects_measure' t fund_dom_t

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : SMulInvariantMeasure G α ν
inst✝² : Countable G
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
t : Set α
fund_dom_t : IsFundamentalDomain G t ν
⊢ Measure.map (Quotient.mk α_mod_G) (ν.restrict s) = Measure.map (Quotient.mk α_mod_G) (ν.restrict t)

Tactic:
rw [fund_dom_s.quotientMeasure_eq _ fund_dom_t]

Result:
no goals
-- Mathlib/Algebra/Small/Group.lean
@[simp]
lemma equivShrink_symm_smul {R : Type*} [SMul R α] [Small α] (r : R) (x : Shrink α) :
    (equivShrink α).symm (r • x) = r • (equivShrink α).symm x

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : SMul R α
inst✝ : Small.{u_3, u_1} α
r : R
x : Shrink.{u_3, u_1} α
⊢ (equivShrink α).symm (r • x) = r • (equivShrink α).symm x

Tactic:
rw [Equiv.smul_def]

Result:
α : Type u_1
R : Type u_2
inst✝¹ : SMul R α
inst✝ : Small.{u_3, u_1} α
r : R
x : Shrink.{u_3, u_1} α
⊢ (equivShrink α).symm ((equivShrink α).symm.symm (r • (equivShrink α).symm x)) = r • (equivShrink α).symm x

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : SMul R α
inst✝ : Small.{u_3, u_1} α
r : R
x : Shrink.{u_3, u_1} α
⊢ (equivShrink α).symm ((equivShrink α).symm.symm (r • (equivShrink α).symm x)) = r • (equivShrink α).symm x

Tactic:
simp

Result:
no goals