harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_array_forM
    (f : γ → α → m PUnit) (xs : Array α) (start stop : Nat) (hmono : monotone f) :
    monotone (fun x => xs.forM (f x) start stop)

Proof state:
case hmono.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m PUnit
xs : Array α
start stop : Nat
hmono : monotone f
⊢ PUnit → monotone fun x => f x

Tactic:
intro y

Result:
case hmono.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m PUnit
xs : Array α
start stop : Nat
hmono : monotone f
y : PUnit
⊢ monotone fun x => f x

Proof state:
case hmono
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m PUnit
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x x_1 => f x

Tactic:
apply monotone_of_monotone_apply

Result:
case hmono.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m PUnit
xs : Array α
start stop : Nat
hmono : monotone f
⊢ PUnit → monotone fun x => f x

Proof state:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m PUnit
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x => Array.forM (f x) xs start stop

Tactic:
unfold Array.forM

Result:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m PUnit
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x => Array.foldlM (fun x_1 => f x) PUnit.unit xs start stop

Proof state:
case hmono.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m PUnit
xs : Array α
start stop : Nat
hmono : monotone f
y : PUnit
⊢ monotone fun x => f x

Tactic:
apply hmono

Result:
no goals

Proof state:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m PUnit
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x => Array.foldlM (fun x_1 => f x) PUnit.unit xs start stop

Tactic:
apply monotone_foldlM

Result:
case hmono
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m PUnit
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x x_1 => f x
-- Mathlib/LinearAlgebra/BilinearForm/Hom.lean
theorem comp_id_left (B : BilinForm R M) (r : M →ₗ[R] M) :
    B.comp LinearMap.id r = B.compRight r

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
r : M →ₗ[R] M
⊢ B.comp id r = B.compRight r

Tactic:
ext

Result:
case H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
r : M →ₗ[R] M
x✝ y✝ : M
⊢ ((B.comp id r) x✝) y✝ = ((B.compRight r) x✝) y✝

Proof state:
case H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
r : M →ₗ[R] M
x✝ y✝ : M
⊢ ((B.comp id r) x✝) y✝ = ((B.compRight r) x✝) y✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Choose/Central.lean
theorem two_dvd_centralBinom_of_one_le {n : ℕ} (h : 0 < n) : 2 ∣ centralBinom n

Proof state:
n : ℕ
h : 0 < n
⊢ 2 ∣ n.pred.succ.centralBinom

Tactic:
exact two_dvd_centralBinom_succ n.pred

Result:
no goals

Proof state:
n : ℕ
h : 0 < n
⊢ 2 ∣ n.centralBinom

Tactic:
rw [← Nat.succ_pred_eq_of_pos h]

Result:
n : ℕ
h : 0 < n
⊢ 2 ∣ n.pred.succ.centralBinom
-- Mathlib/Analysis/Convolution.lean
theorem convolution_zero : f ⋆[L, μ] 0 = 0

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
⊢ f ⋆[L, μ] 0 = 0

Tactic:
ext

Result:
case h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x✝ : G
⊢ (f ⋆[L, μ] 0) x✝ = 0 x✝

Proof state:
case h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x✝ : G
⊢ (f ⋆[L, μ] 0) x✝ = 0 x✝

Tactic:
simp_rw [convolution_def, Pi.zero_apply, (L _).map_zero, integral_zero]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem support_concat {u v w : V} (p : G.Walk u v) (h : G.Adj v w) :
    (p.concat h).support = p.support.concat w

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).support = p.support.concat w

Tactic:
induction p <;> simp [*, concat_nil]

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_inf : (φ ⊓ ψ).Realize v xs ↔ φ.Realize v xs ∧ ψ.Realize v xs

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⊓ ψ).Realize v xs ↔ φ.Realize v xs ∧ ψ.Realize v xs

Tactic:
simp [Inf.inf, Realize]

Result:
no goals
-- Mathlib/Order/Bounded.lean
theorem bounded_lt_Iic [Preorder α] [NoMaxOrder α] (a : α) : Bounded (· < ·) (Iic a)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 < x2) (Iic a)

Tactic:
simp only [← bounded_le_iff_bounded_lt, bounded_le_Iic]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma IsDiameter.right_mem (h : s.IsDiameter p₁ p₂) : p₂ ∈ s

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ p₂ ∈ s

Tactic:
rw [mem_sphere, ← mem_sphere.1 h.left_mem, ← h.midpoint_eq_center,
  dist_left_midpoint_eq_dist_right_midpoint]

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
theorem antilipschitz_equivRealProd : AntilipschitzWith (NNReal.sqrt 2) equivRealProd :=
  AddMonoidHomClass.antilipschitz_of_bound equivRealProdLm fun z ↦ by
    simpa only [Real.coe_sqrt, NNReal.coe_ofNat] using norm_le_sqrt_two_mul_max z

Proof state:
z : ℂ
⊢ ‖z‖ ≤ ↑(NNReal.sqrt 2) * ‖equivRealProdLm z‖

Tactic:
simpa only [Real.coe_sqrt, NNReal.coe_ofNat] using norm_le_sqrt_two_mul_max z

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem head?_range' (n : Nat) : (range' s n).head? = if n = 0 then none else some s

Proof state:
s n : Nat
⊢ (range' s n).head? = if n = 0 then none else some s

Tactic:
induction n <;> simp_all [range'_succ, head?_append]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem zero_max_negSucc (n : Nat) : (max 0 (Int.negSucc n)) = 0

Proof state:
n : Nat
⊢ max 0 -[n+1] = 0

Tactic:
rw [Int.max_eq_left (negSucc_le_zero _)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.toLinAlgEquiv_one : Matrix.toLinAlgEquiv v₁ 1 = LinearMap.id

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
⊢ (toLinAlgEquiv v₁) 1 = LinearMap.id

Tactic:
rw [← LinearMap.toMatrixAlgEquiv_id v₁, Matrix.toLinAlgEquiv_toMatrixAlgEquiv]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem single_swap (a₁ a₂ : α) (b : M) : single a₁ b a₂ = single a₂ b a₁

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b : M
⊢ (single a₁ b) a₂ = (single a₂ b) a₁

Tactic:
simp only [single_apply, eq_comm]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b : M
⊢ (single a₁ b) a₂ = (single a₂ b) a₁

Tactic:
classical simp only [single_apply, eq_comm]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformlyOnFilter.comp (h : TendstoUniformlyOnFilter F f p p') (g : γ → α) :
    TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (p'.comap g)

Proof state:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (comap g p')

Tactic:
rw [tendstoUniformlyOnFilter_iff_tendsto] at h ⊢

Result:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
h : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
g : γ → α
⊢ Tendsto (fun q => ((f ∘ g) q.2, (F q.1 ∘ g) q.2)) (p ×ˢ comap g p') (𝓤 β)

Proof state:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
h : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
g : γ → α
⊢ Tendsto (fun q => ((f ∘ g) q.2, (F q.1 ∘ g) q.2)) (p ×ˢ comap g p') (𝓤 β)

Tactic:
exact h.comp (tendsto_id.prod_map tendsto_comap)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem takeWhile (p : Char → Bool) : ∀ {s}, ValidFor l m r s →
    ValidFor l (m.takeWhile p) (m.dropWhile p ++ r) (s.takeWhile p)
  | _, ⟨⟩ => by
    simp only [Substring.takeWhile, takeWhileAux_of_valid]
    apply ValidFor.of_eq <;> simp
    rw [← List.append_assoc, List.takeWhile_append_dropWhile]

Proof state:
l m r : List Char
p : Char → Bool
⊢ ValidFor l (List.takeWhile p m) (List.dropWhile p m ++ r)
    { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
      stopPos := { byteIdx := utf8Len l + utf8Len (List.takeWhile p m) } }

Tactic:
apply ValidFor.of_eq <;> simp

Result:
case a
l m r : List Char
p : Char → Bool
⊢ m ++ r = List.takeWhile p m ++ (List.dropWhile p m ++ r)

Proof state:
l m r : List Char
p : Char → Bool
⊢ ValidFor l (List.takeWhile p m) (List.dropWhile p m ++ r)
    ({ str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
          stopPos := { byteIdx := utf8Len l + utf8Len m } }.takeWhile
      p)

Tactic:
simp only [Substring.takeWhile, takeWhileAux_of_valid]

Result:
l m r : List Char
p : Char → Bool
⊢ ValidFor l (List.takeWhile p m) (List.dropWhile p m ++ r)
    { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
      stopPos := { byteIdx := utf8Len l + utf8Len (List.takeWhile p m) } }

Proof state:
case a
l m r : List Char
p : Char → Bool
⊢ m ++ r = List.takeWhile p m ++ (List.dropWhile p m ++ r)

Tactic:
rw [← List.append_assoc, List.takeWhile_append_dropWhile]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_X_pow (m n : ℕ) : coeff R m ((X : R⟦X⟧) ^ n) = if m = n then 1 else 0

Proof state:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
⊢ (coeff R m) (X ^ n) = if m = n then 1 else 0

Tactic:
rw [X_pow_eq, coeff_monomial]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma IsDynCoverOf.nonempty {T : X → X} {F : Set X} (h : F.Nonempty) {U : Set (X × X)} {n : ℕ}
    {s : Set X} (h' : IsDynCoverOf T F U n s) :
    s.Nonempty

Proof state:
case intro.intro
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
n : ℕ
s : Set X
h' : IsDynCoverOf T F U n s
x : X
x_s : x ∈ s
right✝ : (ball x (dynEntourage T U n)).Nonempty
⊢ s.Nonempty

Tactic:
exact nonempty_of_mem x_s

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
n : ℕ
s : Set X
h' : IsDynCoverOf T F U n s
⊢ s.Nonempty

Tactic:
rcases nonempty_biUnion.1 (Nonempty.mono h' h) with ⟨x, x_s, _⟩

Result:
case intro.intro
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
n : ℕ
s : Set X
h' : IsDynCoverOf T F U n s
x : X
x_s : x ∈ s
right✝ : (ball x (dynEntourage T U n)).Nonempty
⊢ s.Nonempty
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem mk_eq_bot_iff_zero {f : X ⟶ Y} [Mono f] : Subobject.mk f = ⊥ ↔ f = 0 :=
  ⟨fun h => by simpa [h, bot_factors_iff_zero] using mk_factors_self f, fun h =>
    mk_eq_mk_of_comm _ _ ((isoZeroOfMonoEqZero h).trans HasZeroObject.zeroIsoInitial) (by simp [h])⟩

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : Mono f
h : f = 0
⊢ (isoZeroOfMonoEqZero h ≪≫ HasZeroObject.zeroIsoInitial).hom ≫ initial.to Y = f

Tactic:
simp [h]

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊥
⊢ f = 0

Tactic:
simpa [h, bot_factors_iff_zero] using mk_factors_self f

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem isCompact_closure_interUnionBalls {p : ℕ → Prop} {U : ℕ → Set (α × α)}
    (H : (uniformity α).HasBasis p U) [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) :
    IsCompact (closure (interUnionBalls xs u U))

Proof state:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
inst✝ : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ IsCompact (closure (interUnionBalls xs u U))

Tactic:
rw [isCompact_iff_totallyBounded_isComplete]

Result:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
inst✝ : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (closure (interUnionBalls xs u U)) ∧ IsComplete (closure (interUnionBalls xs u U))

Proof state:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
inst✝ : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (closure (interUnionBalls xs u U)) ∧ IsComplete (closure (interUnionBalls xs u U))

Tactic:
refine ⟨TotallyBounded.closure ?_, isClosed_closure.isComplete⟩

Result:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
inst✝ : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (interUnionBalls xs u U)

Proof state:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
inst✝ : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (interUnionBalls xs u U)

Tactic:
exact totallyBounded_interUnionBalls H xs u

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem hausdorffMeasure_of_lt_dimH {s : Set X} {d : ℝ≥0} (h : ↑d < dimH s) : μH[d] s = ∞

Proof state:
case intro.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d d' : ℝ≥0
hsd' : μH[↑d'] s = ⊤
hdd' : ↑d < ↑d'
⊢ μH[↑d] s = ⊤

Tactic:
exact top_unique (hsd' ▸ hausdorffMeasure_mono hdd'.le _)

Result:
no goals

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ↑d < dimH s
⊢ μH[↑d] s = ⊤

Tactic:
simp only [dimH_def, lt_iSup_iff] at h

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ∃ i, ∃ (_ : μH[↑i] s = ⊤), ↑d < ↑i
⊢ μH[↑d] s = ⊤

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ∃ i, ∃ (_ : μH[↑i] s = ⊤), ↑d < ↑i
⊢ μH[↑d] s = ⊤

Tactic:
rcases h with ⟨d', hsd', hdd'⟩

Result:
case intro.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d d' : ℝ≥0
hsd' : μH[↑d'] s = ⊤
hdd' : ↑d < ↑d'
⊢ μH[↑d] s = ⊤
-- Mathlib/Order/Heyting/Boundary.lean
theorem boundary_sup_le : ∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ b

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢(a ⊔ b) ⊔ b ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b

Tactic:
exact
  sup_le_sup (inf_le_inf_left _ <| hnot_anti le_sup_left)
    (inf_le_inf_left _ <| hnot_anti le_sup_right)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ b

Tactic:
rw [boundary, inf_sup_right]

Result:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢(a ⊔ b) ⊔ b ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b
-- Mathlib/Data/Matroid/Basic.lean
theorem finite_setOf_matroid' {E : Set α} (hE : E.Finite) : {M : Matroid α | M.E = E}.Finite :=
  (finite_setOf_matroid hE).subset (fun M ↦ by rintro rfl; exact rfl.subset)

Proof state:
α : Type u_1
E : Set α
hE : E.Finite
M : Matroid α
⊢ M ∈ {M | M.E = E} → M ∈ {M | M.E ⊆ E}

Tactic:
rintro rfl

Result:
α : Type u_1
M : Matroid α
hE : M.E.Finite
⊢ M ∈ {M_1 | M_1.E ⊆ M.E}

Proof state:
α : Type u_1
M : Matroid α
hE : M.E.Finite
⊢ M ∈ {M_1 | M_1.E ⊆ M.E}

Tactic:
exact rfl.subset

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/RightDerived.lean
/-- The higher derived functors vanish on injective objects. -/
lemma Functor.isZero_rightDerived_obj_injective_succ
    (F : C ⥤ D) [F.Additive] (n : ℕ) (X : C) [Injective X] :
    IsZero ((F.rightDerived (n+1)).obj X)

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Injective X
⊢ IsZero
    ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) (n + 1)).obj
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (InjectiveResolution.self X).cocomplex))

Tactic:
erw [← HomologicalComplex.exactAt_iff_isZero_homology]

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Injective X
⊢ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (InjectiveResolution.self X).cocomplex).ExactAt (n + 1)

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Injective X
⊢ IsZero ((InjectiveResolution.self X).cocomplex.X (n + 1))

Tactic:
apply isZero_zero

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Injective X
⊢ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (InjectiveResolution.self X).cocomplex).ExactAt (n + 1)

Tactic:
exact ShortComplex.exact_of_isZero_X₂ _ (F.map_isZero (by apply isZero_zero))

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Injective X
⊢ IsZero ((F.rightDerived (n + 1)).obj X)

Tactic:
refine IsZero.of_iso ?_ ((InjectiveResolution.self X).isoRightDerivedObj F (n + 1))

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Injective X
⊢ IsZero
    ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) (n + 1)).obj
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (InjectiveResolution.self X).cocomplex))
-- Mathlib/Algebra/MvPolynomial/Rename.lean
lemma rename_id_apply (p : MvPolynomial σ R) : rename id p = p

Proof state:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (rename id) p = p

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem mk_one (h : ∀ x y, dist (f x) (f y) ≤ dist x y) : LipschitzWith 1 f :=
  of_dist_le_mul <| by simpa only [NNReal.coe_one, one_mul] using h

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∀ (x y : α), dist (f x) (f y) ≤ dist x y
⊢ ∀ (x y : α), dist (f x) (f y) ≤ ↑1 * dist x y

Tactic:
simpa only [NNReal.coe_one, one_mul] using h

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma loopyOn_closure_eq (E X : Set α) : (loopyOn E).closure X = E

Proof state:
α : Type u_2
E X : Set α
⊢ (loopyOn E).closure X = E

Tactic:
simp [loopyOn, restrict_closure_eq']

Result:
no goals
-- Mathlib/Algebra/Group/Int/Even.lean
@[parity_simps] lemma even_mul : Even (m * n) ↔ Even m ∨ Even n

Proof state:
m n : ℤ
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases emod_two_eq_zero_or_one m with h₁ | h₁ <;>
rcases emod_two_eq_zero_or_one n with h₂ | h₂ <;>
simp [even_iff, h₁, h₂, Int.mul_emod]

Result:
no goals
-- Mathlib/Order/Bounds/Lattice.lean
theorem isGLB_iUnion_iff_of_isLUB {u : ι → α} (hs : ∀ i, IsGLB (s i) (u i)) (c : α) :
    IsGLB (Set.range u) c ↔ IsGLB (⋃ i, s i) c

Proof state:
α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ lowerBounds (range u) = lowerBounds (⋃ i, s i)

Tactic:
simp_rw [range_eq_iUnion, lowerBounds_iUnion, lowerBounds_singleton, (hs _).lowerBounds_eq]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ IsGLB (range u) c ↔ IsGLB (⋃ i, s i) c

Tactic:
refine isGLB_congr ?_

Result:
α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ lowerBounds (range u) = lowerBounds (⋃ i, s i)
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem fg_bot : (⊥ : Submodule R M).FG :=
  ⟨∅, by rw [Finset.coe_empty, span_empty]⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ span R ↑∅ = ⊥

Tactic:
rw [Finset.coe_empty, span_empty]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem pmap_bind {α β γ} {x : Option α} {g : α → Option β} {p : β → Prop} {f : ∀ b, p b → γ} (H)
    (H' : ∀ (a : α), ∀ b ∈ g a, b ∈ x >>= g) :
    pmap f (x >>= g) H = x >>= fun a ↦ pmap f (g a) fun _ h ↦ H _ (H' a _ h)

Proof state:
α β γ : Type u_5
x : Option α
g : α → Option β
p : β → Prop
f : (b : β) → p b → γ
H : ∀ (a : β), a ∈ x >>= g → p a
H' : ∀ (a : α) (b : β), b ∈ g a → b ∈ x >>= g
⊢ pmap f (x >>= g) H = do
    let a ← x
    pmap f (g a) ⋯

Tactic:
cases x <;> simp only [pmap, bind_eq_bind, none_bind, some_bind]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_neg' (a b : α) : toIocDiv hp (-a) b = -(toIcoDiv hp a (-b) + 1)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp (-a) b = -(toIcoDiv hp a (-b) + 1)

Tactic:
simpa only [neg_neg] using toIocDiv_neg hp (-a) (-b)

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
lemma inter_biUnion (t : Finset β) (s : Finset α) (f : α → Finset β) :
    t ∩ s.biUnion f = s.biUnion fun x ↦ t ∩ f x

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
t : Finset β
s : Finset α
f : α → Finset β
⊢ t ∩ s.biUnion f = s.biUnion fun x => t ∩ f x

Tactic:
rw [inter_comm, biUnion_inter]

Result:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
t : Finset β
s : Finset α
f : α → Finset β
⊢ (s.biUnion fun x => f x ∩ t) = s.biUnion fun x => t ∩ f x

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
t : Finset β
s : Finset α
f : α → Finset β
⊢ (s.biUnion fun x => f x ∩ t) = s.biUnion fun x => t ∩ f x

Tactic:
simp [inter_comm]

Result:
no goals