harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/LocalRing/Subring.lean
theorem of_injective [IsLocalRing S] {f : R →+* S} (hf : Function.Injective f)
    (h : ∀ a, a ∈ R⁰ → IsUnit a) : IsLocalRing R

Proof state:
R : Type u_2
S : Type u_1
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : IsLocalRing S
f : R →+* S
hf : Function.Injective ⇑f
h : ∀ a ∈ R⁰, IsUnit a
⊢ IsLocalRing R

Tactic:
haveI : Nontrivial R := f.domain_nontrivial

Result:
R : Type u_2
S : Type u_1
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : IsLocalRing S
f : R →+* S
hf : Function.Injective ⇑f
h : ∀ a ∈ R⁰, IsUnit a
this : Nontrivial R
⊢ IsLocalRing R

Proof state:
R : Type u_2
S : Type u_1
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : IsLocalRing S
f : R →+* S
hf : Function.Injective ⇑f
h : ∀ a ∈ R⁰, IsUnit a
this : Nontrivial R
⊢ IsLocalRing R

Tactic:
refine .of_is_unit_or_is_unit_of_add_one fun {a b} hab ↦
  (IsLocalRing.isUnit_or_isUnit_of_add_one (map_add f .. ▸ map_one f ▸ congrArg f hab)).imp ?_ ?_
<;> exact h _ ∘ mem_nonZeroDivisors_of_injective hf ∘ IsUnit.mem_nonZeroDivisors

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem?_succ_ofBool (b : Bool) (i : Nat) : (ofBool b)[i + 1]? = none

Proof state:
b : Bool
i : Nat
⊢ (ofBool b)[i + 1]? = none

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem permutationsAux2_fst (t : α) (ts : List α) (r : List β) :
    ∀ (ys : List α) (f : List α → β), (permutationsAux2 t ts r ys f).1 = ys ++ ts
  | [], _ => rfl
  | y :: ys, f => by simp [permutationsAux2, permutationsAux2_fst t _ _ ys]

Proof state:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
y : α
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r (y :: ys) f).1 = y :: ys ++ ts

Tactic:
simp [permutationsAux2, permutationsAux2_fst t _ _ ys]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem norm_pow_le [NormOneClass α] (a : α) (n : ℕ) : ‖a ^ n‖ ≤ ‖a‖ ^ n :=
  Nat.recOn n (by simp only [pow_zero, norm_one, le_rfl])
    fun n _hn => norm_pow_le' a n.succ_pos

Proof state:
α : Type u_2
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
a : α
n : ℕ
⊢ ‖a ^ Nat.zero‖ ≤ ‖a‖ ^ Nat.zero

Tactic:
simp only [pow_zero, norm_one, le_rfl]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem hasFDerivAtFilter_add_const_iff (c : F) :
    HasFDerivAtFilter (f · + c) f' x L ↔ HasFDerivAtFilter f f' x L

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
L : Filter E
c : F
⊢ HasFDerivAtFilter (fun x => f x + c) f' x L ↔ HasFDerivAtFilter f f' x L

Tactic:
simp [hasFDerivAtFilter_iff_isLittleOTVS]

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
/-- The Schnirelmann density of a set not containing `1` is `0`. -/
lemma schnirelmannDensity_eq_zero_of_one_not_mem (h : 1 ∉ A) : schnirelmannDensity A = 0 :=
  ((schnirelmannDensity_le_of_not_mem h).trans (by simp)).antisymm schnirelmannDensity_nonneg

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
h : 1 ∉ A
⊢ 1 - (↑1)⁻¹ ≤ 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_foldlM
    (f : γ → β → α → m β) (init : β) (xs : Array α) (start stop : Nat) (hmono : monotone f) :
    monotone (fun x => xs.foldlM (f x) init start stop)

Proof state:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → β → α → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x =>
    let fold := fun stop h => Array.foldlM.loop (f x) xs stop h (stop - start) start init;
    if h : stop ≤ xs.size then fold stop h else fold xs.size ⋯

Tactic:
split <;> apply monotone_foldlM_loop (hmono := hmono)

Result:
no goals

Proof state:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → β → α → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x => Array.foldlM (f x) init xs start stop

Tactic:
unfold Array.foldlM

Result:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → β → α → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x =>
    let fold := fun stop h => Array.foldlM.loop (f x) xs stop h (stop - start) start init;
    if h : stop ≤ xs.size then fold stop h else fold xs.size ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Basic.lean
theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
    a.toArray[i] = a[i]'(by simpa using h) := rfl

Proof state:
α : Type u
a : List α
i : Nat
h : i < a.toArray.size
⊢ i < a.length

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem rel_iSup_prod [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop)
    (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s : γ → α) (t : Finset γ) :
    R (m (⨆ d ∈ t, s d)) (∏ d ∈ t, m (s d))

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
γ : Type u_5
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : γ → α
t : Finset γ
⊢ R (m (⨆ x, s ↑x)) (∏' (x : { x // x ∈ t }), m (s ↑x))

Tactic:
exact rel_iSup_tprod m m0 R m_iSup _

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
γ : Type u_5
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : γ → α
t : Finset γ
⊢ R (m (⨆ d ∈ t, s d)) (∏ d ∈ t, m (s d))

Tactic:
rw [iSup_subtype', ← Finset.tprod_subtype]

Result:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
γ : Type u_5
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : γ → α
t : Finset γ
⊢ R (m (⨆ x, s ↑x)) (∏' (x : { x // x ∈ t }), m (s ↑x))
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem snd_integral [CompleteSpace E] {f : X → E × F} (hf : Integrable f μ) :
    (∫ x, f x ∂μ).2 = ∫ x, (f x).2 ∂μ

Proof state:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : X → E × F
hf : Integrable f μ
⊢ (∫ (x : X), (f x).swap ∂μ).1 = ∫ (x : X), (f x).2 ∂μ

Tactic:
exact fst_integral <| hf.snd.prod_mk hf.fst

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : X → E × F
hf : Integrable f μ
⊢ (∫ (x : X), f x ∂μ).2 = ∫ (x : X), (f x).2 ∂μ

Tactic:
rw [← Prod.fst_swap, swap_integral]

Result:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : X → E × F
hf : Integrable f μ
⊢ (∫ (x : X), (f x).swap ∂μ).1 = ∫ (x : X), (f x).2 ∂μ
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_self (a : α) : Icc a a = {a}

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Icc a a = {a}

Tactic:
rw [← coe_eq_singleton, coe_Icc, Set.Icc_self]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean
theorem riemannZeta_two : riemannZeta 2 = (π : ℂ) ^ 2 / 6

Proof state:
⊢ riemannZeta 2 = ↑π ^ 2 / 6

Tactic:
convert congr_arg ((↑) : ℝ → ℂ) hasSum_zeta_two.tsum_eq

Result:
case h.e'_2

⊢ riemannZeta 2 = ↑(∑' (b : ℕ), 1 / ↑b ^ 2)

case h.e'_3

⊢ ↑π ^ 2 / 6 = ↑(π ^ 2 / 6)

Proof state:
case h.e'_3

⊢ ↑π ^ 2 / 6 = ↑(π ^ 2 / 6)

Tactic:
norm_cast

Result:
no goals

Proof state:
case h.e'_2

⊢ riemannZeta 2 = ↑(∑' (b : ℕ), 1 / ↑b ^ 2)

Tactic:
rw [← Nat.cast_two, zeta_nat_eq_tsum_of_gt_one one_lt_two]

Result:
case h.e'_2

⊢ ∑' (n : ℕ), 1 / ↑n ^ 2 = ↑(∑' (b : ℕ), 1 / ↑b ^ 2)

Proof state:
case h.e'_2

⊢ ∑' (n : ℕ), 1 / ↑n ^ 2 = ↑(∑' (b : ℕ), 1 / ↑b ^ 2)

Tactic:
simp [push_cast]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem add (h₁ : a ≡ b [MOD n]) (h₂ : c ≡ d [MOD n]) : a + c ≡ b + d [MOD n]

Proof state:
n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ ↑n ∣ ↑b - ↑a + (↑d - ↑c)

Tactic:
exact Int.dvd_add h₁.dvd h₂.dvd

Result:
no goals

Proof state:
n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ a + c ≡ b + d [MOD n]

Tactic:
rw [modEq_iff_dvd, Int.ofNat_add, Int.ofNat_add, add_sub_add_comm]

Result:
n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ ↑n ∣ ↑b - ↑a + (↑d - ↑c)
-- Mathlib/Data/Matroid/Closure.lean
theorem isBase_iff_minimal_spanning : M.IsBase B ↔ Minimal M.Spanning B

Proof state:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ Minimal M.Spanning B

Tactic:
rw [minimal_subset_iff]

Result:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t

Proof state:
α : Type u_2
M : Matroid α
B : Set α
x✝ : M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
h : M.Spanning B
h' : ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
⊢ M.IsBase B

Tactic:
obtain ⟨B', hB', hBB'⟩ := h.exists_isBase_subset

Result:
case intro.intro
α : Type u_2
M : Matroid α
B : Set α
x✝ : M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
h : M.Spanning B
h' : ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
B' : Set α
hB' : M.IsBase B'
hBB' : B' ⊆ B
⊢ M.IsBase B

Proof state:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t

Tactic:
refine ⟨fun h ↦ ⟨h.spanning, fun _ ↦ h.eq_of_superset_spanning⟩, fun ⟨h, h'⟩ ↦ ?_⟩

Result:
α : Type u_2
M : Matroid α
B : Set α
x✝ : M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
h : M.Spanning B
h' : ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
⊢ M.IsBase B

Proof state:
case intro.intro
α : Type u_2
M : Matroid α
B : Set α
x✝ : M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
h : M.Spanning B
h' : ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
B' : Set α
hB' : M.IsBase B'
hBB' : B' ⊆ B
⊢ M.IsBase B

Tactic:
rwa [h' hB'.spanning hBB']

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
theorem lift_π (j : J) : lift f fs w ≫ π arrows j = fs _

Proof state:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
j : J
⊢ lift f fs w ≫ π arrows j = fs j

Tactic:
simp only [limit.lift_π, WidePullbackShape.mkCone_pt, WidePullbackShape.mkCone_π_app]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_submatrix_sum_swap_right (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α)
    (D : Matrix o m α) (f : p → n ⊕ o) :
    (fromBlocks A B C D).submatrix f Sum.swap = (fromBlocks B A D C).submatrix f id

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
j : m ⊕ l
⊢ (fromBlocks A B C D).submatrix f Sum.swap i j = (fromBlocks B A D C).submatrix f id i j

Tactic:
cases j <;> dsimp <;> cases f i <;> rfl

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
⊢ (fromBlocks A B C D).submatrix f Sum.swap = (fromBlocks B A D C).submatrix f id

Tactic:
ext i j

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
j : m ⊕ l
⊢ (fromBlocks A B C D).submatrix f Sum.swap i j = (fromBlocks B A D C).submatrix f id i j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_append (l₁ l₂) : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
toList✝¹ toList✝ : List α
⊢ countP p ({ toList := toList✝¹ } ++ { toList := toList✝ }) =
    countP p { toList := toList✝¹ } + countP p { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : Array α
⊢ countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
p : α → Bool
l₂ : Array α
toList✝ : List α
⊢ countP p ({ toList := toList✝ } ++ l₂) = countP p { toList := toList✝ } + countP p l₂

Proof state:
case mk
α : Type u_1
p : α → Bool
l₂ : Array α
toList✝ : List α
⊢ countP p ({ toList := toList✝ } ++ l₂) = countP p { toList := toList✝ } + countP p l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
p : α → Bool
toList✝¹ toList✝ : List α
⊢ countP p ({ toList := toList✝¹ } ++ { toList := toList✝ }) =
    countP p { toList := toList✝¹ } + countP p { toList := toList✝ }
-- Mathlib/Probability/IdentDistrib.lean
theorem memLp_snd [NormedAddCommGroup γ] [BorelSpace γ] {p : ℝ≥0∞} (h : IdentDistrib f g μ ν)
    (hf : MemLp f p μ) : MemLp g p ν

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g μ ν
hf : MemLp f p μ
⊢ MemLp g p ν

Tactic:
refine ⟨h.aestronglyMeasurable_snd hf.aestronglyMeasurable, ?_⟩

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g μ ν
hf : MemLp f p μ
⊢ eLpNorm g p ν < ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g μ ν
hf : MemLp f p μ
⊢ eLpNorm g p ν < ⊤

Tactic:
rw [← h.eLpNorm_eq]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g μ ν
hf : MemLp f p μ
⊢ eLpNorm f p μ < ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g μ ν
hf : MemLp f p μ
⊢ eLpNorm f p μ < ⊤

Tactic:
exact hf.2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_toNat_mod_cancel {x : BitVec w} (h : ¬ x = 0#w) :
    (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat

Proof state:
w : Nat
x : BitVec w
h : ¬x = 0#w
⊢ (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat

Tactic:
simp only [toNat_eq, toNat_ofNat, Nat.zero_mod] at h

Result:
w : Nat
x : BitVec w
h : ¬x.toNat = 0
⊢ (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat

Proof state:
w : Nat
x : BitVec w
h : ¬x.toNat = 0
⊢ (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat

Tactic:
rw [Nat.mod_eq_of_lt (by omega)]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
h : ¬x.toNat = 0
⊢ 2 ^ w - x.toNat < 2 ^ w

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Lie/OfAssociative.lean
theorem coe_map_toEnd_le :
    (N : Submodule R M).map (LieModule.toEnd R L M x) ≤ N

Proof state:
case intro.intro
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
x : L
m : M
hm : m ∈ ↑↑N
⊢ ((toEnd R L M) x) m ∈ ↑N

Tactic:
exact N.lie_mem hm

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
x : L
⊢ Submodule.map ((toEnd R L M) x) ↑N ≤ ↑N

Tactic:
rintro n ⟨m, hm, rfl⟩

Result:
case intro.intro
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
x : L
m : M
hm : m ∈ ↑↑N
⊢ ((toEnd R L M) x) m ∈ ↑N
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem bot_mul : ⊥ * I = ⊥

Proof state:
R : Type u
inst✝ : Semiring R
I : Ideal R
⊢ ⊥ * I = ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem erase_ne (p : R[X]) (n i : ℕ) (h : i ≠ n) : coeff (p.erase n) i = coeff p i

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n i : ℕ
h : i ≠ n
⊢ (erase n p).coeff i = p.coeff i

Tactic:
simp [coeff_erase, h]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_bliminf {s : ℕ → Set α} {p : ℕ → Prop} (h : ∀ n, p n → MeasurableSet (s n)) :
    MeasurableSet <| Filter.bliminf s Filter.atTop p

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (⋃ i, ⋂ j, ⋂ (_ : p j ∧ i ≤ j), s j)

Tactic:
exact .iUnion fun n => .iInter fun m => .iInter fun hm => h m hm.1

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (bliminf s atTop p)

Tactic:
simp only [Filter.bliminf_eq_iSup_biInf_of_nat, iInf_eq_iInter, iSup_eq_iUnion]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (⋃ i, ⋂ j, ⋂ (_ : p j ∧ i ≤ j), s j)
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem threeGPFree_insert_of_lt (hs : ∀ i ∈ s, i < a) :
    ThreeGPFree (insert a s) ↔
      ThreeGPFree s ∧ ∀ ⦃b⦄, b ∈ s → ∀ ⦃c⦄, c ∈ s → a * c = b * b → a = b

Proof state:
α : Type u_2
inst✝ : OrderedCancelCommMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ (ThreeGPFree s ∧
      (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
        ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
    ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b

Tactic:
rw [← and_assoc]

Result:
α : Type u_2
inst✝ : OrderedCancelCommMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ ((ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
      ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
    ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b

Proof state:
α : Type u_2
inst✝ : OrderedCancelCommMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ ((ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
      ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
    ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b

Tactic:
exact and_iff_left fun b hb c hc h => ((mul_lt_mul_of_lt_of_lt (hs _ hb) (hs _ hc)).ne h).elim

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OrderedCancelCommMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ ThreeGPFree (insert a s) ↔ ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b

Tactic:
refine threeGPFree_insert.trans ?_

Result:
α : Type u_2
inst✝ : OrderedCancelCommMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ (ThreeGPFree s ∧
      (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
        ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
    ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem apply_norm_sq_eq_inner_adjoint_left (A : E →L[𝕜] F) (x : E) :
    ‖A x‖ ^ 2 = re ⟪(A† ∘L A) x, x⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪((adjoint A).comp A) x, x⟫_𝕜 = ⟪(adjoint A) (A x), x⟫_𝕜

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ‖A x‖ ^ 2 = re ⟪((adjoint A).comp A) x, x⟫_𝕜

Tactic:
have h : ⟪(A† ∘L A) x, x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_left]; rfl

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
h : ⟪((adjoint A).comp A) x, x⟫_𝕜 = ⟪A x, A x⟫_𝕜
⊢ ‖A x‖ ^ 2 = re ⟪((adjoint A).comp A) x, x⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪((adjoint A).comp A) x, x⟫_𝕜 = ⟪A x, A x⟫_𝕜

Tactic:
rw [← adjoint_inner_left]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪((adjoint A).comp A) x, x⟫_𝕜 = ⟪(adjoint A) (A x), x⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
h : ⟪((adjoint A).comp A) x, x⟫_𝕜 = ⟪A x, A x⟫_𝕜
⊢ ‖A x‖ ^ 2 = re ⟪((adjoint A).comp A) x, x⟫_𝕜

Tactic:
rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeriesHasSum.neg {f : ℕ → ℂ} {s a : ℂ} (hf : LSeriesHasSum f s a) :
    LSeriesHasSum (-f) s (-a)

Proof state:
f : ℕ → ℂ
s a : ℂ
hf : LSeriesHasSum f s a
⊢ LSeriesHasSum (-f) s (-a)

Tactic:
simpa [LSeriesHasSum, term_neg] using HasSum.neg hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem ne_of_not_mem_push {a b : α} {l : Vector α n} (h : a ∉ l.push b) : a ≠ b

Proof state:
α : Type u_1
n : Nat
a b : α
l : Vector α n
h : ¬a ∈ l.push b
⊢ a ≠ b

Tactic:
simp only [mem_push, not_or] at h

Result:
α : Type u_1
n : Nat
a b : α
l : Vector α n
h : ¬a ∈ l ∧ ¬a = b
⊢ a ≠ b

Proof state:
α : Type u_1
n : Nat
a b : α
l : Vector α n
h : ¬a ∈ l ∧ ¬a = b
⊢ a ≠ b

Tactic:
exact h.2

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem right_inv {f : α → β} {g : β → α} (h : Isometry f) (hg : RightInverse g f) : Isometry g :=
  fun x y => by rw [← h, hg _, hg _]

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
g : β → α
h : Isometry f
hg : RightInverse g f
x y : β
⊢ edist (g x) (g y) = edist x y

Tactic:
rw [← h, hg _, hg _]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem insertEntry_nil [BEq α] {k : α} {v : β k} :
    insertEntry k v ([] : List ((a : α) × β a)) = [⟨k, v⟩] :=
  by simp [insertEntry]

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
v : β k
⊢ insertEntry k v [] = [⟨k, v⟩]

Tactic:
simp [insertEntry]

Result:
no goals