harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[simp]
lemma negPart_one : (1 : A)⁻ = 0

Proof state:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
⊢ 1⁻ = 0

Tactic:
rw [CFC.negPart_def, cfcₙ_eq_cfc]

Result:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
⊢ cfc (fun x => x⁻) 1 = 0

Proof state:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
⊢ cfc (fun x => x⁻) 1 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem algebraMap_ne_zero {x : K[X]} (hx : x ≠ 0) : algebraMap K[X] (RatFunc K) x ≠ 0

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : K[X]
hx : x ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) x ≠ 0

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem not_infinite_real (r : ℝ) : ¬Infinite r

Proof state:
r : ℝ
⊢ ∃ r_1 s, ↑r_1 < ↑r ∧ ↑r < ↑s

Tactic:
exact ⟨r - 1, r + 1, coe_lt_coe.2 <| sub_one_lt r, coe_lt_coe.2 <| lt_add_one r⟩

Result:
no goals

Proof state:
r : ℝ
⊢ ¬(↑r).Infinite

Tactic:
rw [not_infinite_iff_exist_lt_gt]

Result:
r : ℝ
⊢ ∃ r_1 s, ↑r_1 < ↑r ∧ ↑r < ↑s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_filterMap' (f : α → Option β) (g : γ → β → γ) (l : Array α) (init : γ)
    (w : stop = (l.filterMap f).size) :
    (l.filterMap f).foldl g init 0 stop = l.foldl (fun x y => match f y with | some b => g x b | none => x) init

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
init : γ
toList✝ : List α
⊢ foldl g init (filterMap f { toList := toList✝ }) =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init { toList := toList✝ }

Tactic:
simp [List.foldl_filterMap]

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
init : γ
toList✝ : List α
⊢ List.foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init toList✝ =
    List.foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init toList✝

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
l : Array α
init : γ
⊢ foldl g init (filterMap f l) =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
init : γ
toList✝ : List α
⊢ foldl g init (filterMap f { toList := toList✝ }) =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init { toList := toList✝ }

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
stop : Nat
f : α → Option β
g : γ → β → γ
l : Array α
init : γ
w : stop = (filterMap f l).size
⊢ foldl g init (filterMap f l) 0 stop =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init l

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
l : Array α
init : γ
⊢ foldl g init (filterMap f l) =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init l

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
init : γ
toList✝ : List α
⊢ List.foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init toList✝ =
    List.foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init toList✝

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Mem.lean
theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a < sizeOf as

Proof state:
α : Type u_1
a : α
inst✝ : SizeOf α
as : List α
h : a ∈ { toList := as }
⊢ sizeOf { toList := as }.toList < sizeOf { toList := as }

Tactic:
simp_arith

Result:
no goals

Proof state:
case mk
α : Type u_1
a : α
inst✝ : SizeOf α
as : List α
h : a ∈ { toList := as }
⊢ sizeOf a < sizeOf { toList := as }

Tactic:
exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : SizeOf α
as : Array α
h : a ∈ as
⊢ sizeOf a < sizeOf as

Tactic:
cases as with | _ as =>
exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
theorem disjoint_add_left {s t u : Multiset α} :
    Disjoint (s + t) u ↔ Disjoint s u ∧ Disjoint t u

Proof state:
α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint (s + t) u ↔ _root_.Disjoint s u ∧ _root_.Disjoint t u

Tactic:
simp [disjoint_left, or_imp, forall_and]

Result:
no goals
-- Mathlib/Algebra/Order/Group/DenselyOrdered.lean
@[to_additive]
private lemma exists_lt_mul_left [Group α] [LT α] [DenselyOrdered α]
    [CovariantClass α α (Function.swap (· * ·)) (· < ·)] {a b c : α} (hc : c < a * b) :
    ∃ a' < a, c < a' * b

Proof state:
case intro.intro
α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : CovariantClass α α (Function.swap fun x1 x2 => x1 * x2) fun x1 x2 => x1 < x2
a b c : α
hc : c < a * b
a' : α
hc' : c / b < a'
ha' : a' < a
⊢ ∃ a', a' < a ∧ c < a' * b

Tactic:
exact ⟨a', ha', div_lt_iff_lt_mul.1 hc'⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : CovariantClass α α (Function.swap fun x1 x2 => x1 * x2) fun x1 x2 => x1 < x2
a b c : α
hc : c < a * b
⊢ ∃ a', a' < a ∧ c < a' * b

Tactic:
obtain ⟨a', hc', ha'⟩ := exists_between (div_lt_iff_lt_mul.2 hc)

Result:
case intro.intro
α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : CovariantClass α α (Function.swap fun x1 x2 => x1 * x2) fun x1 x2 => x1 < x2
a b c : α
hc : c < a * b
a' : α
hc' : c / b < a'
ha' : a' < a
⊢ ∃ a', a' < a ∧ c < a' * b
-- Mathlib/Data/Nat/Count.lean
theorem count_le_card (hp : (setOf p).Finite) (n : ℕ) : count p n ≤ #hp.toFinset

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
hp : (setOf p).Finite
n : ℕ
⊢ count p n ≤ #hp.toFinset

Tactic:
rw [count_eq_card_filter_range]

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
hp : (setOf p).Finite
n : ℕ
⊢ #(filter (fun x => p x) (range n)) ≤ #hp.toFinset

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
hp : (setOf p).Finite
n : ℕ
⊢ #(filter (fun x => p x) (range n)) ≤ #hp.toFinset

Tactic:
exact Finset.card_mono fun x hx ↦ hp.mem_toFinset.2 (mem_filter.1 hx).2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem get_eq_getValueCast [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.1)
    {a : α} {h : m.contains a} :
    m.get a h = getValueCast a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
h : m.contains a = true
⊢ m.get a h = getValueCast a (toListModel m.val.buckets) ⋯

Tactic:
rw [get_eq_getₘ, getₘ_eq_getValue hm]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem head_cons (a : α) (s) : head (cons a s) = Computation.pure (some a)

Proof state:
α : Type u
a : α
s : WSeq α
⊢ (cons a s).head = Computation.pure (some a)

Tactic:
simp [head]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertManyIfNewUnit_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List α} {k k' fallback : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a == b) = false))
    (mem : k ∈ l) :
    getKeyD (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k' fallback = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' fallback : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
⊢ (insertManyIfNewUnit empty l).val.getKeyD k' fallback = k

Tactic:
exact getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq
  contains_empty distinct mem

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem entourageProd_mem_uniformity [t₁ : UniformSpace α] [t₂ : UniformSpace β] {u : Set (α × α)}
    {v : Set (β × β)} (hu : u ∈ 𝓤 α) (hv : v ∈ 𝓤 β) :
    entourageProd u v ∈ 𝓤 (α × β)

Proof state:
α : Type ua
β : Type ub
t₁ : UniformSpace α
t₂ : UniformSpace β
u : Set (α × α)
v : Set (β × β)
hu : u ∈ 𝓤 α
hv : v ∈ 𝓤 β
⊢ entourageProd u v ∈ 𝓤 (α × β)

Tactic:
rw [uniformity_prod]

Result:
α : Type ua
β : Type ub
t₁ : UniformSpace α
t₂ : UniformSpace β
u : Set (α × α)
v : Set (β × β)
hu : u ∈ 𝓤 α
hv : v ∈ 𝓤 β
⊢ entourageProd u v ∈ Filter.comap (fun p => (p.1.1, p.2.1)) (𝓤 α) ⊓ Filter.comap (fun p => (p.1.2, p.2.2)) (𝓤 β)

Proof state:
α : Type ua
β : Type ub
t₁ : UniformSpace α
t₂ : UniformSpace β
u : Set (α × α)
v : Set (β × β)
hu : u ∈ 𝓤 α
hv : v ∈ 𝓤 β
⊢ entourageProd u v ∈ Filter.comap (fun p => (p.1.1, p.2.1)) (𝓤 α) ⊓ Filter.comap (fun p => (p.1.2, p.2.2)) (𝓤 β)

Tactic:
exact inter_mem_inf (preimage_mem_comap hu) (preimage_mem_comap hv)

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem preimage_mul_right_ball [IsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ≥0∞) :
    (fun x => x * a) ⁻¹' ball b r = ball (b / a) r

Proof state:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x => x * a) ⁻¹' ball b r = ball (b * a⁻¹) r

Tactic:
exact preimage_smul_ball (MulOpposite.op a) b r

Result:
no goals

Proof state:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x => x * a) ⁻¹' ball b r = ball (b / a) r

Tactic:
rw [div_eq_mul_inv]

Result:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x => x * a) ⁻¹' ball b r = ball (b * a⁻¹) r
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem associated_eq_eq : (Associated : M → M → Prop) = Eq

Proof state:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
⊢ Associated = Eq

Tactic:
ext

Result:
case h.h.a
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x✝¹ x✝ : M
⊢ x✝¹ ~ᵤ x✝ ↔ x✝¹ = x✝

Proof state:
case h.h.a
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x✝¹ x✝ : M
⊢ x✝¹ ~ᵤ x✝ ↔ x✝¹ = x✝

Tactic:
rw [associated_iff_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_updateRow_add_self (A : Matrix n n R) {i j : n} (hij : i ≠ j) :
    det (updateRow A i (A i + A j)) = det A

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
⊢ (A.updateRow i (A i + A j)).det = A.det

Tactic:
simp [det_updateRow_add,
  det_zero_of_row_eq hij (updateRow_self.trans (updateRow_ne hij.symm).symm)]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProd_of_not_isSFiniteKernel_left (κ : Kernel α β) (η : Kernel (α × β) γ)
    (h : ¬ IsSFiniteKernel κ) :
    κ ⊗ₖ η = 0

Proof state:
case hnc
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel κ
⊢ ¬(IsSFiniteKernel κ ∧ IsSFiniteKernel η)

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel κ
⊢ κ ⊗ₖ η = 0

Tactic:
rw [compProd, dif_neg]

Result:
case hnc
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel κ
⊢ ¬(IsSFiniteKernel κ ∧ IsSFiniteKernel η)
-- Mathlib/Algebra/Ring/Basic.lean
theorem succ_ne_self {α : Type*} [NonAssocRing α] [Nontrivial α] (a : α) : a + 1 ≠ a := fun h =>
  one_ne_zero ((add_right_inj a).mp (by simp [h]))

Proof state:
α : Type u_2
inst✝¹ : NonAssocRing α
inst✝ : Nontrivial α
a : α
h : a + 1 = a
⊢ a + 1 = a + 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Even.lean
lemma succ_mod_two_eq_one_iff : (m + 1) % 2 = 1 ↔ m % 2 = 0

Proof state:
m : ℕ
⊢ (m + 1) % 2 = 1 ↔ m % 2 = 0

Tactic:
simp [← Nat.even_iff, ← Nat.not_even_iff, parity_simps]

Result:
no goals
-- Mathlib/Algebra/Lie/Abelian.lean
theorem Function.Surjective.isLieAbelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R]
    [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R⁆ L₂}
    (h₁ : Function.Surjective f) (h₂ : IsLieAbelian L₁) : IsLieAbelian L₂ :=
  { trivial := fun x y => by
      obtain ⟨u, rfl⟩ := h₁ x
      obtain ⟨v, rfl⟩ := h₁ y
      rw [← LieHom.map_lie, trivial_lie_zero, LieHom.map_zero] }

Proof state:
case intro.intro
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Surjective ⇑f
h₂ : IsLieAbelian L₁
u v : L₁
⊢ ⁅f u, f v⁆ = 0

Tactic:
rw [← LieHom.map_lie, trivial_lie_zero, LieHom.map_zero]

Result:
no goals

Proof state:
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Surjective ⇑f
h₂ : IsLieAbelian L₁
x y : L₂
⊢ ⁅x, y⁆ = 0

Tactic:
obtain ⟨u, rfl⟩ := h₁ x

Result:
case intro
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Surjective ⇑f
h₂ : IsLieAbelian L₁
y : L₂
u : L₁
⊢ ⁅f u, y⁆ = 0

Proof state:
case intro
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Surjective ⇑f
h₂ : IsLieAbelian L₁
y : L₂
u : L₁
⊢ ⁅f u, y⁆ = 0

Tactic:
obtain ⟨v, rfl⟩ := h₁ y

Result:
case intro.intro
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Surjective ⇑f
h₂ : IsLieAbelian L₁
u v : L₁
⊢ ⁅f u, f v⁆ = 0
-- Mathlib/Data/Set/Image.lean
theorem LeftInverse.image_image {g : β → α} (h : LeftInverse g f) (s : Set α) :
    g '' (f '' s) = s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ g '' (f '' s) = s

Tactic:
rw [← image_comp, h.comp_eq_id, image_id]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_asympBound_r_pos : ∀ᶠ (n : ℕ) in atTop, ∀ i, 0 < asympBound g a b (r i n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < asympBound g a b (r i n)

Tactic:
rw [Filter.eventually_all]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < asympBound g a b (r i x)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < asympBound g a b (r i x)

Tactic:
exact fun i => (R.tendsto_atTop_r i).eventually R.eventually_asympBound_pos

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem spectralRadius_le_nnnorm [NormOneClass A] (a : A) : spectralRadius 𝕜 a ≤ ‖a‖₊

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
a : A
⊢ spectralRadius 𝕜 a ≤ ↑‖a‖₊

Tactic:
refine iSup₂_le fun k hk => ?_

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
a : A
k : 𝕜
hk : k ∈ σ a
⊢ ↑‖k‖₊ ≤ ↑‖a‖₊

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
a : A
k : 𝕜
hk : k ∈ σ a
⊢ ↑‖k‖₊ ≤ ↑‖a‖₊

Tactic:
exact mod_cast norm_le_norm_of_mem hk

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem _root_.Real.hasPDF_iff [SFinite ℙ] :
    HasPDF X ℙ ↔ AEMeasurable X ℙ ∧ map X ℙ ≪ volume

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : SFinite ℙ
⊢ HasPDF X ℙ volume ↔ AEMeasurable X ℙ ∧ map X ℙ ≪ volume

Tactic:
rw [hasPDF_iff, and_iff_right (inferInstance : HaveLebesgueDecomposition _ _)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_replicate (p : α → Bool) (a : α) (n : Nat) :
    countP p (replicate n a) = if p a then n else 0

Proof state:
α : Type u_1
p : α → Bool
a : α
n : Nat
⊢ countP p (replicate n a) = if p a = true then n else 0

Tactic:
simp only [countP_eq_length_filter, filter_replicate]

Result:
α : Type u_1
p : α → Bool
a : α
n : Nat
⊢ (if p a = true then replicate n a else []).length = if p a = true then n else 0

Proof state:
α : Type u_1
p : α → Bool
a : α
n : Nat
⊢ (if p a = true then replicate n a else []).length = if p a = true then n else 0

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem nhds_ne_subtype_eq_bot_iff {S : Set X} {x : S} :
    𝓝[≠] x = ⊥ ↔ 𝓝[≠] (x : X) ⊓ 𝓟 S = ⊥

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set X
x : ↑S
⊢ 𝓝[≠] x = ⊥ ↔ 𝓝[≠] ↑x ⊓ 𝓟 S = ⊥

Tactic:
rw [← nhdsWithin_subtype_eq_bot_iff, preimage_compl, ← image_singleton,
  Subtype.coe_injective.preimage_image]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma add_sSup (hs : s.Nonempty) : a + sSup s = ⨆ b ∈ s, a + b

Proof state:
s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
⊢ a + sSup s = ⨆ b ∈ s, a + b

Tactic:
rw [sSup_eq_iSup, add_biSup hs]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma inr_le_iff (a b : A) (ha : IsSelfAdjoint a

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : autoParam (IsSelfAdjoint a) _auto✝
hb : autoParam (IsSelfAdjoint b) _auto✝
⊢ (∀ x ∈ σₙ ℝ (b - a), 0 ≤ x) ↔ 0 ≤ b - a

Tactic:
exact StarOrderedRing.nonneg_iff_quasispectrum_nonneg _ |>.symm

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : autoParam (IsSelfAdjoint a) _auto✝
hb : autoParam (IsSelfAdjoint b) _auto✝
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
rw [← sub_nonneg, ← sub_nonneg (a := b), StarOrderedRing.nonneg_iff_spectrum_nonneg (R := ℝ) _,
  ← inr_sub ℂ b a, ← Unitization.quasispectrum_eq_spectrum_inr' ℝ ℂ]

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : autoParam (IsSelfAdjoint a) _auto✝
hb : autoParam (IsSelfAdjoint b) _auto✝
⊢ (∀ x ∈ σₙ ℝ (b - a), 0 ≤ x) ↔ 0 ≤ b - a
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem coeff_reverse (f : R[X]) (n : ℕ) : f.reverse.coeff n = f.coeff (revAt f.natDegree n)

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ f.reverse.coeff n = f.coeff ((revAt f.natDegree) n)

Tactic:
rw [reverse, coeff_reflect]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem IsTheta.comp_snd : f =Θ[l] g → (f ∘ Prod.snd) =Θ[l' ×ˢ l] (g ∘ Prod.snd)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g ∧ g =O[l] f → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd) ∧ (g ∘ Prod.snd) =O[l' ×ˢ l] (f ∘ Prod.snd)

Tactic:
exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.comp_snd l', h₂.comp_snd l'⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =Θ[l] g → (f ∘ Prod.snd) =Θ[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
simp only [IsTheta, eventually_and]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g ∧ g =O[l] f → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd) ∧ (g ∘ Prod.snd) =O[l' ×ˢ l] (f ∘ Prod.snd)
-- Mathlib/Algebra/ModEq.lean
theorem self_modEq_zero : p ≡ 0 [PMOD p] :=
  ⟨-1, by simp⟩

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p : α
⊢ 0 - p = -1 • p

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem principalUnitGroup_injective :
    Function.Injective (principalUnitGroup : ValuationSubring K → Subgroup _) := fun A B h => by
  simpa [le_antisymm_iff, principalUnitGroup_le_principalUnitGroup] using h.symm

Proof state:
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.principalUnitGroup = B.principalUnitGroup
⊢ A = B

Tactic:
simpa [le_antisymm_iff, principalUnitGroup_le_principalUnitGroup] using h.symm

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem atTop_Ici_eq [Preorder α] [IsDirected α (· ≤ ·)] (a : α) :
    atTop = comap ((↑) : Ici a → α) atTop

Proof state:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
⊢ atTop = comap Subtype.val atTop

Tactic:
rw [← map_val_Ici_atTop a, comap_map Subtype.coe_injective]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem bind_some_eq_map (f : α → β) (x : Part α) : x.bind (fun y => some (f y)) = map f x :=
  ext <| by simp [eq_comm]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
x : Part α
⊢ ∀ (a : β), (a ∈ x.bind fun y => some (f y)) ↔ a ∈ map f x

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem posTangentConeAt_mono : Monotone fun s => posTangentConeAt s a

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : E
⊢ Monotone fun s => posTangentConeAt s a

Tactic:
rintro s t hst y ⟨c, d, hd, hc, hcd⟩

Result:
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : E
s t : Set E
hst : s ≤ t
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ y ∈ (fun s => posTangentConeAt s a) t

Proof state:
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : E
s t : Set E
hst : s ≤ t
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ y ∈ (fun s => posTangentConeAt s a) t

Tactic:
exact ⟨c, d, mem_of_superset hd fun h hn => hst hn, hc, hcd⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem LinearEquiv.coe_ofIsUnitDet {f : M →ₗ[R] M'} {v : Basis ι R M} {v' : Basis ι R M'}
    (h : IsUnit (LinearMap.toMatrix v v' f).det) :
    (LinearEquiv.ofIsUnitDet h : M →ₗ[R] M') = f

Proof state:
case h
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit ((toMatrix v v') f).det
x : M
⊢ ↑(ofIsUnitDet h) x = f x

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit ((toMatrix v v') f).det
⊢ ↑(ofIsUnitDet h) = f

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit ((toMatrix v v') f).det
x : M
⊢ ↑(ofIsUnitDet h) x = f x