harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Digits.lean
theorem base_pow_length_digits_le' (b m : ℕ) (hm : m ≠ 0) :
    (b + 2) ^ (digits (b + 2) m).length ≤ (b + 2) * m

Proof state:
b m : ℕ
hm : m ≠ 0
this : (b + 2).digits m ≠ []
⊢ (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m

Tactic:
convert @pow_length_le_mul_ofDigits b (digits (b+2) m)
  this (getLast_digit_ne_zero _ hm)

Result:
case h.e'_4.h.e'_6
b m : ℕ
hm : m ≠ 0
this : (b + 2).digits m ≠ []
⊢ m = ofDigits (b + 2) ((b + 2).digits m)

Proof state:
case h.e'_4.h.e'_6
b m : ℕ
hm : m ≠ 0
this : (b + 2).digits m ≠ []
⊢ m = ofDigits (b + 2) ((b + 2).digits m)

Tactic:
rw [ofDigits_digits]

Result:
no goals

Proof state:
b m : ℕ
hm : m ≠ 0
⊢ (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m

Tactic:
have : digits (b + 2) m ≠ [] := digits_ne_nil_iff_ne_zero.mpr hm

Result:
b m : ℕ
hm : m ≠ 0
this : (b + 2).digits m ≠ []
⊢ (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m
-- Mathlib/Data/List/Nodup.lean
theorem nodup_iff_sublist {l : List α} : Nodup l ↔ ∀ a, ¬[a, a] <+ l :=
  ⟨fun d a h => not_nodup_pair a (d.sublist h),
    by
      induction' l with a l IH <;> intro h; · exact nodup_nil
      exact (IH fun a s => h a <| sublist_cons_of_sublist _ s).cons fun al =>
        h a <| (singleton_sublist.2 al).cons_cons _⟩

Proof state:
α : Type u
l : List α
⊢ (∀ (a : α), ¬[a, a] <+ l) → l.Nodup

Tactic:
induction' l with a l IH <;> intro h

Result:
case nil
α : Type u
h : ∀ (a : α), ¬[a, a] <+ []
⊢ [].Nodup

case cons
α : Type u
a : α
l : List α
IH : (∀ (a : α), ¬[a, a] <+ l) → l.Nodup
h : ∀ (a_1 : α), ¬[a_1, a_1] <+ a :: l
⊢ (a :: l).Nodup

Proof state:
case nil
α : Type u
h : ∀ (a : α), ¬[a, a] <+ []
⊢ [].Nodup

Tactic:
exact nodup_nil

Result:
no goals

Proof state:
case cons
α : Type u
a : α
l : List α
IH : (∀ (a : α), ¬[a, a] <+ l) → l.Nodup
h : ∀ (a_1 : α), ¬[a_1, a_1] <+ a :: l
⊢ (a :: l).Nodup

Tactic:
exact (IH fun a s => h a <| sublist_cons_of_sublist _ s).cons fun al =>
  h a <| (singleton_sublist.2 al).cons_cons _

Result:
no goals
-- Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
/-- The **valuative criterion** for proper morphisms. -/
@[stacks 0BX5]
lemma IsProper.of_valuativeCriterion [QuasiCompact f] [QuasiSeparated f] [LocallyOfFiniteType f]
    (H : ValuativeCriterion f) : IsProper f

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : LocallyOfFiniteType f
H : ValuativeCriterion f
⊢ (ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType) f

Tactic:
exact ⟨⟨⟨‹_›, ‹_›⟩, ‹_›⟩, ‹_›⟩

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : LocallyOfFiniteType f
H : ValuativeCriterion f
⊢ IsProper f

Tactic:
rw [eq_valuativeCriterion]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : LocallyOfFiniteType f
H : ValuativeCriterion f
⊢ (ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType) f
-- Mathlib/AlgebraicGeometry/Restrict.lean
@[reassoc (attr := simp)]
lemma Scheme.Opens.isoOfLE_hom_ι {X : Scheme.{u}} {U V : X.Opens}
    (hUV : U ≤ V) :
    (Scheme.Opens.isoOfLE hUV).hom ≫ U.ι = (V.ι ⁻¹ᵁ U).ι ≫ V.ι

Proof state:
X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ (isoOfLE hUV).hom ≫ U.ι = (V.ι ⁻¹ᵁ U).ι ≫ V.ι

Tactic:
simp [isoOfLE]

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive] lemma leOnePart_le_one : a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1

Tactic:
simp [leOnePart]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem isBounded_const (ι' : Type*) [Nonempty ι'] {p : ι → Seminorm 𝕜 E} {q : Seminorm 𝕜₂ F}
    (f : E →ₛₗ[σ₁₂] F) :
    IsBounded p (fun _ : ι' => q) f ↔ ∃ (s : Finset ι) (C : ℝ≥0), q.comp f ≤ C • s.sup p

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι' : Type u_10
inst✝ : Nonempty ι'
p : ι → Seminorm 𝕜 E
q : Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
⊢ IsBounded p (fun x => q) f ↔ ∃ s C, q.comp f ≤ C • s.sup p

Tactic:
simp only [IsBounded, forall_const]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem toWithTop_ofENat (n : ℕ∞) {_ : Decidable (n : PartENat).Dom} : toWithTop (↑n) = n

Proof state:
case top
x✝ : Decidable (↑⊤).Dom
⊢ (↑⊤).toWithTop = ⊤

Tactic:
simp

Result:
no goals

Proof state:
case coe
n : ℕ
x✝ : Decidable (↑↑n).Dom
⊢ (↑↑n).toWithTop = ↑n

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ∞
x✝ : Decidable (↑n).Dom
⊢ (↑n).toWithTop = n

Tactic:
cases n with
| top => simp
| coe n => simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} (h : m.WF) :
    Const.getD (Const.modify m k f) k' fallback =
      if k == k' then
        Const.get? m k |>.map f |>.getD fallback
      else
        Const.getD m k' fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
fallback : β
f : β → β
h : m.WF
⊢ getD (modify m k f) k' fallback =
    if (k == k') = true then (Option.map f (get? m k)).getD fallback else getD m k' fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_modify

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem maximumIndepSet_card_eq_indepNum
    [Fintype α] (t : Finset α) (tmc : G.IsMaximumIndepSet t) : #t = G.indepNum

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
t : Finset α
tmc : G.IsMaximumIndepSet t
⊢ #t = G.indepNum

Tactic:
rw [← isMaximumClique_compl] at tmc

Result:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
t : Finset α
tmc : Gᶜ.IsMaximumClique t
⊢ #t = G.indepNum

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
t : Finset α
tmc : Gᶜ.IsMaximumClique t
⊢ #t = sSup {n | ∃ s, Gᶜ.IsNClique n s}

Tactic:
exact Gᶜ.maximumClique_card_eq_cliqueNum t tmc

Result:
no goals

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
t : Finset α
tmc : Gᶜ.IsMaximumClique t
⊢ #t = G.indepNum

Tactic:
simp_rw [indepNum, ← isNClique_compl]

Result:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
t : Finset α
tmc : Gᶜ.IsMaximumClique t
⊢ #t = sSup {n | ∃ s, Gᶜ.IsNClique n s}
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_insertManyIfNewUnit_empty_list [EquivBEq α] [LawfulHashable α]
    {l : List α} :
    (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1.1.isEmpty = l.isEmpty

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
⊢ (empty.val.isEmpty && l.isEmpty) = l.isEmpty

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
⊢ (insertManyIfNewUnit empty l).val.val.isEmpty = l.isEmpty

Tactic:
rw [isEmpty_insertManyIfNewUnit_list _ Raw.WF.empty₀]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
⊢ (empty.val.isEmpty && l.isEmpty) = l.isEmpty
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem leftUnitor_inv_naturality {X Y : C} (f : X ⟶ Y) :
    f ≫ (λ_ Y).inv = (λ_ X).inv ≫ _ ◁ f

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ f ≫ (λ_ Y).inv = (λ_ X).inv ≫ 𝟙_ C ◁ f

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
@[simp]
lemma shiftIso_zero_hom_app (a : M) (X : C) :
    (F.shiftIso 0 a a (zero_add a)).hom.app X =
      (shift F a).map ((shiftFunctorZero C M).hom.app X)

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_6, u_1} C
inst✝³ : Category.{u_5, u_2} A
F : C ⥤ A
M : Type u_3
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
a : M
X : C
⊢ (F.shiftIso 0 a a ⋯).hom.app X = (F.shift a).map ((shiftFunctorZero C M).hom.app X)

Tactic:
simp [F.shiftIso_zero a]

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
theorem dist_conj_comm (z w : ℂ) : dist (conj z) w = dist z (conj w)

Proof state:
z w : ℂ
⊢ dist ((starRingEnd ℂ) z) w = dist z ((starRingEnd ℂ) w)

Tactic:
rw [← dist_conj_conj, conj_conj]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infDist_le_infDist_add_dist : infDist x s ≤ infDist y s + dist x y

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
⊢ (infEdist x s).toReal ≤ (infEdist y s).toReal + (edist x y).toReal

Tactic:
refine ENNReal.toReal_le_add' infEdist_le_infEdist_add_edist ?_ (flip absurd (edist_ne_top _ _))

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
⊢ infEdist y s = ⊤ → infEdist x s = ⊤

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
⊢ infDist x s ≤ infDist y s + dist x y

Tactic:
rw [infDist, infDist, dist_edist]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
⊢ (infEdist x s).toReal ≤ (infEdist y s).toReal + (edist x y).toReal

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
⊢ infEdist y s = ⊤ → infEdist x s = ⊤

Tactic:
simp only [infEdist_eq_top_iff, imp_self]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem uniformContinuous_iInf_dom {f : α → β} {u₁ : ι → UniformSpace α} {u₂ : UniformSpace β}
    {i : ι} (hf : UniformContinuous[u₁ i, u₂] f) : UniformContinuous[iInf u₁, u₂] f

Proof state:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ UniformContinuous f

Tactic:
delta UniformContinuous

Result:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Proof state:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
rw [iInf_uniformity]

Result:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.1, f x.2)) (⨅ i, 𝓤 α) (𝓤 β)

Proof state:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.1, f x.2)) (⨅ i, 𝓤 α) (𝓤 β)

Tactic:
exact tendsto_iInf' i hf

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem ack_succ_right_le_ack_succ_left (m n : ℕ) : ack m (n + 1) ≤ ack (m + 1) n

Proof state:
case zero
m : ℕ
⊢ ack m (0 + 1) ≤ ack (m + 1) 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack (m + 1) (n + 1)

Tactic:
rw [ack_succ_succ]

Result:
case succ
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack m (ack (m + 1) n)

Proof state:
case succ
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack m (ack (m + 1) n)

Tactic:
apply ack_mono_right m (le_trans _ <| add_add_one_le_ack _ n)

Result:
m n : ℕ
⊢ n + 1 + 1 ≤ m + 1 + n + 1

Proof state:
m n : ℕ
⊢ n + 1 + 1 ≤ m + 1 + n + 1

Tactic:
omega

Result:
no goals

Proof state:
m n : ℕ
⊢ ack m (n + 1) ≤ ack (m + 1) n

Tactic:
rcases n with - | n

Result:
case zero
m : ℕ
⊢ ack m (0 + 1) ≤ ack (m + 1) 0

case succ
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack (m + 1) (n + 1)
-- Mathlib/Probability/Independence/Basic.lean
lemma iIndepSets.meas_iInter [Fintype ι] (h : iIndepSets π μ) (hs : ∀ i, s i ∈ π i) :
    μ (⋂ i, s i) = ∏ i, μ (s i)

Proof state:
Ω : Type u_1
ι : Type u_2
π : ι → Set (Set Ω)
x✝ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndepSets π μ
hs : ∀ (i : ι), s i ∈ π i
⊢ μ (⋂ i, s i) = ∏ i : ι, μ (s i)

Tactic:
simp [← h.meas_biInter _ fun _i _ ↦ hs _]

Result:
no goals
-- Mathlib/Analysis/Calculus/LogDeriv.lean
theorem logDeriv_const_mul {f : 𝕜 → 𝕜'} (x : 𝕜) (a : 𝕜') (ha : a ≠ 0):
    logDeriv (fun z => a * f z) x = logDeriv f x

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
a : 𝕜'
ha : a ≠ 0
⊢ logDeriv (fun z => a * f z) x = logDeriv f x

Tactic:
simp only [logDeriv_apply, deriv_const_mul_field, mul_div_mul_left _ _ ha]

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Basic.lean
theorem coe_iInf {ι : Sort*} {S : ι → Subsemigroup M} : (↑(⨅ i, S i) : Set M) = ⋂ i, S i

Proof state:
M : Type u_1
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem forall_mem_singleton {p : α → Prop} {a : α} : (∀ (x) (_ : x ∈ #[a]), p x) ↔ p a

Proof state:
α : Type u_1
p : α → Prop
a : α
⊢ (∀ (x : α), x ∈ #[a] → p x) ↔ p a

Tactic:
simp only [mem_singleton, forall_eq]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Projections.lean
theorem Q_f_naturality (q n : ℕ) {X Y : SimplicialObject C} (f : X ⟶ Y) :
    f.app (op ⦋n⦌) ≫ (Q q).f n = (Q q).f n ≫ f.app (op ⦋n⦌)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app (op ⦋n⦌) ≫ 𝟙 (Y _⦋n⦌) = 𝟙 (X _⦋n⦌) ≫ f.app (op ⦋n⦌)

Tactic:
simp only [comp_id, id_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app (op ⦋n⦌) ≫ (Q q).f n = (Q q).f n ≫ f.app (op ⦋n⦌)

Tactic:
simp only [Q, HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, P_f_naturality,
  sub_comp, sub_left_inj]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app (op ⦋n⦌) ≫ 𝟙 (K[Y].X n) = 𝟙 (K[X].X n) ≫ f.app (op ⦋n⦌)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app (op ⦋n⦌) ≫ 𝟙 (K[Y].X n) = 𝟙 (K[X].X n) ≫ f.app (op ⦋n⦌)

Tactic:
dsimp

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app (op ⦋n⦌) ≫ 𝟙 (Y _⦋n⦌) = 𝟙 (X _⦋n⦌) ≫ f.app (op ⦋n⦌)
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma norm_or_neg_norm_mem_spectrum [Nontrivial A] {a : A}
    (ha : IsSelfAdjoint a

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : Nontrivial A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
ha' : SpectrumRestricts a ⇑Complex.reCLM
⊢ ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a

Tactic:
rw [← ha.toReal_spectralRadius_eq_norm]

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : Nontrivial A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
ha' : SpectrumRestricts a ⇑Complex.reCLM
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : Nontrivial A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a

Tactic:
have ha' : SpectrumRestricts a Complex.reCLM := ha.spectrumRestricts

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : Nontrivial A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
ha' : SpectrumRestricts a ⇑Complex.reCLM
⊢ ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : Nontrivial A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
ha' : SpectrumRestricts a ⇑Complex.reCLM
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a

Tactic:
exact Real.spectralRadius_mem_spectrum_or (ha'.image ▸ (spectrum.nonempty a).image _)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem IsNClique.insert (hs : G.IsNClique n s) (h : ∀ b ∈ s, G.Adj a b) :
    G.IsNClique (n + 1) (insert a s)

Proof state:
case isClique
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsClique ↑(insert a s)

Tactic:
push_cast

Result:
case isClique
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsClique (insert a ↑s)

Proof state:
case card_eq
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ #(insert a s) = n + 1

Tactic:
rw [card_insert_of_not_mem fun ha => (h _ ha).ne rfl, hs.2]

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsNClique (n + 1) (insert a s)

Tactic:
constructor

Result:
case isClique
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsClique ↑(insert a s)

case card_eq
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ #(insert a s) = n + 1

Proof state:
case isClique
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsClique (insert a ↑s)

Tactic:
exact hs.1.insert fun b hb _ => h _ hb

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem lt_one_div_of_neg (ha : a < 0) (hb : b < 0) : a < 1 / b ↔ b < 1 / a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
ha : a < 0
hb : b < 0
⊢ a < 1 / b ↔ b < 1 / a

Tactic:
simpa using lt_inv_of_neg ha hb

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma jacobiTheta₂''_conj (z τ : ℂ) :
    conj (jacobiTheta₂'' z τ) = jacobiTheta₂'' (conj z) (-conj τ)

Proof state:
z τ : ℂ
⊢ (starRingEnd ℂ) (jacobiTheta₂'' z τ) = jacobiTheta₂'' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
simp [jacobiTheta₂'', jacobiTheta₂'_conj, jacobiTheta₂_conj, ← exp_conj, map_ofNat, div_neg,
  neg_div, jacobiTheta₂'_neg_left]

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem Prop.compl_singleton (p : Prop) : ({p}ᶜ : Set Prop) = {¬p} :=
  ext fun q ↦ by simpa [@Iff.comm q] using not_iff

Proof state:
p q : Prop
⊢ q ∈ {p}ᶜ ↔ q ∈ {¬p}

Tactic:
simpa [@Iff.comm q] using not_iff

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_add_toIcoMod_zero (a b : α) :
    toIocMod hp 0 (a - b) + toIcoMod hp 0 (b - a) = p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp 0 (a - b) + toIcoMod hp 0 (b - a) = p

Tactic:
rw [_root_.add_comm, toIcoMod_add_toIocMod_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_eq {l : List α} : l.any p = decide (∃ x, x ∈ l ∧ p x)

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ l.any p = decide (∃ x, x ∈ l ∧ p x = true)

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Topology/DenseEmbedding.lean
theorem subtype (de : IsDenseEmbedding e) (p : α → Prop) :
    IsDenseEmbedding (subtypeEmb p e) where
  dense :=
    dense_iff_closure_eq.2 <| by
      ext ⟨x, hx⟩
      rw [image_eq_range] at hx
      simpa [closure_subtype, ← range_comp, (· ∘ ·)]
  injective := (de.injective.comp Subtype.coe_injective).codRestrict _
  eq_induced :=
    (induced_iff_nhds_eq _).2 fun ⟨x, hx⟩ => by
      simp [subtypeEmb, nhds_subtype_eq_comap, de.isInducing.nhds_eq_comap, comap_comap,
        Function.comp_def]

Proof state:
case h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
x : β
hx : x ∈ closure (e '' {x | p x})
⊢ ⟨x, hx⟩ ∈ closure (range (subtypeEmb p e)) ↔ ⟨x, hx⟩ ∈ univ

Tactic:
rw [image_eq_range] at hx

Result:
case h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
x : β
hx✝ : x ∈ closure (e '' {x | p x})
hx : x ∈ closure (range fun x => e ↑x)
⊢ ⟨x, hx✝⟩ ∈ closure (range (subtypeEmb p e)) ↔ ⟨x, hx✝⟩ ∈ univ

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
⊢ closure (range (subtypeEmb p e)) = univ

Tactic:
ext ⟨x, hx⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
x : β
hx : x ∈ closure (e '' {x | p x})
⊢ ⟨x, hx⟩ ∈ closure (range (subtypeEmb p e)) ↔ ⟨x, hx⟩ ∈ univ

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
x✝ : { x // p x }
x : α
hx : p x
⊢ 𝓝 ⟨x, hx⟩ = comap (subtypeEmb p e) (𝓝 (subtypeEmb p e ⟨x, hx⟩))

Tactic:
simp [subtypeEmb, nhds_subtype_eq_comap, de.isInducing.nhds_eq_comap, comap_comap,
  Function.comp_def]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_self (a : α) : Icc a a = {a} :=
  Set.ext <| by simp [Icc, le_antisymm_iff, and_comm]

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ ∀ (x : α), x ∈ Icc a a ↔ x ∈ {a}

Tactic:
simp [Icc, le_antisymm_iff, and_comm]

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_zero [AddMonoid α] [StarAddMonoid α] : (0 : Matrix m n α)ᴴ = 0 :=
  Matrix.ext <| by simp

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
⊢ ∀ (i : n) (j : m), 0ᴴ i j = 0 i j

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_nat_add' [AddCommMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b]
    (f : F) (n : ℕ) (x : G) : f (↑n + x) = f x + n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddCommMonoidWithOne G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H 1 b
f : F
n : ℕ
x : G
⊢ f (↑n + x) = f x + n • b

Tactic:
simpa using map_nsmul_add f n x

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_left_comm {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε}
    (h_left_comm : ∀ a b c, f a (g b c) = g' b (f' a c)) :
    image2 f s (image2 g t u) = image2 g' t (image2 f' s u)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 (fun a b => f b a) (image2 g t u) s = image2 g' t (image2 (fun a b => f' b a) u s)

Tactic:
exact image2_assoc fun _ _ _ => h_left_comm _ _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 f s (image2 g t u) = image2 g' t (image2 f' s u)

Tactic:
rw [image2_swap f', image2_swap f]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 (fun a b => f b a) (image2 g t u) s = image2 g' t (image2 (fun a b => f' b a) u s)