harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem thickening_cthickening (hε : 0 < ε) (hδ : 0 ≤ δ) (s : Set E) :
    thickening ε (cthickening δ s) = thickening (ε + δ) s

Proof state:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ✝ : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s

Tactic:
rw [← closure_thickening hδ, thickening_closure, thickening_thickening hε hδ]

Result:
no goals

Proof state:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
ε : ℝ
hε : 0 < ε
s : Set E
hδ : 0 ≤ 0
⊢ thickening ε (cthickening 0 s) = thickening (ε + 0) s

Tactic:
rw [cthickening_zero, thickening_closure, add_zero]

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
s : Set E
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s

Tactic:
obtain rfl | hδ := hδ.eq_or_lt

Result:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
ε : ℝ
hε : 0 < ε
s : Set E
hδ : 0 ≤ 0
⊢ thickening ε (cthickening 0 s) = thickening (ε + 0) s

case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ✝ : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s
-- Mathlib/Data/List/Sigma.lean
theorem kextract_eq_dlookup_kerase (a : α) :
    ∀ l : List (Sigma β), kextract a l = (dlookup a l, kerase a l)
  | [] => rfl
  | ⟨a', b⟩ :: l => by
    simp only [kextract]; dsimp; split_ifs with h
    · subst a'
      simp [kerase]
    · simp [kextract, Ne.symm h, kextract_eq_dlookup_kerase a l, kerase]

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a' = a
⊢ (some (⋯ ▸ b), l) = (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))

Tactic:
subst a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (some (⋯ ▸ b), l) = (dlookup a (⟨a, b⟩ :: l), kerase a (⟨a, b⟩ :: l))

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a' = a
⊢ ((kextract a l).1, ⟨a', b⟩ :: (kextract a l).2) = (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))

Tactic:
simp [kextract, Ne.symm h, kextract_eq_dlookup_kerase a l, kerase]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ kextract a (⟨a', b⟩ :: l) = (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))

Tactic:
simp only [kextract]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (if h : a' = a then (some (⋯ ▸ b), l) else ((kextract a l).1, ⟨a', b⟩ :: (kextract a l).2)) =
    (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (some (⋯ ▸ b), l) = (dlookup a (⟨a, b⟩ :: l), kerase a (⟨a, b⟩ :: l))

Tactic:
simp [kerase]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (if h : a' = a then (some (⋯ ▸ b), l) else ((kextract a l).1, ⟨a', b⟩ :: (kextract a l).2)) =
    (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))

Tactic:
split_ifs with h

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a' = a
⊢ (some (⋯ ▸ b), l) = (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a' = a
⊢ ((kextract a l).1, ⟨a', b⟩ :: (kextract a l).2) = (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} : getValueCast? a (insertEntryIfNew k v l) =
      if h : k == a ∧ containsKey k l = false then some (cast (congrArg β (eq_of_beq h.1)) v)
      else getValueCast? a l

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = true
⊢ getValueCast? a (insertEntryIfNew k v l) =
    if h : (k == a) = true ∧ true = false then some (cast ⋯ v) else getValueCast? a l

Tactic:
simp [insertEntryIfNew_of_containsKey h]

Result:
no goals

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = false
⊢ (if h : (k == a) = true then some (cast ⋯ v) else getValueCast? a l) =
    if h : (k == a) = true ∧ false = false then some (cast ⋯ v) else getValueCast? a l

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = false
⊢ getValueCast? a (insertEntryIfNew k v l) =
    if h : (k == a) = true ∧ false = false then some (cast ⋯ v) else getValueCast? a l

Tactic:
rw [insertEntryIfNew_of_containsKey_eq_false h, getValueCast?_cons]

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = false
⊢ (if h : (k == a) = true then some (cast ⋯ v) else getValueCast? a l) =
    if h : (k == a) = true ∧ false = false then some (cast ⋯ v) else getValueCast? a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ getValueCast? a (insertEntryIfNew k v l) =
    if h : (k == a) = true ∧ containsKey k l = false then some (cast ⋯ v) else getValueCast? a l

Tactic:
cases h : containsKey k l

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = false
⊢ getValueCast? a (insertEntryIfNew k v l) =
    if h : (k == a) = true ∧ false = false then some (cast ⋯ v) else getValueCast? a l

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = true
⊢ getValueCast? a (insertEntryIfNew k v l) =
    if h : (k == a) = true ∧ true = false then some (cast ⋯ v) else getValueCast? a l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsbD x i = false

Proof state:
w : Nat
x : BitVec w
i : Nat
ge : w ≤ i
⊢ (decide (i < w) && x.getLsbD (w - 1 - i)) = false

Tactic:
simp only [Bool.and_eq_false_imp, decide_eq_true_eq]

Result:
w : Nat
x : BitVec w
i : Nat
ge : w ≤ i
⊢ i < w → x.getLsbD (w - 1 - i) = false

Proof state:
w : Nat
x : BitVec w
i : Nat
ge : w ≤ i
⊢ i < w → x.getLsbD (w - 1 - i) = false

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
ge : w ≤ i
⊢ x.getMsbD i = false

Tactic:
rw [getMsbD]

Result:
w : Nat
x : BitVec w
i : Nat
ge : w ≤ i
⊢ (decide (i < w) && x.getLsbD (w - 1 - i)) = false
-- Mathlib/RingTheory/Artinian/Ring.lean
lemma jacobson_eq_radical (I : Ideal R) : I.jacobson = I.radical

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
I : Ideal R
⊢ I.jacobson = I.radical

Tactic:
simp_rw [Ideal.jacobson, Ideal.radical_eq_sInf, IsArtinianRing.isPrime_iff_isMaximal]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
private lemma uniformity_eq_seminorm :
    𝓤 (E →SL[σ₁₂] F) = ⨅ r > 0, 𝓟 {f | ‖f.1 - f.2‖ < r}

Proof state:
case refine_2.intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
x✝¹ : Set E × ℝ
s : Set E
r : ℝ
x✝ : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε * δ < (s, r).2
f : E →SL[σ₁₂] F
hf : f ∈ ContinuousLinearMap.seminorm.ball 0 δ
x : E
hx : x ∈ (s, r).1
⊢ f x ∈ closedBall 0 (s, r).2

Tactic:
simp only [Seminorm.mem_ball_zero, mem_closedBall_zero_iff] at hf ⊢

Result:
case refine_2.intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
x✝¹ : Set E × ℝ
s : Set E
r : ℝ
x✝ : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε * δ < (s, r).2
f : E →SL[σ₁₂] F
x : E
hx : x ∈ (s, r).1
hf : ContinuousLinearMap.seminorm f < δ
⊢ ‖f x‖ ≤ r
-- Mathlib/Data/PNat/Xgcd.lean
theorem start_isSpecial (a b : ℕ+) : (start a b).IsSpecial

Proof state:
a b : ℕ+
⊢ (start a b).IsSpecial

Tactic:
dsimp [start, IsSpecial]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/GammaDeriv.lean
lemma hasDerivAt_Gamma_one : HasDerivAt Gamma (-γ) 1

Proof state:
⊢ HasDerivAt Gamma (-↑γ) 1

Tactic:
simpa only [factorial_zero, cast_one, harmonic_zero, Rat.cast_zero, add_zero, mul_neg, one_mul,
  cast_zero, zero_add] using hasDerivAt_Gamma_nat 0

Result:
no goals
-- Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean
theorem one_lt_goodτ : 1 < goodτ E

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ 1 < 1 + ⋯.choose / 4

Tactic:
linarith [(exists_goodδ E).choose_spec.1]

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ 1 < goodτ E

Tactic:
dsimp [goodτ, goodδ]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ 1 < 1 + ⋯.choose / 4
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addXYZ_self (P : Fin 3 → R) : W'.addXYZ P P = ![0, 0, 0]

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.addXYZ P P = ![0, 0, 0]

Tactic:
rw [addXYZ, addX_self, addY_self, addZ_self]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/FiniteDimension.lean
theorem coe_toContinuousLinearEquivOfDetNeZero (f : E →L[𝕜] E) (hf : f.det ≠ 0) :
    (f.toContinuousLinearEquivOfDetNeZero hf : E →L[𝕜] E) = f

Proof state:
case h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →L[𝕜] E
hf : f.det ≠ 0
x : E
⊢ ↑(f.toContinuousLinearEquivOfDetNeZero hf) x = f x

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →L[𝕜] E
hf : f.det ≠ 0
⊢ ↑(f.toContinuousLinearEquivOfDetNeZero hf) = f

Tactic:
ext x

Result:
case h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →L[𝕜] E
hf : f.det ≠ 0
x : E
⊢ ↑(f.toContinuousLinearEquivOfDetNeZero hf) x = f x
-- Mathlib/GroupTheory/Finiteness.lean
theorem AddSubgroup.fg_iff_mul_fg (P : AddSubgroup H) : P.FG ↔ P.toSubgroup.FG

Proof state:
H : Type u_4
inst✝ : AddGroup H
P : AddSubgroup H
⊢ P.FG ↔ (toSubgroup P).FG

Tactic:
exact AddSubmonoid.fg_iff_mul_fg (AddSubgroup.toAddSubmonoid P)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem eq_iff_flatten_eq {L L' : Array (Array α)} :
    L = L' ↔ L.flatten = L'.flatten ∧ map size L = map size L'

Proof state:
case of
α : Type u_1
L' : Array (Array α)
L : List (List α)
⊢ (List.map List.toArray L).toArray = L' ↔
    (List.map List.toArray L).toArray.flatten = L'.flatten ∧ map size (List.map List.toArray L).toArray = map size L'

Tactic:
cases L' using array₂_induction with
| of L' =>
  simp [Function.comp_def, ← List.eq_iff_flatten_eq]
  rw [List.map_inj_right]
  simp +contextual

Result:
no goals

Proof state:
α : Type u_1
L L' : Array (Array α)
⊢ L = L' ↔ L.flatten = L'.flatten ∧ map size L = map size L'

Tactic:
cases L using array₂_induction with
| of L =>
  cases L' using array₂_induction with
  | of L' =>
    simp [Function.comp_def, ← List.eq_iff_flatten_eq]
    rw [List.map_inj_right]
    simp +contextual

Result:
no goals

Proof state:
case of.of
α : Type u_1
L L' : List (List α)
⊢ List.map List.toArray L = List.map List.toArray L' ↔ L = L'

Tactic:
rw [List.map_inj_right]

Result:
case of.of
α : Type u_1
L L' : List (List α)
⊢ ∀ (x y : List α), x.toArray = y.toArray → x = y

Proof state:
case of.of
α : Type u_1
L L' : List (List α)
⊢ ∀ (x y : List α), x.toArray = y.toArray → x = y

Tactic:
simp +contextual

Result:
no goals

Proof state:
case of.of
α : Type u_1
L L' : List (List α)
⊢ (List.map List.toArray L).toArray = (List.map List.toArray L').toArray ↔
    (List.map List.toArray L).toArray.flatten = (List.map List.toArray L').toArray.flatten ∧
      map size (List.map List.toArray L).toArray = map size (List.map List.toArray L').toArray

Tactic:
simp [Function.comp_def, ← List.eq_iff_flatten_eq]

Result:
case of.of
α : Type u_1
L L' : List (List α)
⊢ List.map List.toArray L = List.map List.toArray L' ↔ L = L'
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
    {k a : α} {v : β} {h} : getValue a (insertEntryIfNew k v l) h =
    if h' : k == a ∧ containsKey k l = false then v
    else getValue a l (containsKey_of_containsKey_insertEntryIfNew' h h')

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : containsKey a (insertEntryIfNew k v l) = true
⊢ (if x : (k == a) = true ∧ containsKey k l = false then some v else getValue? a l) =
    if h : (k == a) = true ∧ containsKey k l = false then some v else some (getValue a l ⋯)

Tactic:
simp [← getValue?_eq_some_getValue]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : containsKey a (insertEntryIfNew k v l) = true
⊢ getValue a (insertEntryIfNew k v l) h = if h' : (k == a) = true ∧ containsKey k l = false then v else getValue a l ⋯

Tactic:
rw [← Option.some_inj, ← getValue?_eq_some_getValue, apply_dite Option.some,
  getValue?_insertEntryIfNew, ← dite_eq_ite]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : containsKey a (insertEntryIfNew k v l) = true
⊢ (if x : (k == a) = true ∧ containsKey k l = false then some v else getValue? a l) =
    if h : (k == a) = true ∧ containsKey k l = false then some v else some (getValue a l ⋯)
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
/-- The second marginal of a product probability measure is the second probability measure. -/
@[simp] lemma map_snd_prod : (μ.prod ν).map measurable_snd.aemeasurable = ν

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ (μ.prod ν).map ⋯ = ν

Tactic:
apply Subtype.ext

Result:
case a
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ ↑((μ.prod ν).map ⋯) = ↑ν

Proof state:
case a
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ ↑((μ.prod ν).map ⋯) = ↑ν

Tactic:
simp only [val_eq_to_measure, toMeasure_map, toMeasure_prod, Measure.map_snd_prod,
           measure_univ, one_smul]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/CommRing.lean
theorem totalDegree_sub_C_le (p : MvPolynomial σ R) (r : R) :
    totalDegree (p - C r) ≤ totalDegree p :=
  (totalDegree_sub _ _).trans_eq <| by rw [totalDegree_C, Nat.max_zero]

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
r : R
⊢ p.totalDegree ⊔ (C r).totalDegree = p.totalDegree

Tactic:
rw [totalDegree_C, Nat.max_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_union_eq_left_of_ae (ht_eq : ∀ᵐ x ∂μ.restrict t, f x = 0) :
    ∫ x in s ∪ t, f x ∂μ = ∫ x in s, 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
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
H : IntegrableOn f (s ∪ t) μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ ∀ᵐ (x : X) ∂μ.restrict t, AEStronglyMeasurable.mk f ⋯ x = 0

Tactic:
filter_upwards [ht_eq,
  ae_mono (Measure.restrict_mono subset_union_right le_rfl) H.1.ae_eq_mk] with x hx h'x

Result:
case h
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
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
H : IntegrableOn f (s ∪ t) μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
x : X
hx : f x = 0
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
⊢ AEStronglyMeasurable.mk f ⋯ x = 0
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem exists_dist_eq_iff_exists_dist_orthogonalProjection_eq {s : AffineSubspace ℝ P} [Nonempty s]
    [HasOrthogonalProjection s.direction] {ps : Set P} (hps : ps ⊆ s) (p : P) :
    (∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑(orthogonalProjection s p) = r

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
ps : Set P
hps : ps ⊆ ↑s
p : P
h :
  (ps.Pairwise fun p₁ p₂ => dist p₁ p = dist p₂ p) ↔
    ps.Pairwise fun p₁ p₂ => dist p₁ ↑((orthogonalProjection s) p) = dist p₂ ↑((orthogonalProjection s) p)
⊢ (∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) p) = r

Tactic:
simp_rw [Set.pairwise_eq_iff_exists_eq] at h

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
ps : Set P
hps : ps ⊆ ↑s
p : P
h : (∃ z, ∀ x ∈ ps, dist x p = z) ↔ ∃ z, ∀ x ∈ ps, dist x ↑((orthogonalProjection s) p) = z
⊢ (∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) p) = r

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
ps : Set P
hps : ps ⊆ ↑s
p : P
h : (∃ z, ∀ x ∈ ps, dist x p = z) ↔ ∃ z, ∀ x ∈ ps, dist x ↑((orthogonalProjection s) p) = z
⊢ (∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) p) = r

Tactic:
exact h

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
ps : Set P
hps : ps ⊆ ↑s
p : P
⊢ (∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) p) = r

Tactic:
have h := dist_set_eq_iff_dist_orthogonalProjection_eq hps p

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
ps : Set P
hps : ps ⊆ ↑s
p : P
h :
  (ps.Pairwise fun p₁ p₂ => dist p₁ p = dist p₂ p) ↔
    ps.Pairwise fun p₁ p₂ => dist p₁ ↑((orthogonalProjection s) p) = dist p₂ ↑((orthogonalProjection s) p)
⊢ (∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) p) = r
-- Mathlib/ModelTheory/LanguageMap.lean
theorem card_withConstants :
    L[[α]].card = Cardinal.lift.{w'} L.card + Cardinal.lift.{max u v} #α

Proof state:
L : Language
α : Type w'
⊢ L[[α]].card = lift.{w', max u v} L.card + lift.{max u v, w'} #α

Tactic:
rw [withConstants, card_sum, card_constantsOn]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma ofENat_eq_zero {m : ℕ∞} : (m : Cardinal) = 0 ↔ m = 0

Proof state:
m : ℕ∞
⊢ ↑m = 0 ↔ m = 0

Tactic:
norm_cast

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem embDomain_zero {f : Γ ↪o Γ'} : embDomain f (0 : HahnSeries Γ R) = 0

Proof state:
case coeff.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x✝ : Γ'
⊢ (embDomain f 0).coeff x✝ = coeff 0 x✝

Tactic:
simp [embDomain_notin_image_support]

Result:
no goals

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
⊢ embDomain f 0 = 0

Tactic:
ext

Result:
case coeff.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x✝ : Γ'
⊢ (embDomain f 0).coeff x✝ = coeff 0 x✝
-- Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean
theorem isIntegrallyClosed_iff :
    IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, algebraMap R K y = x

Proof state:
R : Type u_1
inst✝³ : CommRing R
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, (algebraMap R K) y = x

Tactic:
simp [isIntegrallyClosed_iff_isIntegrallyClosedIn K, isIntegrallyClosedIn_iff,
      IsFractionRing.injective R K]

Result:
no goals
-- Mathlib/Topology/StoneCech.lean
theorem Ultrafilter.tendsto_pure_self (b : Ultrafilter α) : Tendsto pure b (𝓝 b)

Proof state:
case h
α : Type u
b : Ultrafilter α
s : Set α
⊢ s ∈ b ↔ {t | s ∈ t} ∈ map pure b

Tactic:
simp_rw [mem_map, preimage_setOf_eq, mem_pure, setOf_mem_eq]

Result:
no goals

Proof state:
case h
α : Type u
b : Ultrafilter α
s : Set α
⊢ s ∈ b ↔ s ∈ joinM (map pure b)

Tactic:
change s ∈ b ↔ {t | s ∈ t} ∈ map pure b

Result:
case h
α : Type u
b : Ultrafilter α
s : Set α
⊢ s ∈ b ↔ {t | s ∈ t} ∈ map pure b

Proof state:
α : Type u
b : Ultrafilter α
⊢ Tendsto pure (↑b) (𝓝 b)

Tactic:
rw [Tendsto, ← coe_map, ultrafilter_converges_iff]

Result:
α : Type u
b : Ultrafilter α
⊢ b = joinM (map pure b)

Proof state:
α : Type u
b : Ultrafilter α
⊢ b = joinM (map pure b)

Tactic:
ext s

Result:
case h
α : Type u
b : Ultrafilter α
s : Set α
⊢ s ∈ b ↔ s ∈ joinM (map pure b)
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem aleph_zero : ℵ_ 0 = ℵ₀

Proof state:
⊢ ℵ_ 0 = ℵ₀

Tactic:
rw [aleph_eq_preAleph, add_zero, preAleph_omega0]

Result:
no goals