harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_Ico_le_of_lt_one [LinearOrderedField α] {x : α} (hx : 0 ≤ x) (h'x : x < 1)
    {m n : ℕ} : ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)

Proof state:
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ 0 ≤ x ^ m / (1 - x)

Tactic:
apply div_nonneg (pow_nonneg hx _)

Result:
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ 0 ≤ 1 - x

Proof state:
case inl
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : m ≤ n
⊢ (x ^ m - x ^ n) / (1 - x) ≤ x ^ m / (1 - x)

Tactic:
apply div_le_div₀ (pow_nonneg hx _) _ (sub_pos.2 h'x) le_rfl

Result:
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : m ≤ n
⊢ x ^ m - x ^ n ≤ x ^ m

Proof state:
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : m ≤ n
⊢ x ^ m - x ^ n ≤ x ^ m

Tactic:
simpa using pow_nonneg hx _

Result:
no goals

Proof state:
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ ¬m < n

Tactic:
simpa using hmn.le

Result:
no goals

Proof state:
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)

Tactic:
rcases le_or_lt m n with (hmn | hmn)

Result:
case inl
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : m ≤ n
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)

case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)

Proof state:
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ 0 ≤ 1 - x

Tactic:
simpa using h'x.le

Result:
no goals

Proof state:
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)

Tactic:
rw [Ico_eq_empty, sum_empty]

Result:
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ 0 ≤ x ^ m / (1 - x)

case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ ¬m < n

Proof state:
case inl
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : m ≤ n
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)

Tactic:
rw [geom_sum_Ico' h'x.ne hmn]

Result:
case inl
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : m ≤ n
⊢ (x ^ m - x ^ n) / (1 - x) ≤ x ^ m / (1 - x)
-- Mathlib/Data/Fintype/Card.lean
theorem set_fintype_card_eq_univ_iff [Fintype α] (s : Set α) [Fintype s] :
    Fintype.card s = Fintype.card α ↔ s = Set.univ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ Fintype.card ↑s = Fintype.card α ↔ s = Set.univ

Tactic:
rw [← Set.toFinset_card, Finset.card_eq_iff_eq_univ, ← Set.toFinset_univ, Set.toFinset_inj]

Result:
no goals
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem mongePoint_eq_affineCombination_of_pointsWithCircumcenter {n : ℕ}
    (s : Simplex ℝ P (n + 2)) :
    s.mongePoint =
      (univ : Finset (PointsWithCircumcenterIndex (n + 2))).affineCombination ℝ
        s.pointsWithCircumcenter (mongePointWeightsWithCircumcenter n)

Proof state:
case h.e_6.h.h.pointIndex
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
hn1 : ↑n + 1 ≠ 0
a✝ : Fin (n + 2 + 1)
hn3 : ↑n + 2 + 1 ≠ 0
⊢ ↑(n + 2 + 1) / ↑(n + 1) * (↑(n + 2 + 1))⁻¹ = (↑(n + 1))⁻¹

Tactic:
field_simp [hn1, hn3, mul_comm]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
⊢ s.mongePoint = (affineCombination ℝ univ s.pointsWithCircumcenter) (mongePointWeightsWithCircumcenter n)

Tactic:
rw [mongePoint_eq_smul_vsub_vadd_circumcenter,
  centroid_eq_affineCombination_of_pointsWithCircumcenter,
  circumcenter_eq_affineCombination_of_pointsWithCircumcenter, affineCombination_vsub,
  ← LinearMap.map_smul, weightedVSub_vadd_affineCombination]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
⊢ (affineCombination ℝ univ s.pointsWithCircumcenter)
      ((↑(n + 2 + 1) / ↑(n + 2 - 1)) •
          (centroidWeightsWithCircumcenter univ - circumcenterWeightsWithCircumcenter (n + 2)) +
        circumcenterWeightsWithCircumcenter (n + 2)) =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (mongePointWeightsWithCircumcenter n)
-- Mathlib/Analysis/Convex/Deriv.lean
/-- If `f : ℝ → ℝ` is convex on `S` and left-differentiable at `y ∈ S`, then the slope of any secant
line with right endpoint at `y` is bounded above by the left derivative of `f` at `y`. -/
lemma slope_le_of_hasDerivWithinAt_Iio (hfc : ConvexOn ℝ S f)
    (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Iio y) y) :
    slope f x y ≤ f'

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ ∀ᶠ (c : ℝ) in 𝓝[<] y, slope f x y ≤ slope f y c

Tactic:
simp_rw [eventually_nhdsWithin_iff, slope_comm f x y, slope_def_field]

Result:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 y, x_1 ∈ Iio y → (f x - f y) / (x - y) ≤ (f x_1 - f y) / (x_1 - y)

Proof state:
case h
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
t : ℝ
ht : x < t
ht' : t < y
⊢ t ∈ S

Tactic:
exact hfc.1.ordConnected.out hx hy ⟨ht.le, ht'.le⟩

Result:
no goals

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ slope f x y ≤ f'

Tactic:
apply ge_of_tendsto <| (hasDerivWithinAt_iff_tendsto_slope' not_mem_Iio_self).mp hf'

Result:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ ∀ᶠ (c : ℝ) in 𝓝[<] y, slope f x y ≤ slope f y c

Proof state:
case h
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
t : ℝ
ht : x < t
ht' : t < y
⊢ (f x - f y) / (x - y) ≤ (f t - f y) / (t - y)

Tactic:
refine hfc.secant_mono hy hx (?_ : t ∈ S) hxy.ne ht'.ne ht.le

Result:
case h
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
t : ℝ
ht : x < t
ht' : t < y
⊢ t ∈ S

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 y, x_1 ∈ Iio y → (f x - f y) / (x - y) ≤ (f x_1 - f y) / (x_1 - y)

Tactic:
filter_upwards [eventually_gt_nhds hxy] with t ht (ht' : t < y)

Result:
case h
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
t : ℝ
ht : x < t
ht' : t < y
⊢ (f x - f y) / (x - y) ≤ (f t - f y) / (t - y)
-- Mathlib/.lake/packages/batteries/Batteries/Classes/SatisfiesM.lean
theorem SatisfiesM_Except_eq : SatisfiesM (m := Except ε) p x ↔ ∀ a, x = .ok a → p a :=
  ⟨by revert x; intro | .ok _, ⟨.ok ⟨_, h⟩, rfl⟩, _, rfl => exact h,
   fun h => match x with | .ok a => ⟨.ok ⟨a, h _ rfl⟩, rfl⟩ | .error e => ⟨.error e, rfl⟩⟩

Proof state:
ε : Type u_1
α✝ : Type u_2
p : α✝ → Prop
⊢ ∀ {x : Except ε α✝}, SatisfiesM p x → ∀ (a : α✝), x = Except.ok a → p a

Tactic:
intro | .ok _, ⟨.ok ⟨_, h⟩, rfl⟩, _, rfl => exact h

Result:
no goals

Proof state:
ε : Type u_1
α✝ : Type u_2
p : α✝ → Prop
x✝³ : Except ε α✝
x✝² : SatisfiesM p x✝³
x✝¹ : α✝
x✝ : x✝³ = Except.ok x✝¹
val✝ : α✝
h : p val✝
⊢ p ⟨val✝, h⟩.val

Tactic:
exact h

Result:
no goals

Proof state:
ε : Type u_1
α✝ : Type u_2
p : α✝ → Prop
x : Except ε α✝
⊢ SatisfiesM p x → ∀ (a : α✝), x = Except.ok a → p a

Tactic:
revert x

Result:
ε : Type u_1
α✝ : Type u_2
p : α✝ → Prop
⊢ ∀ {x : Except ε α✝}, SatisfiesM p x → ∀ (a : α✝), x = Except.ok a → p a
-- Mathlib/Probability/Kernel/Disintegration/Unique.lean
theorem eq_condKernel_of_kernel_eq_compProd [CountableOrCountablyGenerated α β]
    {ρ : Kernel α (β × Ω)} [IsFiniteKernel ρ] {κ : Kernel (α × β) Ω} [IsFiniteKernel κ]
    (hκ : Kernel.fst ρ ⊗ₖ κ = ρ) (a : α) :
    ∀ᵐ x ∂(Kernel.fst ρ a), κ (a, x) = Kernel.condKernel ρ (a, x)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : CountableOrCountablyGenerated α β
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
⊢ ∀ᵐ (x : β) ∂ρ.fst a, κ (a, x) = ρ.condKernel (a, x)

Tactic:
filter_upwards [Kernel.condKernel_apply_eq_condKernel ρ a,
  Kernel.apply_eq_measure_condKernel_of_compProd_eq hκ a] with a h1 h2

Result:
case h
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : CountableOrCountablyGenerated α β
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a✝ : α
a : β
h1 : ρ.condKernel (a✝, a) = (ρ a✝).condKernel a
h2 : κ (a✝, a) = (ρ a✝).condKernel a
⊢ κ (a✝, a) = ρ.condKernel (a✝, a)

Proof state:
case h
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : CountableOrCountablyGenerated α β
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a✝ : α
a : β
h1 : ρ.condKernel (a✝, a) = (ρ a✝).condKernel a
h2 : κ (a✝, a) = (ρ a✝).condKernel a
⊢ κ (a✝, a) = ρ.condKernel (a✝, a)

Tactic:
rw [h1, h2]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem adj_incidenceSet_inter {v : V} {e : Sym2 V} (he : e ∈ G.edgeSet) (h : v ∈ e) :
    G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) = {e}

Proof state:
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
⊢ G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) = {e}

Tactic:
ext e'

Result:
case h
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
⊢ e' ∈ G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) ↔ e' ∈ {e}

Proof state:
case h.refine_2
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
⊢ e' = e → (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'

Tactic:
rintro rfl

Result:
case h.refine_2
V : Type u
G : SimpleGraph V
v : V
e' : Sym2 V
he : e' ∈ G.edgeSet
h : v ∈ e'
⊢ (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'

Proof state:
case h
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
⊢ e' ∈ G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) ↔ e' ∈ {e}

Tactic:
simp only [incidenceSet, Set.mem_sep_iff, Set.mem_inter_iff, Set.mem_singleton_iff]

Result:
case h
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
⊢ (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e' ↔ e' = e

Proof state:
case h.refine_2
V : Type u
G : SimpleGraph V
v : V
e' : Sym2 V
he : e' ∈ G.edgeSet
h : v ∈ e'
⊢ (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'

Tactic:
exact ⟨⟨he, h⟩, he, Sym2.other_mem _⟩

Result:
no goals

Proof state:
case h
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
⊢ (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e' ↔ e' = e

Tactic:
refine ⟨fun h' => ?_, ?_⟩

Result:
case h.refine_1
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
⊢ e' = e

case h.refine_2
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
⊢ e' = e → (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'

Proof state:
case h.refine_1
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
⊢ e' = s(v, Sym2.Mem.other h)

Tactic:
exact (Sym2.mem_and_mem_iff (edge_other_ne G he h).symm).mp ⟨h'.1.2, h'.2.2⟩

Result:
no goals

Proof state:
case h.refine_1
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
⊢ e' = e

Tactic:
rw [← Sym2.other_spec h]

Result:
case h.refine_1
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
⊢ e' = s(v, Sym2.Mem.other h)
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma rnDeriv_le_one_iff_le [HaveLebesgueDecomposition μ ν] [SigmaFinite ν] (hμν : μ ≪ ν) :
    μ.rnDeriv ν ≤ᵐ[ν] 1 ↔ μ ≤ ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν ≤ᶠ[ae ν] 1
s : Set α
⊢ μ s ≤ ν s

Tactic:
rw [← withDensity_rnDeriv_eq _ _ hμν, withDensity_apply', ← setLIntegral_one]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν ≤ᶠ[ae ν] 1
s : Set α
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν ≤ ∫⁻ (x : α) in s, 1 ∂ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv ν ≤ᶠ[ae ν] 1 ↔ μ ≤ ν

Tactic:
refine ⟨fun h s ↦ ?_, fun h ↦ rnDeriv_le_one_of_le h⟩

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν ≤ᶠ[ae ν] 1
s : Set α
⊢ μ s ≤ ν s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν ≤ᶠ[ae ν] 1
s : Set α
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν ≤ ∫⁻ (x : α) in s, 1 ∂ν

Tactic:
exact setLIntegral_mono_ae aemeasurable_const (h.mono fun _ hh _ ↦ hh)

Result:
no goals
-- Mathlib/Data/Prod/TProd.lean
theorem elim_preimage_pi [DecidableEq ι] {l : List ι} (hnd : l.Nodup) (h : ∀ i, i ∈ l)
    (t : ∀ i, Set (α i)) : TProd.elim' h ⁻¹' pi univ t = Set.tprod l t

Proof state:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ (fun x => TProd.mk l (TProd.elim' h x)) ⁻¹' Set.tprod l t = Set.tprod l t

Tactic:
simp only [TProd.mk_elim hnd h]

Result:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ (fun x => x) ⁻¹' Set.tprod l t = Set.tprod l t

Proof state:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
⊢ TProd.elim' h ⁻¹' univ.pi t = Set.tprod l t

Tactic:
have h2 : { i | i ∈ l } = univ := by
  ext i
  simp [h]

Result:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ TProd.elim' h ⁻¹' univ.pi t = Set.tprod l t

Proof state:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ (fun x => x) ⁻¹' Set.tprod l t = Set.tprod l t

Tactic:
dsimp

Result:
no goals

Proof state:
case h
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
i : ι
⊢ i ∈ {i | i ∈ l} ↔ i ∈ univ

Tactic:
simp [h]

Result:
no goals

Proof state:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ TProd.elim' h ⁻¹' univ.pi t = Set.tprod l t

Tactic:
rw [← h2, ← mk_preimage_tprod, preimage_preimage]

Result:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ (fun x => TProd.mk l (TProd.elim' h x)) ⁻¹' Set.tprod l t = Set.tprod l t

Proof state:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
⊢ {i | i ∈ l} = univ

Tactic:
ext i

Result:
case h
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
i : ι
⊢ i ∈ {i | i ∈ l} ↔ i ∈ univ
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem AnalyticAt.iterated_deriv [CompleteSpace F] (h : AnalyticAt 𝕜 f x) (n : ℕ) :
    AnalyticAt 𝕜 (deriv^[n] f) x

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
n : ℕ
⊢ AnalyticAt 𝕜 (deriv^[n] f) x

Tactic:
induction n with
| zero => exact h
| succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
n : ℕ
IH : AnalyticAt 𝕜 (deriv^[n] f) x
⊢ AnalyticAt 𝕜 (deriv^[n + 1] f) x

Tactic:
simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (deriv^[0] f) x

Tactic:
exact h

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem isGLB_iff_isLeast [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) :
    IsGLB (s : Set α) i ↔ IsLeast (↑s) i

Proof state:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
⊢ i = s.min' hs

Tactic:
rw [IsGLB, IsGreatest, mem_lowerBounds, mem_upperBounds] at his

Result:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : (∀ x ∈ ↑s, i ≤ x) ∧ ∀ x ∈ lowerBounds ↑s, x ≤ i
⊢ i = s.min' hs

Proof state:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
⊢ IsLeast (↑s) i

Tactic:
suffices i = min' s hs by
  rw [this]
  exact isLeast_min' s hs

Result:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
⊢ i = s.min' hs

Proof state:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : (∀ x ∈ ↑s, i ≤ x) ∧ ∀ x ∈ lowerBounds ↑s, x ≤ i
⊢ i = s.min' hs

Tactic:
exact le_antisymm (his.1 (Finset.min' s hs) (Finset.min'_mem s hs)) (his.2 _ (Finset.min'_le s))

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
this : i = s.min' hs
⊢ IsLeast (↑s) (s.min' hs)

Tactic:
exact isLeast_min' s hs

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
this : i = s.min' hs
⊢ IsLeast (↑s) i

Tactic:
rw [this]

Result:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
this : i = s.min' hs
⊢ IsLeast (↑s) (s.min' hs)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
⊢ IsGLB (↑s) i ↔ IsLeast (↑s) i

Tactic:
refine ⟨fun his => ?_, IsLeast.isGLB⟩

Result:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
⊢ IsLeast (↑s) i
-- Mathlib/Order/LiminfLimsup.lean
theorem _root_.OrderIso.apply_blimsup [CompleteLattice γ] (e : α ≃o γ) :
    e (blimsup u f p) = blimsup (e ∘ u) f p

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ e (blimsup u f p) = blimsup (⇑e ∘ u) f p

Tactic:
simp only [blimsup_eq, map_sInf, Function.comp_apply, e.image_eq_preimage,
  Set.preimage_setOf_eq, e.le_symm_apply]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem ofMulEquivOfLocalizations_id : f.ofMulEquivOfLocalizations (MulEquiv.refl N) = f

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
⊢ f.ofMulEquivOfLocalizations (MulEquiv.refl N) = f

Tactic:
ext

Result:
case h
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x✝ : M
⊢ (f.ofMulEquivOfLocalizations (MulEquiv.refl N)).toMap x✝ = f.toMap x✝

Proof state:
case h
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x✝ : M
⊢ (f.ofMulEquivOfLocalizations (MulEquiv.refl N)).toMap x✝ = f.toMap x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_coe_eq_self_iff {θ : ℝ} : (θ : Angle).toReal = θ ↔ -π < θ ∧ θ ≤ π

Proof state:
θ : ℝ
⊢ (↑θ).toReal = θ ↔ -π < θ ∧ θ ≤ π

Tactic:
rw [toReal_coe, toIocMod_eq_self two_pi_pos]

Result:
θ : ℝ
⊢ θ ∈ Set.Ioc (-π) (-π + 2 * π) ↔ -π < θ ∧ θ ≤ π

Proof state:
θ : ℝ
⊢ θ ∈ Set.Ioc (-π) π ↔ -π < θ ∧ θ ≤ π

Tactic:
rfl

Result:
no goals

Proof state:
θ : ℝ
⊢ θ ∈ Set.Ioc (-π) (-π + 2 * π) ↔ -π < θ ∧ θ ≤ π

Tactic:
ring_nf

Result:
θ : ℝ
⊢ θ ∈ Set.Ioc (-π) π ↔ -π < θ ∧ θ ≤ π
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem exists_mem_factors_of_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :
    p ∣ a → ∃ q ∈ factors a, p ~ᵤ q := fun ⟨b, hb⟩ =>
  have hb0 : b ≠ 0 := fun hb0 => by simp_all
  have : Multiset.Rel Associated (p ::ₘ factors b) (factors a) :=
    factors_unique
      (fun _ hx => (Multiset.mem_cons.1 hx).elim (fun h => h.symm ▸ hp) (irreducible_of_factor _))
      irreducible_of_factor
      (Associated.symm <|
        calc
          Multiset.prod (factors a) ~ᵤ a := factors_prod ha0
          _ = p * b := hb
          _ ~ᵤ Multiset.prod (p ::ₘ factors b)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ (p ::ₘ factors b).prod

Tactic:
rw [Multiset.prod_cons]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ p * (factors b).prod

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b = 0
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
this : Multiset.Rel Associated (p ::ₘ factors b) (factors a)
⊢ p ∈ p ::ₘ factors b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ p * (factors b).prod

Tactic:
exact (factors_prod hb0).symm.mul_left _

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma div_le_iff_le_mul_add_pred (hb : 0 < b) : a / b ≤ c ↔ a ≤ b * c + (b - 1)

Proof state:
a b c : ℕ
hb : 0 < b
⊢ a / b ≤ c ↔ a ≤ b * c + (b - 1)

Tactic:
rw [← Nat.lt_succ_iff, div_lt_iff_lt_mul hb, succ_mul, Nat.mul_comm]

Result:
a b c : ℕ
hb : 0 < b
⊢ a < b * c + b ↔ a ≤ b * c + (b - 1)

Proof state:
a b c : ℕ
hb : 0 < b
⊢ a < b * c + b ↔ a ≤ b * c + (b - 1)

Tactic:
cases hb <;> exact Nat.lt_succ_iff

Result:
no goals