harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
theorem karoubi_alternatingFaceMapComplex_d (P : Karoubi (SimplicialObject C)) (n : ℕ) :
    ((AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)).d (n + 1) n).f =
      P.p.app (op ⦋n + 1⦌) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ ∑ x : Fin (n + 2), (-1) ^ ↑x • (SimplicialObject.δ (KaroubiFunctorCategoryEmbedding.obj P) x).f =
    ∑ x : Fin (n + 2), (-1) ^ ↑x • P.p.app (op ⦋n + 1⦌) ≫ P.X.δ x

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ ((AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)).d (n + 1) n).f =
    P.p.app (op ⦋n + 1⦌) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n

Tactic:
simp only [AlternatingFaceMapComplex.obj_d_eq, Karoubi.sum_hom, Preadditive.comp_sum,
  Karoubi.zsmul_hom, Preadditive.comp_zsmul]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ ∑ x : Fin (n + 2), (-1) ^ ↑x • (SimplicialObject.δ (KaroubiFunctorCategoryEmbedding.obj P) x).f =
    ∑ x : Fin (n + 2), (-1) ^ ↑x • P.p.app (op ⦋n + 1⦌) ≫ P.X.δ x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem insertMany_cons {l : List ((a : α) × β a)} {k : α} {v : β k} [EquivBEq α] [LawfulHashable α]
    (h : m.WF) :
    m.insertMany (⟨k, v⟩ :: l) = (m.insert k v).insertMany l

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
l : List ((a : α) × β a)
k : α
v : β k
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ m.insertMany (⟨k, v⟩ :: l) = (m.insert k v).insertMany l

Tactic:
simp_to_raw

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
l : List ((a : α) × β a)
k : α
v : β k
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ (Raw₀.insertMany ⟨m, ⋯⟩ (⟨k, v⟩ :: l)).val.val = ((Raw₀.insert ⟨m, ⋯⟩ k v).insertMany l).val.val

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
l : List ((a : α) × β a)
k : α
v : β k
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ (Raw₀.insertMany ⟨m, ⋯⟩ (⟨k, v⟩ :: l)).val.val = ((Raw₀.insert ⟨m, ⋯⟩ k v).insertMany l).val.val

Tactic:
rw [Raw₀.insertMany_cons]

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem Field.Emb.cardinal_separableClosure [Algebra.IsAlgebraic F E] :
    #(Field.Emb F <| separableClosure F E) = #(Field.Emb F E)

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ #(Emb F ↥(separableClosure F E)) = #(Emb F E)

Tactic:
rw [← (embProdEmbOfIsAlgebraic F (separableClosure F E) E).cardinal_eq,
  mk_prod, mk_eq_one (Emb _ E), lift_one, mul_one, lift_id]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem Sublist.erase_diff_erase_sublist {a : α} :
    ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → (l₂.erase a).diff (l₁.erase a) <+ l₂.diff l₁
  | [], _, _ => erase_sublist _ _
  | b :: l₁, l₂, h => by
    if heq : b = a then
      simp [heq]
    else
      simp [heq, erase_comm a]
      exact (erase_cons_head b _ ▸ h.erase b).erase_diff_erase_sublist

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : b = a
⊢ (l₂.erase a).diff ((b :: l₁).erase a) <+ l₂.diff (b :: l₁)

Tactic:
simp [heq]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : ¬b = a
⊢ (l₂.erase a).diff ((b :: l₁).erase a) <+ l₂.diff (b :: l₁)

Tactic:
simp [heq, erase_comm a]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : ¬b = a
⊢ ((l₂.erase b).erase a).diff (l₁.erase a) <+ (l₂.erase b).diff l₁

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : ¬b = a
⊢ ((l₂.erase b).erase a).diff (l₁.erase a) <+ (l₂.erase b).diff l₁

Tactic:
exact (erase_cons_head b _ ▸ h.erase b).erase_diff_erase_sublist

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
⊢ (l₂.erase a).diff ((b :: l₁).erase a) <+ l₂.diff (b :: l₁)

Tactic:
if heq : b = a then
  simp [heq]
else
  simp [heq, erase_comm a]
  exact (erase_cons_head b _ ▸ h.erase b).erase_diff_erase_sublist

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
theorem lieBracketWithin_univ : lieBracketWithin 𝕜 V W univ = lieBracket 𝕜 V W

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
⊢ lieBracketWithin 𝕜 V W univ x = lieBracket 𝕜 V W x

Tactic:
simp [lieBracketWithin, lieBracket]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
⊢ lieBracketWithin 𝕜 V W univ = lieBracket 𝕜 V W

Tactic:
ext1 x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
⊢ lieBracketWithin 𝕜 V W univ x = lieBracket 𝕜 V W x
-- Mathlib/FieldTheory/AlgebraicClosure.lean
theorem le_algebraicClosure_iff (L : IntermediateField F E) :
    L ≤ algebraicClosure F E ↔ Algebra.IsAlgebraic F L :=
  ⟨fun h ↦ ⟨fun x ↦ by simpa only [IsAlgebraic, ne_eq, ← aeval_algebraMap_eq_zero_iff E,
    IntermediateField.algebraMap_apply,
    Algebra.id.map_eq_id, RingHomCompTriple.comp_apply, mem_algebraicClosure_iff] using h x.2⟩,
    fun _ ↦ le_algebraicClosure _ _ _⟩

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : L ≤ algebraicClosure F E
x : ↥L
⊢ IsAlgebraic F x

Tactic:
simpa only [IsAlgebraic, ne_eq, ← aeval_algebraMap_eq_zero_iff E,
IntermediateField.algebraMap_apply,
Algebra.id.map_eq_id, RingHomCompTriple.comp_apply, mem_algebraicClosure_iff] using h x.2

Result:
no goals
-- Mathlib/Computability/RegularExpressions.lean
theorem map_map (g : β → γ) (f : α → β) : ∀ P : RegularExpression α, (P.map f).map g = P.map (g ∘ f)
  | 0 => rfl
  | 1 => rfl
  | char _ => rfl
  | R + S => by simp only [map, Function.comp_apply, map_map]
  | R * S => by simp only [map, Function.comp_apply, map_map]
  | star R => by simp only [map, Function.comp_apply, map_map]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
R : RegularExpression α
⊢ map g (map f R.star) = map (g ∘ f) R.star

Tactic:
simp only [map, Function.comp_apply, map_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
R S : RegularExpression α
⊢ map g (map f (R * S)) = map (g ∘ f) (R * S)

Tactic:
simp only [map, Function.comp_apply, map_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
R S : RegularExpression α
⊢ map g (map f (R + S)) = map (g ∘ f) (R + S)

Tactic:
simp only [map, Function.comp_apply, map_map]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
theorem isSheaf_iff_extensiveSheaf_of_projective [Preregular C] [FinitaryExtensive C]
    [∀ (X : C), Projective X] :
    IsSheaf (coherentTopology C) F ↔ IsSheaf (extensiveTopology C) F

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
inst✝ : ∀ (X : C), Projective X
⊢ IsSheaf (coherentTopology C) F ↔ IsSheaf (extensiveTopology C) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_of_projective, isSheaf_iff_preservesFiniteProducts]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mlieBracketWithin_swap :
    mlieBracketWithin I V W s = - mlieBracketWithin I W V s

Proof state:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
V W : (x : M) → TangentSpace I x
x : M
⊢ mlieBracketWithin I V W s x = (-mlieBracketWithin I W V s) x

Tactic:
exact mlieBracketWithin_swap_apply

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
V W : (x : M) → TangentSpace I x
⊢ mlieBracketWithin I V W s = -mlieBracketWithin I W V s

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
V W : (x : M) → TangentSpace I x
x : M
⊢ mlieBracketWithin I V W s x = (-mlieBracketWithin I W V s) x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get?_eq_some_get! [LawfulBEq α] {a : α} [Inhabited (β a)] :
    a ∈ m → m.get? a = some (m.get! a)

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
a : α
inst✝ : Inhabited (β a)
⊢ a ∈ m → m.get? a = some (m.get! a)

Tactic:
simpa [mem_iff_contains] using get?_eq_some_get!_of_contains

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem exists_signed_sum {α : Type u_1} [DecidableEq α] (s : Finset α) (f : α → ℤ) :
    ∃ (β : Type u_1) (_ : Fintype β) (sgn : β → SignType) (g : β → α),
      (∀ b, g b ∈ s) ∧
        (Fintype.card β = ∑ a ∈ s, (f a).natAbs) ∧
          ∀ a ∈ s, (∑ b, if g b = a then (sgn b : ℤ) else 0) = f a :=
  let ⟨β, t, sgn, g, hg, ht, hf⟩ := exists_signed_sum_aux s f
  ⟨t, inferInstance, fun b => sgn b, fun b => g b, fun b => hg b, by simp [ht], fun a ha =>
    (sum_attach t fun b ↦ ite (g b = a) (sgn b : ℤ) 0).trans <| hf _ ha⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
β : Type u_1
t : Finset β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
ht : #t = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b ∈ t, if g b = a then ↑(sgn b) else 0) = f a
⊢ Fintype.card { x // x ∈ t } = ∑ a ∈ s, (f a).natAbs

Tactic:
simp [ht]

Result:
no goals
-- Mathlib/Order/Cover.lean
@[simp] lemma coe_wcovBy_top : (a : WithTop α) ⩿ ⊤ ↔ IsMax a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ↑a ⩿ ⊤ ↔ IsMax a

Tactic:
simp only [wcovBy_iff_Ioo_eq, ← image_coe_Ioi, le_top, image_eq_empty, true_and, Ioi_eq_empty_iff]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_units (u : ℤ_[p]ˣ) : ‖(u : ℤ_[p])‖ = 1 := isUnit_iff.mp <| by simp

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℤ_[p]ˣ
⊢ IsUnit ↑u

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem basis_pair_left (hij : i ≠ j) : Lagrange.basis {i, j} v i = basisDivisor (v i) (v j)

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v : ι → F
i j : ι
hij : i ≠ j
⊢ Lagrange.basis {i, j} v i = basisDivisor (v i) (v j)

Tactic:
simp only [Lagrange.basis, hij, erase_insert_eq_erase, erase_eq_of_not_mem, mem_singleton,
  not_false_iff, prod_singleton]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearPMap.lean
theorem IsClosable.closure_isClosed {f : E →ₗ.[R] F} (hf : f.IsClosable) : f.closure.IsClosed

Proof state:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ _root_.IsClosed ↑f.graph.topologicalClosure

Tactic:
exact f.graph.isClosed_topologicalClosure

Result:
no goals

Proof state:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f.closure.IsClosed

Tactic:
rw [IsClosed, ← hf.graph_closure_eq_closure_graph]

Result:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ _root_.IsClosed ↑f.graph.topologicalClosure
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem ContinuousLinearMap.isBoundedBilinearMap (f : E →L[𝕜] F →L[𝕜] G) :
    IsBoundedBilinearMap 𝕜 fun x : E × F => f x.1 x.2 :=
  { add_left := f.map_add₂
    smul_left := f.map_smul₂
    add_right := fun x => (f x).map_add
    smul_right := fun c x => (f x).map_smul c
    bound :=
      ⟨max ‖f‖ 1, zero_lt_one.trans_le (le_max_right _ _), fun x y =>
        (f.le_opNorm₂ x y).trans <| by
          apply_rules [mul_le_mul_of_nonneg_right, norm_nonneg, le_max_left] ⟩ }

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ ‖f‖ * ‖x‖ * ‖y‖ ≤ (‖f‖ ⊔ 1) * ‖x‖ * ‖y‖

Tactic:
apply_rules [mul_le_mul_of_nonneg_right, norm_nonneg, le_max_left]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_dirac' (a : α) {f : α → ℝ≥0∞} (hf : Measurable f) : ∫⁻ a, f a ∂dirac a = f a

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂dirac a = f a

Tactic:
simp [lintegral_congr_ae (ae_eq_dirac' hf)]

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem sub_eq_zero_of_upcrossingsBefore_lt (hab : a < b) (hn : upcrossingsBefore a b f N ω < n) :
    stoppedValue f (upperCrossingTime a b f N (n + 1)) ω -
      stoppedValue f (lowerCrossingTime a b f N n) ω = 0

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
this : N ≤ upperCrossingTime a b f N n ω
⊢ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω - stoppedValue f (lowerCrossingTime a b f N n) ω = 0

Tactic:
simp [stoppedValue, upperCrossingTime_stabilize' (Nat.le_succ n) this,
  lowerCrossingTime_stabilize' le_rfl (le_trans this upperCrossingTime_le_lowerCrossingTime)]

Result:
no goals

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ N ≤ upperCrossingTime a b f N n ω

Tactic:
rw [upcrossingsBefore] at hn

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : sSup {n | upperCrossingTime a b f N n ω < N} < n
⊢ N ≤ upperCrossingTime a b f N n ω

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : sSup {n | upperCrossingTime a b f N n ω < N} < n
⊢ ¬upperCrossingTime a b f N n ω < N

Tactic:
exact fun h => not_le.2 hn (le_csSup (upperCrossingTime_lt_bddAbove hab) h)

Result:
no goals

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω - stoppedValue f (lowerCrossingTime a b f N n) ω = 0

Tactic:
have : N ≤ upperCrossingTime a b f N n ω := by
  rw [upcrossingsBefore] at hn
  rw [← not_lt]
  exact fun h => not_le.2 hn (le_csSup (upperCrossingTime_lt_bddAbove hab) h)

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
this : N ≤ upperCrossingTime a b f N n ω
⊢ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω - stoppedValue f (lowerCrossingTime a b f N n) ω = 0

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : sSup {n | upperCrossingTime a b f N n ω < N} < n
⊢ N ≤ upperCrossingTime a b f N n ω

Tactic:
rw [← not_lt]

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : sSup {n | upperCrossingTime a b f N n ω < N} < n
⊢ ¬upperCrossingTime a b f N n ω < N
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
lemma prob_compl_lt_one_sub_of_lt_prob {p : ℝ≥0∞} (hμs : p < μ s) (s_mble : MeasurableSet s) :
    μ sᶜ < 1 - p

Proof state:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ 1 - (1 - p) < μ s

Tactic:
convert hμs

Result:
case h.e'_3
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ 1 - (1 - p) = p

Proof state:
case inl
α : Type u_1
m0 : MeasurableSpace α
s : Set α
p : ℝ≥0∞
s_mble : MeasurableSet s
inst✝ : IsZeroOrProbabilityMeasure 0
hμs : p < 0 s
⊢ 0 sᶜ < 1 - p

Tactic:
simp at hμs

Result:
no goals

Proof state:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ 1 - μ s < 1 - p

Tactic:
apply ENNReal.sub_lt_of_sub_lt prob_le_one (Or.inl one_ne_top)

Result:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ 1 - (1 - p) < μ s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
⊢ μ sᶜ < 1 - p

Tactic:
rcases eq_zero_or_isProbabilityMeasure μ with rfl | h

Result:
case inl
α : Type u_1
m0 : MeasurableSpace α
s : Set α
p : ℝ≥0∞
s_mble : MeasurableSet s
inst✝ : IsZeroOrProbabilityMeasure 0
hμs : p < 0 s
⊢ 0 sᶜ < 1 - p

case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ μ sᶜ < 1 - p

Proof state:
case h.e'_3
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ 1 - (1 - p) = p

Tactic:
exact ENNReal.sub_sub_cancel one_ne_top (lt_of_lt_of_le hμs prob_le_one).le

Result:
no goals

Proof state:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ μ sᶜ < 1 - p

Tactic:
rw [prob_compl_eq_one_sub s_mble]

Result:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ 1 - μ s < 1 - p
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem subOneIntegralPowerBasis'_gen_prime [IsCyclotomicExtension {p} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑p) :
    Prime hζ.subOneIntegralPowerBasis'.gen

Proof state:
p : ℕ+
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ Prime hζ.subOneIntegralPowerBasis'.gen

Tactic:
simpa only [subOneIntegralPowerBasis'_gen] using hζ.zeta_sub_one_prime'

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem disjoint_of_erase_left (ha : a ∉ t) (hst : Disjoint (s.erase a) t) : Disjoint s t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ Disjoint s t

Tactic:
rw [← erase_insert ha, ← disjoint_erase_comm, disjoint_insert_right]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ a ∉ s.erase a ∧ Disjoint (s.erase a) t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ a ∉ s.erase a ∧ Disjoint (s.erase a) t

Tactic:
exact ⟨not_mem_erase _ _, hst⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Doubling.lean
theorem eventually_measure_le_scaling_constant_mul (K : ℝ) :
    ∀ᶠ r in 𝓝[>] 0, ∀ x, μ (closedBall x (K * r)) ≤ scalingConstantOf μ K * μ (closedBall x r)

Proof state:
case h
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K r : ℝ
hr : ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * r)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x r)
x : α
⊢ μ (closedBall x (K * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)

Tactic:
exact (hr x K le_rfl).trans (mul_le_mul_right' (ENNReal.coe_le_coe.2 (le_max_left _ _)) _)

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (K * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)

Tactic:
filter_upwards [Classical.choose_spec
    (exists_eventually_forall_measure_closedBall_le_mul μ K)] with r hr x

Result:
case h
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K r : ℝ
hr : ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * r)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x r)
x : α
⊢ μ (closedBall x (K * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)
-- Mathlib/NumberTheory/NumberField/Norm.lean
theorem norm_norm [Algebra.IsSeparable K L] [Algebra F L] [Algebra.IsSeparable F L]
    [FiniteDimensional F L] [IsScalarTower K F L] (x : 𝓞 L) : norm K (norm F x) = norm K x

Proof state:
L : Type u_1
K : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
F : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Algebra K F
inst✝⁶ : Algebra.IsSeparable K F
inst✝⁵ : FiniteDimensional K F
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : Algebra F L
inst✝² : Algebra.IsSeparable F L
inst✝¹ : FiniteDimensional F L
inst✝ : IsScalarTower K F L
x : 𝓞 L
⊢ (norm K) ((norm F) x) = (norm K) x

Tactic:
rw [RingOfIntegers.ext_iff, coe_norm, coe_norm, coe_norm, Algebra.norm_norm]

Result:
no goals