harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Prod.lean
theorem prod_map_fst : (prod p q).map (fst R M M₂) = p

Proof state:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x : M
⊢ x ∈ map (fst R M M₂) (p.prod q) ↔ x ∈ p

Tactic:
simp [(⟨0, zero_mem _⟩ : ∃ x, x ∈ q)]

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ map (fst R M M₂) (p.prod q) = p

Tactic:
ext x

Result:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x : M
⊢ x ∈ map (fst R M M₂) (p.prod q) ↔ x ∈ p
-- Mathlib/Data/Finset/Fold.lean
theorem fold_ite' {g : α → β} (hb : op b b = b) (p : α → Prop) [DecidablePred p] :
    Finset.fold op b (fun i => ite (p i) (f i) (g i)) s =
      op (Finset.fold op b f (s.filter p)) (Finset.fold op b g (s.filter fun i => ¬p i))

Proof state:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : p x
⊢ op (f x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))

Tactic:
have : x ∉ Finset.filter p s := by simp [hx]

Result:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : p x
this : x ∉ filter p s
⊢ op (f x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
-- Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean
theorem riemannZeta_eulerProduct (hs : 1 < s.re) :
    Tendsto (fun n : ℕ ↦ ∏ p ∈ primesBelow n, (1 - (p : ℂ) ^ (-s))⁻¹) atTop
      (𝓝 (riemannZeta s))

Proof state:
s : ℂ
hs : 1 < s.re
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - ↑p ^ (-s))⁻¹) atTop (𝓝 (∑' (n : ℕ), (riemannZetaSummandHom ⋯) n))

Tactic:
apply eulerProduct_completely_multiplicative <| summable_riemannZetaSummand hs

Result:
no goals

Proof state:
s : ℂ
hs : 1 < s.re
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - ↑p ^ (-s))⁻¹) atTop (𝓝 (riemannZeta s))

Tactic:
rw [← tsum_riemannZetaSummand hs]

Result:
s : ℂ
hs : 1 < s.re
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - ↑p ^ (-s))⁻¹) atTop (𝓝 (∑' (n : ℕ), (riemannZetaSummandHom ⋯) n))
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_liftAt_one_self {n : ℕ} {φ : L.BoundedFormula α n} {v : α → M}
    {xs : Fin (n + 1) → M} : (φ.liftAt 1 n).Realize v xs ↔ φ.Realize v (xs ∘ castSucc)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
i : Fin n
⊢ (if ↑i < n then i.castSucc else i.succ) = i.castSucc

Tactic:
rw [if_pos i.is_lt]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
⊢ φ.Realize v (xs ∘ fun i => if ↑i < n then i.castSucc else i.succ) = φ.Realize v (xs ∘ castSucc)

Tactic:
refine congr rfl (congr rfl (funext fun i => ?_))

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
i : Fin n
⊢ (if ↑i < n then i.castSucc else i.succ) = i.castSucc

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
⊢ (liftAt 1 n φ).Realize v xs ↔ φ.Realize v (xs ∘ castSucc)

Tactic:
rw [realize_liftAt_one (refl n), iff_eq_eq]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
⊢ φ.Realize v (xs ∘ fun i => if ↑i < n then i.castSucc else i.succ) = φ.Realize v (xs ∘ castSucc)
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem tendsto_rpow_div_mul_add (a b c : ℝ) (hb : 0 ≠ b) :
    Tendsto (fun x => x ^ (a / (b * x + c))) atTop (𝓝 1)

Proof state:
a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto ?m.21718 atTop (𝓝 0)

Tactic:
simpa only [mul_zero, pow_one] using
  (tendsto_const_nhds (x := a)).mul
    (tendsto_div_pow_mul_exp_add_atTop b c 1 hb)

Result:
no goals

Proof state:
a b c : ℝ
hb : 0 ≠ b
⊢ EqOn ((rexp ∘ fun x => a * (x / (b * rexp x + c))) ∘ log) (fun x => x ^ (a / (b * x + c))) (Set.Ioi 0)

Tactic:
intro x hx

Result:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ ((rexp ∘ fun x => a * (x / (b * rexp x + c))) ∘ log) x = (fun x => x ^ (a / (b * x + c))) x

Proof state:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ ((rexp ∘ fun x => a * (x / (b * rexp x + c))) ∘ log) x = (fun x => x ^ (a / (b * x + c))) x

Tactic:
simp only [Set.mem_Ioi, Function.comp_apply] at hx ⊢

Result:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ rexp (a * (log x / (b * rexp (log x) + c))) = x ^ (a / (b * x + c))

Proof state:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ rexp (a * (log x / (b * rexp (log x) + c))) = x ^ (a / (b * x + c))

Tactic:
rw [exp_log hx, ← exp_log (rpow_pos_of_pos hx (a / (b * x + c))), log_rpow hx (a / (b * x + c))]

Result:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ rexp (a * (log x / (b * x + c))) = rexp (a / (b * x + c) * log x)

Proof state:
a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto (fun x => x ^ (a / (b * x + c))) atTop (𝓝 1)

Tactic:
refine
  Tendsto.congr' ?_
    ((tendsto_exp_nhds_zero_nhds_one.comp
          (by
            simpa only [mul_zero, pow_one] using
              (tendsto_const_nhds (x := a)).mul
                (tendsto_div_pow_mul_exp_add_atTop b c 1 hb))).comp
      tendsto_log_atTop)

Result:
a b c : ℝ
hb : 0 ≠ b
⊢ (rexp ∘ fun x => a * (x / (b * rexp x + c))) ∘ log =ᶠ[atTop] fun x => x ^ (a / (b * x + c))

Proof state:
a b c : ℝ
hb : 0 ≠ b
⊢ (rexp ∘ fun x => a * (x / (b * rexp x + c))) ∘ log =ᶠ[atTop] fun x => x ^ (a / (b * x + c))

Tactic:
apply eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ))

Result:
a b c : ℝ
hb : 0 ≠ b
⊢ EqOn ((rexp ∘ fun x => a * (x / (b * rexp x + c))) ∘ log) (fun x => x ^ (a / (b * x + c))) (Set.Ioi 0)

Proof state:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ rexp (a * (log x / (b * x + c))) = rexp (a / (b * x + c) * log x)

Tactic:
field_simp

Result:
no goals
-- Mathlib/Topology/Order/MonotoneConvergence.lean
theorem tendsto_atBot_isGLB (h_mono : Monotone f) (ha : IsGLB (Set.range f) a) :
    Tendsto f atBot (𝓝 a)

Proof state:
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsGLB (range f) a
⊢ Tendsto f atBot (𝓝 a)

Tactic:
convert tendsto_atTop_isLUB h_mono.dual ha.dual using 1

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma reflection_perm_eq_reflection_perm_iff_of_isSMulRegular (h2 : IsSMulRegular M 2) :
    P.reflection_perm i = P.reflection_perm j ↔ P.reflection i = P.reflection j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h2 : IsSMulRegular M 2
h : P.reflection_perm i = P.reflection_perm j
⊢ P.reflection i = P.reflection j

Tactic:
suffices ⇑(P.reflection i) = ⇑(P.reflection j) from DFunLike.coe_injective this

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h2 : IsSMulRegular M 2
h : P.reflection_perm i = P.reflection_perm j
⊢ ⇑(P.reflection i) = ⇑(P.reflection j)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h : P.reflection_perm i = P.reflection_perm j
h2 : IsSMulRegular (M → M) 2
⊢ ⇑(P.reflection i) = ⇑(P.reflection j)

Tactic:
exact h2 <| P.two_nsmul_reflection_eq_of_perm_eq i j h

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h2 : IsSMulRegular M 2
h : P.reflection_perm i = P.reflection_perm j
⊢ ⇑(P.reflection i) = ⇑(P.reflection j)

Tactic:
replace h2 : IsSMulRegular (M → M) 2 := IsSMulRegular.pi fun _ ↦ h2

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h : P.reflection_perm i = P.reflection_perm j
h2 : IsSMulRegular (M → M) 2
⊢ ⇑(P.reflection i) = ⇑(P.reflection j)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h2 : IsSMulRegular M 2
h : P.reflection i = P.reflection j
k : ι
⊢ P.root ((P.reflection_perm i) k) = P.root ((P.reflection_perm j) k)

Tactic:
simp [h]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h2 : IsSMulRegular M 2
⊢ P.reflection_perm i = P.reflection_perm j ↔ P.reflection i = P.reflection j

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Equiv.ext fun k ↦ P.root.injective <| by simp [h]⟩

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h2 : IsSMulRegular M 2
h : P.reflection_perm i = P.reflection_perm j
⊢ P.reflection i = P.reflection j
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_sdiff_right {α β : Type*} [GeneralizedBooleanAlgebra α] (s : Finset β) (f : β → α)
    (a : α) : (s.sup fun b => f b \ a) = s.sup f \ a

Proof state:
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
s : Finset β
f : β → α
a : α
⊢ (s.sup fun b => f b \ a) = s.sup f \ a

Tactic:
induction s using Finset.cons_induction with
| empty => rw [sup_empty, sup_empty, bot_sdiff]
| cons _ _ _ h => rw [sup_cons, sup_cons, h, sup_sdiff]

Result:
no goals

Proof state:
case empty
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
⊢ (∅.sup fun b => f b \ a) = ∅.sup f \ a

Tactic:
rw [sup_empty, sup_empty, bot_sdiff]

Result:
no goals

Proof state:
case cons
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b => f b \ a) = s✝.sup f \ a
⊢ ((cons a✝ s✝ h✝).sup fun b => f b \ a) = (cons a✝ s✝ h✝).sup f \ a

Tactic:
rw [sup_cons, sup_cons, h, sup_sdiff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
theorem of_targetAffineLocally_of_isPullback
    {P : AffineTargetMorphismProperty} [P.IsLocal]
    {X Y UX UY : Scheme.{u}} [IsAffine UY] {f : X ⟶ Y} {iY : UY ⟶ Y} [IsOpenImmersion iY]
    {iX : UX ⟶ X} {f' : UX ⟶ UY} (h : IsPullback iX f' f iY) (hf : targetAffineLocally P f) :
    P f'

Proof state:
P : AffineTargetMorphismProperty
inst✝² : P.IsLocal
X Y UX UY : Scheme
inst✝¹ : IsAffine UY
f : X ⟶ Y
iY : UY ⟶ Y
inst✝ : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
hf : targetAffineLocally P f
⊢ P (pullback.snd f iY)

Tactic:
exact (P.arrow_mk_iso_iff
  (morphismRestrictOpensRange f _)).mp (hf ⟨_, isAffineOpen_opensRange iY⟩)

Result:
no goals

Proof state:
P : AffineTargetMorphismProperty
inst✝² : P.IsLocal
X Y UX UY : Scheme
inst✝¹ : IsAffine UY
f : X ⟶ Y
iY : UY ⟶ Y
inst✝ : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
hf : targetAffineLocally P f
⊢ P f'

Tactic:
rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_snd]

Result:
P : AffineTargetMorphismProperty
inst✝² : P.IsLocal
X Y UX UY : Scheme
inst✝¹ : IsAffine UY
f : X ⟶ Y
iY : UY ⟶ Y
inst✝ : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
hf : targetAffineLocally P f
⊢ P (pullback.snd f iY)
-- Mathlib/Algebra/LinearRecurrence.lean
theorem mkSol_eq_init (init : Fin E.order → α) : ∀ n : Fin E.order, E.mkSol init n = init n

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : Fin E.order
⊢ (if h : ↑n < E.order then init ⟨↑n, h⟩
    else
      ∑ k : Fin E.order,
        let_fun x := ⋯;
        E.coeffs k * E.mkSol init (↑n - E.order + ↑k)) =
    init n

Tactic:
simp only [n.is_lt, dif_pos, Fin.mk_val, Fin.eta]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
⊢ ∀ (n : Fin E.order), E.mkSol init ↑n = init n

Tactic:
intro n

Result:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : Fin E.order
⊢ E.mkSol init ↑n = init n

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : Fin E.order
⊢ E.mkSol init ↑n = init n

Tactic:
rw [mkSol]

Result:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : Fin E.order
⊢ (if h : ↑n < E.order then init ⟨↑n, h⟩
    else
      ∑ k : Fin E.order,
        let_fun x := ⋯;
        E.coeffs k * E.mkSol init (↑n - E.order + ↑k)) =
    init n
-- Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
/-- Any morphism between affine schemes that is surjective on global sections is a
closed immersion. -/
lemma of_surjective_of_isAffine {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y)
    (h : Function.Surjective (f.appTop)) : IsClosedImmersion f

Proof state:
case h
X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Tactic:
exact h

Result:
no goals

Proof state:
X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ IsClosedImmersion (Spec.map (Scheme.Hom.appTop f))

Tactic:
apply spec_of_surjective

Result:
case h
X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Proof state:
X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ IsClosedImmersion f

Tactic:
rw [MorphismProperty.arrow_mk_iso_iff @IsClosedImmersion (arrowIsoSpecΓOfIsAffine f)]

Result:
X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ IsClosedImmersion (Spec.map (Scheme.Hom.appTop f))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
    {x : BitVec w} {i : Nat} (hx : x.getLsbD i = true) :
    setWidth w (x.setWidth (i + 1)) =
      setWidth w (x.setWidth i) ||| (twoPow w i)

Proof state:
case pos
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = true
h : i < w
⊢ (decide (i < i + 1) && x.getLsbD i) = (decide (i < i) && x.getLsbD i || (twoPow w i).getLsbD i)

Tactic:
simp [hx, h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = true
⊢ setWidth w (setWidth (i + 1) x) = setWidth w (setWidth i x) ||| twoPow w i

Tactic:
ext k h

Result:
case pred
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = true
k : Nat
h : k < w
⊢ (setWidth w (setWidth (i + 1) x)).getLsbD k = (setWidth w (setWidth i x) ||| twoPow w i).getLsbD k

Proof state:
case neg
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = true
k : Nat
h : k < w
hik : ¬i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k || (twoPow w i).getLsbD k)

Tactic:
by_cases hik' : k < i + 1 <;> simp [hik, hik'] <;> omega

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = true
k : Nat
h : k < w
⊢ (setWidth w (setWidth (i + 1) x)).getLsbD k = (setWidth w (setWidth i x) ||| twoPow w i).getLsbD k

Tactic:
simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]

Result:
case pred
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = true
k : Nat
h : k < w
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k || (twoPow w i).getLsbD k)

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = true
k : Nat
h : k < w
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k || (twoPow w i).getLsbD k)

Tactic:
by_cases hik : i = k

Result:
case pos
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = true
k : Nat
h : k < w
hik : i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k || (twoPow w i).getLsbD k)

case neg
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = true
k : Nat
h : k < w
hik : ¬i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k || (twoPow w i).getLsbD k)

Proof state:
case pos
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = true
k : Nat
h : k < w
hik : i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k || (twoPow w i).getLsbD k)

Tactic:
subst hik

Result:
case pos
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = true
h : i < w
⊢ (decide (i < i + 1) && x.getLsbD i) = (decide (i < i) && x.getLsbD i || (twoPow w i).getLsbD i)
-- Mathlib/Data/Fintype/Pi.lean
theorem piFinset_empty [Nonempty α] : piFinset (fun _ => ∅ : ∀ i, Finset (δ i)) = ∅

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : Nonempty α
⊢ (piFinset fun x => ∅) = ∅

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i] = b[i]) : a = b

Proof state:
case h₁
α : Type u_1
n : Nat
a b : Vector α n
h : ∀ (i : Nat) (x : i < n), a[i] = b[i]
⊢ a.size = b.size

Tactic:
rw [a.size_toArray, b.size_toArray]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a b : Vector α n
h : ∀ (i : Nat) (x : i < n), a[i] = b[i]
⊢ a.toArray = b.toArray

Tactic:
apply Array.ext

Result:
case h₁
α : Type u_1
n : Nat
a b : Vector α n
h : ∀ (i : Nat) (x : i < n), a[i] = b[i]
⊢ a.size = b.size

case h₂
α : Type u_1
n : Nat
a b : Vector α n
h : ∀ (i : Nat) (x : i < n), a[i] = b[i]
⊢ ∀ (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b.size), a.toArray[i] = b.toArray[i]

Proof state:
case h₂
α : Type u_1
n : Nat
a b : Vector α n
h : ∀ (i : Nat) (x : i < n), a[i] = b[i]
⊢ ∀ (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b.size), a.toArray[i] = b.toArray[i]

Tactic:
intro i hi _

Result:
case h₂
α : Type u_1
n : Nat
a b : Vector α n
h : ∀ (i : Nat) (x : i < n), a[i] = b[i]
i : Nat
hi : i < a.size
hi₂✝ : i < b.size
⊢ a.toArray[i] = b.toArray[i]

Proof state:
case h₂
α : Type u_1
n : Nat
a b : Vector α n
h : ∀ (i : Nat) (x : i < n), a[i] = b[i]
i : Nat
hi : i < a.size
hi₂✝ : i < b.size
⊢ a.toArray[i] = b.toArray[i]

Tactic:
rw [a.size_toArray] at hi

Result:
case h₂
α : Type u_1
n : Nat
a b : Vector α n
h : ∀ (i : Nat) (x : i < n), a[i] = b[i]
i : Nat
hi✝ : i < a.size
hi : i < n
hi₂✝ : i < b.size
⊢ a.toArray[i] = b.toArray[i]

Proof state:
α : Type u_1
n : Nat
a b : Vector α n
h : ∀ (i : Nat) (x : i < n), a[i] = b[i]
⊢ a = b

Tactic:
apply Vector.toArray_inj.1

Result:
α : Type u_1
n : Nat
a b : Vector α n
h : ∀ (i : Nat) (x : i < n), a[i] = b[i]
⊢ a.toArray = b.toArray

Proof state:
case h₂
α : Type u_1
n : Nat
a b : Vector α n
h : ∀ (i : Nat) (x : i < n), a[i] = b[i]
i : Nat
hi✝ : i < a.size
hi : i < n
hi₂✝ : i < b.size
⊢ a.toArray[i] = b.toArray[i]

Tactic:
exact h i hi

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_le_iff (f g : 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_1) [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 g : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ (∀ (a_1 : ↑(spectrum R a)),
      { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } a_1 ≤
        { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ } a_1) ↔
    ∀ x ∈ spectrum R a, f x ≤ g x

Tactic:
simp

Result:
no goals

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.787295) [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 g : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum R a, f x ≤ g x

Tactic:
rw [cfc_apply f a, cfc_apply g a, cfcHom_le_iff (show p a from ha), ContinuousMap.le_def]

Result:
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_1) [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 g : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ (∀ (a_1 : ↑(spectrum R a)),
      { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } a_1 ≤
        { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ } a_1) ↔
    ∀ x ∈ spectrum R a, f x ≤ g x