harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma IsMeasurableRatCDF.measurable_stieltjesFunction (x : ℝ) :
    Measurable fun a ↦ hf.stieltjesFunction a x

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
⊢ (fun a => ↑(hf.stieltjesFunction a) x) = fun a => ⨅ r, f a ↑r

Tactic:
ext1 a

Result:
case h
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
⊢ ↑(hf.stieltjesFunction a) x = ⨅ r, f a ↑r

Proof state:
case h
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
⊢ ↑(hf.stieltjesFunction a) x = ⨅ r, f a ↑r

Tactic:
rw [← StieltjesFunction.iInf_rat_gt_eq]

Result:
case h
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
⊢ ⨅ r, ↑(hf.stieltjesFunction a) ↑↑r = ⨅ r, f a ↑r

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
this : (fun a => ↑(hf.stieltjesFunction a) x) = fun a => ⨅ r, f a ↑r
⊢ Measurable fun a => ⨅ r, f a ↑r

Tactic:
exact .iInf (fun q ↦ hf.measurable.eval)

Result:
no goals

Proof state:
case h.e_s.h
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
q : { r' // x < ↑r' }
⊢ ↑(hf.stieltjesFunction a) ↑↑q = f a ↑q

Tactic:
rw [stieltjesFunction_eq]

Result:
no goals

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
this : (fun a => ↑(hf.stieltjesFunction a) x) = fun a => ⨅ r, f a ↑r
⊢ Measurable fun a => ↑(hf.stieltjesFunction a) x

Tactic:
rw [this]

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
this : (fun a => ↑(hf.stieltjesFunction a) x) = fun a => ⨅ r, f a ↑r
⊢ Measurable fun a => ⨅ r, f a ↑r

Proof state:
case h
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
⊢ ⨅ r, ↑(hf.stieltjesFunction a) ↑↑r = ⨅ r, f a ↑r

Tactic:
congr with q

Result:
case h.e_s.h
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
q : { r' // x < ↑r' }
⊢ ↑(hf.stieltjesFunction a) ↑↑q = f a ↑q

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
⊢ Measurable fun a => ↑(hf.stieltjesFunction a) x

Tactic:
have : (fun a ↦ hf.stieltjesFunction a x) = fun a ↦ ⨅ r : { r' : ℚ // x < r' }, f a ↑r := by
  ext1 a
  rw [← StieltjesFunction.iInf_rat_gt_eq]
  congr with q
  rw [stieltjesFunction_eq]

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
this : (fun a => ↑(hf.stieltjesFunction a) x) = fun a => ⨅ r, f a ↑r
⊢ Measurable fun a => ↑(hf.stieltjesFunction a) x
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem homEquiv_naturality_left_symm (f : X' ⟶ X) (g : X ⟶ G.obj Y) :
    (adj.homEquiv X' Y).symm (f ≫ g) = F.map f ≫ (adj.homEquiv X Y).symm g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ (adj.homEquiv X' Y).symm (f ≫ g) = F.map f ≫ (adj.homEquiv X Y).symm g

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem natTrailingDegree_natCast (n : ℕ) : natTrailingDegree (n : R[X]) = 0

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (↑n).natTrailingDegree = 0

Tactic:
simp only [← C_eq_natCast, natTrailingDegree_C]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem blsub_eq_zero_iff {o} {f : ∀ a < o, Ordinal} : blsub o f = 0 ↔ o = 0

Proof state:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}
⊢ o.blsub f = 0 ↔ o = 0

Tactic:
rw [← lsub_eq_blsub, lsub_eq_zero_iff]

Result:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}
⊢ IsEmpty o.toType ↔ o = 0

Proof state:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}
⊢ IsEmpty o.toType ↔ o = 0

Tactic:
exact toType_empty_iff_eq_zero

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem find_parent_1 (self : UnionFind) (x : Fin self.size) :
    (self.find x).1.parent x = self.rootD x

Proof state:
self : UnionFind
x : Fin self.size
⊢ parentD (self.findAux x).s ↑x = self.rootD ↑x

Tactic:
rw [parentD_findAux, if_pos rfl]

Result:
no goals

Proof state:
self : UnionFind
x : Fin self.size
⊢ (self.find x).fst.parent ↑x = self.rootD ↑x

Tactic:
simp only [parent, Array.length_toList, find]

Result:
self : UnionFind
x : Fin self.size
⊢ parentD (self.findAux x).s ↑x = self.rootD ↑x
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_nonneg : 0 ≤ mgf X μ t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
⊢ 0 ≤ ∫ (x : Ω), (fun ω => rexp (t * X ω)) x ∂μ

Tactic:
positivity

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
⊢ 0 ≤ mgf X μ t

Tactic:
unfold mgf

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
⊢ 0 ≤ ∫ (x : Ω), (fun ω => rexp (t * X ω)) x ∂μ
-- Mathlib/Data/ENNReal/Real.lean
theorem lt_ofReal_iff_toReal_lt {a : ℝ≥0∞} {b : ℝ} (ha : a ≠ ∞) :
    a < ENNReal.ofReal b ↔ ENNReal.toReal a < b

Proof state:
a : ℝ≥0∞
b : ℝ
ha : a ≠ ⊤
⊢ a < ENNReal.ofReal b ↔ a.toReal < b

Tactic:
lift a to ℝ≥0 using ha

Result:
case intro
b : ℝ
a : ℝ≥0
⊢ ↑a < ENNReal.ofReal b ↔ (↑a).toReal < b

Proof state:
case intro
b : ℝ
a : ℝ≥0
⊢ ↑a < ENNReal.ofReal b ↔ (↑a).toReal < b

Tactic:
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.lt_toNNReal_iff_coe_lt

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_setIfInBounds (a : Array α) (i x) :
    (a.setIfInBounds i x).toList = a.toList.set i x

Proof state:
α : Type u_1
a : Array α
i : Nat
x : α
⊢ (if h : i < a.size then a.set i x h else a).toList = a.toList.set i x

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
a : Array α
i : Nat
x : α
h : i < a.size
⊢ (a.set i x h).toList = a.toList.set i x

case isFalse
α : Type u_1
a : Array α
i : Nat
x : α
h : ¬i < a.size
⊢ a.toList = a.toList.set i x

Proof state:
α : Type u_1
a : Array α
i : Nat
x : α
⊢ (a.setIfInBounds i x).toList = a.toList.set i x

Tactic:
simp only [setIfInBounds]

Result:
α : Type u_1
a : Array α
i : Nat
x : α
⊢ (if h : i < a.size then a.set i x h else a).toList = a.toList.set i x

Proof state:
case isFalse
α : Type u_1
a : Array α
i : Nat
x : α
h : ¬i < a.size
⊢ a.toList = a.toList.set i x

Tactic:
simp [List.set_eq_of_length_le (by simpa using h)]

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i : Nat
x : α
h : ¬i < a.size
⊢ List.length ?m.143006 ≤ ?m.143007

Tactic:
simpa using h

Result:
no goals

Proof state:
case isTrue
α : Type u_1
a : Array α
i : Nat
x : α
h : i < a.size
⊢ (a.set i x h).toList = a.toList.set i x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem add_eq_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b = c) = (a = c - b)

Proof state:
a b c : Nat
h : b ≤ c
r : (a + b = c) = (a = c - b)
⊢ (a + b = c) = (a = c - b)

Tactic:
exact r

Result:
no goals

Proof state:
a b c : Nat
h : b ≤ c
r : (a + b = 0 + c) = (a = 0 + (c - b))
⊢ (a + b = c) = (a = c - b)

Tactic:
simp only [Nat.zero_add] at r

Result:
a b c : Nat
h : b ≤ c
r : (a + b = c) = (a = c - b)
⊢ (a + b = c) = (a = c - b)

Proof state:
a b c : Nat
h : b ≤ c
⊢ (a + b = c) = (a = c - b)

Tactic:
have r := add_eq_add_le a 0 h

Result:
a b c : Nat
h : b ≤ c
r : (a + b = 0 + c) = (a = 0 + (c - b))
⊢ (a + b = c) = (a = c - b)
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem bot_right : A.LinearDisjoint ⊥

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
A : Subalgebra R S
⊢ (toSubmodule A).LinearDisjoint 1

Tactic:
exact Submodule.LinearDisjoint.one_right _

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
A : Subalgebra R S
⊢ A.LinearDisjoint ⊥

Tactic:
rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot]

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
A : Subalgebra R S
⊢ (toSubmodule A).LinearDisjoint 1
-- Mathlib/Data/Finset/Insert.lean
theorem toFinset_eq_empty_iff (l : List α) : l.toFinset = ∅ ↔ l = nil

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.toFinset = ∅ ↔ l = []

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem le_of_sub_one_lt (h : x - 1 < y) : x ≤ y

Proof state:
α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : pred x < y
⊢ x ≤ y

Tactic:
exact le_of_pred_lt h

Result:
no goals

Proof state:
α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : x - 1 < y
⊢ x ≤ y

Tactic:
rw [← pred_eq_sub_one] at h

Result:
α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : pred x < y
⊢ x ≤ y
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonAssocSemiring_injective :
    Function.Injective (@toNonAssocSemiring R)

Proof state:
R : Type u
a₁✝ a₂✝ : Semiring R
h : toNonAssocSemiring = toNonAssocSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Result:
case h_add.h.h
R : Type u
a₁✝ a₂✝ : Semiring R
h : toNonAssocSemiring = toNonAssocSemiring
x y : R
⊢ x + y = x + y

case h_mul.h.h
R : Type u
a₁✝ a₂✝ : Semiring R
h : toNonAssocSemiring = toNonAssocSemiring
x y : R
⊢ x * y = x * y

Proof state:
R : Type u
⊢ Function.Injective (@toNonAssocSemiring R)

Tactic:
intro _ _ h

Result:
R : Type u
a₁✝ a₂✝ : Semiring R
h : toNonAssocSemiring = toNonAssocSemiring
⊢ a₁✝ = a₂✝
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_δ' {n} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j) :
    X.δ j ≫ X.δ i =
      X.δ (Fin.castSucc i) ≫
        X.δ (j.pred fun (hj : j = 0) => by simp [hj, Fin.not_lt_zero] at H)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ (j.pred ⋯)).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ' H]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
hj : j = 0
⊢ False

Tactic:
simp [hj, Fin.not_lt_zero] at H

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ X.δ j ≫ X.δ i = X.δ i.castSucc ≫ X.δ (j.pred ⋯)

Tactic:
dsimp [δ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ (j.pred ⋯)).op
-- Mathlib/Data/Finset/Image.lean
theorem subtype_map_of_mem {p : α → Prop} [DecidablePred p] {s : Finset α} (h : ∀ x ∈ s, p x) :
    (s.subtype p).map (Embedding.subtype _) = s := ext <| by simpa [subtype_map] using h

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
h : ∀ x ∈ s, p x
⊢ ∀ (a : α), a ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ a ∈ s

Tactic:
simpa [subtype_map] using h

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem succ_iterate [AddMonoidWithOne α] [SuccAddOrder α] (x : α) (n : ℕ) :
    succ^[n] x = x + n

Proof state:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
IH : succ^[n] x = x + ↑n
⊢ succ^[n + 1] x = x + ↑(n + 1)

Tactic:
rw [Function.iterate_succ_apply', IH, Nat.cast_add, succ_eq_add_one, Nat.cast_one, add_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
⊢ succ^[n] x = x + ↑n

Tactic:
induction n with
| zero =>
  rw [Function.iterate_zero_apply, Nat.cast_zero, add_zero]
| succ n IH =>
  rw [Function.iterate_succ_apply', IH, Nat.cast_add, succ_eq_add_one, Nat.cast_one, add_assoc]

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
⊢ succ^[0] x = x + ↑0

Tactic:
rw [Function.iterate_zero_apply, Nat.cast_zero, add_zero]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem cthickening_eq_iInter_cthickening {δ : ℝ} (E : Set α) :
    cthickening δ E = ⋂ (ε : ℝ) (_ : δ < ε), cthickening ε E

Proof state:
case hs
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty

Tactic:
simp_rw [inter_eq_right.mpr Ioc_subset_Ioi_self]

Result:
case hs
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioc δ ε).Nonempty

Proof state:
case hs
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioc δ ε).Nonempty

Tactic:
exact fun _ hε => nonempty_Ioc.mpr hε

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening δ E = ⋂ ε, ⋂ (_ : δ < ε), cthickening ε E

Tactic:
apply cthickening_eq_iInter_cthickening' (Ioi δ) rfl.subset

Result:
case hs
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Sized.pos {s l x r} (h : Sized (@node α s l x r)) : 0 < s

Proof state:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ 0 < s

Tactic:
rw [h.1]

Result:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ 0 < l.size + r.size + 1

Proof state:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ 0 < l.size + r.size + 1

Tactic:
apply Nat.le_add_left

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem norm_id_le : ‖(id V : NormedAddGroupHom V V)‖ ≤ 1 :=
  opNorm_le_bound _ zero_le_one fun x => by simp

Proof state:
V : Type u_1
inst✝ : SeminormedAddCommGroup V
x : V
⊢ ‖(id V) x‖ ≤ 1 * ‖x‖

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
@[simp]
lemma ringHomComp_one (f : R' →+* R'') : (1 : MulChar R R').ringHomComp f = 1

Proof state:
case h
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
a✝ : Rˣ
⊢ (ringHomComp 1 f) ↑a✝ = 1 ↑a✝

Tactic:
simp only [MulChar.ringHomComp_apply, MulChar.one_apply_coe, map_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
⊢ ringHomComp 1 f = 1

Tactic:
ext1

Result:
case h
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
a✝ : Rˣ
⊢ (ringHomComp 1 f) ↑a✝ = 1 ↑a✝
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem Associated.eq_zero_iff [MonoidWithZero M] {a b : M} (h : a ~ᵤ b) : a = 0 ↔ b = 0

Proof state:
case intro
M : Type u_1
inst✝ : MonoidWithZero M
a : M
u : Mˣ
⊢ a = 0 ↔ a * ↑u = 0

Tactic:
rw [← Units.eq_mul_inv_iff_mul_eq, zero_mul]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : MonoidWithZero M
a b : M
h : a ~ᵤ b
⊢ a = 0 ↔ b = 0

Tactic:
obtain ⟨u, rfl⟩ := h

Result:
case intro
M : Type u_1
inst✝ : MonoidWithZero M
a : M
u : Mˣ
⊢ a = 0 ↔ a * ↑u = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem BitVec.lt_ult (x y : BitVec w) : (x < y) = (BitVec.ult x y = true)

Proof state:
w : Nat
x y : BitVec w
⊢ (x < y) = (x.ult y = true)

Tactic:
rw [BitVec.ult]

Result:
w : Nat
x y : BitVec w
⊢ (x < y) = (decide (x.toNat < y.toNat) = true)

Proof state:
w : Nat
x y : BitVec w
⊢ x.toNat.lt y.toNat = (decide (x.toNat.lt y.toNat) = true)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get?_insertIfNew [LawfulBEq α] {k a : α} {v : β k} : (m.insertIfNew k v).get? a =
    if h : k == a ∧ ¬k ∈ m then some (cast (congrArg β (eq_of_beq h.1)) v) else m.get? a

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k a : α
v : β k
⊢ (m.insertIfNew k v).get? a = if h : (k == a) = true ∧ m.contains k = false then some (cast ⋯ v) else m.get? a

Tactic:
exact Raw₀.get?_insertIfNew ⟨m.1, _⟩ m.2

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k a : α
v : β k
⊢ (m.insertIfNew k v).get? a = if h : (k == a) = true ∧ ¬k ∈ m then some (cast ⋯ v) else m.get? a

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k a : α
v : β k
⊢ (m.insertIfNew k v).get? a = if h : (k == a) = true ∧ m.contains k = false then some (cast ⋯ v) else m.get? a
-- Mathlib/Data/Matrix/Basis.lean
theorem apply_of_ne (h : ¬(i = i' ∧ j = j')) : stdBasisMatrix i j c i' j' = 0

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ stdBasisMatrix i j c i' j' = 0

Tactic:
simp only [stdBasisMatrix, and_imp, ite_eq_right_iff, of_apply]

Result:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ i = i' → j = j' → c = 0

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ i = i' → j = j' → c = 0

Tactic:
tauto

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem card_opow_eq_of_omega0_le_left {a b : Ordinal} (ha : ω ≤ a) (hb : 0 < b) :
    (a ^ b).card = max a.card b.card

Proof state:
case a
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ b ≤ a ^ b

Tactic:
exact right_le_opow b (one_lt_omega0.trans_le ha)

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ (a ^ b).card = a.card ⊔ b.card

Tactic:
apply (card_opow_le_of_omega0_le_left ha b).antisymm (max_le _ _) <;> apply card_le_card

Result:
case a
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ a ≤ a ^ b

case a
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ b ≤ a ^ b

Proof state:
case a
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ a ≤ a ^ b

Tactic:
exact left_le_opow a hb

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_exp_exists (z : ℂ) :
    ∃ n : ℤ, log (exp z) = z + n * (2 * π * I)

Proof state:
z : ℂ
⊢ cexp z ≠ 0

Tactic:
exact exp_ne_zero z

Result:
no goals

Proof state:
z : ℂ
⊢ ∃ n, log (cexp z) = z + ↑n * (2 * ↑π * I)

Tactic:
rw [← exp_eq_exp_iff_exists_int, exp_log]

Result:
z : ℂ
⊢ cexp z ≠ 0
-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/-- A Mahler series whose coefficients tend to 0 is convergent. -/
lemma hasSum_mahlerSeries (ha : Tendsto a atTop (𝓝 0)) :
    HasSum (fun n ↦ mahlerTerm (a n) n) (mahlerSeries a : C(ℤ_[p], E))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto (fun x => ‖a x‖) atTop (𝓝 0)
⊢ Tendsto (fun x => ‖mahlerTerm (a x) x‖) cofinite (𝓝 0)

Tactic:
simpa only [norm_mahlerTerm, Nat.cofinite_eq_atTop] using ha

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
⊢ Tendsto (fun n => mahlerTerm (a n) n) cofinite (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero] at ha ⊢

Result:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto (fun x => ‖a x‖) atTop (𝓝 0)
⊢ Tendsto (fun x => ‖mahlerTerm (a x) x‖) cofinite (𝓝 0)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
⊢ HasSum (fun n => mahlerTerm (a n) n) (mahlerSeries a)

Tactic:
refine (NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero ?_).hasSum

Result:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
⊢ Tendsto (fun n => mahlerTerm (a n) n) cofinite (𝓝 0)
-- Mathlib/AlgebraicGeometry/RationalMap.lean
@[ext]
lemma ext (f g : X.PartialMap Y) (e : f.domain = g.domain)
    (H : f.hom = (X.isoOfEq e).hom ≫ g.hom) : f = g

Proof state:
X Y : Scheme
f g : X.PartialMap Y
e : f.domain = g.domain
H : f.hom = (X.isoOfEq e).hom ≫ g.hom
⊢ ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom

Tactic:
exact ⟨e, H⟩

Result:
no goals

Proof state:
X Y : Scheme
f g : X.PartialMap Y
e : f.domain = g.domain
H : f.hom = (X.isoOfEq e).hom ≫ g.hom
⊢ f = g

Tactic:
rw [ext_iff]

Result:
X Y : Scheme
f g : X.PartialMap Y
e : f.domain = g.domain
H : f.hom = (X.isoOfEq e).hom ≫ g.hom
⊢ ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem ι_mul_ι_add_swap_of_isOrtho {a b : M} (h : Q.IsOrtho a b) :
    ι Q a * ι Q b + ι Q b * ι Q a = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ (ι Q) a * (ι Q) b + (ι Q) b * (ι Q) a = 0

Tactic:
rw [ι_mul_ι_add_swap, h.polar_eq_zero]

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ (algebraMap R (CliffordAlgebra Q)) 0 = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ (algebraMap R (CliffordAlgebra Q)) 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem fold_zero {α : Type u} (f : (i : Nat) → i < 0 → α → α) (init : α) :
    fold 0 f init = init

Proof state:
α : Type u
f : (i : Nat) → i < 0 → α → α
init : α
⊢ fold 0 f init = init

Tactic:
simp [fold]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
lemma mk_eq_zero_of_den (f : NumDenSameDeg 𝒜 x) (h : f.den = 0) : mk f = 0

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
f : NumDenSameDeg 𝒜 x
h : f.den = 0
⊢ mk f = 0

Tactic:
have := subsingleton 𝒜 (h ▸ f.den_mem)

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
f : NumDenSameDeg 𝒜 x
h : f.den = 0
this : Subsingleton (HomogeneousLocalization 𝒜 x)
⊢ mk f = 0

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
f : NumDenSameDeg 𝒜 x
h : f.den = 0
this : Subsingleton (HomogeneousLocalization 𝒜 x)
⊢ mk f = 0

Tactic:
exact Subsingleton.elim _ _

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem _root_.FreeMonoid.mrange_lift {α} (f : α → M) :
    mrange (FreeMonoid.lift f) = closure (Set.range f)

Proof state:
M : Type u_1
inst✝ : Monoid M
α : Type u_4
f : α → M
⊢ mrange (FreeMonoid.lift f) = closure (Set.range f)

Tactic:
rw [mrange_eq_map, ← FreeMonoid.closure_range_of, map_mclosure, ← Set.range_comp,
  FreeMonoid.lift_comp_of]

Result:
no goals