harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/Spectrum.lean
theorem eigenvalues_mem_spectrum_real (i : n) : hA.eigenvalues i ∈ spectrum ℝ A

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ hA.eigenvalues i ∈ spectrum ℝ A

Tactic:
apply spectrum.of_algebraMap_mem 𝕜

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ (algebraMap ℝ 𝕜) (hA.eigenvalues i) ∈ spectrum 𝕜 A

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ (algebraMap ℝ 𝕜) (hA.eigenvalues i) ∈ spectrum 𝕜 (toEuclideanLin A)

Tactic:
exact LinearMap.IsSymmetric.hasEigenvalue_eigenvalues _ _ _ |>.mem_spectrum

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ (algebraMap ℝ 𝕜) (hA.eigenvalues i) ∈ spectrum 𝕜 A

Tactic:
rw [← spectrum_toEuclideanLin]

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ (algebraMap ℝ 𝕜) (hA.eigenvalues i) ∈ spectrum 𝕜 (toEuclideanLin A)
-- Mathlib/Order/SuccPred/Limit.lean
theorem isGLB_Ioi_iff_isPredPrelimit : IsGLB (Ioi a) a ↔ IsPredPrelimit a

Proof state:
α : Type u_1
a : α
inst✝ : LinearOrder α
⊢ IsGLB (Ioi a) a ↔ IsPredPrelimit a

Tactic:
simpa using isLUB_Iio_iff_isSuccPrelimit (a := toDual a)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_laverage_le_pos (hμ : μ ≠ 0) (hint : ∫⁻ a, f a ∂μ ≠ ∞) :
    0 < μ {x | ⨍⁻ a, f a ∂μ ≤ f x}

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤
⊢ 0 < μ {x | ⨍⁻ (a : α), f a ∂μ ≤ f x}

Tactic:
simpa [hint] using
  @measure_setLaverage_le_pos _ _ _ _ f (measure_univ_ne_zero.2 hμ) nullMeasurableSet_univ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min b c

Proof state:
a b c : Nat
⊢ min (b * a) (c * a) = min b c * a

Tactic:
exact Nat.mul_min_mul_right ..

Result:
no goals

Proof state:
a b c : Nat
⊢ min (a * b) (a * c) = a * min b c

Tactic:
repeat rw [Nat.mul_comm a]

Result:
a b c : Nat
⊢ min (b * a) (c * a) = min b c * a

Proof state:
a b c : Nat
⊢ min (b * a) (c * a) = a * min b c

Tactic:
rw [Nat.mul_comm a]

Result:
a b c : Nat
⊢ min (b * a) (c * a) = min b c * a
-- Mathlib/Data/Matroid/IndepAxioms.lean
theorem ofFinset_indep' [DecidableEq α] (E : Set α) Indep indep_empty indep_subset indep_aug
    subset_ground {I : Set α} : (IndepMatroid.ofFinset
      E Indep indep_empty indep_subset indep_aug subset_ground).Indep I ↔
        ∀ (J : Finset α), (J : Set α) ⊆ I → Indep J

Proof state:
α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I : Set α
⊢ (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep I ↔
    ∀ (J : Finset α), ↑J ⊆ I → Indep J

Tactic:
simp only [IndepMatroid.ofFinset, ofFinitaryCardAugment_indep]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma WithTop.ofDual_le_iff {x : WithTop αᵒᵈ} {y : WithBot α} :
    WithTop.ofDual x ≤ y ↔ y.toDual ≤ x

Proof state:
α : Type u_1
inst✝ : LE α
x : WithTop αᵒᵈ
y : WithBot α
⊢ WithTop.ofDual x ≤ y ↔ WithBot.toDual y ≤ x

Tactic:
cases x <;> cases y <;> simp [toDual_le]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/WithLp.lean
theorem contDiffWithinAt_piLp :
    ContDiffWithinAt 𝕜 n f t y ↔ ∀ i, ContDiffWithinAt 𝕜 n (fun x => f x i) t y

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
y : H
⊢ (∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) t y) ↔
    ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => f x i) t y

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
y : H
⊢ ContDiffWithinAt 𝕜 n f t y ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => f x i) t y

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffWithinAt_iff, contDiffWithinAt_pi]

Result:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
y : H
⊢ (∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) t y) ↔
    ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => f x i) t y
-- Mathlib/Data/List/Basic.lean
theorem filterMap_congr {f g : α → Option β} {l : List α}
    (h : ∀ x ∈ l, f x = g x) : l.filterMap f = l.filterMap g

Proof state:
α : Type u
β : Type v
f g : α → Option β
l : List α
h : ∀ (x : α), x ∈ l → f x = g x
⊢ filterMap f l = filterMap g l

Tactic:
induction l <;> simp_all [filterMap_cons]

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem mem_singleton (x y : α) (b : β y) : x ∈ singleton y b ↔ x = y

Proof state:
α : Type u
β : α → Type v
x y : α
b : β y
⊢ x ∈ ⟦AList.singleton y b⟧ ↔ x = y

Tactic:
erw [mem_cons, mem_nil_iff, or_false]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x y : α
b : β y
⊢ x ∈ singleton y b ↔ x = y

Tactic:
simp only [singleton]

Result:
α : Type u
β : α → Type v
x y : α
b : β y
⊢ x ∈ ⟦AList.singleton y b⟧ ↔ x = y
-- Mathlib/Probability/Kernel/Basic.lean
theorem lintegral_restrict (κ : Kernel α β) (hs : MeasurableSet s) (a : α) (f : β → ℝ≥0∞) :
    ∫⁻ b, f b ∂κ.restrict hs a = ∫⁻ b in s, f b ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
κ : Kernel α β
hs : MeasurableSet s
a : α
f : β → ℝ≥0∞
⊢ ∫⁻ (b : β), f b ∂(κ.restrict hs) a = ∫⁻ (b : β) in s, f b ∂κ a

Tactic:
rw [restrict_apply]

Result:
no goals
-- Mathlib/NumberTheory/BernoulliPolynomials.lean
theorem bernoulli_zero : bernoulli 0 = 1

Proof state:
⊢ bernoulli 0 = 1

Tactic:
simp [bernoulli]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
/-- See also `Irreducible.coprime_iff_not_dvd`. -/
lemma Irreducible.isRelPrime_iff_not_dvd [Monoid M] {p n : M} (hp : Irreducible p) :
    IsRelPrime p n ↔ ¬ p ∣ n

Proof state:
M : Type u_1
inst✝ : Monoid M
p n : M
hp : Irreducible p
d : M
hdp : d ∣ p
hdn : d ∣ n
hpn : ¬IsUnit d
⊢ p ∣ n

Tactic:
suffices Associated p d from this.dvd.trans hdn

Result:
M : Type u_1
inst✝ : Monoid M
p n : M
hp : Irreducible p
d : M
hdp : d ∣ p
hdn : d ∣ n
hpn : ¬IsUnit d
⊢ p ~ᵤ d

Proof state:
M : Type u_1
inst✝ : Monoid M
p n : M
hp : Irreducible p
d : M
hdp : d ∣ p
hdn : d ∣ n
hpn : ¬IsUnit d
⊢ p ~ᵤ d

Tactic:
exact (hp.dvd_iff.mp hdp).resolve_left hpn

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
p n : M
hp : Irreducible p
hpn : ¬p ∣ n
d : M
hdp : d ∣ p
hdn : d ∣ n
⊢ IsUnit d

Tactic:
contrapose! hpn

Result:
M : Type u_1
inst✝ : Monoid M
p n : M
hp : Irreducible p
d : M
hdp : d ∣ p
hdn : d ∣ n
hpn : ¬IsUnit d
⊢ p ∣ n

Proof state:
M : Type u_1
inst✝ : Monoid M
p n : M
hp : Irreducible p
⊢ IsRelPrime p n ↔ ¬p ∣ n

Tactic:
refine ⟨fun h contra ↦ hp.not_unit (h dvd_rfl contra), fun hpn d hdp hdn ↦ ?_⟩

Result:
M : Type u_1
inst✝ : Monoid M
p n : M
hp : Irreducible p
hpn : ¬p ∣ n
d : M
hdp : d ∣ p
hdn : d ∣ n
⊢ IsUnit d
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem prod_lt_one (h : ∀ i ∈ s, f i < 1) (hs : s.Nonempty) : ∏ i ∈ s, f i < 1 :=
  (prod_lt_prod_of_nonempty' hs h).trans_le (by rw [prod_const_one])

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s : Finset ι
h : ∀ i ∈ s, f i < 1
hs : s.Nonempty
⊢ ∏ i ∈ s, 1 ≤ 1

Tactic:
rw [prod_const_one]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
theorem zpowers_eq_closure (g : G) : zpowers g = closure {g}

Proof state:
G : Type u_1
inst✝ : Group G
g : G
⊢ zpowers g = closure {g}

Tactic:
ext

Result:
case h
G : Type u_1
inst✝ : Group G
g x✝ : G
⊢ x✝ ∈ zpowers g ↔ x✝ ∈ closure {g}

Proof state:
case h
G : Type u_1
inst✝ : Group G
g x✝ : G
⊢ x✝ ∈ zpowers g ↔ x✝ ∈ closure {g}

Tactic:
exact mem_closure_singleton.symm

Result:
no goals
-- Mathlib/FieldTheory/Normal/Closure.lean
lemma normalClosure_of_normal [Normal F K] : normalClosure F K L = K

Proof state:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F ↥K
⊢ normalClosure F (↥K) L = K

Tactic:
simp only [normalClosure_def, AlgHom.fieldRange_of_normal, iSup_const]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem lowerClosure_prod (s : Set α) (t : Set β) :
    lowerClosure (s ×ˢ t) = lowerClosure s ×ˢ lowerClosure t

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
⊢ lowerClosure (s ×ˢ t) = lowerClosure s ×ˢ lowerClosure t

Tactic:
ext

Result:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ ↑(lowerClosure (s ×ˢ t)) ↔ x✝ ∈ ↑(lowerClosure s ×ˢ lowerClosure t)

Proof state:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ ↑(lowerClosure (s ×ˢ t)) ↔ x✝ ∈ ↑(lowerClosure s ×ˢ lowerClosure t)

Tactic:
simp [Prod.le_def, @and_and_and_comm _ (_ ∈ t)]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem map_tail (f : α → β) : ∀ s, map f (tail s) = tail (map f s)
  | ⟨s, al⟩ => by apply Subtype.eq; dsimp [tail, map]

Proof state:
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : s.IsSeq
⊢ map f (tail ⟨s, al⟩) = (map f ⟨s, al⟩).tail

Tactic:
apply Subtype.eq

Result:
case a
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map f (tail ⟨s, al⟩)) = ↑(map f ⟨s, al⟩).tail

Proof state:
case a
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map f (tail ⟨s, al⟩)) = ↑(map f ⟨s, al⟩).tail

Tactic:
dsimp [tail, map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_eq_append_iff {p : α → Bool} :
    filter p l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂

Proof state:
α : Type u_1
l L₁ L₂ : List α
p : α → Bool
⊢ filter p l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂

Tactic:
rw [← filterMap_eq_filter, filterMap_eq_append_iff]

Result:
no goals
-- Mathlib/Topology/Basic.lean
lemma Equiv.isOpenMap_symm_iff (e : X ≃ Y) : IsOpenMap e.symm ↔ Continuous e

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ IsOpenMap ⇑e.symm ↔ Continuous ⇑e

Tactic:
simp_rw [← Equiv.continuous_symm_iff, Equiv.symm_symm]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem lineMap_same_apply (p : P1) (c : k) : lineMap p p c = p

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p : P1
c : k
⊢ (lineMap p p) c = p

Tactic:
simp [lineMap_apply]

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

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

Tactic:
simp_to_raw using Raw₀.Const.getKey_insertMany_empty_list_of_mem

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_eq_pred_iff : pred a = pred b ↔ a = b

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
⊢ pred a = pred b ↔ a = b

Tactic:
simp_rw [eq_iff_le_not_lt, pred_le_pred_iff, pred_lt_pred_iff]

Result:
no goals
-- Mathlib/Algebra/QuaternionBasis.lean
theorem lift_one : q.lift (1 : ℍ[R,c₁,c₂,c₃]) = 1

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.lift 1 = 1

Tactic:
simp [lift]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive]
lemma enorm_div_le : ‖a / b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a / b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

Tactic:
simpa [enorm, ← ENNReal.coe_add] using nnnorm_div_le a b

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
@[simp]
lemma arrow_mk_comp_eqToHom {X Y Y' : T} (f : X ⟶ Y) (h : Y = Y') :
    Arrow.mk (f ≫ eqToHom h) = Arrow.mk f :=
  ext rfl h.symm (by simp)

Proof state:
T : Type u
inst✝ : Category.{v, u} T
X Y Y' : T
f : X ⟶ Y
h : Y = Y'
⊢ (mk (f ≫ eqToHom h)).hom = eqToHom ⋯ ≫ (mk f).hom ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findSome?_replicate_of_isSome (_ : (f a).isSome) : findSome? f (replicate n a) = if n = 0 then none else f a

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
x✝ : (f a).isSome = true
⊢ findSome? f (replicate n a) = if n = 0 then none else f a

Tactic:
simp [findSome?_replicate]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem map_id : ∀ s : Seq1 α, map id s = s
  | ⟨a, s⟩ => by simp [map]

Proof state:
α : Type u
a : α
s : Seq α
⊢ map id (a, s) = (a, s)

Tactic:
simp [map]

Result:
no goals
-- Mathlib/Data/String/Basic.lean
theorem asString_eq {l : List Char} {s : String} : l.asString = s ↔ l = s.toList

Proof state:
l : List Char
s : String
⊢ l.asString = s ↔ l = s.toList

Tactic:
rw [← asString_toList s, asString_inj, asString_toList s]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem LinearEquiv.det_coe_symm {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] (f : M ≃ₗ[𝕜] M) :
    LinearMap.det (f.symm : M →ₗ[𝕜] M) = (LinearMap.det (f : M →ₗ[𝕜] M))⁻¹

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_5
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M ≃ₗ[𝕜] M
⊢ LinearMap.det ↑f.symm = (LinearMap.det ↑f)⁻¹

Tactic:
field_simp [IsUnit.ne_zero f.isUnit_det']

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem find?_insert [@TransCmp α cmp] (t : RBMap α β cmp) (k v k') :
    (t.insert k v).find? k' = if cmp k' k = .eq then some v else t.find? k'

Proof state:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
inst✝ : TransCmp cmp
t : RBMap α β cmp
k : α
v : β
k' : α
⊢ (t.insert k v).find? k' = if cmp k' k = Ordering.eq then some v else t.find? k'

Tactic:
split <;> [exact find?_insert_of_eq t ‹_›; exact find?_insert_of_ne t ‹_›]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_le_algebraMap_iff (f : R → R) (r : R) (a : A)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.809602) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f : R → R
r : R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc f a ≤ (algebraMap R A) r ↔ ∀ x ∈ spectrum R a, f x ≤ r

Tactic:
rw [← cfc_const r a, cfc_le_iff ..]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivWithinAt.mul (hc : HasDerivWithinAt c c' s x) (hd : HasDerivWithinAt d d' s x) :
    HasDerivWithinAt (fun y => c y * d y) (c' * d x + c x * d') s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
this : HasDerivWithinAt (fun y => c y * d y) ((c x • smulRight 1 d' + (smulRight 1 c').smulRight (d x)) 1) s x
⊢ HasDerivWithinAt (fun y => c y * d y) (c' * d x + c x * d') s x

Tactic:
rwa [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
  ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.smulRight_apply,
  ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, one_smul, one_smul,
  add_comm] at this

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
⊢ HasDerivWithinAt (fun y => c y * d y) (c' * d x + c x * d') s x

Tactic:
have := (HasFDerivWithinAt.mul' hc hd).hasDerivWithinAt

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
this : HasDerivWithinAt (fun y => c y * d y) ((c x • smulRight 1 d' + (smulRight 1 c').smulRight (d x)) 1) s x
⊢ HasDerivWithinAt (fun y => c y * d y) (c' * d x + c x * d') s x
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_inter_mulSupport (s : Set α) (f : α → M) :
    mulIndicator (s ∩ mulSupport f) f = mulIndicator s f

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
⊢ (s ∩ mulSupport f).mulIndicator f = s.mulIndicator f

Tactic:
rw [← mulIndicator_mulIndicator, mulIndicator_mulSupport]

Result:
no goals
-- Mathlib/Data/Semiquot.lean
theorem eq_pure {q : Semiquot α} (p) : q = pure (get q p) :=
  ext.2 fun a => by simpa using ⟨fun h => p _ h _ (get_mem _), fun e => e.symm ▸ get_mem _⟩

Proof state:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
⊢ a ∈ q ↔ a ∈ pure (q.get p)

Tactic:
simpa using ⟨fun h => p _ h _ (get_mem _), fun e => e.symm ▸ get_mem _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem extractLsb_xor {x : BitVec w} {hi lo : Nat} :
   (x ^^^ y).extractLsb lo hi = (x.extractLsb lo hi) ^^^ (y.extractLsb lo hi)

Proof state:
w : Nat
y x : BitVec w
hi lo : Nat
⊢ extractLsb lo hi (x ^^^ y) = extractLsb lo hi x ^^^ extractLsb lo hi y

Tactic:
ext k hk

Result:
case pred
w : Nat
y x : BitVec w
hi lo k : Nat
hk : k < lo - hi + 1
⊢ (extractLsb lo hi (x ^^^ y)).getLsbD k = (extractLsb lo hi x ^^^ extractLsb lo hi y).getLsbD k

Proof state:
w : Nat
y x : BitVec w
hi lo k : Nat
hk : k < lo - hi + 1
⊢ k ≤ lo - hi

Tactic:
omega

Result:
no goals

Proof state:
case pred
w : Nat
y x : BitVec w
hi lo k : Nat
hk : k < lo - hi + 1
⊢ (extractLsb lo hi (x ^^^ y)).getLsbD k = (extractLsb lo hi x ^^^ extractLsb lo hi y).getLsbD k

Tactic:
simp [hk, show k ≤ lo - hi by omega]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem le_self_nadd {a b} : a ≤ a ♯ b

Proof state:
a b : Ordinal.{u_1}
⊢ a ≤ a ♯ b

Tactic:
simpa using nadd_le_nadd_left (Ordinal.zero_le b) a

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
@[simp] lemma nhdsWithin_univ (a : α) : 𝓝[Set.univ] a = 𝓝 a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[univ] a = 𝓝 a

Tactic:
rw [nhdsWithin, principal_univ, inf_top_eq]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_sub_eq_left_of_degree_lt (h : degree q < degree p) : degree (p - q) = degree p

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ (p - q).degree = p.degree

Tactic:
rw [sub_eq_add_neg, degree_add_eq_left_of_degree_lt h]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree < p.degree
⊢ (p - q).degree = p.degree

Tactic:
rw [← degree_neg q] at h

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ (p - q).degree = p.degree
-- Mathlib/Algebra/Group/End.lean
theorem subtypeCongrHom_injective (p : α → Prop) [DecidablePred p] :
    Function.Injective (subtypeCongrHom p)

Proof state:
case mk.mk
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)

Tactic:
rw [Prod.mk.inj_iff]

Result:
case mk.mk
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝

Proof state:
case mk.mk
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝

Tactic:
constructor <;> ext i <;> simpa using Equiv.congr_fun h i

Result:
no goals

Proof state:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective ⇑(subtypeCongrHom p)

Tactic:
rintro ⟨⟩ ⟨⟩ h

Result:
case mk.mk
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
-- Mathlib/ModelTheory/Order.lean
@[simp]
lemma card_eq_one : Language.order.card = 1

Proof state:
⊢ Language.order.card = 1

Tactic:
simp [card]

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_nat [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1]
    (f : F) (n : ℕ) : f n = f 0 + n

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
inst✝² : AddMonoidWithOne G
inst✝¹ : AddMonoidWithOne H
inst✝ : AddConstMapClass F G H 1 1
f : F
n : ℕ
⊢ f ↑n = f 0 + ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Basic.lean
@[to_additive]
lemma id_apply (X : CommGrp) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : CommGrp
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem foldl_induction' (f : β → α → β) [RightCommutative f] (x : β) (q : α → Prop)
    (p : β → Prop) (s : Multiset α) (hpqf : ∀ a b, q a → p b → p (f b a)) (px : p x)
    (q_s : ∀ a ∈ s, q a) : p (foldl f x s)

Proof state:
α : Type u_1
β : Type v
f : β → α → β
inst✝ : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ a ∈ s, q a
⊢ p (foldr (fun x y => f y x) x s)

Tactic:
exact foldr_induction' (fun x y => f y x) x q p s hpqf px q_s

Result:
no goals

Proof state:
α : Type u_1
β : Type v
f : β → α → β
inst✝ : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ a ∈ s, q a
⊢ p (foldl f x s)

Tactic:
rw [foldl_swap]

Result:
α : Type u_1
β : Type v
f : β → α → β
inst✝ : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ a ∈ s, q a
⊢ p (foldr (fun x y => f y x) x s)