harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/IsPrimePow.lean
theorem Prime.isPrimePow {p : R} (hp : Prime p) : IsPrimePow p :=
  ⟨p, 1, hp, zero_lt_one, by simp⟩

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
p : R
hp : Prime p
⊢ p ^ 1 = p

Tactic:
simp

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Finset.Nonempty.ciSup_mem_image {s : Finset ι} (h : s.Nonempty) :
    ⨆ i ∈ s, f i ∈ s.image f :=
  s.ciSup_mem_image _ (h.imp (by simp))

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Finset ι
h : s.Nonempty
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem zipIdx_mk (a : Array α) (h : a.size = n) (k : Nat := 0) :
    (Vector.mk a h).zipIdx k = Vector.mk (a.zipIdx k) (by simp [h]) := rfl

Proof state:
α : Type ?u.17743
n : Nat
a : Array α
h : a.size = n
k : optParam Nat 0
⊢ (a.zipIdx k).size = n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
@[simp] lemma image_snd_graphOn (f : α → β) : Prod.snd '' s.graphOn f = f '' s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ Prod.snd '' graphOn f s = f '' s

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
s : Set α
f : α → β
x : β
⊢ x ∈ Prod.snd '' graphOn f s ↔ x ∈ f '' s

Proof state:
case h
α : Type u_1
β : Type u_2
s : Set α
f : α → β
x : β
⊢ x ∈ Prod.snd '' graphOn f s ↔ x ∈ f '' s

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.diag_map_fst_snd {X Y : C} [HasBinaryProduct X Y] [HasBinaryProduct (X ⨯ Y) (X ⨯ Y)] :
    diag (X ⨯ Y) ≫ prod.map prod.fst prod.snd = 𝟙 (X ⨯ Y)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (X ⨯ Y) (X ⨯ Y)
⊢ diag (X ⨯ Y) ≫ map fst snd = 𝟙 (X ⨯ Y)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/Basic.lean
theorem fst_map (x : P α) (f : α → β) : (P.map f x).1 = x.1

Proof state:
case mk
P : PFunctor.{u}
α : Type v₁
β : Type v₂
f : α → β
fst✝ : P.A
snd✝ : P.B fst✝ → α
⊢ (P.map f ⟨fst✝, snd✝⟩).fst = ⟨fst✝, snd✝⟩.fst

Tactic:
rfl

Result:
no goals

Proof state:
P : PFunctor.{u}
α : Type v₁
β : Type v₂
x : ↑P α
f : α → β
⊢ (P.map f x).fst = x.fst

Tactic:
cases x

Result:
case mk
P : PFunctor.{u}
α : Type v₁
β : Type v₂
f : α → β
fst✝ : P.A
snd✝ : P.B fst✝ → α
⊢ (P.map f ⟨fst✝, snd✝⟩).fst = ⟨fst✝, snd✝⟩.fst
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma LeftHomologyData.leftHomologyIso_hom_naturality
    (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
    h₁.homologyIso.hom ≫ leftHomologyMap' φ h₁ h₂ =
      homologyMap φ ≫ h₂.homologyIso.hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.homologyIso.hom ≫ leftHomologyMap' φ h₁ h₂ = homologyMap φ ≫ h₂.homologyIso.hom

Tactic:
dsimp [homologyIso, ShortComplex.leftHomologyIso, homologyMap, homologyMap', leftHomologyIso]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ (leftHomologyMap' (𝟙 S₁) S₁.homologyData.left S₁.leftHomologyData ≫ leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁) ≫
      leftHomologyMap' φ h₁ h₂ =
    leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left ≫
      leftHomologyMap' (𝟙 S₂) S₂.homologyData.left S₂.leftHomologyData ≫ leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData h₂

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ (leftHomologyMap' (𝟙 S₁) S₁.homologyData.left S₁.leftHomologyData ≫ leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁) ≫
      leftHomologyMap' φ h₁ h₂ =
    leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left ≫
      leftHomologyMap' (𝟙 S₂) S₂.homologyData.left S₂.leftHomologyData ≫ leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData h₂

Tactic:
simp only [← leftHomologyMap'_comp, id_comp, comp_id]

Result:
no goals
-- Mathlib/Topology/DiscreteQuotient.lean
theorem ofLE_refl_apply (a : A) : ofLE (le_refl A) a = a

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
a : Quotient A.toSetoid
⊢ ofLE ⋯ a = a

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_Iic {a : ℝ} : volume (Iic a) = ∞

Proof state:
a : ℝ
⊢ volume (Iio a) = ⊤

Tactic:
simp

Result:
no goals

Proof state:
a : ℝ
⊢ volume (Iic a) = ⊤

Tactic:
rw [← measure_congr Iio_ae_eq_Iic]

Result:
a : ℝ
⊢ volume (Iio a) = ⊤
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_union_ae (hst : AEDisjoint μ s t) (ht : NullMeasurableSet t μ)
    (hfs : IntegrableOn f s μ) (hft : IntegrableOn f t μ) :
    ∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ + ∫ x in t, f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
hst : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in t, f x ∂μ

Tactic:
simp only [IntegrableOn, Measure.restrict_union₀ hst ht, integral_add_measure hfs hft]

Result:
no goals
-- Mathlib/NumberTheory/Fermat.lean
theorem fermatNumber_eq_prod_add_two (n : ℕ) :
    fermatNumber n = ∏ k ∈ range n, fermatNumber k + 2

Proof state:
n : ℕ
⊢ n.fermatNumber = ∏ k ∈ range n, k.fermatNumber + 2

Tactic:
rw [prod_fermatNumber, Nat.sub_add_cancel]

Result:
n : ℕ
⊢ 2 ≤ n.fermatNumber

Proof state:
n : ℕ
⊢ 2 ≤ n.fermatNumber

Tactic:
exact le_of_lt <| two_lt_fermatNumber _

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Basic.lean
lemma tsub_tsub_eq_min (a b : α) : a - (a - b) = min a b

Proof state:
α : Type u_1
inst✝⁴ : LinearOrderedAddCommMonoid α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
⊢ a - (a - b) = a ⊓ b

Tactic:
rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
theorem indepSet_iff_indepSets_singleton {m0 : MeasurableSpace Ω} (hs_meas : MeasurableSet s)
    (ht_meas : MeasurableSet t) (κ : Kernel α Ω) (μ : Measure α)
    [IsZeroOrMarkovKernel κ] :
    IndepSet s t κ μ ↔ IndepSets {s} {t} κ μ :=
  ⟨Indep.indepSets, fun h =>
    IndepSets.indep
      (generateFrom_le fun u hu => by rwa [Set.mem_singleton_iff.mp hu])
      (generateFrom_le fun u hu => by rwa [Set.mem_singleton_iff.mp hu])
      (IsPiSystem.singleton s) (IsPiSystem.singleton t) rfl rfl h⟩

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
m0 : MeasurableSpace Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h : IndepSets {s} {t} κ μ
u : Set Ω
hu : u ∈ {s}
⊢ MeasurableSet u

Tactic:
rwa [Set.mem_singleton_iff.mp hu]

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
m0 : MeasurableSpace Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h : IndepSets {s} {t} κ μ
u : Set Ω
hu : u ∈ {t}
⊢ MeasurableSet u

Tactic:
rwa [Set.mem_singleton_iff.mp hu]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem zipIdx_map_fst (n) (l : Array α) : map Prod.fst (zipIdx l n) = l

Proof state:
α : Type u_1
n : Nat
l : Array α
⊢ map Prod.fst (l.zipIdx n) = l

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
toList✝ : List α
⊢ map Prod.fst ({ toList := toList✝ }.zipIdx n) = { toList := toList✝ }

Proof state:
case mk
α : Type u_1
n : Nat
toList✝ : List α
⊢ map Prod.fst ({ toList := toList✝ }.zipIdx n) = { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_else_not_self {p : Prop} [Decidable p] {q : Prop} : (if p then q else ¬p) ↔ p → q

Proof state:
p : Prop
inst✝ : Decidable p
q : Prop
⊢ (if p then q else ¬p) ↔ p → q

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem Prod.noncompactSpace_iff :
    NoncompactSpace (X × Y) ↔ NoncompactSpace X ∧ Nonempty Y ∨ Nonempty X ∧ NoncompactSpace Y

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ NoncompactSpace (X × Y) ↔ NoncompactSpace X ∧ Nonempty Y ∨ Nonempty X ∧ NoncompactSpace Y

Tactic:
simp [← Filter.cocompact_neBot_iff, ← Filter.coprod_cocompact, Filter.coprod_neBot_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
    (concat x b)[i] = if i = 0 then b else x.getLsbD (i - 1)

Proof state:
w : Nat
x : BitVec w
b : Bool
i : Nat
h : i < w + 1
⊢ (x.concat b)[i] = if i = 0 then b else x.getLsbD (i - 1)

Tactic:
simp only [concat, getElem_eq_testBit_toNat, getLsbD, toNat_append,
  toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq]

Result:
w : Nat
x : BitVec w
b : Bool
i : Nat
h : i < w + 1
⊢ ((x.toNat * 2 ^ 1).testBit i || b.toNat.testBit i) = if i = 0 then b else x.toNat.testBit (i - 1)

Proof state:
case zero
w : Nat
x : BitVec w
b : Bool
h : 0 < w + 1
⊢ ((x.toNat * 2 ^ 1).testBit 0 || b.toNat.testBit 0) = if 0 = 0 then b else x.toNat.testBit (0 - 1)

Tactic:
simp [Nat.mod_eq_of_lt b.toNat_lt]

Result:
no goals

Proof state:
case succ
w : Nat
x : BitVec w
b : Bool
n✝ : Nat
h : n✝ + 1 < w + 1
⊢ ((x.toNat * 2 ^ 1).testBit (n✝ + 1) || b.toNat.testBit (n✝ + 1)) =
    if n✝ + 1 = 0 then b else x.toNat.testBit (n✝ + 1 - 1)

Tactic:
simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
b : Bool
i : Nat
h : i < w + 1
⊢ ((x.toNat * 2 ^ 1).testBit i || b.toNat.testBit i) = if i = 0 then b else x.toNat.testBit (i - 1)

Tactic:
cases i

Result:
case zero
w : Nat
x : BitVec w
b : Bool
h : 0 < w + 1
⊢ ((x.toNat * 2 ^ 1).testBit 0 || b.toNat.testBit 0) = if 0 = 0 then b else x.toNat.testBit (0 - 1)

case succ
w : Nat
x : BitVec w
b : Bool
n✝ : Nat
h : n✝ + 1 < w + 1
⊢ ((x.toNat * 2 ^ 1).testBit (n✝ + 1) || b.toNat.testBit (n✝ + 1)) =
    if n✝ + 1 = 0 then b else x.toNat.testBit (n✝ + 1 - 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_min {a b c : Int} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c :=
  ⟨fun h => ⟨Int.le_trans h (Int.min_le_left ..), Int.le_trans h (Int.min_le_right ..)⟩,
   fun ⟨h₁, h₂⟩ => by rw [Int.min_def]; split <;> assumption⟩

Proof state:
a b c : Int
x✝ : a ≤ b ∧ a ≤ c
h₁ : a ≤ b
h₂ : a ≤ c
⊢ a ≤ if b ≤ c then b else c

Tactic:
split <;> assumption

Result:
no goals

Proof state:
a b c : Int
x✝ : a ≤ b ∧ a ≤ c
h₁ : a ≤ b
h₂ : a ≤ c
⊢ a ≤ min b c

Tactic:
rw [Int.min_def]

Result:
a b c : Int
x✝ : a ≤ b ∧ a ≤ c
h₁ : a ≤ b
h₂ : a ≤ c
⊢ a ≤ if b ≤ c then b else c
-- Mathlib/RepresentationTheory/Rep.lean
theorem leftRegularHom_hom_single {A : Rep k G} (g : G) (x : A) (r : k) :
    (leftRegularHom A x).hom (Finsupp.single g r) = r • A.ρ g x

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
A : Rep k G
g : G
x : ↑A.V
r : k
⊢ (ConcreteCategory.hom (A.leftRegularHom x).hom) (Finsupp.single g r) = r • (A.ρ g) x

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean
@[simp]
lemma tsum_const (c : ℝ≥0∞) : ∑' _ : α, c = ENat.card α * c

Proof state:
α : Type u_1
c : ℝ≥0∞
⊢ ∑' (x : ↑univ), c = ↑(ENat.card α) * c

Tactic:
simpa [encard_univ] using tsum_set_const univ c

Result:
no goals

Proof state:
α : Type u_1
c : ℝ≥0∞
⊢ ∑' (x : α), c = ↑(ENat.card α) * c

Tactic:
rw [← tsum_univ]

Result:
α : Type u_1
c : ℝ≥0∞
⊢ ∑' (x : ↑univ), c = ↑(ENat.card α) * c
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem isAdjoinRootMonic_root_eq_root (hf : Monic f) :
    (AdjoinRoot.isAdjoinRootMonic f hf).root = AdjoinRoot.root f

Proof state:
R : Type u
inst✝ : CommRing R
f : R[X]
hf : f.Monic
⊢ (AdjoinRoot.isAdjoinRootMonic f hf).root = root f

Tactic:
simp only [IsAdjoinRoot.root, AdjoinRoot.root, AdjoinRoot.isAdjoinRootMonic_map_eq_mk]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.Finset.stronglyMeasurable_prod {ι : Type*} {f : ι → α → M} (s : Finset ι)
    (hf : ∀ i ∈ s, StronglyMeasurable (f i)) : StronglyMeasurable fun a => ∏ i ∈ s, f i a

Proof state:
α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
ι : Type u_6
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, StronglyMeasurable (f i)
⊢ StronglyMeasurable fun a => ∏ i ∈ s, f i a

Tactic:
simpa only [← Finset.prod_apply] using s.stronglyMeasurable_prod' hf

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem IntegrableAtFilter.smul {𝕜 : Type*} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 E]
    [BoundedSMul 𝕜 E] {f : α → E} (hf : IntegrableAtFilter f l μ) (c : 𝕜) :
    IntegrableAtFilter (c • f) l μ

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_6
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : α → E
hf : IntegrableAtFilter f l μ
c : 𝕜
⊢ IntegrableAtFilter (c • f) l μ

Tactic:
rcases hf with ⟨s, sl, hs⟩

Result:
case intro.intro
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_6
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : α → E
c : 𝕜
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
⊢ IntegrableAtFilter (c • f) l μ

Proof state:
case intro.intro
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_6
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : α → E
c : 𝕜
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
⊢ IntegrableAtFilter (c • f) l μ

Tactic:
exact ⟨s, sl, hs.smul c⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem fderivWithin_continuousMultilinear_apply_const_apply (hxs : UniqueDiffWithinAt 𝕜 s x)
    (hc : DifferentiableWithinAt 𝕜 c s x) (u : ∀ i, M i) (m : E) :
    (fderivWithin 𝕜 (fun y ↦ (c y) u) s x) m = (fderivWithin 𝕜 c s x) m u

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
x : E
s : Set E
ι : Type u_5
inst✝⁴ : Fintype ι
M : ι → Type u_6
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
H : Type u_7
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
u : (i : ι) → M i
m : E
⊢ (fderivWithin 𝕜 (fun y => (c y) u) s x) m = ((fderivWithin 𝕜 c s x) m) u

Tactic:
simp [fderivWithin_continuousMultilinear_apply_const hxs hc]

Result:
no goals
-- Mathlib/Data/Set/MemPartition.lean
@[simp]
lemma memPartitionSet_zero (f : ℕ → Set α) (a : α) : memPartitionSet f 0 a = univ

Proof state:
α : Type u_1
f : ℕ → Set α
a : α
⊢ memPartitionSet f 0 a = univ

Tactic:
simp [memPartitionSet]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_comm : a ∆ b = b ∆ a

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b = b ∆ a

Tactic:
simp only [symmDiff, sup_comm]

Result:
no goals
-- Mathlib/Probability/Martingale/Centering.lean
theorem integrable_martingalePart (hf_int : ∀ n, Integrable (f n) μ) (n : ℕ) :
    Integrable (martingalePart f ℱ μ n) μ

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf_int : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
⊢ Integrable ((fun n => f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i])) n) μ

Tactic:
fun_prop

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf_int : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
⊢ Integrable (martingalePart f ℱ μ n) μ

Tactic:
rw [martingalePart_eq_sum]

Result:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf_int : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
⊢ Integrable ((fun n => f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i])) n) μ
-- Mathlib/RingTheory/Extension.lean
/-- The action of `P` on `P.Cotangent` for an extension `P → S`. -/
@[simp]
lemma Cotangent.val_smul' (r : P.Ring) (x : P.Cotangent) : (r • x).val = r • x.val

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
r : P.Ring
x : P.Cotangent
⊢ (P.σ ((algebraMap P.Ring S) r) - r) • x.val = 0

Tactic:
exact Cotangent.smul_eq_zero_of_mem _ (by simp) _

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
r : P.Ring
x : P.Cotangent
⊢ P.σ ((algebraMap P.Ring S) r) - r ∈ P.ker

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
r : P.Ring
x : P.Cotangent
⊢ (r • x).val = r • x.val

Tactic:
rw [val_smul''', ← sub_eq_zero, ← sub_smul]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
r : P.Ring
x : P.Cotangent
⊢ (P.σ ((algebraMap P.Ring S) r) - r) • x.val = 0
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma d_comp_XIsoOfEq_inv (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₃ = p₂) (p₁ : ι) :
    K.d p₁ p₂ ≫ (K.XIsoOfEq h).inv = K.d p₁ p₃

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₃ p₁ : ι
⊢ K.d p₁ p₃ ≫ (K.XIsoOfEq ⋯).inv = K.d p₁ p₃

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
h : p₃ = p₂
p₁ : ι
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq h).inv = K.d p₁ p₃

Tactic:
subst h

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₃ p₁ : ι
⊢ K.d p₁ p₃ ≫ (K.XIsoOfEq ⋯).inv = K.d p₁ p₃
-- Mathlib/Order/RelClasses.lean
theorem Prod.wellFoundedLT' [PartialOrder α] [WellFoundedLT α] [Preorder β] [WellFoundedLT β] :
    WellFoundedLT (α × β) :=
  Subrelation.isWellFounded (Prod.Lex (· < ·) (· < ·))
    fun {x y} h ↦ (Prod.lt_iff.mp h).elim (fun h ↦ .left _ _ h.1)
    fun h ↦ h.1.lt_or_eq.elim (.left _ _) <| by cases x; cases y; rintro rfl; exact .right _ h.2

Proof state:
α : Type u
β : Type v
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
x y : α × β
h✝ : x < y
h : x.fst ≤ y.fst ∧ x.snd < y.snd
⊢ x.fst = y.fst → Prod.Lex (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) x y

Tactic:
cases x

Result:
case mk
α : Type u
β : Type v
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
y : α × β
fst✝ : α
snd✝ : β
h✝ : (fst✝, snd✝) < y
h : (fst✝, snd✝).fst ≤ y.fst ∧ (fst✝, snd✝).snd < y.snd
⊢ (fst✝, snd✝).fst = y.fst → Prod.Lex (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) (fst✝, snd✝) y

Proof state:
case mk.mk
α : Type u
β : Type v
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
fst✝ : α
snd✝¹ snd✝ : β
h✝ : (fst✝, snd✝¹) < ((fst✝, snd✝¹).fst, snd✝)
h : (fst✝, snd✝¹).fst ≤ ((fst✝, snd✝¹).fst, snd✝).fst ∧ (fst✝, snd✝¹).snd < ((fst✝, snd✝¹).fst, snd✝).snd
⊢ Prod.Lex (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) (fst✝, snd✝¹) ((fst✝, snd✝¹).fst, snd✝)

Tactic:
exact .right _ h.2

Result:
no goals

Proof state:
case mk
α : Type u
β : Type v
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
y : α × β
fst✝ : α
snd✝ : β
h✝ : (fst✝, snd✝) < y
h : (fst✝, snd✝).fst ≤ y.fst ∧ (fst✝, snd✝).snd < y.snd
⊢ (fst✝, snd✝).fst = y.fst → Prod.Lex (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) (fst✝, snd✝) y

Tactic:
cases y

Result:
case mk.mk
α : Type u
β : Type v
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
fst✝¹ : α
snd✝¹ : β
fst✝ : α
snd✝ : β
h✝ : (fst✝¹, snd✝¹) < (fst✝, snd✝)
h : (fst✝¹, snd✝¹).fst ≤ (fst✝, snd✝).fst ∧ (fst✝¹, snd✝¹).snd < (fst✝, snd✝).snd
⊢ (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst →
    Prod.Lex (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) (fst✝¹, snd✝¹) (fst✝, snd✝)

Proof state:
case mk.mk
α : Type u
β : Type v
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
fst✝¹ : α
snd✝¹ : β
fst✝ : α
snd✝ : β
h✝ : (fst✝¹, snd✝¹) < (fst✝, snd✝)
h : (fst✝¹, snd✝¹).fst ≤ (fst✝, snd✝).fst ∧ (fst✝¹, snd✝¹).snd < (fst✝, snd✝).snd
⊢ (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst →
    Prod.Lex (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) (fst✝¹, snd✝¹) (fst✝, snd✝)

Tactic:
rintro rfl

Result:
case mk.mk
α : Type u
β : Type v
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
fst✝ : α
snd✝¹ snd✝ : β
h✝ : (fst✝, snd✝¹) < ((fst✝, snd✝¹).fst, snd✝)
h : (fst✝, snd✝¹).fst ≤ ((fst✝, snd✝¹).fst, snd✝).fst ∧ (fst✝, snd✝¹).snd < ((fst✝, snd✝¹).fst, snd✝).snd
⊢ Prod.Lex (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) (fst✝, snd✝¹) ((fst✝, snd✝¹).fst, snd✝)
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_mul_right {L : Type*} [RCLike L] (r : L) (f : α → L) :
    ∫ a, f a * r ∂μ = (∫ a, f a ∂μ) * r

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
L : Type u_6
inst✝ : RCLike L
r : L
f : α → L
⊢ ∫ (a : α), r * f a ∂μ = r * ∫ (a : α), f a ∂μ

Tactic:
exact integral_mul_left r f

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
L : Type u_6
inst✝ : RCLike L
r : L
f : α → L
⊢ ∫ (a : α), f a * r ∂μ = (∫ (a : α), f a ∂μ) * r

Tactic:
simp only [mul_comm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
L : Type u_6
inst✝ : RCLike L
r : L
f : α → L
⊢ ∫ (a : α), r * f a ∂μ = r * ∫ (a : α), f a ∂μ
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma ΨSq_odd (m : ℤ) : W.ΨSq (2 * m + 1) =
    (W.preΨ (m + 2) * W.preΨ m ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
      W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2)) ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ W.ΨSq (2 * m + 1) =
    ((W.preΨ (m + 2) * W.preΨ m ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
        W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) ^
      2

Tactic:
rw [ΨSq, preΨ_odd, if_neg m.not_even_two_mul_add_one, mul_one]

Result:
no goals