harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/Derivation/Basic.lean
theorem iterate_apply_lie' (D : LieDerivation R L L) (n : ℕ) (a b : L) :
    D^[n] ⁅a, b⁆ = ∑ i ∈ range (n + 1), n.choose i • ⁅D^[i] a, D^[n - i] b⁆

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
n : ℕ
a b : L
⊢ (⇑D)^[n] ⁅a, b⁆ = ∑ i ∈ range (n + 1), n.choose i • ⁅(⇑D)^[i] a, (⇑D)^[n - i] b⁆

Tactic:
rw [iterate_apply_lie D n a b]

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
n : ℕ
a b : L
⊢ ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆ =
    ∑ i ∈ range (n + 1), n.choose i • ⁅(⇑D)^[i] a, (⇑D)^[n - i] b⁆

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
n : ℕ
a b : L
⊢ ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆ =
    ∑ i ∈ range (n + 1), n.choose i • ⁅(⇑D)^[i] a, (⇑D)^[n - i] b⁆

Tactic:
exact sum_antidiagonal_eq_sum_range_succ (fun i j ↦ n.choose i • ⁅D^[i] a, D^[j] b⁆) n

Result:
no goals
-- Mathlib/Computability/Language.lean
theorem one_add_kstar_mul_self_eq_kstar (l : Language α) : 1 + l∗ * l = l∗

Proof state:
α : Type u_1
l : Language α
⊢ 1 + l∗ * l = l∗

Tactic:
rw [mul_self_kstar_comm, one_add_self_mul_kstar_eq_kstar]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem binomial_eq_binomial {k l m n : ℕ} {u v : R} (hu : u ≠ 0) (hv : v ≠ 0) :
    C u * X ^ k + C v * X ^ l = C u * X ^ m + C v * X ^ n ↔
      k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

Proof state:
R : Type u
inst✝ : Semiring R
k l m n : ℕ
u v : R
hu : u ≠ 0
hv : v ≠ 0
⊢ Finsupp.single k u + Finsupp.single l v = Finsupp.single m u + Finsupp.single n v ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

Tactic:
exact Finsupp.single_add_single_eq_single_add_single hu hv

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
k l m n : ℕ
u v : R
hu : u ≠ 0
hv : v ≠ 0
⊢ C u * X ^ k + C v * X ^ l = C u * X ^ m + C v * X ^ n ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

Tactic:
simp_rw [C_mul_X_pow_eq_monomial, ← toFinsupp_inj, toFinsupp_add, toFinsupp_monomial]

Result:
R : Type u
inst✝ : Semiring R
k l m n : ℕ
u v : R
hu : u ≠ 0
hv : v ≠ 0
⊢ Finsupp.single k u + Finsupp.single l v = Finsupp.single m u + Finsupp.single n v ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
-- Mathlib/Data/Set/Finite/Lemmas.lean
theorem Finite.induction_to_univ [Finite α] {C : Set α → Prop} (S0 : Set α)
    (H0 : C S0) (H1 : ∀ S ≠ univ, C S → ∃ a ∉ S, C (insert a S)) : C univ :=
  finite_univ.induction_to S0 (subset_univ S0) H0 (by simpa [ssubset_univ_iff])

Proof state:
α : Type u
inst✝ : Finite α
C : Set α → Prop
S0 : Set α
H0 : C S0
H1 : ∀ (S : Set α), S ≠ univ → C S → ∃ a ∉ S, C (insert a S)
⊢ ∀ s ⊂ univ, C s → ∃ a ∈ univ \ s, C (insert a s)

Tactic:
simpa [ssubset_univ_iff]

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem isEmbedding_coe_ennreal : IsEmbedding ((↑) : ℝ≥0∞ → EReal) :=
  coe_ennreal_strictMono.isEmbedding_of_ordConnected <| by
    rw [range_coe_ennreal]; exact ordConnected_Ici

Proof state:
⊢ (range ENNReal.toEReal).OrdConnected

Tactic:
rw [range_coe_ennreal]

Result:
⊢ (Ici 0).OrdConnected

Proof state:
⊢ (Ici 0).OrdConnected

Tactic:
exact ordConnected_Ici

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_compl_eq_mk_compl_finite {α β : Type u} [Finite α] {s : Set α} {t : Set β}
    (h1 : #α = #β) (h : #s = #t) : #(sᶜ : Set α) = #(tᶜ : Set β)

Proof state:
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ #↑sᶜ = #↑tᶜ

Tactic:
rw [← lift_inj.{u, u}]

Result:
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ lift.{u, u} #↑sᶜ = lift.{u, u} #↑tᶜ

Proof state:
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ lift.{u, u} #↑sᶜ = lift.{u, u} #↑tᶜ

Tactic:
apply mk_compl_eq_mk_compl_finite_lift.{u, u, u}
<;> rwa [lift_inj]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@[reassoc]
lemma naturality_φ₂ (f : S₁ ⟶ S₂) : S₁.φ₂ ≫ f.f₂.τ₂ = functorP.map f ≫ S₂.φ₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ (pullback.fst S₁.L₁.g S₁.v₀₁.τ₃ ≫ S₁.v₁₂.τ₂) ≫ f.f₂.τ₂ =
    pullback.map S₁.L₁.g S₁.v₀₁.τ₃ S₂.L₁.g S₂.v₀₁.τ₃ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ ⋯ ⋯ ≫
      pullback.fst S₂.L₁.g S₂.v₀₁.τ₃ ≫ S₂.v₁₂.τ₂

Tactic:
simp only [assoc, pullback.lift_fst_assoc, ← comp_τ₂, f.comm₁₂]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ S₁.φ₂ ≫ f.f₂.τ₂ = functorP.map f ≫ S₂.φ₂

Tactic:
dsimp [φ₂]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ (pullback.fst S₁.L₁.g S₁.v₀₁.τ₃ ≫ S₁.v₁₂.τ₂) ≫ f.f₂.τ₂ =
    pullback.map S₁.L₁.g S₁.v₀₁.τ₃ S₂.L₁.g S₂.v₀₁.τ₃ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ ⋯ ⋯ ≫
      pullback.fst S₂.L₁.g S₂.v₀₁.τ₃ ≫ S₂.v₁₂.τ₂
-- Mathlib/Data/Finset/Insert.lean
theorem insert_subset_iff : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Tactic:
simp only [subset_iff, mem_insert, forall_eq, or_imp, forall_and]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal_conjTranspose {α : Type*} [AddMonoid α] [StarAddMonoid α]
    (M : o → Matrix m n α) : (blockDiagonal M)ᴴ = blockDiagonal fun k => (M k)ᴴ

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
inst✝² : DecidableEq o
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : o → Matrix m n α
⊢ (blockDiagonal M)ᴴ = blockDiagonal fun k => (M k)ᴴ

Tactic:
simp only [conjTranspose, blockDiagonal_transpose]

Result:
m : Type u_2
n : Type u_3
o : Type u_4
inst✝² : DecidableEq o
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : o → Matrix m n α
⊢ (blockDiagonal fun k => (M k)ᵀ).map star = blockDiagonal fun k => (M k)ᵀ.map star

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
inst✝² : DecidableEq o
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : o → Matrix m n α
⊢ (blockDiagonal fun k => (M k)ᵀ).map star = blockDiagonal fun k => (M k)ᵀ.map star

Tactic:
rw [blockDiagonal_map _ star (star_zero α)]

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem summable_rpow {p : ℝ} : Summable (fun n => (n : ℝ≥0) ^ p : ℕ → ℝ≥0) ↔ p < -1

Proof state:
p : ℝ
⊢ (Summable fun n => ↑n ^ p) ↔ p < -1

Tactic:
simp [← NNReal.summable_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Perm.lean
theorem perm_toArray (as bs : List α) : as.toArray ~ bs.toArray ↔ as ~ bs

Proof state:
α : Type u_1
as bs : List α
⊢ as.toArray ~ bs.toArray ↔ as ~ bs

Tactic:
simp [perm_iff_toList_perm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_alter [LawfulBEq α] [Inhabited α] {k k' : α} (h : m.1.WF)
    {f : Option (β k) → Option (β k)} (hc : (m.alter k f).contains k') :
    (m.alter k f).getKey k' hc =
      if heq : k == k' then
        k
      else
        haveI h' : m.contains k'

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
h : m.val.WF
f : Option (β k) → Option (β k)
hc : (m.alter k f).contains k' = true
heq : ¬(k == k') = true
⊢ m.contains k' = true

Tactic:
rwa [contains_alter _ h, if_neg heq] at hc

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
h : m.val.WF
f : Option (β k) → Option (β k)
hc : (m.alter k f).contains k' = true
⊢ (m.alter k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯

Tactic:
simp_to_model [alter] using List.getKey_alterKey

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_div (hx : x ≠ 0) (hy : y ≠ 0) : log (x / y) = log x - log y :=
  exp_injective <| by
    rw [exp_log_eq_abs (div_ne_zero hx hy), exp_sub, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_div]

Proof state:
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ rexp (log (x / y)) = rexp (log x - log y)

Tactic:
rw [exp_log_eq_abs (div_ne_zero hx hy), exp_sub, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_div]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma equation_of_Z_eq_zero {P : Fin 3 → R} (hPz : P z = 0) : W'.Equation P ↔ P x ^ 3 = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.Equation P ↔ P x ^ 3 = 0

Tactic:
simp only [equation_iff, hPz, add_zero, zero_sub, mul_zero, zero_pow <| OfNat.ofNat_ne_zero _,
  neg_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma π_homologyIsoSc'_hom :
    K.homologyπ j ≫ (K.homologyIsoSc' i j k hi hk).hom =
      (K.cyclesIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).homologyπ

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ K.homologyπ j ≫ (K.homologyIsoSc' i j k hi hk).hom = (K.cyclesIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).homologyπ

Tactic:
apply ShortComplex.homologyπ_naturality

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_swap_right (a : Vector α n) {i j : Nat} {hi hj} :
    (a.swap i j hi hj)[j]'(by simpa using hj) = a[i]

Proof state:
α : Type ?u.453920
n : Nat
a : Vector α n
i j : Nat
hi : i < n
hj : j < n
⊢ j < n

Tactic:
simpa using hj

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i j : Nat
hi : i < n
hj : j < n
⊢ (a.swap i j hi hj)[j] = a[i]

Tactic:
simp +contextual [getElem_swap]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean
theorem mem_Lp (f : α →ᵇ E) : f.toContinuousMap.toAEEqFun μ ∈ Lp E p μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ᵐ (x : α) ∂μ, ‖↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x‖ ≤ ‖f‖

Tactic:
filter_upwards [f.toContinuousMap.coeFn_toAEEqFun μ] with x _

Result:
case h
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
x : α
a✝ : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = f.toContinuousMap x
⊢ ‖↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x‖ ≤ ‖f‖

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ Lp E p μ

Tactic:
refine Lp.mem_Lp_of_ae_bound ‖f‖ ?_

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ᵐ (x : α) ∂μ, ‖↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x‖ ≤ ‖f‖

Proof state:
case h
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
x : α
a✝ : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = f.toContinuousMap x
⊢ ‖↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x‖ ≤ ‖f‖

Tactic:
convert f.norm_coe_le_norm x using 2

Result:
no goals
-- Mathlib/Algebra/Module/Basic.lean
lemma support_smul_subset_left [Zero R] [Zero M] [SMulWithZero R M] (f : α → R) (g : α → M) :
    support (f • g) ⊆ support f := fun x hfg hf ↦
  hfg <| by rw [Pi.smul_apply', hf, zero_smul]

Proof state:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
g : α → M
x : α
hfg : x ∈ support (f • g)
hf : f x = 0
⊢ (f • g) x = 0

Tactic:
rw [Pi.smul_apply', hf, zero_smul]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem down_neg : down < 0

Proof state:
⊢ down ≤ 0 ∧ ∃ j, ∀ (i : (down.moveRight j).LeftMoves), (down.moveRight j).moveLeft i ⧏ 0

Tactic:
simp [le_zero_lf, star_lf_zero]

Result:
no goals

Proof state:
⊢ down < 0

Tactic:
rw [lt_iff_le_and_lf, lf_zero]

Result:
⊢ down ≤ 0 ∧ ∃ j, ∀ (i : (down.moveRight j).LeftMoves), (down.moveRight j).moveLeft i ⧏ 0
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem memLp_of_bounded [IsFiniteMeasure μ]
    {a b : ℝ} {f : α → ℝ} (h : ∀ᵐ x ∂μ, f x ∈ Set.Icc a b)
    (hX : AEStronglyMeasurable f μ) (p : ENNReal) : MemLp f p μ :=
  have ha : ∀ᵐ x ∂μ, a ≤ f x := h.mono fun ω h => h.1
  have hb : ∀ᵐ x ∂μ, f x ≤ b := h.mono fun ω h => h.2
  (memLp_const (max |a| |b|)).mono' hX (by filter_upwards [ha, hb] with x using abs_le_max_abs_abs)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
a b : ℝ
f : α → ℝ
h : ∀ᵐ (x : α) ∂μ, f x ∈ Set.Icc a b
hX : AEStronglyMeasurable f μ
p : ℝ≥0∞
ha : ∀ᵐ (x : α) ∂μ, a ≤ f x
hb : ∀ᵐ (x : α) ∂μ, f x ≤ b
⊢ ∀ᵐ (a_1 : α) ∂μ, ‖f a_1‖ ≤ |a| ⊔ |b|

Tactic:
filter_upwards [ha, hb] with x using abs_le_max_abs_abs

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem eps_pos {ε : ℝ} {n : ℕ} (h : 100 ≤ (4 : ℝ) ^ n * ε ^ 5) : 0 < ε :=
  (Odd.pow_pos_iff (by decide)).mp
    (pos_of_mul_pos_right ((show 0 < (100 : ℝ) by norm_num).trans_le h) (by positivity))

Proof state:
ε : ℝ
n : ℕ
h : 100 ≤ 4 ^ n * ε ^ 5
⊢ 0 < 100

Tactic:
norm_num

Result:
no goals

Proof state:
ε : ℝ
n : ℕ
h : 100 ≤ 4 ^ n * ε ^ 5
⊢ Odd 5

Tactic:
decide

Result:
no goals

Proof state:
ε : ℝ
n : ℕ
h : 100 ≤ 4 ^ n * ε ^ 5
⊢ 0 ≤ 4 ^ n

Tactic:
positivity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_flatMap (l : Vector α n) (f : α → Vector β m) (i : Nat) (hi : i < n * m) :
    (l.flatMap f)[i] =
      haveI : i / m < n

Proof state:
α : Type u_1
n : Nat
β : Type u_2
m : Nat
l : Vector α n
f : α → Vector β m
i : Nat
hi : i < n * m
⊢ (l.flatMap f)[i] = (f l[i / m])[i % m]

Tactic:
rw [flatMap_def, getElem_flatten, getElem_map]

Result:
no goals

Proof state:
α : Type ?u.321934
n : Nat
β : Type ?u.321939
m : Nat
l : Vector α n
f : α → Vector β m
i : Nat
hi : i < n * m
⊢ i / m < n

Tactic:
rwa [Nat.div_lt_iff_lt_mul (Nat.pos_of_lt_mul_left hi)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_eq_toNat {x : BitVec w}:
    x.msb = decide (x.toNat ≥ 2 ^ (w - 1))

Proof state:
w : Nat
x : BitVec w
⊢ x.msb = decide (x.toNat ≥ 2 ^ (w - 1))

Tactic:
simp only [msb_eq_decide, ge_iff_le]

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem inr_mul_inl [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] (r : R) (m : M) :
    (inr m * inl r : tsze R M) = inr (m <• r) :=
  ext (zero_mul r) <|
    show (0 : R) •> (0 : M) + m <• r = m <• r by rw [smul_zero, zero_add]

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
r : R
m : M
⊢ 0 •> 0 + m <• r = m <• r

Tactic:
rw [smul_zero, zero_add]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_comap_comap_eq_relrank_inf
    {L : Type v} [Field L] (f : L →+* E) :
    relrank (A.comap f) (B.comap f) = relrank A (B ⊓ f.fieldRange)

Proof state:
E : Type v
inst✝¹ : Field E
A B : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
⊢ (comap f A).relrank (comap f B) = A.relrank (B ⊓ f.fieldRange)

Tactic:
simpa only [lift_id] using lift_relrank_comap_comap_eq_lift_relrank_inf A B f

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem contains_iff (s : String) (c : Char) : contains s c ↔ c ∈ s.1

Proof state:
s : String
c : Char
⊢ s.contains c = true ↔ c ∈ s.data

Tactic:
simp [contains, any_iff]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem mapsTo_emetric_closedBall (x : α) (r' : ℝ≥0∞) :
    MapsTo (f : α → β) (EMetric.closedBall x r') (EMetric.closedBall (f x) (ratio f * r')) :=
  -- Porting note: Added `by exact`
  fun y hy => (edist_eq f y x).trans_le <| mul_le_mul_left' (by exact hy) _

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r' : ℝ≥0∞
y : α
hy : y ∈ EMetric.closedBall x r'
⊢ edist y x ≤ r'

Tactic:
exact hy

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear (B : E →L[𝕜] F →L[𝕜] G) {f : D → E}
    {g : D → F} {N : WithTop ℕ∞} (hf : ContDiff 𝕜 N f) (hg : ContDiff 𝕜 N g) (x : D) {n : ℕ}
    (hn : n ≤ N) :
    ‖iteratedFDeriv 𝕜 n (fun y => B (f y) (g y)) x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1),
      (n.choose i : ℝ) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : WithTop ℕ∞
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : D
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) univ x‖ ≤
    ‖B‖ *
      ∑ x_1 ∈ Finset.range (n + 1),
        ↑(n.choose x_1) * ‖iteratedFDerivWithin 𝕜 x_1 f univ x‖ * ‖iteratedFDerivWithin 𝕜 (n - x_1) g univ x‖

Tactic:
exact B.norm_iteratedFDerivWithin_le_of_bilinear hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ
  (mem_univ x) hn

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : WithTop ℕ∞
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : D
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun y => (B (f y)) (g y)) x‖ ≤
    ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

Tactic:
simp_rw [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : WithTop ℕ∞
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : D
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) univ x‖ ≤
    ‖B‖ *
      ∑ x_1 ∈ Finset.range (n + 1),
        ↑(n.choose x_1) * ‖iteratedFDerivWithin 𝕜 x_1 f univ x‖ * ‖iteratedFDerivWithin 𝕜 (n - x_1) g univ x‖
-- Mathlib/Analysis/Normed/Ring/Seminorm.lean
theorem map_pow_le_pow {F α : Type*} [Ring α] [FunLike F α ℝ] [RingSeminormClass F α ℝ] (f : F)
    (a : α) : ∀ {n : ℕ}, n ≠ 0 → f (a ^ n) ≤ f a ^ n
  | 0, h => absurd rfl h
  | 1, _ => by simp only [pow_one, le_refl]
  | n + 2, _ => by
    simp only [pow_succ _ (n + 1)]
    exact
      le_trans (map_mul_le_mul f _ a)
        (mul_le_mul_of_nonneg_right (map_pow_le_pow _ _ n.succ_ne_zero) (apply_nonneg f a))

Proof state:
F : Type u_2
α : Type u_3
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
a : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ f (a ^ (n + 1) * a) ≤ f a ^ (n + 1) * f a

Tactic:
exact
  le_trans (map_mul_le_mul f _ a)
    (mul_le_mul_of_nonneg_right (map_pow_le_pow _ _ n.succ_ne_zero) (apply_nonneg f a))

Result:
no goals

Proof state:
F : Type u_2
α : Type u_3
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
a : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ f (a ^ (n + 2)) ≤ f a ^ (n + 2)

Tactic:
simp only [pow_succ _ (n + 1)]

Result:
F : Type u_2
α : Type u_3
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
a : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ f (a ^ (n + 1) * a) ≤ f a ^ (n + 1) * f a

Proof state:
F : Type u_2
α : Type u_3
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
a : α
x✝ : 1 ≠ 0
⊢ f (a ^ 1) ≤ f a ^ 1

Tactic:
simp only [pow_one, le_refl]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem normSq_nonneg : 0 ≤ normSq a

Proof state:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ 0 ≤ normSq a

Tactic:
rw [normSq_def']

Result:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2

Proof state:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2

Tactic:
apply_rules [sq_nonneg, add_nonneg]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem map_surjective (hf : Function.Surjective f) : Function.Surjective (map f) := fun p =>
  Polynomial.induction_on' p
    (fun p q hp hq =>
      let ⟨p', hp'⟩ := hp
      let ⟨q', hq'⟩ := hq
      ⟨p' + q', by rw [Polynomial.map_add f, hp', hq']⟩)
    fun n s =>
    let ⟨r, hr⟩ := hf s
    ⟨monomial n r, by rw [map_monomial f, hr]⟩

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
p : S[X]
n : ℕ
s : S
r : R
hr : f r = s
⊢ map f ((monomial n) r) = (monomial n) s

Tactic:
rw [map_monomial f, hr]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
p✝ p q : S[X]
hp : ∃ a, map f a = p
hq : ∃ a, map f a = q
p' : R[X]
hp' : map f p' = p
q' : R[X]
hq' : map f q' = q
⊢ map f (p' + q') = p + q

Tactic:
rw [Polynomial.map_add f, hp', hq']

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem coeff_one_one : coeff (1 : SkewMonoidAlgebra k G) 1 = 1

Proof state:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
inst✝¹ : One G
inst✝ : One k
⊢ coeff 1 1 = 1

Tactic:
simp only [coeff, toFinsupp_single, Finsupp.single_eq_same]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem Filter.Tendsto.piecewise_nhdsWithin {f g : α → β} {t : Set α} [∀ x, Decidable (x ∈ t)]
    {a : α} {s : Set α} {l : Filter β} (h₀ : Tendsto f (𝓝[s ∩ t] a) l)
    (h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l) : Tendsto (piecewise t f g) (𝓝[s] a) l

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f g : α → β
t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto (t.piecewise f g) (𝓝[s] a) l

Tactic:
apply Tendsto.piecewise <;> rwa [← nhdsWithin_inter']

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
lemma integral_eq_const [IsProbabilityMeasure μ] {f : α → E} {c : E} (hf : ∀ᵐ x ∂μ, f x = c) :
    ∫ x, f x ∂μ = c

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → E
c : E
hf : ∀ᵐ (x : α) ∂μ, f x = c
⊢ ∫ (x : α), f x ∂μ = c

Tactic:
simp [integral_congr_ae hf]

Result:
no goals