harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean
lemma compactSpace {R S A : Type*} [Semifield R] [Semifield S] [Ring A]
    [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [TopologicalSpace R]
    [TopologicalSpace S] {a : A} (f : C(S, R)) (h : SpectrumRestricts a f)
    [h_cpct : CompactSpace (spectrum S a)] : CompactSpace (spectrum R a)

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : Semifield R
inst✝⁷ : Semifield S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace S
a : A
f : C(S, R)
h : SpectrumRestricts a ⇑f
h_cpct : CompactSpace ↑(spectrum S a)
⊢ CompactSpace ↑(spectrum R a)

Tactic:
rw [← isCompact_iff_compactSpace] at h_cpct ⊢

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : Semifield R
inst✝⁷ : Semifield S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace S
a : A
f : C(S, R)
h : SpectrumRestricts a ⇑f
h_cpct : IsCompact (spectrum S a)
⊢ IsCompact (spectrum R a)

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : Semifield R
inst✝⁷ : Semifield S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace S
a : A
f : C(S, R)
h : SpectrumRestricts a ⇑f
h_cpct : IsCompact (spectrum S a)
⊢ IsCompact (spectrum R a)

Tactic:
exact h.image ▸ h_cpct.image (map_continuous f)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.pow (hp : Monic p) : ∀ n : ℕ, Monic (p ^ n)
  | 0 => monic_one
  | n + 1 => by
    rw [pow_succ]
    exact (Monic.pow hp n).mul hp

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ (n + 1)).Monic

Tactic:
rw [pow_succ]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ n * p).Monic

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ n * p).Monic

Tactic:
exact (Monic.pow hp n).mul hp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem norm_eq_iInf_iff_real_inner_eq_zero (K : Submodule ℝ F) {u : F} {v : F} (hv : v ∈ K) :
    (‖u - v‖ = ⨅ w : (↑K : Set F), ‖u - w‖) ↔ ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0 :=
  Iff.intro
    (by
      intro h
      have h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
have : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 := by
  intro w hw
  let w' := w - v
  have : w' ∈ K := Submodule.sub_mem _ hw hv
  have h₁ := h w' this
  exact le_of_eq h₁

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
this : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖
-- Mathlib/RingTheory/Valuation/Integers.lean
lemma isPrincipal_iff_exists_isGreatest (hv : Integers v O) {I : Ideal O} :
    I.IsPrincipal ↔ ∃ x, IsGreatest (v ∘ algebraMap O F '' I) x

Proof state:
case mp.mk.intro.refine_2
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = Submodule.span O {x}
⊢ (⇑v ∘ ⇑(algebraMap O F)) x ∈ upperBounds (⇑v ∘ ⇑(algebraMap O F) '' ↑I)

Tactic:
intro y hy

Result:
case mp.mk.intro.refine_2
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = Submodule.span O {x}
y : Γ₀
hy : y ∈ ⇑v ∘ ⇑(algebraMap O F) '' ↑I
⊢ y ≤ (⇑v ∘ ⇑(algebraMap O F)) x

Proof state:
case mp.mk.intro.refine_2
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = Submodule.span O {x}
y : Γ₀
hy : ∃ x_1, x ∣ x_1 ∧ v ((algebraMap O F) x_1) = y
⊢ y ≤ (⇑v ∘ ⇑(algebraMap O F)) x

Tactic:
obtain ⟨y, hy, rfl⟩ := hy

Result:
case mp.mk.intro.refine_2.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = Submodule.span O {x}
y : O
hy : x ∣ y
⊢ v ((algebraMap O F) y) ≤ (⇑v ∘ ⇑(algebraMap O F)) x
-- Mathlib/Topology/Order/NhdsSet.lean
theorem hasBasis_nhdsSet_Iic_Iic (a : α) [NeBot (𝓝[>] a)] :
    HasBasis (𝓝ˢ (Iic a)) (a < ·) Iic

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : (𝓝[>] a).NeBot
this : Nonempty ↑(Ioi a)
⊢ (𝓝ˢ (Iic a)).HasBasis (fun x => a < x) Iic

Tactic:
refine (hasBasis_nhdsSet_Iic_Iio _).to_hasBasis
  (fun c hc ↦ ?_) (fun _ h ↦ ⟨_, h, Iio_subset_Iic_self⟩)

Result:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : (𝓝[>] a).NeBot
this : Nonempty ↑(Ioi a)
c : α
hc : a < c
⊢ ∃ i', a < i' ∧ Iic i' ⊆ Iio c

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : (𝓝[>] a).NeBot
this : Nonempty ↑(Ioi a)
c : α
hc : a < c
⊢ ∃ i', a < i' ∧ Iic i' ⊆ Iio c

Tactic:
simpa only [Iic_subset_Iio] using Filter.nonempty_of_mem (Ioo_mem_nhdsGT hc)

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : (𝓝[>] a).NeBot
⊢ (𝓝ˢ (Iic a)).HasBasis (fun x => a < x) Iic

Tactic:
have : Nonempty (Ioi a) :=
  (Filter.nonempty_of_mem (self_mem_nhdsWithin : Ioi a ∈ 𝓝[>] a)).to_subtype

Result:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : (𝓝[>] a).NeBot
this : Nonempty ↑(Ioi a)
⊢ (𝓝ˢ (Iic a)).HasBasis (fun x => a < x) Iic
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma leftShift_neg (a n' : ℤ) (hn' : n + a = n') :
    (-γ).leftShift a n' hn' = -γ.leftShift a n' hn'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn') (-γ) = -γ.leftShift a n' hn'

Tactic:
apply _root_.map_neg

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
⊢ (-γ).leftShift a n' hn' = -γ.leftShift a n' hn'

Tactic:
change leftShiftAddEquiv K L n a n' hn' (-γ) = _

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn') (-γ) = -γ.leftShift a n' hn'
-- Mathlib/Topology/VectorBundle/Constructions.lean
theorem Trivialization.continuousLinearEquivAt_prod {e₁ : Trivialization F₁ (π F₁ E₁)}
    {e₂ : Trivialization F₂ (π F₂ E₂)} [e₁.IsLinear 𝕜] [e₂.IsLinear 𝕜] {x : B}
    (hx : x ∈ (e₁.prod e₂).baseSet) :
    (e₁.prod e₂).continuousLinearEquivAt 𝕜 x hx =
      (e₁.continuousLinearEquivAt 𝕜 x hx.1).prod (e₂.continuousLinearEquivAt 𝕜 x hx.2)

Proof state:
case h.h.mk
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : Trivialization.IsLinear 𝕜 e₁
inst✝ : Trivialization.IsLinear 𝕜 e₂
x : B
hx : x ∈ (e₁.prod e₂).baseSet
v₁ : E₁ x
v₂ : E₂ x
⊢ (fun y =>
        (↑{ toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet), target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯,
                continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, baseSet := e₁.baseSet ∩ e₂.baseSet,
                open_baseSet := ⋯, source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ }
            { proj := x, snd := y }).2)
      (v₁, v₂) =
    ((continuousLinearEquivAt 𝕜 e₁ x ⋯).prod (continuousLinearEquivAt 𝕜 e₂ x ⋯)) (v₁, v₂)

Tactic:
exact (congr_arg Prod.snd (prod_apply 𝕜 hx.1 hx.2 v₁ v₂) :)

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem squarefree_iff_minSqFac {n : ℕ} : Squarefree n ↔ n.minSqFac = none

Proof state:
case mp.some
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
d : ℕ
e : n.minSqFac = some d
⊢ some d = none

Tactic:
rw [e] at this

Result:
case mp.some
n : ℕ
H : Squarefree n
d : ℕ
this : n.MinSqFacProp (some d)
e : n.minSqFac = some d
⊢ some d = none

Proof state:
case mpr
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : n.minSqFac = none
⊢ Squarefree n

Tactic:
rwa [H] at this

Result:
no goals

Proof state:
n : ℕ
this : n.MinSqFacProp n.minSqFac
⊢ Squarefree n ↔ n.minSqFac = none

Tactic:
constructor <;> intro H

Result:
case mp
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
⊢ n.minSqFac = none

case mpr
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : n.minSqFac = none
⊢ Squarefree n

Proof state:
case mp.none
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
e : n.minSqFac = none
⊢ none = none

Tactic:
rfl

Result:
no goals

Proof state:
case mp.some
n : ℕ
H : Squarefree n
d : ℕ
this : n.MinSqFacProp (some d)
e : n.minSqFac = some d
⊢ some d = none

Tactic:
cases squarefree_iff_prime_squarefree.1 H _ this.1 this.2.1

Result:
no goals

Proof state:
case mp
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
⊢ n.minSqFac = none

Tactic:
rcases e : n.minSqFac with - | d

Result:
case mp.none
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
e : n.minSqFac = none
⊢ none = none

case mp.some
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
d : ℕ
e : n.minSqFac = some d
⊢ some d = none

Proof state:
n : ℕ
⊢ Squarefree n ↔ n.minSqFac = none

Tactic:
have := minSqFac_has_prop n

Result:
n : ℕ
this : n.MinSqFacProp n.minSqFac
⊢ Squarefree n ↔ n.minSqFac = none
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem le_div_iff_mul_le' : b ≤ c / a ↔ a * b ≤ c

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ b ≤ c / a ↔ a * b ≤ c

Tactic:
rw [le_div_iff_mul_le, mul_comm]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_eq_of_bijective (f : ∀ i, i < n → α) (hf : ∀ a ∈ s, ∃ i, ∃ h : i < n, f i h = a)
    (hf' : ∀ i (h : i < n), f i h ∈ s)
    (f_inj : ∀ i j (hi : i < n) (hj : j < n), f i hi = f j hj → i = j) : #s = n

Proof state:
case H
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun i => f ↑i ⋯) (range n).attach
⊢ Injective fun i => f ↑i ⋯

Tactic:
intro ⟨i, hi⟩ ⟨j, hj⟩ eq

Result:
case H
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun i => f ↑i ⋯) (range n).attach
i : ℕ
hi : i ∈ range n
j : ℕ
hj : j ∈ range n
eq : (fun i => f ↑i ⋯) ⟨i, hi⟩ = (fun i => f ↑i ⋯) ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma pow_monotone {a : A} (ha : 1 ≤ a) : Monotone (a ^ · : ℕ → A)

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ∀ x ∈ spectrum ℝ a, 1 ≤ x
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m

Tactic:
peel ha with x hx _

Result:
case h.h
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ∀ x ∈ spectrum ℝ a, 1 ≤ x
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
x : ℝ
hx : x ∈ spectrum ℝ a
this : 1 ≤ x
⊢ x ^ n ≤ x ^ m

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
⊢ Monotone fun x => a ^ x

Tactic:
have ha' : 0 ≤ a := zero_le_one.trans ha

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
⊢ Monotone fun x => a ^ x

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ a ^ n ≤ a ^ m

Tactic:
rw [← cfc_pow_id (R := ℝ) a, ← cfc_pow_id (R := ℝ) a, cfc_le_iff ..]

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ (fun x => a ^ x) n ≤ (fun x => a ^ x) m

Tactic:
simp only

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ a ^ n ≤ a ^ m

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
⊢ Monotone fun x => a ^ x

Tactic:
intro n m hnm

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ (fun x => a ^ x) n ≤ (fun x => a ^ x) m

Proof state:
case h.h
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ∀ x ∈ spectrum ℝ a, 1 ≤ x
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
x : ℝ
hx : x ∈ spectrum ℝ a
this : 1 ≤ x
⊢ x ^ n ≤ x ^ m

Tactic:
exact pow_le_pow_right₀ (ha x hx) hnm

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m

Tactic:
rw [CFC.one_le_iff (R := ℝ) a] at ha

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ∀ x ∈ spectrum ℝ a, 1 ≤ x
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n)

Proof state:
s n : Nat
⊢ range' s n = range' (s + 0) n

Tactic:
rfl

Result:
no goals

Proof state:
s n : Nat
⊢ range' s n = map (fun x => s + x) (range n)

Tactic:
rw [range_eq_range', map_add_range']

Result:
s n : Nat
⊢ range' s n = range' (s + 0) n
-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem accPt_subtype {p o : Ordinal} (S : Set Ordinal) (hpo : p < o) :
    AccPt p (𝓟 S) ↔ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))

Proof state:
case h.right
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
q : Ordinal.{u_1}
hq : p = succ q
y✝ : ↑(Iio o)
mem : y✝ ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S
aux1 : q < ↑y✝
aux2 : ↑y✝ < p + 1
⊢ y✝ = ⟨p, hpo⟩

Tactic:
rw [Subtype.mk_eq_mk]

Result:
case h.right
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
q : Ordinal.{u_1}
hq : p = succ q
y✝ : ↑(Iio o)
mem : y✝ ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S
aux1 : q < ↑y✝
aux2 : ↑y✝ < p + 1
⊢ ↑y✝ = p

Proof state:
case mpr
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))
⊢ AccPt p (𝓟 S)

Tactic:
rw [accPt_iff_nhds] at *

Result:
case mpr
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
⊢ ∀ U ∈ 𝓝 p, ∃ y ∈ U ∩ S, y ≠ p

Proof state:
o : Ordinal.{u_1}
S u : Set Ordinal.{u_1}
hpo : 0 < o
h : ∀ U ∈ 𝓝 ⟨0, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨0, hpo⟩
hu : u ∈ 𝓝 0
ho : ¬0 + 1 < o
hp : o = 0 + 1
⊢ False

Tactic:
obtain ⟨x, hx⟩ := h Set.univ univ_mem

Result:
case intro
o : Ordinal.{u_1}
S u : Set Ordinal.{u_1}
hpo : 0 < o
h : ∀ U ∈ 𝓝 ⟨0, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨0, hpo⟩
hu : u ∈ 𝓝 0
ho : ¬0 + 1 < o
hp : o = 0 + 1
x : ↑(Iio o)
hx : x ∈ Set.univ ∩ Iio o ↓∩ S ∧ x ≠ ⟨0, hpo⟩
⊢ False

Proof state:
case mp
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
⊢ AccPt p (𝓟 S) → AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))

Tactic:
intro h

Result:
case mp
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : AccPt p (𝓟 S)
⊢ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))

Proof state:
case mp.intro
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 p, ∃ y ∈ U ∩ S, y ≠ p
plim : p.IsLimit
u : Set ↑(Iio o)
hu : u ∈ 𝓝 ⟨p, hpo⟩
l : ↑(Iio o)
hl : l < ⟨p, hpo⟩ ∧ Ioc l ⟨p, hpo⟩ ⊆ u
⊢ ∃ y ∈ u ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩

Tactic:
obtain ⟨x, hx⟩ := h (Ioo l (p + 1)) (Ioo_mem_nhds hl.1 (lt_add_one _))

Result:
case mp.intro.intro
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 p, ∃ y ∈ U ∩ S, y ≠ p
plim : p.IsLimit
u : Set ↑(Iio o)
hu : u ∈ 𝓝 ⟨p, hpo⟩
l : ↑(Iio o)
hl : l < ⟨p, hpo⟩ ∧ Ioc l ⟨p, hpo⟩ ⊆ u
x : Ordinal.{u_1}
hx : x ∈ Ioo (↑l) (p + 1) ∩ S ∧ x ≠ p
⊢ ∃ y ∈ u ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
-- Mathlib/Combinatorics/SetFamily/Intersecting.lean
theorem Intersecting.card_le [Fintype α] {s : Finset α} (hs : (s : Set α).Intersecting) :
    2 * #s ≤ Fintype.card α

Proof state:
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
⊢ 2 * #s ≤ Fintype.card α

Tactic:
refine (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' ?_

Result:
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
⊢ 2 * #s = #(s.disjUnion (map { toFun := compl, inj' := ⋯ } s) ⋯)

Proof state:
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
⊢ 2 * #s ≤ Fintype.card α

Tactic:
classical
  refine (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' ?_
  rw [Nat.two_mul, card_disjUnion, card_map]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
⊢ 2 * #s = #(s.disjUnion (map { toFun := compl, inj' := ⋯ } s) ⋯)

Tactic:
rw [Nat.two_mul, card_disjUnion, card_map]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma equation_iff' (x y : R) : W'.Equation x y ↔
    y ^ 2 + W'.a₁ * x * y + W'.a₃ * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆) = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x y ↔ y ^ 2 + W'.a₁ * x * y + W'.a₃ * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆) = 0

Tactic:
rw [Equation, evalEval_polynomial]

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem sort_univ (n : ℕ) : Finset.univ.sort (fun x y : Fin n => x ≤ y) = List.finRange n :=
  List.eq_of_perm_of_sorted
    (List.perm_of_nodup_nodup_toFinset_eq
      (Finset.univ.sort_nodup _) (List.nodup_finRange n) (by simp))
    (Finset.univ.sort_sorted LE.le)
    (List.pairwise_le_finRange n)

Proof state:
n : ℕ
⊢ (Finset.sort (fun x y => x ≤ y) Finset.univ).toFinset = (List.finRange n).toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem map_eq_zero_iff (h : IsAdjoinRoot S f) {p} : h.map p = 0 ↔ f ∣ p

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRoot S f
p : R[X]
⊢ h.map p = 0 ↔ f ∣ p

Tactic:
rw [← h.mem_ker_map, RingHom.mem_ker]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem heq_ext_iff {k l : ℕ} (h : k = l) {i : Fin k} {j : Fin l} :
    HEq i j ↔ (i : ℕ) = (j : ℕ)

Proof state:
k l : ℕ
h : k = l
i : Fin k
j : Fin l
⊢ HEq i j ↔ ↑i = ↑j

Tactic:
subst h

Result:
k : ℕ
i j : Fin k
⊢ HEq i j ↔ ↑i = ↑j

Proof state:
k : ℕ
i j : Fin k
⊢ HEq i j ↔ ↑i = ↑j

Tactic:
simp [val_eq_val]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_setIfInBounds_self (as : Array α) {i : Nat} (v : α) :
    (as.setIfInBounds i v)[i]? = if i < as.size then some v else none

Proof state:
α : Type u_1
as : Array α
i : Nat
v : α
⊢ (as.setIfInBounds i v)[i]? = if i < as.size then some v else none

Tactic:
simp [getElem?_setIfInBounds]

Result:
no goals
-- Mathlib/GroupTheory/Submonoid/Center.lean
theorem _root_.MulEquivClass.apply_mem_center {F} [EquivLike F M N] [Mul M] [Mul N]
    [MulEquivClass F M N] (e : F) {x : M} (hx : x ∈ Set.center M) : e x ∈ Set.center N

Proof state:
case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
⊢ ∀ (a b : N), a * b * e x = a * (b * e x)

Tactic:
intros

Result:
case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
a✝ b✝ : N
⊢ a✝ * b✝ * e x = a✝ * (b✝ * e x)

Proof state:
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
⊢ e✝ x ∈ Set.center N

Tactic:
show e x ∈ Set.center N

Result:
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
⊢ e x ∈ Set.center N

Proof state:
case right_assoc.a
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
a✝ b✝ : N
⊢ e.symm (a✝ * b✝ * e x) = e.symm (a✝ * (b✝ * e x))

Tactic:
simp only [map_mul, e.symm_apply_apply, (isMulCentral_iff _).mp hx]

Result:
no goals

Proof state:
case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
a✝ b✝ : N
⊢ a✝ * b✝ * e x = a✝ * (b✝ * e x)

Tactic:
apply e.symm.injective

Result:
case right_assoc.a
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
a✝ b✝ : N
⊢ e.symm (a✝ * b✝ * e x) = e.symm (a✝ * (b✝ * e x))

Proof state:
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
⊢ e x ∈ Set.center N

Tactic:
constructor <;>
(intros; apply e.symm.injective;
  simp only [map_mul, e.symm_apply_apply, (isMulCentral_iff _).mp hx])

Result:
no goals

Proof state:
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e : F
x : M
hx : x ∈ Set.center M
⊢ e x ∈ Set.center N

Tactic:
let e := MulEquivClass.toMulEquiv e

Result:
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
⊢ e✝ x ∈ Set.center N
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a

Proof state:
α : Type u_1
a : α
l : List α
⊢ a ∈ l ↔ ∃ n, l.get? n = some a

Tactic:
simp [getElem?_eq_some_iff, Fin.exists_iff, mem_iff_get]

Result:
no goals