harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_add_eq_left_of_totalDegree_lt {p q : MvPolynomial σ R}
    (h : q.totalDegree < p.totalDegree) : (p + q).totalDegree = p.totalDegree

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
h : b ∈ q.support
⊢ p.totalDegree ≤ q.totalDegree

Tactic:
rw [totalDegree_eq p, hb₂, totalDegree_eq]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
h : b ∈ q.support
⊢ (toMultiset b).card ≤ q.support.sup fun m => (toMultiset m).card

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
h : b ∈ q.support
⊢ (toMultiset b).card ≤ q.support.sup fun m => (toMultiset m).card

Tactic:
apply Finset.le_sup h

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem left_lt_opow {a b : Ordinal} (ha : 1 < a) (hb : 1 < b) : a < a ^ b

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

Tactic:
conv_lhs => rw [← opow_one a]

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

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

Tactic:
rwa [opow_lt_opow_iff_right ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem or_allOnes {x : BitVec w} : x ||| allOnes w = allOnes w

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (x ||| allOnes w).getLsbD i = (allOnes w).getLsbD i

Tactic:
simp [h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x ||| allOnes w = allOnes w

Tactic:
ext i h

Result:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (x ||| allOnes w).getLsbD i = (allOnes w).getLsbD i
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
lemma ne_int (z : ℍ) : ∀ n : ℤ, z.1 ≠ n

Proof state:
z : ℍ
n : ℤ
⊢ ↑z ≠ ↑n

Tactic:
have h1 := z.2

Result:
z : ℍ
n : ℤ
h1 : 0 < (↑z).im
⊢ ↑z ≠ ↑n

Proof state:
z : ℍ
⊢ ∀ (n : ℤ), ↑z ≠ ↑n

Tactic:
intro n

Result:
z : ℍ
n : ℤ
⊢ ↑z ≠ ↑n

Proof state:
z : ℍ
n : ℤ
h1 : 0 < (↑z).im
⊢ ↑z ≠ ↑n

Tactic:
aesop

Result:
no goals
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem le_succ_rank_sUnion (x : ZFSet) : rank x ≤ succ (rank (⋃₀ x))

Proof state:
x : ZFSet.{u_1}
⊢ x.rank ≤ succ (⋃₀ x).rank

Tactic:
rw [← rank_powerset]

Result:
x : ZFSet.{u_1}
⊢ x.rank ≤ (⋃₀ x).powerset.rank

Proof state:
case h
x z : ZFSet.{u_1}
a✝¹ : z ∈ x
z✝ : ZFSet.{u_1}
a✝ : z✝ ∈ z
⊢ ∃ z ∈ x, z✝ ∈ z

Tactic:
exists z

Result:
no goals

Proof state:
case h
x z : ZFSet.{u_1}
a✝ : z ∈ x
⊢ z ⊆ ⋃₀ x

Tactic:
intro _ _

Result:
case h
x z : ZFSet.{u_1}
a✝¹ : z ∈ x
z✝ : ZFSet.{u_1}
a✝ : z✝ ∈ z
⊢ z✝ ∈ ⋃₀ x

Proof state:
case h
x z : ZFSet.{u_1}
a✝ : z ∈ x
⊢ z ∈ (⋃₀ x).powerset

Tactic:
rw [mem_powerset]

Result:
case h
x z : ZFSet.{u_1}
a✝ : z ∈ x
⊢ z ⊆ ⋃₀ x

Proof state:
case h
x : ZFSet.{u_1}
⊢ x ⊆ (⋃₀ x).powerset

Tactic:
intro z _

Result:
case h
x z : ZFSet.{u_1}
a✝ : z ∈ x
⊢ z ∈ (⋃₀ x).powerset

Proof state:
case h
x z : ZFSet.{u_1}
a✝¹ : z ∈ x
z✝ : ZFSet.{u_1}
a✝ : z✝ ∈ z
⊢ z✝ ∈ ⋃₀ x

Tactic:
rw [mem_sUnion]

Result:
case h
x z : ZFSet.{u_1}
a✝¹ : z ∈ x
z✝ : ZFSet.{u_1}
a✝ : z✝ ∈ z
⊢ ∃ z ∈ x, z✝ ∈ z

Proof state:
x : ZFSet.{u_1}
⊢ x.rank ≤ (⋃₀ x).powerset.rank

Tactic:
apply rank_mono

Result:
case h
x : ZFSet.{u_1}
⊢ x ⊆ (⋃₀ x).powerset
-- Mathlib/CategoryTheory/Abelian/SerreClass/Basic.lean
lemma prop_X₂_of_exact {S : ShortComplex C} (hS : S.Exact)
    (h₁ : P S.X₁) (h₃ : P S.X₃) : P S.X₂

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
S : ShortComplex C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
⊢ P S.X₂

Tactic:
let d := S.homologyData

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
S : ShortComplex C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
⊢ P S.X₂

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
S : ShortComplex C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
⊢ P S.X₂

Tactic:
have := hS.epi_f' d.left

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
S : ShortComplex C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
this : Epi d.left.f'
⊢ P S.X₂

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
S : ShortComplex C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
this : Epi d.left.f'
⊢ P S.X₂

Tactic:
have := hS.mono_g' d.right

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
S : ShortComplex C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
this✝ : Epi d.left.f'
this : Mono d.right.g'
⊢ P S.X₂

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
S : ShortComplex C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
this✝ : Epi d.left.f'
this : Mono d.right.g'
⊢ P S.X₂

Tactic:
exact (P.prop_X₂_of_shortExact (hS.shortExact d)
  (P.prop_of_epi d.left.f' h₁) (P.prop_of_mono d.right.g' h₃) :)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Presheaf.lean
theorem final_toCostructuredArrow_comp_pre {c : Cocone (F ⋙ yoneda)} (hc : IsColimit c) :
    Functor.Final (c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt)

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
⊢ IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))

Tactic:
apply IsTerminal.ofIso Over.mkIdTerminal

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
⊢ Over.mk (𝟙 c.pt) ≅
    colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt)

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
isc : IsColimit
  ((Over.forget c.pt).mapCocone
    (colimit.cocone
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))) :=
  isColimitOfPreserves (Over.forget c.pt)
    (colimit.isColimit
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ Over.mk (𝟙 c.pt) ≅
    colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt)

Tactic:
exact Over.isoMk (hc.coconePointUniqueUpToIso isc) (hc.hom_ext fun i => by simp)

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
⊢ Over.mk (𝟙 c.pt) ≅
    colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt)

Tactic:
let isc : IsColimit ((Over.forget _).mapCocone _) := isColimitOfPreserves _
  (colimit.isColimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙
    CostructuredArrow.toOver yoneda c.pt))

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
isc : IsColimit
  ((Over.forget c.pt).mapCocone
    (colimit.cocone
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))) :=
  isColimitOfPreserves (Over.forget c.pt)
    (colimit.isColimit
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ Over.mk (𝟙 c.pt) ≅
    colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt)
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem tendsto_card_div_pow₄ (hs₁ : IsBounded s)
    (hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) :
    ∀ᶠ x : ℝ in atTop, (Nat.card ↑(s ∩ x⁻¹ • L) : ℝ) / x ^ card ι ≤
      (Nat.card ↑(s ∩ (⌈x⌉₊ : ℝ)⁻¹ • L) : ℝ) / x ^ card ι

Proof state:
case h.hab.h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 0 < x
⊢ Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) ≤
    Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))

Tactic:
exact tendsto_card_div_pow₂ s hs₁ hs₄ hx (Nat.le_ceil _)

Result:
no goals

Proof state:
case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 0 < x
⊢ ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι ≤
    ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
gcongr

Result:
case h.hab.h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 0 < x
⊢ Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) ≤
    Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ ∀ᶠ (x : ℝ) in atTop,
    ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι ≤
      ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

Result:
case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 0 < x
⊢ ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι ≤
    ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι
-- Mathlib/Data/Rel.lean
theorem image_comp (s : Rel β γ) (t : Set α) : image (r • s) t = image s (image r t)

Proof state:
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, (∃ x_1 ∈ t, r x_1 x) ∧ s x z) → ∃ x ∈ t, (r • s) x z

Tactic:
rintro ⟨y, ⟨x, xt, rxy⟩, syz⟩

Result:
case h.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
y : β
syz : s y z
x : α
xt : x ∈ t
rxy : r x y
⊢ ∃ x ∈ t, (r • s) x z

Proof state:
case h.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
x : α
xt : x ∈ t
y : β
rxy : r x y
syz : s y z
⊢ ∃ x, (∃ x_1 ∈ t, r x_1 x) ∧ s x z

Tactic:
exact ⟨y, ⟨x, xt, rxy⟩, syz⟩

Result:
no goals

Proof state:
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x ∈ t, (r • s) x z) → ∃ x, (∃ x_1 ∈ t, r x_1 x) ∧ s x z

Tactic:
rintro ⟨x, xt, y, rxy, syz⟩

Result:
case h.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
x : α
xt : x ∈ t
y : β
rxy : r x y
syz : s y z
⊢ ∃ x, (∃ x_1 ∈ t, r x_1 x) ∧ s x z

Proof state:
case h.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
y : β
syz : s y z
x : α
xt : x ∈ t
rxy : r x y
⊢ ∃ x ∈ t, (r • s) x z

Tactic:
exact ⟨x, xt, y, rxy, syz⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
⊢ (r • s).image t = s.image (r.image t)

Tactic:
ext z

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ z ∈ (r • s).image t ↔ z ∈ s.image (r.image t)

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ z ∈ (r • s).image t ↔ z ∈ s.image (r.image t)

Tactic:
simp only [mem_image]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x ∈ t, (r • s) x z) ↔ ∃ x, (∃ x_1 ∈ t, r x_1 x) ∧ s x z

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x ∈ t, (r • s) x z) ↔ ∃ x, (∃ x_1 ∈ t, r x_1 x) ∧ s x z

Tactic:
constructor

Result:
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x ∈ t, (r • s) x z) → ∃ x, (∃ x_1 ∈ t, r x_1 x) ∧ s x z

case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, (∃ x_1 ∈ t, r x_1 x) ∧ s x z) → ∃ x ∈ t, (r • s) x z
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem nontrivial_toCycle (f : Perm α) (hf : IsCycle f) : (toCycle f hf).Nontrivial

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
⊢ (f.toCycle hf).Nontrivial

Tactic:
simp [toCycle_eq_toList f hf x hx, hx, Cycle.nontrivial_coe_nodup_iff (nodup_toList _ _)]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ (f.toCycle hf).Nontrivial

Tactic:
obtain ⟨x, hx, -⟩ := id hf

Result:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
⊢ (f.toCycle hf).Nontrivial
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
@[simp]
lemma lift_mk_one (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (m : M) :
    (LocalizedModule.lift S g h) (LocalizedModule.mk m 1) = g m

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
m : M
⊢ (lift S g h) (mk m 1) = g m

Tactic:
simp [lift_mk]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
theorem mulMap_range : LinearMap.range (mulMap M N) = M * N

Proof state:
case intro.add
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
a b : ↥M ⊗[R] ↥N
ha : (M.mulMap N) a ∈ M * N
hb : (M.mulMap N) b ∈ M * N
⊢ (M.mulMap N) a + (M.mulMap N) b ∈ M * N

Tactic:
exact add_mem ha hb

Result:
no goals

Proof state:
case intro.tmul
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
a : ↥M
b : ↥N
⊢ (M.mulMap N) (a ⊗ₜ[R] b) ∈ M * N

Tactic:
exact mul_mem_mul a.2 b.2

Result:
no goals

Proof state:
case intro.add
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
a b : ↥M ⊗[R] ↥N
ha : (M.mulMap N) a ∈ M * N
hb : (M.mulMap N) b ∈ M * N
⊢ (M.mulMap N) (a + b) ∈ M * N

Tactic:
rw [_root_.map_add]

Result:
case intro.add
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
a b : ↥M ⊗[R] ↥N
ha : (M.mulMap N) a ∈ M * N
hb : (M.mulMap N) b ∈ M * N
⊢ (M.mulMap N) a + (M.mulMap N) b ∈ M * N

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ LinearMap.range (M.mulMap N) = M * N

Tactic:
refine le_antisymm ?_ (mul_le.2 fun m hm n hn ↦ ⟨⟨m, hm⟩ ⊗ₜ[R] ⟨n, hn⟩, rfl⟩)

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ LinearMap.range (M.mulMap N) ≤ M * N

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
x : ↥M ⊗[R] ↥N
⊢ (M.mulMap N) x ∈ M * N

Tactic:
induction x with
| zero => rw [_root_.map_zero]; exact zero_mem _
| tmul a b => exact mul_mem_mul a.2 b.2
| add a b ha hb => rw [_root_.map_add]; exact add_mem ha hb

Result:
no goals

Proof state:
case intro.zero
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ (M.mulMap N) 0 ∈ M * N

Tactic:
rw [_root_.map_zero]

Result:
case intro.zero
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ 0 ∈ M * N

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ LinearMap.range (M.mulMap N) ≤ M * N

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
x : ↥M ⊗[R] ↥N
⊢ (M.mulMap N) x ∈ M * N

Proof state:
case intro.zero
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ 0 ∈ M * N

Tactic:
exact zero_mem _

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem unifIntegrable_of' (hp : 1 ≤ p) (hp' : p ≠ ∞) {f : ι → α → β}
    (hf : ∀ i, StronglyMeasurable (f i))
    (h : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ≥0, 0 < C ∧
      ∀ i, eLpNorm ({ x | C ≤ ‖f i x‖₊ }.indicator (f i)) p μ ≤ ENNReal.ofReal ε) :
    UnifIntegrable f p μ

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
⊢ eLpNorm (s.indicator (f i)) p μ ≤
    eLpNorm ((s ∩ {x | C ≤ ‖f i x‖₊}).indicator (f i)) p μ + eLpNorm ((s ∩ {x | ‖f i x‖₊ < C}).indicator (f i)) p μ

Tactic:
refine le_trans (Eq.le ?_) (eLpNorm_add_le
  (StronglyMeasurable.aestronglyMeasurable
    ((hf i).indicator (hs.inter (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))))
  (StronglyMeasurable.aestronglyMeasurable
    ((hf i).indicator (hs.inter ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const))))
  hp)

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
⊢ eLpNorm (s.indicator (f i)) p μ =
    eLpNorm ((s ∩ {x | C ≤ ‖f i x‖₊}).indicator (f i) + (s ∩ {x | ‖f i x‖₊ < C}).indicator (f i)) p μ
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem le_natTrailingDegree_mul (h : p * q ≠ 0) :
    p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p = 0
⊢ p * q = 0

Tactic:
rw [hp, zero_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

Tactic:
exact le_trailingDegree_mul

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree

Tactic:
rw [← WithTop.coe_le_coe, WithTop.coe_add, ← Nat.cast_withTop (natTrailingDegree p),
  ← Nat.cast_withTop (natTrailingDegree q), ← Nat.cast_withTop (natTrailingDegree (p * q)),
  ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq,
  ← trailingDegree_eq_natTrailingDegree h]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p * q = 0

Tactic:
rw [hq, mul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
⊢ p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree

Tactic:
have hq : q ≠ 0 := fun hq => h (by rw [hq, mul_zero])

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
⊢ p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree

Tactic:
have hp : p ≠ 0 := fun hp => h (by rw [hp, zero_mul])

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
⊢ p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree
-- Mathlib/Probability/Process/Stopping.lean
theorem stoppedProcess_eq' (n : ℕ) : stoppedProcess u τ n = Set.indicator {a | n + 1 ≤ τ a} (u n) +
    ∑ i ∈ Finset.range (n + 1), Set.indicator {a | τ a = i} (u i)

Proof state:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
⊢ {a | n ≤ τ a}.indicator (u n) = {a | n + 1 ≤ τ a}.indicator (u n) + {a | τ a = n}.indicator (u n)

Tactic:
ext x

Result:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ {a | n ≤ τ a}.indicator (u n) x = ({a | n + 1 ≤ τ a}.indicator (u n) + {a | τ a = n}.indicator (u n)) x

Proof state:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ {a | n ≤ τ a}.indicator (u n) x = ({a | τ a = n} ∪ {a | n + 1 ≤ τ a}).indicator (u n) x

Tactic:
simp_rw [@eq_comm _ _ n, @le_iff_eq_or_lt _ _ n, Nat.succ_le_iff, Set.setOf_or]

Result:
no goals

Proof state:
case h.h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ x ∉ {a | τ a = n} ∩ {a | n + 1 ≤ τ a}

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case h.h.intro
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
h₁ : x ∈ {a | τ a = n}
h₂ : x ∈ {a | n + 1 ≤ τ a}
⊢ False

Proof state:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
this : {a | n ≤ τ a}.indicator (u n) = {a | n + 1 ≤ τ a}.indicator (u n) + {a | τ a = n}.indicator (u n)
⊢ stoppedProcess u τ n = {a | n + 1 ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range (n + 1), {a | τ a = i}.indicator (u i)

Tactic:
rw [stoppedProcess_eq, this, Finset.sum_range_succ_comm, ← add_assoc]

Result:
no goals

Proof state:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ {a | n ≤ τ a}.indicator (u n) x = ({a | n + 1 ≤ τ a}.indicator (u n) + {a | τ a = n}.indicator (u n)) x

Tactic:
rw [add_comm, Pi.add_apply, ← Set.indicator_union_of_not_mem_inter]

Result:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ {a | n ≤ τ a}.indicator (u n) x = ({a | τ a = n} ∪ {a | n + 1 ≤ τ a}).indicator (u n) x

case h.h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ x ∉ {a | τ a = n} ∩ {a | n + 1 ≤ τ a}

Proof state:
case h.h.intro
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
h₁ : x ∈ {a | τ a = n}
h₂ : x ∈ {a | n + 1 ≤ τ a}
⊢ False

Tactic:
rw [Set.mem_setOf] at h₁ h₂

Result:
case h.h.intro
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
h₁ : τ x = n
h₂ : n + 1 ≤ τ x
⊢ False

Proof state:
case h.h.intro
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
h₁ : τ x = n
h₂ : n + 1 ≤ τ x
⊢ False

Tactic:
exact (Nat.succ_le_iff.1 h₂).ne h₁.symm

Result:
no goals