harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem derivWithin_of_bilinear
    (hu : DifferentiableWithinAt 𝕜 u s x) (hv : DifferentiableWithinAt 𝕜 v s x) :
    derivWithin (fun y => B (u y) (v y)) s x =
      B (u x) (derivWithin v s x) + B (derivWithin u s x) (v x)

Proof state:
case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
⊢ derivWithin (fun y => (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)

case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)

Proof state:
case inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)

Tactic:
exact (B.hasDerivWithinAt_of_bilinear hu.hasDerivWithinAt hv.hasDerivWithinAt).derivWithin hxs

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
protected lemma lt_iff_le_and_ne : a < b ↔ a ≤ b ∧ a ≠ b

Proof state:
n : ℕ
a b : Fin n
⊢ a < b ↔ a ≤ b ∧ a ≠ b

Tactic:
rw [← val_ne_iff]

Result:
n : ℕ
a b : Fin n
⊢ a < b ↔ a ≤ b ∧ ↑a ≠ ↑b

Proof state:
n : ℕ
a b : Fin n
⊢ a < b ↔ a ≤ b ∧ ↑a ≠ ↑b

Tactic:
exact Nat.lt_iff_le_and_ne

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem iff (hk : 0 < k) :
    IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ l : ℕ, 0 < l → l < k → ζ ^ l ≠ 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < k
⊢ ζ ^ l ≠ 1

Tactic:
rw [h.eq_orderOf] at hl

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < orderOf ζ
⊢ ζ ^ l ≠ 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
⊢ IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1

Tactic:
refine ⟨fun h ↦ ⟨h.pow_eq_one, fun l hl' hl ↦ ?_⟩,
  fun ⟨hζ, hl⟩ ↦ IsPrimitiveRoot.mk_of_lt ζ hk hζ hl⟩

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < k
⊢ ζ ^ l ≠ 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < orderOf ζ
⊢ ζ ^ l ≠ 1

Tactic:
exact pow_ne_one_of_lt_orderOf hl'.ne' hl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem derivBFamily_lt_ord {o : Ordinal} {f : ∀ a < o, Ordinal → Ordinal} {c} (hc : IsRegular c)
    (hι : o.card < c) (hc' : c ≠ ℵ₀) (hf : ∀ (i hi), ∀ b < c.ord, f i hi b < c.ord) {a} :
    a < c.ord → derivBFamily.{u, u} o f a < c.ord :=
  derivBFamily_lt_ord_lift hc (by rwa [lift_id]) hc' hf

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : o.card < c
hc' : c ≠ ℵ₀
hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord
a : Ordinal.{u}
⊢ lift.{u, u} o.card < c

Tactic:
rwa [lift_id]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem dist_eq_zero_iff_eq_or_not_reachable :
    G.dist u v = 0 ↔ u = v ∨ ¬G.Reachable u v

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v = 0 ↔ u = v ∨ ¬G.Reachable u v

Tactic:
simp [dist_eq_sInf, Nat.sInf_eq_zero, Reachable]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
@[simp]
lemma conjTranspose_swap {R : Type*} [Semiring R] [StarRing R] (i j : n) :
    (swap R i j).conjTranspose = swap R i j

Proof state:
n : Type u_2
inst✝² : DecidableEq n
R : Type u_3
inst✝¹ : Semiring R
inst✝ : StarRing R
i j : n
⊢ (swap R i j)ᴴ = swap R i j

Tactic:
simp [swap]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem dite_apply (f : P → ∀ a, σ a) (g : ¬P → ∀ a, σ a) (a : α) :
    (dite P f g) a = dite P (fun h ↦ f h a) fun h ↦ g h a

Proof state:
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst✝ : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
⊢ dite P f g a = if h : P then f h a else g h a

Tactic:
by_cases h : P <;> simp [h]

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem nhds_top : 𝓝 (⊤ : EReal) = ⨅ (a) (_ : a ≠ ⊤), 𝓟 (Ioi a) :=
  nhds_top_order.trans <| by simp only [lt_top_iff_ne_top]

Proof state:
⊢ ⨅ l, ⨅ (_ : l < ⊤), 𝓟 (Ioi l) = ⨅ a, ⨅ (_ : a ≠ ⊤), 𝓟 (Ioi a)

Tactic:
simp only [lt_top_iff_ne_top]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem smul_apply_eq_smul_apply_inv_smul (f : F) (S : H.LeftTransversal) (q : G ⧸ H) :
    ((f • S).2.leftQuotientEquiv q : G) = f • (S.2.leftQuotientEquiv (f⁻¹ • q) : G)

Proof state:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
S : H.LeftTransversal
q : G ⧸ H
⊢ ↑(⋯.leftQuotientEquiv q) = f • ↑(⋯.leftQuotientEquiv (f⁻¹ • q))

Tactic:
rw [smul_leftQuotientEquiv, smul_inv_smul]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem mul_one (a : R) : a * (nat_lit 1).rawCast = a

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a * Nat.rawCast 1 = a

Tactic:
simp [Nat.rawCast]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma genWeightSpace_add_chainTop :
    genWeightSpace M (α + chainTop α β : L → R) = ⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ genWeightSpace M (α + ⇑(chainTop α β)) = ⊥

Tactic:
rw [coe_chainTop', ← add_assoc, ← succ_nsmul',
  genWeightSpace_chainTopCoeff_add_one_nsmul_add _ _ hα]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma infClosure_empty : infClosure (∅ : Set α) = ∅

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
⊢ infClosure ∅ = ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Equiv/Fin.lean
theorem finAddFlip_apply_castAdd (k : Fin m) (n : ℕ) :
    finAddFlip (Fin.castAdd n k) = Fin.natAdd n k

Proof state:
m : ℕ
k : Fin m
n : ℕ
⊢ finAddFlip (Fin.castAdd n k) = Fin.natAdd n k

Tactic:
simp [finAddFlip]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem segment_eq_image' (x y : E) :
    [x -[𝕜] y] = (fun θ : 𝕜 => x + θ • (y - x)) '' Icc (0 : 𝕜) 1

Proof state:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y

Tactic:
abel

Result:
no goals

Proof state:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + a✝¹ • (y - x) = (1 - a✝¹) • x + a✝¹ • y

Tactic:
simp only [smul_sub, sub_smul, one_smul]

Result:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
⊢ [x-[𝕜]y] = (fun θ => x + θ • (y - x)) '' Icc 0 1

Tactic:
convert segment_eq_image 𝕜 x y using 2

Result:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + a✝¹ • (y - x) = (1 - a✝¹) • x + a✝¹ • y
-- Mathlib/Analysis/Normed/Group/Int.lean
theorem abs_le_floor_nnreal_iff (z : ℤ) (c : ℝ≥0) : |z| ≤ ⌊c⌋₊ ↔ ‖z‖₊ ≤ c

Proof state:
z : ℤ
c : ℝ≥0
⊢ |z| ≤ ↑⌊c⌋₊ ↔ ‖z‖₊ ≤ c

Tactic:
rw [Int.abs_eq_natAbs, Int.ofNat_le, Nat.le_floor_iff (zero_le c), NNReal.natCast_natAbs z]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Basic.lean
theorem size_toArray (as : List α) : as.toArray.size = as.length

Proof state:
α : Type u
as : List α
⊢ as.toArray.size = as.length

Tactic:
simp [size]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_map_map (f : E →ₐ[F] L) :
    relfinrank (A.map f) (B.map f) = relfinrank A B

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : Type w
inst✝¹ : Field L
inst✝ : Algebra F L
A B : IntermediateField F E
f : E →ₐ[F] L
⊢ (map f A).relfinrank (map f B) = A.relfinrank B

Tactic:
simpa using congr(toNat $(lift_relrank_map_map A B f))

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigO.exists_mem_basis {ι} {p : ι → Prop} {s : ι → Set α} (h : f =O[l] g')
    (hb : l.HasBasis p s) :
    ∃ c > 0, ∃ i : ι, p i ∧ ∀ x ∈ s i, ‖f x‖ ≤ c * ‖g' x‖ :=
  flip Exists.imp h.exists_pos fun c h => by
    simpa only [isBigOWith_iff, hb.eventually_iff, exists_prop] using h

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
ι : Sort u_17
p : ι → Prop
s : ι → Set α
h✝ : f =O[l] g'
hb : l.HasBasis p s
c : ℝ
h : c > 0 ∧ IsBigOWith c l f g'
⊢ c > 0 ∧ ∃ i, p i ∧ ∀ x ∈ s i, ‖f x‖ ≤ c * ‖g' x‖

Tactic:
simpa only [isBigOWith_iff, hb.eventually_iff, exists_prop] using h

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_X_pow [DecidableEq σ] (m : σ →₀ ℕ) (s : σ) (n : ℕ) :
    coeff R m ((X s : MvPowerSeries σ R) ^ n) = if m = single s n then 1 else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
n : ℕ
⊢ (coeff R m) (X s ^ n) = if m = single s n then 1 else 0

Tactic:
rw [X_pow_eq s n, coeff_monomial]

Result:
no goals
-- Mathlib/Algebra/Ring/Basic.lean
lemma one_div_neg_eq_neg_one_div (a : R) : 1 / -a = -(1 / a) :=
  calc
    1 / -a = 1 / (-1 * a)

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ 1 / -a = 1 / (-1 * a)

Tactic:
rw [neg_eq_neg_one_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ 1 / a * -1 = -(1 / a)

Tactic:
rw [mul_neg, mul_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ 1 / (-1 * a) = 1 / a * (1 / -1)

Tactic:
rw [one_div_mul_one_div_rev]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ 1 / a * (1 / -1) = 1 / a * -1

Tactic:
rw [one_div_neg_one_eq_neg_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem op_fst {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) :
    c.op.fst = c.inl.op

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.op.fst = c.inl.op

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
@[simp, norm_cast]
lemma coe_disjiUnion {h} : (s.disjiUnion t h : Set β) = ⋃ x ∈ (s : Set α), t x

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
h : (↑s).PairwiseDisjoint t
⊢ ↑(s.disjiUnion t h) = ⋃ x ∈ ↑s, ↑(t x)

Tactic:
simp [Set.ext_iff, mem_disjiUnion, Set.mem_iUnion, mem_coe, imp_true_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem LECmp.cmp_iff_ge [LE α] [LECmp (α := α) cmp] : cmp x y ≠ .lt ↔ y ≤ x

Proof state:
α : Type u_1
cmp : α → α → Ordering
x y : α
inst✝¹ : LE α
inst✝ : LECmp cmp
⊢ cmp x y ≠ Ordering.lt ↔ y ≤ x

Tactic:
rw [← OrientedCmp.cmp_ne_gt, LECmp.cmp_iff_le]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem mem_closedBall_comm : x ∈ closedBall y ε ↔ y ∈ closedBall x ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ x ∈ closedBall y ε ↔ y ∈ closedBall x ε

Tactic:
rw [mem_closedBall', mem_closedBall]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem coe_centralizer_centralizer (s : Set A) :
    (centralizer R (centralizer R s : Set A)) = (s ∪ star s).centralizer.centralizer

Proof state:
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalSemiring A
inst✝³ : StarRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
⊢ ↑(centralizer R ↑(centralizer R s)) = (s ∪ star s).centralizer.centralizer

Tactic:
rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_ushiftRight (x : BitVec n) (i j : Nat) :
    getLsbD (x >>> i) j = getLsbD x (i+j)

Proof state:
n : Nat
x : BitVec n
i j : Nat
⊢ (x >>> i).toNat.testBit j = x.toNat.testBit (i + j)

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
x : BitVec n
i j : Nat
⊢ (x >>> i).getLsbD j = x.getLsbD (i + j)

Tactic:
unfold getLsbD

Result:
n : Nat
x : BitVec n
i j : Nat
⊢ (x >>> i).toNat.testBit j = x.toNat.testBit (i + j)
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem IsLittleO.rpow (hr : 0 < r) (hg : 0 ≤ᶠ[l] g) (h : f =o[l] g) :
    (fun x => f x ^ r) =o[l] fun x => g x ^ r

Proof state:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
⊢ (fun x => f x ^ r) =o[l] fun x => g x ^ r

Tactic:
refine .of_isBigOWith fun c hc ↦ ?_

Result:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ IsBigOWith c l (fun x => f x ^ r) fun x => g x ^ r

Proof state:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ IsBigOWith c l (fun x => f x ^ r) fun x => g x ^ r

Tactic:
rw [← rpow_inv_rpow hc.le hr.ne']

Result:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ IsBigOWith ((c ^ r⁻¹) ^ r) l (fun x => f x ^ r) fun x => g x ^ r

Proof state:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ IsBigOWith ((c ^ r⁻¹) ^ r) l (fun x => f x ^ r) fun x => g x ^ r

Tactic:
refine (h.forall_isBigOWith ?_).rpow ?_ ?_ hg <;> positivity

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_add_expect_comm (f₁ f₂ g₁ g₂ : ι → M) :
    𝔼 i ∈ s, (f₁ i + f₂ i) + 𝔼 i ∈ s, (g₁ i + g₂ i) =
      𝔼 i ∈ s, (f₁ i + g₁ i) + 𝔼 i ∈ s, (f₂ i + g₂ i)

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f₁ f₂ g₁ g₂ : ι → M
⊢ 𝔼 i ∈ s, (f₁ i + f₂ i) + 𝔼 i ∈ s, (g₁ i + g₂ i) = 𝔼 i ∈ s, (f₁ i + g₁ i) + 𝔼 i ∈ s, (f₂ i + g₂ i)

Tactic:
simp_rw [expect_add_distrib, add_add_add_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Pointwise.lean
theorem MeasurableSet.const_smul₀ {G₀ α : Type*} [GroupWithZero G₀] [Zero α]
    [MulActionWithZero G₀ α] [MeasurableSpace G₀] [MeasurableSpace α] [MeasurableSMul G₀ α]
    [MeasurableSingletonClass α] {s : Set α} (hs : MeasurableSet s) (a : G₀) :
    MeasurableSet (a • s)

Proof state:
case inl
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (0 • s)

case inr
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (a • s)

Tactic:
exacts [(subsingleton_zero_smul_set s).measurableSet, hs.const_smul_of_ne_zero ha]

Result:
no goals

Proof state:
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
⊢ MeasurableSet (a • s)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case inl
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (0 • s)

case inr
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (a • s)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_keys_eq_length (l : List ((a : α) × β a)) : (keys l).length = l.length

Proof state:
α : Type u
β : α → Type v
l : List ((a : α) × β a)
⊢ (keys l).length = l.length

Tactic:
induction l using assoc_induction <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
    l.toArray.foldlM f init = l.foldlM f init

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
init : β
l : List α
⊢ foldlM f init l.toArray = List.foldlM f init l

Tactic:
rw [foldlM_toList]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem cthickening_of_nonpos {δ : ℝ} (hδ : δ ≤ 0) (E : Set α) : cthickening δ E = closure E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
hδ : δ ≤ 0
E : Set α
⊢ cthickening δ E = closure E

Tactic:
ext x

Result:
case h
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
hδ : δ ≤ 0
E : Set α
x : α
⊢ x ∈ cthickening δ E ↔ x ∈ closure E

Proof state:
case h
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
hδ : δ ≤ 0
E : Set α
x : α
⊢ x ∈ cthickening δ E ↔ x ∈ closure E

Tactic:
simp [mem_closure_iff_infEdist_zero, cthickening, ENNReal.ofReal_eq_zero.2 hδ]

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
/-- A column partitioned matrix in a Star ring when conjugate transposed gives a row partitioned
matrix with the columns of the initial matrix conjugate transposed to become rows. -/
lemma conjTranspose_fromCols_eq_fromRows_conjTranspose (A₁ : Matrix m n₁ R)
    (A₂ : Matrix m n₂ R) :
    conjTranspose (fromCols A₁ A₂) = fromRows (conjTranspose A₁) (conjTranspose A₂)

Proof state:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
⊢ (A₁.fromCols A₂)ᴴ = A₁ᴴ.fromRows A₂ᴴ

Tactic:
ext (_ | _) _ <;> simp

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem dropFun_toSubtype {α} (p : α ⟹ «repeat» (n + 1) Prop) :
    dropFun (toSubtype p) = toSubtype _

Proof state:
case a.h
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
i : Fin2 n
x✝ : drop (fun i => { x // ofRepeat (p i x) }) i
⊢ dropFun (toSubtype p) i x✝ = toSubtype (fun i => p i.fs) i x✝

Tactic:
induction i <;> simp [dropFun, *] <;> rfl

Result:
no goals

Proof state:
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
⊢ dropFun (toSubtype p) = toSubtype fun i => p i.fs

Tactic:
ext i

Result:
case a.h
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
i : Fin2 n
x✝ : drop (fun i => { x // ofRepeat (p i x) }) i
⊢ dropFun (toSubtype p) i x✝ = toSubtype (fun i => p i.fs) i x✝
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma partialSups_mem {ι : Type*} [Preorder ι] [LocallyFiniteOrderBot ι]
    (hC : IsSetRing C) {s : ι → Set α} (hs : ∀ n, s n ∈ C) (n : ι) :
    partialSups s n ∈ C

Proof state:
α : Type u_1
C : Set (Set α)
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
hC : IsSetRing C
s : ι → Set α
hs : ∀ (n : ι), s n ∈ C
n : ι
⊢ (partialSups s) n ∈ C

Tactic:
simpa only [partialSups_apply, sup'_eq_sup] using hC.finsetSup_mem (fun i hi ↦ hs i)

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Defs.lean
theorem mod_zero (a : R) : a % 0 = a

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a : R
⊢ a % 0 = a

Tactic:
simpa only [zero_mul, zero_add] using div_add_mod a 0

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst)
    {h'} :
    (ofList l).getKey k' h' = k

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
h' : k' ∈ ofList l
⊢ (ofList l).getKey k' h' = k

Tactic:
simp_to_raw using Raw₀.getKey_insertMany_empty_list_of_mem

Result:
no goals