harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_sdiff (x y : ZFSet.{u}) : (x \ y).toSet = x.toSet \ y.toSet

Proof state:
case h
x y x✝ : ZFSet.{u}
⊢ x✝ ∈ (ZFSet.sep (fun z => z ∉ y) x).toSet ↔ x✝ ∈ x.toSet \ y.toSet

Tactic:
simp

Result:
no goals

Proof state:
x y : ZFSet.{u}
⊢ (ZFSet.sep (fun z => z ∉ y) x).toSet = x.toSet \ y.toSet

Tactic:
ext

Result:
case h
x y x✝ : ZFSet.{u}
⊢ x✝ ∈ (ZFSet.sep (fun z => z ∉ y) x).toSet ↔ x✝ ∈ x.toSet \ y.toSet

Proof state:
x y : ZFSet.{u}
⊢ (x \ y).toSet = x.toSet \ y.toSet

Tactic:
change (ZFSet.sep (fun z => z ∉ y) x).toSet = _

Result:
x y : ZFSet.{u}
⊢ (ZFSet.sep (fun z => z ∉ y) x).toSet = x.toSet \ y.toSet
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_of_mem {a : α} {l : Array α} (h : a ∈ l) : ∃ s t : Array α, l = s.push a ++ t

Proof state:
α : Type u_1
a : α
l : Array α
h : a ∈ l
⊢ ∃ s t, l = s.push a ++ t

Tactic:
obtain ⟨s, t, w⟩ := List.append_of_mem (l := l.toList) (by simpa using h)

Result:
case intro.intro
α : Type u_1
a : α
l : Array α
h : a ∈ l
s t : List α
w : l.toList = s ++ a :: t
⊢ ∃ s t, l = s.push a ++ t

Proof state:
α : Type u_1
a : α
l : Array α
h : a ∈ l
s t : List α
w : l.toList.toArray = (s ++ a :: t).toArray
⊢ l = s.toArray.push a ++ t.toArray

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
a : α
l : Array α
h : a ∈ l
⊢ ?m.226977 ∈ l.toList

Tactic:
simpa using h

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
a : α
l : Array α
h : a ∈ l
s t : List α
w : l.toList.toArray = (s ++ a :: t).toArray
⊢ ∃ s t, l = s.push a ++ t

Tactic:
refine ⟨s.toArray, t.toArray, by simp_all⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
a : α
l : Array α
h : a ∈ l
s t : List α
w : l.toList = s ++ a :: t
⊢ ∃ s t, l = s.push a ++ t

Tactic:
replace w := congrArg List.toArray w

Result:
case intro.intro
α : Type u_1
a : α
l : Array α
h : a ∈ l
s t : List α
w : l.toList.toArray = (s ++ a :: t).toArray
⊢ ∃ s t, l = s.push a ++ t
-- Mathlib/Data/Matrix/Reflection.lean
theorem mulVecᵣ_eq [NonUnitalNonAssocSemiring α] (A : Matrix (Fin l) (Fin m) α) (v : Fin m → α) :
    mulVecᵣ A v = A *ᵥ v

Proof state:
l m : ℕ
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix (Fin l) (Fin m) α
v : Fin m → α
⊢ (fun a => a ⬝ᵥ v) ∘ A = A *ᵥ v

Tactic:
rfl

Result:
no goals

Proof state:
l m : ℕ
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix (Fin l) (Fin m) α
v : Fin m → α
⊢ A.mulVecᵣ v = A *ᵥ v

Tactic:
simp [mulVecᵣ, Function.comp]

Result:
l m : ℕ
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix (Fin l) (Fin m) α
v : Fin m → α
⊢ (fun a => a ⬝ᵥ v) ∘ A = A *ᵥ v
-- Mathlib/Algebra/Lie/Derivation/Basic.lean
theorem eqOn_lieSpan {s : Set L} (h : Set.EqOn D1 D2 s) :
    Set.EqOn D1 D2 (LieSubalgebra.lieSpan R L s) :=
    fun _ hz =>
      have zero : D1 0 = D2 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn (⇑D1) (⇑D2) s
x✝² : L
hz : x✝² ∈ ↑(LieSubalgebra.lieSpan R L s)
zero : D1 0 = D2 0
smul : ∀ (r : R) {x : L}, D1 x = D2 x → D1 (r • x) = D2 (r • x)
add : ∀ (x y : L), D1 x = D2 x → D1 y = D2 y → D1 (x + y) = D2 (x + y)
x✝¹ x✝ : L
hx : D1 x✝¹ = D2 x✝¹
hy : D1 x✝ = D2 x✝
⊢ D1 ⁅x✝¹, x✝⁆ = D2 ⁅x✝¹, x✝⁆

Tactic:
simp only [apply_lie_eq_sub, hx, hy]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn (⇑D1) (⇑D2) s
x✝ : L
hz : x✝ ∈ ↑(LieSubalgebra.lieSpan R L s)
⊢ D1 0 = D2 0

Tactic:
simp only [map_zero]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn (⇑D1) (⇑D2) s
x✝² : L
hz : x✝² ∈ ↑(LieSubalgebra.lieSpan R L s)
zero : D1 0 = D2 0
smul : ∀ (r : R) {x : L}, D1 x = D2 x → D1 (r • x) = D2 (r • x)
x✝¹ x✝ : L
hx : D1 x✝¹ = D2 x✝¹
hy : D1 x✝ = D2 x✝
⊢ D1 (x✝¹ + x✝) = D2 (x✝¹ + x✝)

Tactic:
simp only [map_add, hx, hy]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn (⇑D1) (⇑D2) s
x✝² : L
hz : x✝² ∈ ↑(LieSubalgebra.lieSpan R L s)
zero : D1 0 = D2 0
x✝¹ : R
x✝ : L
hx : D1 x✝ = D2 x✝
⊢ D1 (x✝¹ • x✝) = D2 (x✝¹ • x✝)

Tactic:
simp only [map_smul, hx]

Result:
no goals
-- Mathlib/Algebra/Lie/TraceForm.lean
@[simp] lemma traceForm_eq_zero_of_isTrivial [IsTrivial L M] :
    traceForm R L M = 0

Proof state:
case H.h
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
x y : L
m : M
⊢ (φ x ∘ₗ φ y) m = 0 m

Tactic:
simp

Result:
no goals

Proof state:
case H
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
x y : L
⊢ ((traceForm R L M) x) y = (0 x) y

Tactic:
suffices φ x ∘ₗ φ y = 0 by simp [traceForm_apply_apply, this]

Result:
case H
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
x y : L
⊢ φ x ∘ₗ φ y = 0

Proof state:
case H
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
x y : L
⊢ φ x ∘ₗ φ y = 0

Tactic:
ext m

Result:
case H.h
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
x y : L
m : M
⊢ (φ x ∘ₗ φ y) m = 0 m

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
⊢ traceForm R L M = 0

Tactic:
ext x y

Result:
case H
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
x y : L
⊢ ((traceForm R L M) x) y = (0 x) y

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
x y : L
this : φ x ∘ₗ φ y = 0
⊢ ((traceForm R L M) x) y = (0 x) y

Tactic:
simp [traceForm_apply_apply, this]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
lemma map_comp {U : Type*} {G'' : SimpleGraph U} (H : G.Subgraph) (f : G →g G') (g : G' →g G'') :
    H.map (g.comp f) = (H.map f).map g

Proof state:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
⊢ Subgraph.map (g.comp f) H = Subgraph.map g (Subgraph.map f H)

Tactic:
ext <;> simp [Subgraph.map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Char/Basic.lean
theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < UInt32.size

Proof state:
n : Nat
h : isValidCharNat n
left✝ : 57343 < n
h₂ : n < 1114112
⊢ n < UInt32.size

Tactic:
apply Nat.lt_trans h₂

Result:
n : Nat
h : isValidCharNat n
left✝ : 57343 < n
h₂ : n < 1114112
⊢ 1114112 < UInt32.size

Proof state:
n : Nat
h : isValidCharNat n
left✝ : 57343 < n
h₂ : n < 1114112
⊢ 1114112 < UInt32.size

Tactic:
decide

Result:
no goals

Proof state:
n : Nat
h✝ : isValidCharNat n
h : n < 55296
⊢ 55296 < UInt32.size

Tactic:
decide

Result:
no goals

Proof state:
n : Nat
h : isValidCharNat n
⊢ n < UInt32.size

Tactic:
match h with
| Or.inl h        =>
  apply Nat.lt_trans h
  decide
| Or.inr ⟨_,  h₂⟩ =>
  apply Nat.lt_trans h₂
  decide

Result:
no goals

Proof state:
n : Nat
h✝ : isValidCharNat n
h : n < 55296
⊢ n < UInt32.size

Tactic:
apply Nat.lt_trans h

Result:
n : Nat
h✝ : isValidCharNat n
h : n < 55296
⊢ 55296 < UInt32.size
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem unop_snd {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) :
    c.unop.snd = c.inr.unop

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ c.unop.snd = c.inr.unop

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
lemma exists_mem_image2 {p : γ → Prop} :
    (∃ z ∈ image2 f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
p : γ → Prop
⊢ (∃ z ∈ image2 f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y)

Tactic:
aesop

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
/-- The `covolume` can be computed by taking the `volume` of any given fundamental domain `s`. -/
@[to_additive]
lemma IsFundamentalDomain.covolume_eq_volume (ν : Measure α) [Countable G]
    [MeasurableSpace G] [MeasurableSMul G α] [SMulInvariantMeasure G α ν] {s : Set α}
    (fund_dom_s : IsFundamentalDomain G s ν) : covolume G α ν = ν s

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α ν
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ covolume G α ν = ν s

Tactic:
dsimp [covolume]

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α ν
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ (if funDom : HasFundamentalDomain G α ν then ν ⋯.choose else 0) = ν s

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α ν
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ IsFundamentalDomain G ⋯.choose ν

Tactic:
exact (fund_dom_s.hasFundamentalDomain ν).ExistsIsFundamentalDomain.choose_spec

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α ν
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ ν ⋯.choose = ν s

Tactic:
rw [fund_dom_s.measure_eq]

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α ν
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ IsFundamentalDomain G ⋯.choose ν

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α ν
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ (if funDom : HasFundamentalDomain G α ν then ν ⋯.choose else 0) = ν s

Tactic:
simp only [(fund_dom_s.hasFundamentalDomain ν), ↓reduceDIte]

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α ν
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ ν ⋯.choose = ν s
-- Mathlib/NumberTheory/PrimeCounting.lean
theorem primeCounting_sub_one (n : ℕ) : π (n - 1) = π' n

Proof state:
n : ℕ
⊢ π (n - 1) = π' n

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
/-- The interior is the complement of the boundary. -/
lemma compl_boundary : (I.boundary M)ᶜ = I.interior M

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ (ModelWithCorners.boundary M)ᶜ = ModelWithCorners.interior M

Tactic:
rw [← compl_interior, compl_compl]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_union_inter_subset_union :
    image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
rw [image2_union_left]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f s (t ∩ t') ∪ image2 f s' (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f s (t ∩ t') ∪ image2 f s' (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
exact
  union_subset_union (image2_subset_left inter_subset_left)
    (image2_subset_left inter_subset_right)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_signExtend {x : BitVec w} {v i : Nat} :
    (x.signExtend v).getMsbD i =
      (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else x.msb)

Proof state:
case false
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = false
⊢ (decide (v - w ≤ i) && x.getMsbD (i + w - v)) = (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else false)

Tactic:
by_cases h : v - w ≤ i <;> simp [h, getMsbD] <;> omega

Result:
no goals

Proof state:
case false
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = false
⊢ (signExtend v x).getMsbD i = (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else false)

Tactic:
simp only [signExtend_eq_setWidth_of_msb_false hmsb, getMsbD_setWidth]

Result:
case false
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = false
⊢ (decide (v - w ≤ i) && x.getMsbD (i + w - v)) = (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else false)

Proof state:
case true
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = true
⊢ (signExtend v x).getMsbD i = (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else true)

Tactic:
simp only [signExtend_eq_not_setWidth_not_of_msb_true hmsb, getMsbD_not, getMsbD_setWidth]

Result:
case true
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = true
⊢ (decide (i < v) && !(decide (v - w ≤ i) && (decide (i + w - v < w) && !x.getMsbD (i + w - v)))) =
    (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else true)

Proof state:
case true
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = true
⊢ (decide (i < v) && !(decide (v - w ≤ i) && (decide (i + w - v < w) && !x.getMsbD (i + w - v)))) =
    (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else true)

Tactic:
by_cases h : i < v <;> by_cases h' : v - w ≤ i <;> simp [h, h'] <;> omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
v i : Nat
⊢ (signExtend v x).getMsbD i = (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else x.msb)

Tactic:
rcases hmsb : x.msb with rfl | rfl

Result:
case false
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = false
⊢ (signExtend v x).getMsbD i = (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else false)

case true
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = true
⊢ (signExtend v x).getMsbD i = (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else true)
-- Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean
theorem map_inv₀ : f a⁻¹ = (f a)⁻¹

Proof state:
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
⊢ f a⁻¹ = (f a)⁻¹

Tactic:
by_cases h : a = 0

Result:
case pos
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : a = 0
⊢ f a⁻¹ = (f a)⁻¹

case neg
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ f a⁻¹ = (f a)⁻¹

Proof state:
case pos
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : a = 0
⊢ f a⁻¹ = (f a)⁻¹

Tactic:
simp [h, map_zero f]

Result:
no goals

Proof state:
case neg.h
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ f a⁻¹ * f a = 1

Tactic:
rw [← map_mul, inv_mul_cancel₀ h, map_one]

Result:
no goals

Proof state:
case neg
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ f a⁻¹ = (f a)⁻¹

Tactic:
apply eq_inv_of_mul_eq_one_left

Result:
case neg.h
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ f a⁻¹ * f a = 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_rotateLeft : eval (rotateLeft n) = ((BitVec.rotateLeft · n) : BitVec w → BitVec w)

Proof state:
n w : Nat
⊢ (rotateLeft n).eval = fun x => x.rotateLeft n

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueD_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((_ : α) × β)} {a : α}
    {fallback : β} (hl : DistinctKeys l) (h : Perm l l') :
    getValueD a l fallback = getValueD a l' fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((_ : α) × β)
a : α
fallback : β
hl : DistinctKeys l
h : l.Perm l'
⊢ getValueD a l fallback = getValueD a l' fallback

Tactic:
simp only [getValueD_eq_getValue?, getValue?_of_perm hl h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_eq_setToFun (f : α → E) :
    ∫ a, f a ∂μ = setToFun μ (weightedSMul μ) (dominatedFinMeasAdditive_weightedSMul μ) f

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
⊢ ∫ (a : α), f a ∂μ = setToFun μ (weightedSMul μ) ⋯ f

Tactic:
simp only [integral, hE, L1.integral]

Result:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
⊢ (if h : True then if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
    else 0) =
    setToFun μ (weightedSMul μ) ⋯ f

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
⊢ (if h : True then if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
    else 0) =
    setToFun μ (weightedSMul μ) ⋯ f

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
lemma map_injective {φ : R →+* A} (hφ : Function.Injective φ) :
    Function.Injective <| map (φ := φ) := fun _ _ h => by
  rcases mk.inj h with ⟨h, _, _, _⟩
  replace h := (Units.mk.inj h).left
  ext <;> apply_fun _ using hφ <;> assumption

Proof state:
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h : map φ x✝¹ = map φ x✝
⊢ x✝¹ = x✝

Tactic:
rcases mk.inj h with ⟨h, _, _, _⟩

Result:
case intro.intro.intro
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : map φ x✝¹ = map φ x✝
h : (Units.map ↑φ) x✝¹.u = (Units.map ↑φ) x✝.u
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
⊢ x✝¹ = x✝

Proof state:
case intro.intro.intro
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : map φ x✝¹ = map φ x✝
h : (Units.map ↑φ) x✝¹.u = (Units.map ↑φ) x✝.u
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
⊢ x✝¹ = x✝

Tactic:
replace h := (Units.mk.inj h).left

Result:
case intro.intro.intro
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : map φ x✝¹ = map φ x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ x✝¹ = x✝

Proof state:
case intro.intro.intro
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : map φ x✝¹ = map φ x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ x✝¹ = x✝

Tactic:
ext <;> apply_fun _ using hφ <;> assumption

Result:
no goals
-- Mathlib/Data/Prod/Basic.lean
theorem mk.inj_right {α β : Type*} (b : β) :
    Function.Injective (fun a ↦ Prod.mk a b : α → α × β)

Proof state:
α : Type u_5
β : Type u_6
b : β
⊢ Function.Injective fun a => (a, b)

Tactic:
intro b₁ b₂ h

Result:
α : Type u_5
β : Type u_6
b : β
b₁ b₂ : α
h : (fun a => (a, b)) b₁ = (fun a => (a, b)) b₂
⊢ b₁ = b₂

Proof state:
α : Type u_5
β : Type u_6
b : β
b₁ b₂ : α
h : (fun a => (a, b)) b₁ = (fun a => (a, b)) b₂
⊢ b₁ = b₂

Tactic:
simpa only [and_true, eq_self_iff_true, mk.inj_iff] using h

Result:
no goals
-- Mathlib/Data/ENNReal/Operations.lean
theorem sum_lt_sum_of_nonempty {s : Finset α} (hs : s.Nonempty) {f g : α → ℝ≥0∞}
    (Hlt : ∀ i ∈ s, f i < g i) : ∑ i ∈ s, f i < ∑ i ∈ s, g i

Proof state:
case cons
α : Type u_1
s : Finset α
f g : α → ℝ≥0∞
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (∀ i ∈ s✝, f i < g i) → ∑ i ∈ s✝, f i < ∑ i ∈ s✝, g i
Hlt : ∀ i ∈ cons a✝ s✝ h✝, f i < g i
⊢ ∑ i ∈ cons a✝ s✝ h✝, f i < ∑ i ∈ cons a✝ s✝ h✝, g i

Tactic:
simp only [Finset.sum_cons, forall_mem_cons] at Hlt ⊢

Result:
case cons
α : Type u_1
s : Finset α
f g : α → ℝ≥0∞
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (∀ i ∈ s✝, f i < g i) → ∑ i ∈ s✝, f i < ∑ i ∈ s✝, g i
Hlt : f a✝ < g a✝ ∧ ∀ x ∈ s✝, f x < g x
⊢ f a✝ + ∑ i ∈ s✝, f i < g a✝ + ∑ i ∈ s✝, g i

Proof state:
case cons
α : Type u_1
s : Finset α
f g : α → ℝ≥0∞
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (∀ i ∈ s✝, f i < g i) → ∑ i ∈ s✝, f i < ∑ i ∈ s✝, g i
Hlt : f a✝ < g a✝ ∧ ∀ x ∈ s✝, f x < g x
⊢ f a✝ + ∑ i ∈ s✝, f i < g a✝ + ∑ i ∈ s✝, g i

Tactic:
exact ENNReal.add_lt_add Hlt.1 (ih Hlt.2)

Result:
no goals

Proof state:
case singleton
α : Type u_1
s : Finset α
f g : α → ℝ≥0∞
a✝ : α
Hlt : ∀ i ∈ {a✝}, f i < g i
⊢ ∑ i ∈ {a✝}, f i < ∑ i ∈ {a✝}, g i

Tactic:
simp [Hlt _ (Finset.mem_singleton_self _)]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hlt : ∀ i ∈ s, f i < g i
⊢ ∑ i ∈ s, f i < ∑ i ∈ s, g i

Tactic:
induction hs using Finset.Nonempty.cons_induction with
| singleton => simp [Hlt _ (Finset.mem_singleton_self _)]
| cons _ _ _ _ ih =>
  simp only [Finset.sum_cons, forall_mem_cons] at Hlt ⊢
  exact ENNReal.add_lt_add Hlt.1 (ih Hlt.2)

Result:
no goals