harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_le_iff {α β} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β}
    (h₁ : f.IsCoboundedUnder (· ≤ ·) u

Proof state:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
⊢ limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a < y

Tactic:
refine ⟨fun h _ h' ↦ eventually_lt_of_limsup_lt (lt_of_le_of_lt h h') h₂, fun h ↦ ?_⟩

Result:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
⊢ limsup u f ≤ x
-- Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean
lemma neg_llr [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
    - llr μ ν =ᵐ[μ] llr ν μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ -llr μ ν =ᶠ[ae μ] llr ν μ

Tactic:
filter_upwards [Measure.inv_rnDeriv hμν] with x hx

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ (-llr μ ν) x = llr ν μ x

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ log (μ.rnDeriv ν x)⁻¹.toReal = log (ν.rnDeriv μ x).toReal

Tactic:
congr

Result:
no goals

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ (-llr μ ν) x = llr ν μ x

Tactic:
rw [Pi.neg_apply, llr, llr, ← log_inv, ← ENNReal.toReal_inv]

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ log (μ.rnDeriv ν x)⁻¹.toReal = log (ν.rnDeriv μ x).toReal
-- Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
theorem integral_comp_neg_Iic {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (c : ℝ) (f : ℝ → E) : (∫ x in Iic c, f (-x)) = ∫ x in Ioi (-c), f x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x

Tactic:
have := MeasurableEmbedding.setIntegral_map (μ := volume) A f (Ici (-c))

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
this : ∫ (y : ℝ) in Ici (-c), f y ∂Measure.map (fun x => -x) volume = ∫ (x : ℝ) in (fun x => -x) ⁻¹' Ici (-c), f (-x)
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
this : ∫ (y : ℝ) in Ici (-c), f y ∂Measure.map (fun x => -x) volume = ∫ (x : ℝ) in (fun x => -x) ⁻¹' Ici (-c), f (-x)
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x

Tactic:
rw [Measure.map_neg_eq_self (volume : Measure ℝ)] at this

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
this : ∫ (y : ℝ) in Ici (-c), f y ∂volume = ∫ (x : ℝ) in (fun x => -x) ⁻¹' Ici (-c), f (-x)
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x

Tactic:
have A : MeasurableEmbedding fun x : ℝ => -x :=
  (Homeomorph.neg ℝ).isClosedEmbedding.measurableEmbedding

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
this : ∫ (y : ℝ) in Ici (-c), f y ∂volume = ∫ (x : ℝ) in (fun x => -x) ⁻¹' Ici (-c), f (-x)
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x

Tactic:
simp_rw [← integral_Ici_eq_integral_Ioi, this, neg_preimage, neg_Ici, neg_neg]

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
lemma divNat_mul_left {a : ℕ} (ha : a ≠ 0) (n d : ℕ) : divNat (a * n) (a * d) = divNat n d

Proof state:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ divNat (a * n) (a * d) = divNat n d

Tactic:
ext

Result:
case a
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ ↑(divNat (a * n) (a * d)) = ↑(divNat n d)

Proof state:
case a
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (↑a * ↑n) (↑a * ↑d) = Rat.divInt ↑n ↑d

Tactic:
exact Rat.divInt_mul_left (mod_cast ha)

Result:
no goals

Proof state:
case a
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ ↑(divNat (a * n) (a * d)) = ↑(divNat n d)

Tactic:
push_cast

Result:
case a
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (↑a * ↑n) (↑a * ↑d) = Rat.divInt ↑n ↑d
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/RArray.lean
theorem RArray.get_eq_getImpl : @RArray.get = @RArray.getImpl

Proof state:
case h.h.h.branch
α : Type
n p : Nat
l r : RArray α
ihl : l.get n = l.getImpl n
ihr : r.get n = r.getImpl n
⊢ Bool.rec (l.getImpl n) (r.getImpl n) (p.ble n) = if p.ble n = true then r.getImpl n else l.getImpl n

Tactic:
cases hnp : Nat.ble p n <;> rfl

Result:
no goals

Proof state:
case h.h.h
α : Type
a : RArray α
n : Nat
⊢ a.get n = a.getImpl n

Tactic:
induction a with
| leaf _ => rfl
| branch p l r ihl ihr =>
  rw [RArray.getImpl, RArray.get_eq_def]
  simp only [ihl, ihr, ← Nat.not_le, ← Nat.ble_eq, ite_not]
  cases hnp : Nat.ble p n <;> rfl

Result:
no goals

Proof state:
⊢ @get = @getImpl

Tactic:
funext α a n

Result:
case h.h.h
α : Type
a : RArray α
n : Nat
⊢ a.get n = a.getImpl n

Proof state:
case h.h.h.branch
α : Type
n p : Nat
l r : RArray α
ihl : l.get n = l.getImpl n
ihr : r.get n = r.getImpl n
⊢ (match branch p l r with
    | leaf x => x
    | branch p l r => Bool.rec (l.get n) (r.get n) (p.ble n)) =
    if n < p then l.getImpl n else r.getImpl n

Tactic:
simp only [ihl, ihr, ← Nat.not_le, ← Nat.ble_eq, ite_not]

Result:
case h.h.h.branch
α : Type
n p : Nat
l r : RArray α
ihl : l.get n = l.getImpl n
ihr : r.get n = r.getImpl n
⊢ Bool.rec (l.getImpl n) (r.getImpl n) (p.ble n) = if p.ble n = true then r.getImpl n else l.getImpl n

Proof state:
case h.h.h.branch
α : Type
n p : Nat
l r : RArray α
ihl : l.get n = l.getImpl n
ihr : r.get n = r.getImpl n
⊢ (branch p l r).get n = (branch p l r).getImpl n

Tactic:
rw [RArray.getImpl, RArray.get_eq_def]

Result:
case h.h.h.branch
α : Type
n p : Nat
l r : RArray α
ihl : l.get n = l.getImpl n
ihr : r.get n = r.getImpl n
⊢ (match branch p l r with
    | leaf x => x
    | branch p l r => Bool.rec (l.get n) (r.get n) (p.ble n)) =
    if n < p then l.getImpl n else r.getImpl n

Proof state:
case h.h.h.leaf
α : Type
n : Nat
a✝ : α
⊢ (leaf a✝).get n = (leaf a✝).getImpl n

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma natDegree_Ψ₂Sq_le : W.Ψ₂Sq.natDegree ≤ 3

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Ψ₂Sq.natDegree ≤ 3

Tactic:
rw [Ψ₂Sq]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆).natDegree ≤ 3

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆).natDegree ≤ 3

Tactic:
compute_degree

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.add_smul (h_conv : Convex 𝕜 s) {p q : 𝕜} (hp : 0 ≤ p) (hq : 0 ≤ q) :
    (p + q) • s = p • s + q • s := (add_smul_subset _ _ _).antisymm <| by
  rintro _ ⟨_, ⟨v₁, h₁, rfl⟩, _, ⟨v₂, h₂, rfl⟩, rfl⟩
  exact h_conv.exists_mem_add_smul_eq h₁ h₂ hp hq

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
v₁ : E
h₁ : v₁ ∈ s
v₂ : E
h₂ : v₂ ∈ s
⊢ (fun x1 x2 => x1 + x2) ((fun x => p • x) v₁) ((fun x => q • x) v₂) ∈ (p + q) • s

Tactic:
exact h_conv.exists_mem_add_smul_eq h₁ h₂ hp hq

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
⊢ p • s + q • s ⊆ (p + q) • s

Tactic:
rintro _ ⟨_, ⟨v₁, h₁, rfl⟩, _, ⟨v₂, h₂, rfl⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
v₁ : E
h₁ : v₁ ∈ s
v₂ : E
h₂ : v₂ ∈ s
⊢ (fun x1 x2 => x1 + x2) ((fun x => p • x) v₁) ((fun x => q • x) v₂) ∈ (p + q) • s
-- Mathlib/Algebra/DirectSum/Internal.lean
theorem coe_of_mul_apply {i : ι} (r : A i) (r' : ⨁ i, A i) (n : ι) [Decidable (i ≤ n)] :
    ((of (fun i => A i) i r * r') n : R) = if i ≤ n then (r * r' (n - i) : R) else 0

Proof state:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
⊢ ↑(((of (fun i => ↥(A i)) i) r * r') n) = if i ≤ n then ↑r * ↑(r' (n - i)) else 0

Tactic:
split_ifs with h

Result:
case pos
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : i ≤ n
⊢ ↑(((of (fun i => ↥(A i)) i) r * r') n) = ↑r * ↑(r' (n - i))

case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : ¬i ≤ n
⊢ ↑(((of (fun i => ↥(A i)) i) r * r') n) = 0

Proof state:
case pos
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : i ≤ n
⊢ ↑(((of (fun i => ↥(A i)) i) r * r') n) = ↑r * ↑(r' (n - i))

case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : ¬i ≤ n
⊢ ↑(((of (fun i => ↥(A i)) i) r * r') n) = 0

Tactic:
exacts [coe_of_mul_apply_of_le _ _ _ n h, coe_of_mul_apply_of_not_le _ _ _ n h]

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem map_eq_singleton {f : α → β} {s : Multiset α} {b : β} :
    map f s = {b} ↔ ∃ a : α, s = {a} ∧ f a = b

Proof state:
case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ ∃ a, s = {a} ∧ f a = b

Tactic:
obtain ⟨a, ha⟩ : ∃ a, s = {a} := by rw [← card_eq_one, ← card_map, h, card_singleton]

Result:
case mp.intro
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ ∃ a, s = {a} ∧ f a = b

Proof state:
case mp.intro
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ ∃ a, s = {a} ∧ f a = b

Tactic:
refine ⟨a, ha, ?_⟩

Result:
case mp.intro
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ f a = b

Proof state:
case mp.intro
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ f a = b

Tactic:
rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ (∃ a, s = {a} ∧ f a = b) → map f s = {b}

Tactic:
rintro ⟨a, rfl, rfl⟩

Result:
case mpr.intro.intro
α : Type u_1
β : Type v
f : α → β
a : α
⊢ map f {a} = {f a}

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type v
f : α → β
a : α
⊢ map f {a} = {f a}

Tactic:
simp

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} → ∃ a, s = {a} ∧ f a = b

Tactic:
intro h

Result:
case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ ∃ a, s = {a} ∧ f a = b

Proof state:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} ↔ ∃ a, s = {a} ∧ f a = b

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} → ∃ a, s = {a} ∧ f a = b

case mpr
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ (∃ a, s = {a} ∧ f a = b) → map f s = {b}

Proof state:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ ∃ a, s = {a}

Tactic:
rw [← card_eq_one, ← card_map, h, card_singleton]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean
theorem card_eq_of_mem_parts_chunk (hs : s ∈ (chunk hP G ε hU).parts) :
    #s = m ∨ #s = m + 1

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
s : Finset α
hs : s ∈ (chunk hP G ε hU).parts
⊢ #s = m ∨ #s = m + 1

Tactic:
unfold chunk at hs

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
s : Finset α
hs :
  s ∈
    (if hUcard : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts) then equitabilise ⋯
      else equitabilise ⋯).parts
⊢ #s = m ∨ #s = m + 1

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
s : Finset α
hs :
  s ∈
    (if hUcard : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts) then equitabilise ⋯
      else equitabilise ⋯).parts
⊢ #s = m ∨ #s = m + 1

Tactic:
split_ifs at hs <;> exact card_eq_of_mem_parts_equitabilise hs

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ConstantSheaf.lean
lemma isConstant_iff_mem_essImage {L : D ⥤ Sheaf J D} {T : C} (hT : IsTerminal T)
    (adj : L ⊣ (sheafSections J D).obj ⟨T⟩)
    (F : Sheaf J D) : IsConstant J F ↔ L.essImage F

Proof state:
C : Type u_1
inst✝² : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹ : Category.{u_3, u_2} D
inst✝ : HasWeakSheafify J D
L : D ⥤ Sheaf J D
T : C
hT : IsTerminal T
adj : L ⊣ (sheafSections J D).obj (op T)
F : Sheaf J D
⊢ IsConstant J F ↔ L.essImage F

Tactic:
rw [essImage_eq_of_natIso (adj.leftAdjointUniq (constantSheafAdj J D hT))]

Result:
C : Type u_1
inst✝² : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹ : Category.{u_3, u_2} D
inst✝ : HasWeakSheafify J D
L : D ⥤ Sheaf J D
T : C
hT : IsTerminal T
adj : L ⊣ (sheafSections J D).obj (op T)
F : Sheaf J D
⊢ IsConstant J F ↔ (constantSheaf J D).essImage F

Proof state:
C : Type u_1
inst✝² : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹ : Category.{u_3, u_2} D
inst✝ : HasWeakSheafify J D
L : D ⥤ Sheaf J D
T : C
hT : IsTerminal T
adj : L ⊣ (sheafSections J D).obj (op T)
F : Sheaf J D
⊢ IsConstant J F ↔ (constantSheaf J D).essImage F

Tactic:
exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem uniformity_lift_le_comp {f : Set (α × α) → Filter β} (h : Monotone f) :
    ((𝓤 α).lift fun s => f (s ○ s)) ≤ (𝓤 α).lift f :=
  calc
    ((𝓤 α).lift fun s => f (s ○ s)) = ((𝓤 α).lift' fun s : Set (α × α) => s ○ s).lift f

Proof state:
case hg
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Set (α × α) → Filter β
h : Monotone f
⊢ Monotone fun s => s ○ s

Tactic:
exact monotone_id.compRel monotone_id

Result:
no goals

Proof state:
case hh
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Set (α × α) → Filter β
h : Monotone f
⊢ Monotone f

Tactic:
exact h

Result:
no goals

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Set (α × α) → Filter β
h : Monotone f
⊢ ((𝓤 α).lift fun s => f (s ○ s)) = ((𝓤 α).lift' fun s => s ○ s).lift f

Tactic:
rw [lift_lift'_assoc]

Result:
case hg
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Set (α × α) → Filter β
h : Monotone f
⊢ Monotone fun s => s ○ s

case hh
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Set (α × α) → Filter β
h : Monotone f
⊢ Monotone f
-- Mathlib/Geometry/RingedSpace/Stalks.lean
theorem congr {X Y : PresheafedSpace.{_, _, v} C} (α β : X ⟶ Y)
    (h₁ : α = β) (x x' : X) (h₂ : x = x') :
    α.stalkMap x ≫ eqToHom (show X.presheaf.stalk x = X.presheaf.stalk x' by rw [h₂]) =
      eqToHom (show Y.presheaf.stalk (α.base x) = Y.presheaf.stalk (β.base x') by rw [h₁, h₂]) ≫
        β.stalkMap x'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ Y.presheaf.stalk ((ConcreteCategory.hom α.base) x) = Y.presheaf.stalk ((ConcreteCategory.hom β.base) x')

Tactic:
rw [h₁, h₂]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ Hom.stalkMap α x ≫ eqToHom ⋯ = eqToHom ⋯ ≫ Hom.stalkMap β x'

Tactic:
ext

Result:
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
U✝ : Opens ↑↑Y
hxU✝ : (ConcreteCategory.hom α.base) x ∈ U✝
⊢ Y.presheaf.germ U✝ ((ConcreteCategory.hom α.base) x) hxU✝ ≫ Hom.stalkMap α x ≫ eqToHom ⋯ =
    Y.presheaf.germ U✝ ((ConcreteCategory.hom α.base) x) hxU✝ ≫ eqToHom ⋯ ≫ Hom.stalkMap β x'

Proof state:
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x : ↑↑X
U✝ : Opens ↑↑Y
hxU✝ : (ConcreteCategory.hom α.base) x ∈ U✝
⊢ Y.presheaf.germ U✝ ((ConcreteCategory.hom α.base) x) hxU✝ ≫ Hom.stalkMap α x ≫ eqToHom ⋯ =
    Y.presheaf.germ U✝ ((ConcreteCategory.hom α.base) x) hxU✝ ≫ eqToHom ⋯ ≫ Hom.stalkMap α x

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ X.presheaf.stalk x = X.presheaf.stalk x'

Tactic:
rw [h₂]

Result:
no goals

Proof state:
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
U✝ : Opens ↑↑Y
hxU✝ : (ConcreteCategory.hom α.base) x ∈ U✝
⊢ Y.presheaf.germ U✝ ((ConcreteCategory.hom α.base) x) hxU✝ ≫ Hom.stalkMap α x ≫ eqToHom ⋯ =
    Y.presheaf.germ U✝ ((ConcreteCategory.hom α.base) x) hxU✝ ≫ eqToHom ⋯ ≫ Hom.stalkMap β x'

Tactic:
substs h₁ h₂

Result:
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x : ↑↑X
U✝ : Opens ↑↑Y
hxU✝ : (ConcreteCategory.hom α.base) x ∈ U✝
⊢ Y.presheaf.germ U✝ ((ConcreteCategory.hom α.base) x) hxU✝ ≫ Hom.stalkMap α x ≫ eqToHom ⋯ =
    Y.presheaf.germ U✝ ((ConcreteCategory.hom α.base) x) hxU✝ ≫ eqToHom ⋯ ≫ Hom.stalkMap α x
-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem continuousOn_primitive_interval_left (h_int : IntegrableOn f (uIcc a b) μ) :
    ContinuousOn (fun x => ∫ t in x..b, f t ∂μ) (uIcc a b)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f [[b, a]] μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in x..b, f t ∂μ) [[b, a]]

Tactic:
simp only [integral_symm b]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f [[b, a]] μ
⊢ ContinuousOn (fun x => -∫ (t : ℝ) in b..x, f t ∂μ) [[b, a]]

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f [[b, a]] μ
⊢ ContinuousOn (fun x => -∫ (t : ℝ) in b..x, f t ∂μ) [[b, a]]

Tactic:
exact (continuousOn_primitive_interval h_int).neg

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f [[a, b]] μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in x..b, f t ∂μ) [[a, b]]

Tactic:
rw [uIcc_comm a b] at h_int ⊢

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f [[b, a]] μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in x..b, f t ∂μ) [[b, a]]