harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[reassoc]
lemma mapOpcyclesIso_hom_naturality [S₁.HasRightHomology] [S₂.HasRightHomology]
    [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
    opcyclesMap (F.mapShortComplex.map φ) ≫ (S₂.mapOpcyclesIso F).hom =
      (S₁.mapOpcyclesIso F).hom ≫ F.map (opcyclesMap φ)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Category.{u_4, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ opcyclesMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).rightHomologyData
        (F.mapShortComplex.obj S₂).rightHomologyData ≫
      opcyclesMap' (𝟙 (S₂.map F)) (S₂.map F).rightHomologyData (S₂.rightHomologyData.map F) =
    opcyclesMap' (𝟙 (S₁.map F)) (S₁.map F).rightHomologyData (S₁.rightHomologyData.map F) ≫
      F.map (opcyclesMap' φ S₁.rightHomologyData S₂.rightHomologyData)

Tactic:
simp only [RightHomologyData.map_opcyclesMap', Functor.mapShortComplex_obj, ← opcyclesMap'_comp,
  comp_id, id_comp]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Category.{u_4, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ opcyclesMap (F.mapShortComplex.map φ) ≫ (S₂.mapOpcyclesIso F).hom = (S₁.mapOpcyclesIso F).hom ≫ F.map (opcyclesMap φ)

Tactic:
dsimp only [opcyclesMap, mapOpcyclesIso, RightHomologyData.opcyclesIso,
  opcyclesMapIso', Iso.refl]

Result:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Category.{u_4, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ opcyclesMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).rightHomologyData
        (F.mapShortComplex.obj S₂).rightHomologyData ≫
      opcyclesMap' (𝟙 (S₂.map F)) (S₂.map F).rightHomologyData (S₂.rightHomologyData.map F) =
    opcyclesMap' (𝟙 (S₁.map F)) (S₁.map F).rightHomologyData (S₁.rightHomologyData.map F) ≫
      F.map (opcyclesMap' φ S₁.rightHomologyData S₂.rightHomologyData)
-- Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
theorem unitors_equal : (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom

Tactic:
monoidal_coherence

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addXYZ_of_Z_eq_zero_left {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.addXYZ P Q = (P x * Q z) • Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.addXYZ P Q = (P x * Q z) • Q

Tactic:
rw [addXYZ, addX_of_Z_eq_zero_left hPz, addY_of_Z_eq_zero_left hP hPz, addZ_of_Z_eq_zero_left hPz,
  smul_fin3]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mk_Iio_ordinal (o : Ordinal.{u}) :
    #(Iio o) = Cardinal.lift.{u + 1} o.card

Proof state:
o : Ordinal.{u}
⊢ #↑(Iio o) = Cardinal.lift.{u + 1, u} o.card

Tactic:
rw [lift_card, ← typein_ordinal]

Result:
o : Ordinal.{u}
⊢ #↑(Iio o) = ((typein fun x1 x2 => x1 < x2).toRelEmbedding o).card

Proof state:
o : Ordinal.{u}
⊢ #↑(Iio o) = ((typein fun x1 x2 => x1 < x2).toRelEmbedding o).card

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[ext]
lemma rightHomology_ext {A : C} (f₁ f₂ : A ⟶ S.rightHomology)
    (h : f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι) : f₁ = f₂

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
A : C
f₁ f₂ : A ⟶ S.rightHomology
h : f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι
⊢ f₁ = f₂

Tactic:
simpa only [rightHomology_ext_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_eq_iff {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
    l.mapFinIdx f = l' ↔ ∀ (i : Nat) (h : i < n), l'[i] = f i l[i] h

Proof state:
case mk
α : Type u_1
β : Type u_2
l : Array α
l' : Vector β l.size
f : (i : Nat) → α → i < l.size → β
⊢ { toArray := l, size_toArray := ⋯ }.mapFinIdx f = l' ↔
    ∀ (i : Nat) (h : i < l.size), l'[i] = f i { toArray := l, size_toArray := ⋯ }[i] h

Tactic:
rcases l' with ⟨l', h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
l : Array α
f : (i : Nat) → α → i < l.size → β
l' : Array β
h : l'.size = l.size
⊢ { toArray := l, size_toArray := ⋯ }.mapFinIdx f = { toArray := l', size_toArray := h } ↔
    ∀ (i : Nat) (h_1 : i < l.size),
      { toArray := l', size_toArray := h }[i] = f i { toArray := l, size_toArray := ⋯ }[i] h_1

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l' : Vector β n
l : Vector α n
f : (i : Nat) → α → i < n → β
⊢ l.mapFinIdx f = l' ↔ ∀ (i : Nat) (h : i < n), l'[i] = f i l[i] h

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
l : Array α
l' : Vector β l.size
f : (i : Nat) → α → i < l.size → β
⊢ { toArray := l, size_toArray := ⋯ }.mapFinIdx f = l' ↔
    ∀ (i : Nat) (h : i < l.size), l'[i] = f i { toArray := l, size_toArray := ⋯ }[i] h

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
l : Array α
f : (i : Nat) → α → i < l.size → β
l' : Array β
h : l'.size = l.size
⊢ { toArray := l, size_toArray := ⋯ }.mapFinIdx f = { toArray := l', size_toArray := h } ↔
    ∀ (i : Nat) (h_1 : i < l.size),
      { toArray := l', size_toArray := h }[i] = f i { toArray := l, size_toArray := ⋯ }[i] h_1

Tactic:
simp [mapFinIdx_mk, eq_mk, getElem_mk, Array.mapFinIdx_eq_iff, h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
theorem wideEqualizer.lift_ι [Nonempty J] {W : C} (k : W ⟶ X)
    (h : ∀ j₁ j₂, k ≫ f j₁ = k ≫ f j₂) :
    wideEqualizer.lift k h ≫ wideEqualizer.ι f = k

Proof state:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝¹ : HasWideEqualizer f
inst✝ : Nonempty J
W : C
k : W ⟶ X
h : ∀ (j₁ j₂ : J), k ≫ f j₁ = k ≫ f j₂
⊢ lift k h ≫ ι f = k

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem sup_lt_ord {ι} {f : ι → Ordinal} {c : Ordinal} (hι : #ι < c.cof) :
    (∀ i, f i < c) → sup.{u, u} f < c :=
  sup_lt_ord_lift (by rwa [(#ι).lift_id])

Proof state:
ι : Type u
f : ι → Ordinal.{u}
c : Ordinal.{u}
hι : #ι < c.cof
⊢ Cardinal.lift.{u, u} #ι < c.cof

Tactic:
rwa [(#ι).lift_id]

Result:
no goals
-- Mathlib/Data/List/Iterate.lean
theorem mem_iterate {f : α → α} {a : α} {n : ℕ} {b : α} :
    b ∈ iterate f a n ↔ ∃ m < n, b = f^[m] a

Proof state:
α : Type u_1
f : α → α
a : α
n : ℕ
b : α
⊢ b ∈ iterate f a n ↔ ∃ m < n, b = f^[m] a

Tactic:
simp [List.mem_iff_get, Fin.exists_iff, eq_comm (b := b)]

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
/-- `klFun` is continuous. -/
@[continuity, fun_prop]
lemma continuous_klFun : Continuous klFun

Proof state:
⊢ Continuous klFun

Tactic:
unfold klFun

Result:
⊢ Continuous fun x => x * log x + 1 - x

Proof state:
⊢ Continuous fun x => x * log x + 1 - x

Tactic:
fun_prop

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Defs.lean
theorem isNilpotent_mul_left (h_comm : Commute x y) (h : IsNilpotent x) : IsNilpotent (x * y)

Proof state:
case h
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
⊢ (x * y) ^ n = 0

Tactic:
rw [h_comm.mul_pow, hn, zero_mul]

Result:
no goals

Proof state:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
h : IsNilpotent x
⊢ IsNilpotent (x * y)

Tactic:
obtain ⟨n, hn⟩ := h

Result:
case intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (x * y)

Proof state:
case intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (x * y)

Tactic:
use n

Result:
case h
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
⊢ (x * y) ^ n = 0
-- Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean
lemma projectiveFamilyFun_congr (hP : IsProjectiveMeasureFamily P)
    (hs : s ∈ measurableCylinders α) (hs_eq : s = cylinder I S) (hS : MeasurableSet S) :
    projectiveFamilyFun P s = P I S

Proof state:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
s : Set ((i : ι) → α i)
I : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
hs_eq : s = cylinder I S
hS : MeasurableSet S
⊢ (P (measurableCylinders.finset hs)) (measurableCylinders.set hs) = (P I) S

Tactic:
exact hP.congr_cylinder (measurableCylinders.measurableSet hs) hS
  ((measurableCylinders.eq_cylinder hs).symm.trans hs_eq)

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
s : Set ((i : ι) → α i)
I : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
hs_eq : s = cylinder I S
hS : MeasurableSet S
⊢ projectiveFamilyFun P s = (P I) S

Tactic:
rw [projectiveFamilyFun, dif_pos hs]

Result:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
s : Set ((i : ι) → α i)
I : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
hs_eq : s = cylinder I S
hS : MeasurableSet S
⊢ (P (measurableCylinders.finset hs)) (measurableCylinders.set hs) = (P I) S
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem get_map {xs : IntList} (h : f 0 = 0) : get (xs.map f) i = f (xs.get i)

Proof state:
f : Int → Int
i : Nat
xs : IntList
h : f 0 = 0
⊢ (Option.map f xs[i]?).getD 0 = f (xs[i]?.getD 0)

Tactic:
cases xs[i]? <;> simp_all

Result:
no goals

Proof state:
f : Int → Int
i : Nat
xs : IntList
h : f 0 = 0
⊢ get (List.map f xs) i = f (xs.get i)

Tactic:
simp only [get, List.get?_eq_getElem?, List.getElem?_map]

Result:
f : Int → Int
i : Nat
xs : IntList
h : f 0 = 0
⊢ (Option.map f xs[i]?).getD 0 = f (xs[i]?.getD 0)
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem replaceF_cons_of_none {l : List α} (p) (h : p a = none) :
    (a :: l).replaceF p = a :: l.replaceF p

Proof state:
α : Type u_1
a : α
l : List α
p : α → Option α
h : p a = none
⊢ replaceF p (a :: l) = a :: replaceF p l

Tactic:
simp [replaceF_cons, h]

Result:
no goals
-- Mathlib/Data/Set/List.lean
theorem range_list_get : range l.get = { x | x ∈ l }

Proof state:
α : Type u_1
l : List α
⊢ range l.get = {x | x ∈ l}

Tactic:
ext x

Result:
case h
α : Type u_1
l : List α
x : α
⊢ x ∈ range l.get ↔ x ∈ {x | x ∈ l}

Proof state:
case h
α : Type u_1
l : List α
x : α
⊢ x ∈ range l.get ↔ x ∈ {x | x ∈ l}

Tactic:
rw [mem_setOf_eq, mem_iff_get, mem_range]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean
lemma norm_mkContinuous₂_aux (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) (C : ℝ)
    (h : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) (x : E) :
    ‖(f x).mkContinuous (C * ‖x‖) (h x)‖ ≤ max C 0 * ‖x‖ :=
  (mkContinuous_norm_le' (f x) (h x)).trans_eq <| by
    rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup F
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NontriviallyNormedField 𝕜₃
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
C : ℝ
h : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖
x : E
⊢ C * ‖x‖ ⊔ 0 = (C ⊔ 0) * ‖x‖

Tactic:
rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem WCovBy.Icc_eq (h : a ⩿ b) : Icc a b = {a, b}

Proof state:
case h
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
c : α
⊢ c ∈ Icc a b ↔ c ∈ {a, b}

Tactic:
exact h.le_and_le_iff

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Icc a b = {a, b}

Tactic:
ext c

Result:
case h
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
c : α
⊢ c ∈ Icc a b ↔ c ∈ {a, b}
-- Mathlib/Order/LiminfLimsup.lean
lemma isCoboundedUnder_ge_mul_of_nonneg [Mul α] [Zero α] [LinearOrder α] [PosMulMono α]
    [MulPosMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : 0 ≤ᶠ[f] u)
    (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u)
    (h₃ : 0 ≤ᶠ[f] v)
    (h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v) :
    IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f (u * v)

Proof state:
α : Type u_1
ι : Type u_4
inst✝⁵ : Mul α
inst✝⁴ : Zero α
inst✝³ : LinearOrder α
inst✝² : PosMulMono α
inst✝¹ : MulPosMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u * v)

Tactic:
obtain ⟨U, hU⟩ := h₂.eventually_le

Result:
case intro
α : Type u_1
ι : Type u_4
inst✝⁵ : Mul α
inst✝⁴ : Zero α
inst✝³ : LinearOrder α
inst✝² : PosMulMono α
inst✝¹ : MulPosMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u * v)

Proof state:
case intro
α : Type u_1
ι : Type u_4
inst✝⁵ : Mul α
inst✝⁴ : Zero α
inst✝³ : LinearOrder α
inst✝² : PosMulMono α
inst✝¹ : MulPosMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u * v)

Tactic:
obtain ⟨V, hV⟩ := h₄.frequently_le

Result:
case intro.intro
α : Type u_1
ι : Type u_4
inst✝⁵ : Mul α
inst✝⁴ : Zero α
inst✝³ : LinearOrder α
inst✝² : PosMulMono α
inst✝¹ : MulPosMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u * v)

Proof state:
case intro.intro
α : Type u_1
ι : Type u_4
inst✝⁵ : Mul α
inst✝⁴ : Zero α
inst✝³ : LinearOrder α
inst✝² : PosMulMono α
inst✝¹ : MulPosMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u * v)

Tactic:
exact IsCoboundedUnder.of_frequently_le (a := U * V)
  <| (hV.and_eventually (hU.and (h₁.and h₃))).mono fun x ⟨x_V, x_U, u_0, v_0⟩ ↦
  mul_le_mul x_U x_V v_0 (u_0.trans x_U)

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp] lemma pow_pos (ha : 0 < a) : ∀ n, 0 < a ^ n
  | 0 => by nontriviality; rw [pow_zero]; exact zero_lt_one
  | _ + 1 => pow_succ a _ ▸ mul_pos (pow_pos ha _) ha

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
ha : 0 < a
inst✝ : Nontrivial M₀
⊢ 0 < 1

Tactic:
exact zero_lt_one

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulStrictMono M₀
ha : 0 < a
⊢ 0 < a ^ 0

Tactic:
nontriviality

Result:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
ha : 0 < a
inst✝ : Nontrivial M₀
⊢ 0 < a ^ 0

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
ha : 0 < a
inst✝ : Nontrivial M₀
⊢ 0 < a ^ 0

Tactic:
rw [pow_zero]

Result:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
ha : 0 < a
inst✝ : Nontrivial M₀
⊢ 0 < 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem fmod_one (a : Int) : a.fmod 1 = 0

Proof state:
a : Int
⊢ a.fmod 1 = 0

Tactic:
simp [fmod_def, Int.one_mul, Int.sub_self]

Result:
no goals
-- Mathlib/Topology/Order/IsLUB.lean
theorem exists_seq_strictAnti_tendsto' [DenselyOrdered α] [FirstCountableTopology α] {x y : α}
    (hy : x < y) : ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, u n ∈ Ioo x y) ∧ Tendsto u atTop (𝓝 x)

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
x y : α
hy : x < y
⊢ ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo x y) ∧ Tendsto u atTop (𝓝 x)

Tactic:
simpa only [dual_Ioo]
  using exists_seq_strictMono_tendsto' (α := αᵒᵈ) (OrderDual.toDual_lt_toDual.2 hy)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_subset_right_1 {s m n : Nat} : range' s m ⊆ range' s n ↔ m ≤ n :=
  range'_subset_right (by decide)

Proof state:
s m n : Nat
⊢ 0 < 1

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem le_emultiplicity_of_le_multiplicity {n : ℕ} (h : n ≤ multiplicity a b) :
    n ≤ emultiplicity a b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≤ multiplicity a b
⊢ ↑n ≤ emultiplicity a b

Tactic:
exact_mod_cast (WithTop.coe_mono h).trans multiplicity_le_emultiplicity

Result:
no goals
-- Mathlib/Tactic/LinearCombination/Lemmas.lean
theorem eq_of_eq [Add α] [IsRightCancelAdd α] (p : (a:α) = b) (H : a' + b = b' + a) : a' = b'

Proof state:
α : Type u_1
a a' b b' : α
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
p : a = b
H : a' + b = b' + b
⊢ a' = b'

Tactic:
exact add_right_cancel H

Result:
no goals

Proof state:
α : Type u_1
a a' b b' : α
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
p : a = b
H : a' + b = b' + a
⊢ a' = b'

Tactic:
rw [p] at H

Result:
α : Type u_1
a a' b b' : α
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
p : a = b
H : a' + b = b' + b
⊢ a' = b'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem run_modifyGet [Monad m] (f : σ → α × σ) (s : σ) : (modifyGet f : StateT σ m α).run s = pure ((f s).1, (f s).2)

Proof state:
m : Type u_1 → Type u_2
σ α : Type u_1
inst✝ : Monad m
f : σ → α × σ
s : σ
⊢ (modifyGet f).run s = pure ((f s).fst, (f s).snd)

Tactic:
simp [modifyGet, MonadStateOf.modifyGet, StateT.modifyGet, run]

Result:
no goals
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma iterateFrobenius_zero_apply : iterateFrobenius R p 0 x = x

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p 0) x = x

Tactic:
rw [iterateFrobenius_def, pow_zero, pow_one]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem isClosed_C0 : IsClosed (C0 C ho)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ IsClosed (C0 C ho)

Tactic:
refine hC.inter ?_

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ IsClosed {f | f (term I ho) = false}

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Continuous fun f => f (term I ho)
⊢ IsClosed {f | f (term I ho) = false}

Tactic:
exact IsClosed.preimage h (t := {false}) (isClosed_discrete _)

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ IsClosed {f | f (term I ho) = false}

Tactic:
have h : Continuous (fun (f : I → Bool) ↦ f (term I ho)) := continuous_apply (term I ho)

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Continuous fun f => f (term I ho)
⊢ IsClosed {f | f (term I ho) = false}
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem linearIndependent_left_op_of_flat (H : A.LinearDisjoint B) [Module.Flat R B]
    {ι : Type*} {a : ι → A} (ha : LinearIndependent R a) :
    LinearIndependent B.op (MulOpposite.op ∘ A.val ∘ a)

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Module.Flat R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
⊢ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)

Tactic:
have h := Submodule.LinearDisjoint.linearIndependent_left_of_flat H ha

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Module.Flat R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
h : LinearMap.ker (Submodule.mulLeftMap (toSubmodule B) a) = ⊥
⊢ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Module.Flat R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
h : LinearMap.ker (Submodule.mulLeftMap (toSubmodule B) a) = ⊥
⊢ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)

Tactic:
rwa [mulLeftMap_ker_eq_bot_iff_linearIndependent_op] at h

Result:
no goals
-- Mathlib/Logic/Function/FiberPartition.lean
lemma map_preimage_eq_image_map {W : Type*} (f : Y → Z) (g : Z → W) (a : Fiber (g ∘ f)) :
    g (f a.preimage) = a.image

Proof state:
Y : Type u_2
Z : Type u_3
W : Type u_4
f : Y → Z
g : Z → W
a : Fiber (g ∘ f)
⊢ g (f (preimage (g ∘ f) a)) = image (g ∘ f) a

Tactic:
rw [← map_preimage_eq_image, comp_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
theorem IsCompact.closure_subset_measurableSet [R1Space γ] {K s : Set γ} (hK : IsCompact K)
    (hs : MeasurableSet s) (hKs : K ⊆ s) : closure K ⊆ s

Proof state:
γ : Type u_3
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : R1Space γ
K s : Set γ
hK : IsCompact K
hs : MeasurableSet s
hKs : K ⊆ s
⊢ closure K ⊆ s

Tactic:
rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]

Result:
γ : Type u_3
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : R1Space γ
K s : Set γ
hK : IsCompact K
hs : MeasurableSet s
hKs : K ⊆ s
⊢ ∀ i ∈ K, {y | Inseparable i y} ⊆ s

Proof state:
γ : Type u_3
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : R1Space γ
K s : Set γ
hK : IsCompact K
hs : MeasurableSet s
hKs : K ⊆ s
⊢ ∀ i ∈ K, {y | Inseparable i y} ⊆ s

Tactic:
exact fun x hx y hy ↦ (hy.mem_measurableSet_iff hs).1 (hKs hx)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem?_zero_ofNat_one : (BitVec.ofNat (w+1) 1)[0]? = some true

Proof state:
w : Nat
⊢ (1#(w + 1))[0]? = some true

Tactic:
simp

Result:
no goals