harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Continuous.lean
lemma isContinuous_comp' {F₁ : C ⥤ D} {F₂ : D ⥤ E} {F₁₂ : C ⥤ E}
    (e : F₁ ⋙ F₂ ≅ F₁₂) (J : GrothendieckTopology C)
    (K : GrothendieckTopology D) (L : GrothendieckTopology E)
    [Functor.IsContinuous.{t} F₁ J K] [Functor.IsContinuous.{t} F₂ K L] :
    Functor.IsContinuous.{t} F₁₂ J L

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F₁ : C ⥤ D
F₂ : D ⥤ E
F₁₂ : C ⥤ E
e : F₁ ⋙ F₂ ≅ F₁₂
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F₁.IsContinuous J K
inst✝ : F₂.IsContinuous K L
⊢ F₁₂.IsContinuous J L

Tactic:
have := Functor.isContinuous_comp F₁ F₂ J K L

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F₁ : C ⥤ D
F₂ : D ⥤ E
F₁₂ : C ⥤ E
e : F₁ ⋙ F₂ ≅ F₁₂
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F₁.IsContinuous J K
inst✝ : F₂.IsContinuous K L
this : (F₁ ⋙ F₂).IsContinuous J L
⊢ F₁₂.IsContinuous J L

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F₁ : C ⥤ D
F₂ : D ⥤ E
F₁₂ : C ⥤ E
e : F₁ ⋙ F₂ ≅ F₁₂
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F₁.IsContinuous J K
inst✝ : F₂.IsContinuous K L
this : (F₁ ⋙ F₂).IsContinuous J L
⊢ F₁₂.IsContinuous J L

Tactic:
apply Functor.isContinuous_of_iso e

Result:
no goals
-- Mathlib/Data/Real/Pi/Wallis.lean
theorem W_le (k : ℕ) : W k ≤ π / 2

Proof state:
k : ℕ
⊢ W k ≤ π / 2

Tactic:
rw [← div_le_one pi_div_two_pos, div_eq_inv_mul]

Result:
k : ℕ
⊢ (π / 2)⁻¹ * W k ≤ 1

Proof state:
k : ℕ
⊢ (π / 2)⁻¹ * W k ≤ 1

Tactic:
rw [W_eq_integral_sin_pow_div_integral_sin_pow, div_le_one (integral_sin_pow_pos _)]

Result:
k : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)

Proof state:
k : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)

Tactic:
apply integral_sin_pow_succ_le

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem toJordanDecomposition_toSignedMeasure (j : JordanDecomposition α) :
    j.toSignedMeasure.toJordanDecomposition = j :=
  (@toSignedMeasure_injective _ _ j j.toSignedMeasure.toJordanDecomposition (by simp)).symm

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
⊢ j.toSignedMeasure = j.toSignedMeasure.toJordanDecomposition.toSignedMeasure

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Antisymmetrization.lean
theorem wellFoundedGT_antisymmetrization_iff :
    WellFoundedGT (Antisymmetrization α (· ≤ ·)) ↔ WellFoundedGT α

Proof state:
case convert_4
α : Type u_1
inst✝ : Preorder α
⊢ ∀ (a₁ a₂ b₁ b₂ : α),
    (AntisymmRel.setoid α fun x1 x2 => x1 ≤ x2) a₁ b₁ →
      (AntisymmRel.setoid α fun x1 x2 => x1 ≤ x2) a₂ b₂ → (a₂ < a₁) = (b₂ < b₁)

Tactic:
exact fun _ _ _ _ h₁ h₂ ↦ propext
  ⟨fun h ↦ (h₂.2.trans_lt h).trans_le h₁.1, fun h ↦ (h₂.1.trans_lt h).trans_le h₁.2⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ (WellFounded fun x1 x2 => x1 > x2) ↔ WellFounded fun x1 x2 => x1 > x2

Tactic:
convert wellFounded_liftOn₂'_iff with ⟨_⟩ ⟨_⟩

Result:
case convert_4
α : Type u_1
inst✝ : Preorder α
⊢ ∀ (a₁ a₂ b₁ b₂ : α),
    (AntisymmRel.setoid α fun x1 x2 => x1 ≤ x2) a₁ b₁ →
      (AntisymmRel.setoid α fun x1 x2 => x1 ≤ x2) a₂ b₂ → (a₂ < a₁) = (b₂ < b₁)

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ WellFoundedGT (Antisymmetrization α fun x1 x2 => x1 ≤ x2) ↔ WellFoundedGT α

Tactic:
simp_rw [isWellFounded_iff]

Result:
α : Type u_1
inst✝ : Preorder α
⊢ (WellFounded fun x1 x2 => x1 > x2) ↔ WellFounded fun x1 x2 => x1 > x2
-- Mathlib/Topology/PartialHomeomorph.lean
theorem subtypeRestr_source : (e.subtypeRestr hs).source = (↑) ⁻¹' e.source

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
⊢ (e.subtypeRestr hs).source = Subtype.val ⁻¹' e.source

Tactic:
simp only [subtypeRestr_def, mfld_simps]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Weierstrass.lean
theorem polynomialFunctions_closure_eq_top' : (polynomialFunctions I).topologicalClosure = ⊤

Proof state:
case h
f : C(↑I, ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ (polynomialFunctions I).toSubsemiring

Tactic:
apply Subalgebra.sum_mem

Result:
case h.h
f : C(↑I, ℝ)
n : ℕ
⊢ ∀ x ∈ Finset.univ, f (bernstein.z x) • bernstein n ↑x ∈ polynomialFunctions I

Proof state:
f : C(↑I, ℝ)
⊢ ∃ᶠ (x : C(↑I, ℝ)) in nhds f, x ∈ ↑(polynomialFunctions I).toSubsemiring

Tactic:
refine Filter.Tendsto.frequently (bernsteinApproximation_uniform f) ?_

Result:
f : C(↑I, ℝ)
⊢ ∃ᶠ (x : ℕ) in atTop, bernsteinApproximation x f ∈ ↑(polynomialFunctions I).toSubsemiring

Proof state:
f : C(↑I, ℝ)
⊢ ∃ᶠ (x : ℕ) in atTop, bernsteinApproximation x f ∈ ↑(polynomialFunctions I).toSubsemiring

Tactic:
apply Frequently.of_forall

Result:
case h
f : C(↑I, ℝ)
⊢ ∀ (x : ℕ), bernsteinApproximation x f ∈ ↑(polynomialFunctions I).toSubsemiring

Proof state:
case h
f : C(↑I, ℝ)
⊢ ∀ (x : ℕ), bernsteinApproximation x f ∈ ↑(polynomialFunctions I).toSubsemiring

Tactic:
intro n

Result:
case h
f : C(↑I, ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ ↑(polynomialFunctions I).toSubsemiring

Proof state:
case h
f : C(↑I, ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ ↑(polynomialFunctions I).toSubsemiring

Tactic:
simp only [SetLike.mem_coe]

Result:
case h
f : C(↑I, ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ (polynomialFunctions I).toSubsemiring

Proof state:
⊢ (polynomialFunctions I).topologicalClosure = ⊤

Tactic:
rw [eq_top_iff]

Result:
⊢ ⊤ ≤ (polynomialFunctions I).topologicalClosure

Proof state:
case h.h.hx
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ bernstein n✝ ↑n ∈ polynomialFunctions I

Tactic:
dsimp [bernstein, polynomialFunctions]

Result:
case h.h.hx
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ (bernsteinPolynomial ℝ n✝ ↑n).toContinuousMapOn I ∈ Subalgebra.map (Polynomial.toContinuousMapOnAlgHom I) ⊤

Proof state:
⊢ ⊤ ≤ (polynomialFunctions I).topologicalClosure

Tactic:
rintro f -

Result:
f : C(↑I, ℝ)
⊢ f ∈ (polynomialFunctions I).topologicalClosure

Proof state:
case h.h
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ f (bernstein.z n) • bernstein n✝ ↑n ∈ polynomialFunctions I

Tactic:
apply Subalgebra.smul_mem

Result:
case h.h.hx
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ bernstein n✝ ↑n ∈ polynomialFunctions I

Proof state:
case h.h
f : C(↑I, ℝ)
n : ℕ
⊢ ∀ x ∈ Finset.univ, f (bernstein.z x) • bernstein n ↑x ∈ polynomialFunctions I

Tactic:
rintro n -

Result:
case h.h
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ f (bernstein.z n) • bernstein n✝ ↑n ∈ polynomialFunctions I

Proof state:
case h.h.hx
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ (bernsteinPolynomial ℝ n✝ ↑n).toContinuousMapOn I ∈ Subalgebra.map (Polynomial.toContinuousMapOnAlgHom I) ⊤

Tactic:
simp

Result:
no goals

Proof state:
f : C(↑I, ℝ)
⊢ f ∈ (polynomialFunctions I).topologicalClosure

Tactic:
refine Filter.Frequently.mem_closure ?_

Result:
f : C(↑I, ℝ)
⊢ ∃ᶠ (x : C(↑I, ℝ)) in nhds f, x ∈ ↑(polynomialFunctions I).toSubsemiring
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_pow_apply_getElem (l : List α) (w : Nodup l) (n : ℕ) (i : ℕ) (h : i < l.length) :
    (formPerm l ^ n) l[i] =
      l[(i + n) % l.length]'(Nat.mod_lt _ (i.zero_le.trans_lt h))

Proof state:
case succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
w : l.Nodup
i : ℕ
h : i < l.length
n : ℕ
hn : (l.formPerm ^ n) l[i] = l[(i + n) % l.length]
⊢ (l.formPerm ^ (n + 1)) l[i] = l[(i + (n + 1)) % l.length]

Tactic:
simp [pow_succ', mul_apply, hn, formPerm_apply_getElem _ w, Nat.succ_eq_add_one,
  ← Nat.add_assoc]

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
w : l.Nodup
i : ℕ
h : i < l.length
⊢ (l.formPerm ^ 0) l[i] = l[(i + 0) % l.length]

Tactic:
simp [Nat.mod_eq_of_lt h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
w : l.Nodup
n i : ℕ
h : i < l.length
⊢ (l.formPerm ^ n) l[i] = l[(i + n) % l.length]

Tactic:
induction n with
| zero => simp [Nat.mod_eq_of_lt h]
| succ n hn =>
  simp [pow_succ', mul_apply, hn, formPerm_apply_getElem _ w, Nat.succ_eq_add_one,
    ← Nat.add_assoc]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem destruct_think (s : WSeq α) : destruct (think s) = (destruct s).think :=
  Computation.destruct_eq_think <| by simp [destruct, think, Computation.rmap]

Proof state:
α : Type u
s : WSeq α
⊢ s.think.destruct.destruct = Sum.inr s.destruct

Tactic:
simp [destruct, think, Computation.rmap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem isSome_min?_of_mem {l : List α} [Min α] {a : α} (h : a ∈ l) :
    l.min?.isSome

Proof state:
α : Type u_1
l : List α
inst✝ : Min α
a : α
h : a ∈ l
⊢ l.min?.isSome = true

Tactic:
cases l <;> simp_all [List.min?_cons']

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem parentD_push {arr : Array UFNode} :
    parentD (arr.push ⟨arr.size, 0⟩) a = parentD arr a

Proof state:
a : Nat
arr : Array UFNode
h1 : a ≤ arr.size
h2 : arr.size ≤ a
⊢ arr.size = a

Tactic:
exact Nat.le_antisymm h2 h1

Result:
no goals

Proof state:
case isFalse.isTrue
a : Nat
arr : Array UFNode
h✝¹ : ¬a < arr.size + 1
h✝ : a < arr.size
⊢ a = arr[a].parent

Tactic:
next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)

Result:
no goals

Proof state:
a : Nat
arr : Array UFNode
⊢ (if h : a < arr.size + 1 then (arr.push { parent := arr.size, rank := 0 })[a].parent else a) =
    if h : a < arr.size then arr[a].parent else a

Tactic:
split <;> split <;> try simp [Array.getElem_push, *]

Result:
case isTrue.isFalse
a : Nat
arr : Array UFNode
h✝¹ : a < arr.size + 1
h✝ : ¬a < arr.size
⊢ arr.size = a

case isFalse.isTrue
a : Nat
arr : Array UFNode
h✝¹ : ¬a < arr.size + 1
h✝ : a < arr.size
⊢ a = arr[a].parent

Proof state:
a : Nat
arr : Array UFNode
⊢ parentD (arr.push { parent := arr.size, rank := 0 }) a = parentD arr a

Tactic:
simp [parentD]

Result:
a : Nat
arr : Array UFNode
⊢ (if h : a < arr.size + 1 then (arr.push { parent := arr.size, rank := 0 })[a].parent else a) =
    if h : a < arr.size then arr[a].parent else a

Proof state:
case isTrue.isFalse
a : Nat
arr : Array UFNode
h✝¹ : a < arr.size + 1
h✝ : ¬a < arr.size
⊢ arr.size = a

Tactic:
next h1 h2 =>
simp [Nat.lt_succ] at h1 h2
exact Nat.le_antisymm h2 h1

Result:
no goals

Proof state:
a : Nat
arr : Array UFNode
h1 : a < arr.size + 1
h2 : ¬a < arr.size
⊢ arr.size = a

Tactic:
simp [Nat.lt_succ] at h1 h2

Result:
a : Nat
arr : Array UFNode
h1 : a ≤ arr.size
h2 : arr.size ≤ a
⊢ arr.size = a

Proof state:
case isFalse.isFalse
a : Nat
arr : Array UFNode
h✝¹ : ¬a < arr.size + 1
h✝ : ¬a < arr.size
⊢ a = a

Tactic:
simp [Array.getElem_push, *]

Result:
no goals

Proof state:
a : Nat
arr : Array UFNode
h1 : ¬a < arr.size + 1
h2 : a < arr.size
⊢ a = arr[a].parent

Tactic:
cases h1 (Nat.lt_succ_of_lt h2)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem getElem?_mapFinIdx {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {i : Nat} :
    (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f i x (by simp [getElem?_eq_some_iff] at m; exact m.1)

Proof state:
α : Type ?u.18057
β : Type ?u.18089
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
x : α
m : ∃ h, l[i] = x
⊢ i < l.length

Tactic:
exact m.1

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
⊢ (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => some (f i x ⋯)

Tactic:
simp only [getElem?_def, length_mapFinIdx, getElem_mapFinIdx]

Result:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
⊢ (if h : i < l.length then some (f i l[i] ⋯) else none) =
    (if h : i < l.length then some l[i] else none).pbind fun a h => some (f i a ⋯)

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
⊢ (if h : i < l.length then some (f i l[i] ⋯) else none) =
    (if h : i < l.length then some l[i] else none).pbind fun a h => some (f i a ⋯)

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type ?u.18057
β : Type ?u.18089
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
x : α
m : x ∈ l[i]?
⊢ i < l.length

Tactic:
simp [getElem?_eq_some_iff] at m

Result:
α : Type ?u.18057
β : Type ?u.18089
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
x : α
m : ∃ h, l[i] = x
⊢ i < l.length
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem allM_toList [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
    as.toList.allM p = as.allM p

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
⊢ List.allM p as.toList = (fun x => !x) <$> List.anyM (fun x => (fun x => !x) <$> p x) as.toList

Tactic:
rw [List.allM_eq_not_anyM_not]

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
⊢ List.allM p as.toList = allM p as

Tactic:
rw [allM_eq_not_anyM_not]

Result:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
⊢ List.allM p as.toList = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) as

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
⊢ List.allM p as.toList = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) as

Tactic:
rw [← anyM_toList]

Result:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
⊢ List.allM p as.toList = (fun x => !x) <$> List.anyM (fun x => (fun x => !x) <$> p x) as.toList
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The product of two `s`-factored numbers is again `s`-factored. -/
lemma mul_mem_factoredNumbers {s : Finset ℕ} {m n : ℕ} (hm : m ∈ factoredNumbers s)
    (hn : n ∈ factoredNumbers s) :
    m * n ∈ factoredNumbers s

Proof state:
s : Finset ℕ
m n : ℕ
hm : m ∈ factoredNumbers s
hn : n ∈ factoredNumbers s
⊢ m * n ∈ factoredNumbers s

Tactic:
have hm' := primeFactors_subset_of_mem_factoredNumbers hm

Result:
s : Finset ℕ
m n : ℕ
hm : m ∈ factoredNumbers s
hn : n ∈ factoredNumbers s
hm' : m.primeFactors ⊆ s
⊢ m * n ∈ factoredNumbers s

Proof state:
s : Finset ℕ
m n : ℕ
hm : m ∈ factoredNumbers s
hn : n ∈ factoredNumbers s
hm' : m.primeFactors ⊆ s
hn' : n.primeFactors ⊆ s
⊢ m * n ∈ factoredNumbers s

Tactic:
exact mem_factoredNumbers_of_primeFactors_subset (mul_ne_zero hm.1 hn.1)
  <| primeFactors_mul hm.1 hn.1 ▸ Finset.union_subset hm' hn'

Result:
no goals

Proof state:
s : Finset ℕ
m n : ℕ
hm : m ∈ factoredNumbers s
hn : n ∈ factoredNumbers s
hm' : m.primeFactors ⊆ s
⊢ m * n ∈ factoredNumbers s

Tactic:
have hn' := primeFactors_subset_of_mem_factoredNumbers hn

Result:
s : Finset ℕ
m n : ℕ
hm : m ∈ factoredNumbers s
hn : n ∈ factoredNumbers s
hm' : m.primeFactors ⊆ s
hn' : n.primeFactors ⊆ s
⊢ m * n ∈ factoredNumbers s
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem prevD_zero_cochainComplex (f : ∀ i j, P.X i ⟶ Q.X j) : prevD 0 f = 0

Proof state:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0

Tactic:
rw [CochainComplex.prev_nat_zero]

Result:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.up ℕ).Rel 0 0

Proof state:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.up ℕ).Rel 0 0

Tactic:
dsimp

Result:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬1 = 0

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ f 0 ((ComplexShape.up ℕ).prev 0) ≫ Q.d ((ComplexShape.up ℕ).prev 0) 0 = 0

Tactic:
rw [Q.shape, comp_zero]

Result:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0

Proof state:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬1 = 0

Tactic:
decide

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ (prevD 0) f = 0

Tactic:
dsimp [prevD]

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ f 0 ((ComplexShape.up ℕ).prev 0) ≫ Q.d ((ComplexShape.up ℕ).prev 0) 0 = 0
-- Mathlib/Analysis/Normed/Field/Basic.lean
/-- This inequality is particularly useful when `c = 1` and `‖a‖ = ‖b‖ = 1` as it then shows that
chord length is a metric on the unit complex numbers. -/
lemma norm_sub_mul_le' (hb : ‖b‖ ≤ 1) : ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b c : α
hb : ‖b‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖

Tactic:
rw [add_comm]

Result:
α : Type u_2
inst✝ : SeminormedRing α
a b c : α
hb : ‖b‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖c - b‖ + ‖1 - a‖

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b c : α
hb : ‖b‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖c - b‖ + ‖1 - a‖

Tactic:
exact norm_sub_mul_le (α := αᵐᵒᵖ) hb

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem diff_singleton_subset_iff {x : α} {s t : Set α} : s \ {x} ⊆ t ↔ s ⊆ insert x t

Proof state:
α : Type u
x : α
s t : Set α
⊢ s \ {x} ⊆ t ↔ s ⊆ insert x t

Tactic:
rw [← union_singleton, union_comm]

Result:
α : Type u
x : α
s t : Set α
⊢ s \ {x} ⊆ t ↔ s ⊆ {x} ∪ t

Proof state:
α : Type u
x : α
s t : Set α
⊢ s \ {x} ⊆ t ↔ s ⊆ {x} ∪ t

Tactic:
apply diff_subset_iff

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_zero_measure : mgf X (0 : Measure Ω) = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
⊢ mgf X 0 = 0

Tactic:
ext

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
x✝ : ℝ
⊢ mgf X 0 x✝ = 0 x✝

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
x✝ : ℝ
⊢ mgf X 0 x✝ = 0 x✝

Tactic:
simp [mgf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem erase_cons [BEq α] (a b : α) (l : List α) :
    (b :: l).erase a = if b == a then l else b :: l.erase a

Proof state:
α : Type u
inst✝ : BEq α
a b : α
l : List α
⊢ (match b == a with
    | true => l
    | false => b :: l.erase a) =
    ite ((b == a) = true) l (b :: l.erase a)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u
inst✝ : BEq α
a b : α
l : List α
⊢ (b :: l).erase a = ite ((b == a) = true) l (b :: l.erase a)

Tactic:
simp only [List.erase]

Result:
α : Type u
inst✝ : BEq α
a b : α
l : List α
⊢ (match b == a with
    | true => l
    | false => b :: l.erase a) =
    ite ((b == a) = true) l (b :: l.erase a)
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_apply_le_norm (hp : p ≠ 0) (f : lp E p) (i : α) : ‖f i‖ ≤ ‖f‖

Proof state:
case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ⊤
hp'' : 0 < p.toReal
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ ‖↑f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal

Tactic:
convert le_hasSum (hasSum_norm hp'' f) i fun i _ => this i

Result:
no goals

Proof state:
case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ⊤
hp'' : 0 < p.toReal
⊢ ‖↑f i‖ ≤ ‖f‖

Tactic:
have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i => Real.rpow_nonneg (norm_nonneg _) _

Result:
case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ⊤
hp'' : 0 < p.toReal
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ ‖↑f i‖ ≤ ‖f‖

Proof state:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
i : α
hp : ⊤ ≠ 0
f : ↥(lp E ⊤)
⊢ ‖↑f i‖ ≤ ‖f‖

Tactic:
haveI : Nonempty α := ⟨i⟩

Result:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
i : α
hp : ⊤ ≠ 0
f : ↥(lp E ⊤)
this : Nonempty α
⊢ ‖↑f i‖ ≤ ‖f‖

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
⊢ ‖↑f i‖ ≤ ‖f‖

Tactic:
rcases eq_or_ne p ∞ with (rfl | hp')

Result:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
i : α
hp : ⊤ ≠ 0
f : ↥(lp E ⊤)
⊢ ‖↑f i‖ ≤ ‖f‖

case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ⊤
⊢ ‖↑f i‖ ≤ ‖f‖

Proof state:
case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ⊤
hp'' : 0 < p.toReal
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ ‖↑f i‖ ≤ ‖f‖

Tactic:
rw [← Real.rpow_le_rpow_iff (norm_nonneg _) (norm_nonneg' _) hp'']

Result:
case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ⊤
hp'' : 0 < p.toReal
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ ‖↑f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal

Proof state:
case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ⊤
⊢ ‖↑f i‖ ≤ ‖f‖

Tactic:
have hp'' : 0 < p.toReal := ENNReal.toReal_pos hp hp'

Result:
case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ⊤
hp'' : 0 < p.toReal
⊢ ‖↑f i‖ ≤ ‖f‖

Proof state:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
i : α
hp : ⊤ ≠ 0
f : ↥(lp E ⊤)
this : Nonempty α
⊢ ‖↑f i‖ ≤ ‖f‖

Tactic:
exact (isLUB_norm f).1 ⟨i, rfl⟩

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem prod_primeFactors_gcd_mul_prod_primeFactors_mul {β : Type*} [CommMonoid β] (m n : ℕ)
    (f : ℕ → β) :
    (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f =
      m.primeFactors.prod f * n.primeFactors.prod f

Proof state:
case inl
β : Type u_1
inst✝ : CommMonoid β
n : ℕ
f : ℕ → β
⊢ (gcd 0 n).primeFactors.prod f * (0 * n).primeFactors.prod f = (primeFactors 0).prod f * n.primeFactors.prod f

Tactic:
simp

Result:
no goals

Proof state:
case inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
obtain rfl | hn₀ := eq_or_ne n 0

Result:
case inr.inl
β : Type u_1
inst✝ : CommMonoid β
m : ℕ
f : ℕ → β
hm₀ : m ≠ 0
⊢ (m.gcd 0).primeFactors.prod f * (m * 0).primeFactors.prod f = m.primeFactors.prod f * (primeFactors 0).prod f

case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Proof state:
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
obtain rfl | hm₀ := eq_or_ne m 0

Result:
case inl
β : Type u_1
inst✝ : CommMonoid β
n : ℕ
f : ℕ → β
⊢ (gcd 0 n).primeFactors.prod f * (0 * n).primeFactors.prod f = (primeFactors 0).prod f * n.primeFactors.prod f

case inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Proof state:
case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
rw [primeFactors_mul hm₀ hn₀, primeFactors_gcd hm₀ hn₀, mul_comm, Finset.prod_union_inter]

Result:
no goals

Proof state:
case inr.inl
β : Type u_1
inst✝ : CommMonoid β
m : ℕ
f : ℕ → β
hm₀ : m ≠ 0
⊢ (m.gcd 0).primeFactors.prod f * (m * 0).primeFactors.prod f = m.primeFactors.prod f * (primeFactors 0).prod f

Tactic:
simp

Result:
no goals