harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem exists_gt (f : CauSeq α abs) : ∃ a : α, f < const a :=
  let ⟨K, H⟩ := f.bounded
  ⟨K + 1, 1, zero_lt_one, 0, fun i _ => by
    rw [sub_apply, const_apply, le_sub_iff_add_le', add_le_add_iff_right]
    exact le_of_lt (abs_lt.1 (H _)).2⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |↑f i| < K
i : ℕ
x✝ : i ≥ 0
⊢ ↑f i ≤ K

Tactic:
exact le_of_lt (abs_lt.1 (H _)).2

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |↑f i| < K
i : ℕ
x✝ : i ≥ 0
⊢ 1 ≤ ↑(const (K + 1) - f) i

Tactic:
rw [sub_apply, const_apply, le_sub_iff_add_le', add_le_add_iff_right]

Result:
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |↑f i| < K
i : ℕ
x✝ : i ≥ 0
⊢ ↑f i ≤ K
-- Mathlib/Logic/Equiv/Fin.lean
theorem finSuccAboveEquiv_symm_apply_ne_last {p : Fin (n + 1)} (h : p ≠ Fin.last n)
    (x : { x : Fin (n + 1) // x ≠ p }) :
    (finSuccAboveEquiv p).symm x = (p.castLT (Fin.val_lt_last h)).predAbove x

Proof state:
n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x // x ≠ p }
⊢ (finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x

Tactic:
rw [← Option.some_inj]

Result:
n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x // x ≠ p }
⊢ some ((finSuccAboveEquiv p).symm x) = some ((p.castLT ⋯).predAbove ↑x)

Proof state:
n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x // x ≠ p }
⊢ some ((finSuccAboveEquiv p).symm x) = some ((p.castLT ⋯).predAbove ↑x)

Tactic:
simpa [finSuccAboveEquiv] using finSuccEquiv'_ne_last_apply h x.property

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
@[simp] lemma dens_mul_card (s : Finset α) : s.dens * Fintype.card α = s.card

Proof state:
α : Type u_2
inst✝ : Fintype α
s : Finset α
⊢ s.dens * ↑(Fintype.card α) = ↑(#s)

Tactic:
rw [mul_comm, card_mul_dens]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem NNReal.tendsto_const_div_atTop_nhds_zero_nat (C : ℝ≥0) :
    Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0)

Proof state:
C : ℝ≥0
⊢ Tendsto (fun n => C / ↑n) atTop (𝓝 0)

Tactic:
simpa using tendsto_const_nhds.mul NNReal.tendsto_inverse_atTop_nhds_zero_nat

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem ofFinsupp_add {a b} : (⟨a + b⟩ : SkewMonoidAlgebra k G) = ⟨a⟩ + ⟨b⟩ :=
  show _ = add _ _ by rw [add]

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a b : G →₀ k
⊢ { toFinsupp := a + b } = SkewMonoidAlgebra.add { toFinsupp := a } { toFinsupp := b }

Tactic:
rw [add]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma closure_range_comap :
    closure (Set.range (comap f)) = zeroLocus (RingHom.ker f)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ closure (Set.range ⇑(comap f)) = zeroLocus ↑(RingHom.ker f)

Tactic:
rw [← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_range_comap, zeroLocus_radical]

Result:
no goals
-- Mathlib/RingTheory/Artinian/Module.lean
theorem IsArtinian.isSemisimpleModule_iff_jacobson [IsArtinian R M] :
    IsSemisimpleModule R M ↔ Module.jacobson R M = ⊥ :=
  ⟨fun _ ↦ IsSemisimpleModule.jacobson_eq_bot R M, fun h ↦
    have ⟨s, hs⟩ := Finset.exists_inf_le (Subtype.val (p := fun m : Submodule R M ↦ IsCoatom m))
    have _ (m : s) : IsSimpleModule R (M ⧸ m.1.1) := isSimpleModule_iff_isCoatom.mpr m.1.2
    let f : M →ₗ[R] ∀ m : s, M ⧸ m.1.1 := LinearMap.pi fun m ↦ m.1.1.mkQ
    .of_injective f <| LinearMap.ker_eq_bot.mp <| le_bot_iff.mp fun x hx ↦ by
      rw [← h, Module.jacobson, Submodule.mem_sInf]
      exact fun m hm ↦ hs ⟨m, hm⟩ <| Submodule.mem_finset_inf.mpr fun i hi ↦
        (Submodule.Quotient.mk_eq_zero i.1).mp <| congr_fun hx ⟨i, hi⟩⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
h : Module.jacobson R M = ⊥
s : Finset { m // IsCoatom m }
hs : ∀ (a : { m // IsCoatom m }), s.inf Subtype.val ≤ ↑a
x✝ : ∀ (m : { x // x ∈ s }), IsSimpleModule R (M ⧸ ↑↑m)
f : M →ₗ[R] (m : { x // x ∈ s }) → M ⧸ ↑↑m := LinearMap.pi fun m => (↑↑m).mkQ
x : M
hx : x ∈ LinearMap.ker f
⊢ ∀ p ∈ {m | IsCoatom m}, x ∈ p

Tactic:
exact fun m hm ↦ hs ⟨m, hm⟩ <| Submodule.mem_finset_inf.mpr fun i hi ↦
  (Submodule.Quotient.mk_eq_zero i.1).mp <| congr_fun hx ⟨i, hi⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
h : Module.jacobson R M = ⊥
s : Finset { m // IsCoatom m }
hs : ∀ (a : { m // IsCoatom m }), s.inf Subtype.val ≤ ↑a
x✝ : ∀ (m : { x // x ∈ s }), IsSimpleModule R (M ⧸ ↑↑m)
f : M →ₗ[R] (m : { x // x ∈ s }) → M ⧸ ↑↑m := LinearMap.pi fun m => (↑↑m).mkQ
x : M
hx : x ∈ LinearMap.ker f
⊢ x ∈ ⊥

Tactic:
rw [← h, Module.jacobson, Submodule.mem_sInf]

Result:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
h : Module.jacobson R M = ⊥
s : Finset { m // IsCoatom m }
hs : ∀ (a : { m // IsCoatom m }), s.inf Subtype.val ≤ ↑a
x✝ : ∀ (m : { x // x ∈ s }), IsSimpleModule R (M ⧸ ↑↑m)
f : M →ₗ[R] (m : { x // x ∈ s }) → M ⧸ ↑↑m := LinearMap.pi fun m => (↑↑m).mkQ
x : M
hx : x ∈ LinearMap.ker f
⊢ ∀ p ∈ {m | IsCoatom m}, x ∈ p
-- Mathlib/Data/Fin/Basic.lean
theorem coe_int_add_eq_ite {n : Nat} (u v : Fin n) :
    ((u + v : Fin n) : Int) = if (u + v : ℕ) < n then (u + v : Int) else (u + v : Int) - n

Proof state:
case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = ↑↑u + ↑↑v

Tactic:
rw [ofNat_emod, Int.emod_eq_of_lt] <;> omega

Result:
no goals

Proof state:
n : ℕ
u v : Fin n
⊢ ↑↑(u + v) = if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n

Tactic:
rw [Fin.add_def]

Result:
n : ℕ
u v : Fin n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n

Proof state:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = ↑↑u + ↑↑v - ↑n

Tactic:
rw [ofNat_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt] <;> omega

Result:
no goals

Proof state:
n : ℕ
u v : Fin n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n

Tactic:
split

Result:
case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = ↑↑u + ↑↑v

case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = ↑↑u + ↑↑v - ↑n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem set_map {f : α → β} {l : List α} {n : Nat} {a : α} :
    (map f l).set n (f a) = map f (l.set n a)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
n : Nat
a : α
⊢ (map f l).set n (f a) = map f (l.set n a)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem inv_hom_id_assoc (f : X ⟶ Y) [I : IsIso f] {Z} (g : Y ⟶ Z) : inv f ≫ f ≫ g = g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : IsIso f
Z : C
g : Y ⟶ Z
⊢ inv f ≫ f ≫ g = g

Tactic:
simp [← Category.assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem bind_zero_left (f : α → Measure β) : bind (0 : Measure α) f = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → Measure β
⊢ bind 0 f = 0

Tactic:
simp [bind]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem prod_X_sub_C_coeff_card_pred (s : Finset ι) (f : ι → R) (hs : 0 < #s) :
    (∏ i ∈ s, (X - C (f i))).coeff (#s - 1) = -∑ i ∈ s, f i

Proof state:
R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < #s
⊢ (∏ i ∈ s, (X - C (f i))).coeff (#s - 1) = -∑ i ∈ s, f i

Tactic:
simpa using multiset_prod_X_sub_C_coeff_card_pred (s.1.map f) (by simpa using hs)

Result:
no goals

Proof state:
R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < #s
⊢ 0 < (Multiset.map f s.val).card

Tactic:
simpa using hs

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma whiskerLeft_fst (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :
    (X ◁ g) ≫ fst _ _ = fst _ _ :=
  (tensorHom_fst _ _).trans (by simp)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ fst X Y₁ ≫ 𝟙 X = fst X Y₁

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem map_comp_heq (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hz : F.obj Z = G.obj Z)
    (hf : HEq (F.map f) (G.map f)) (hg : HEq (F.map g) (G.map g)) :
    HEq (F.map (f ≫ g)) (G.map (f ≫ g))

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : HEq (F.map f) (G.map f)
hg : HEq (F.map g) (G.map g)
⊢ HEq (F.map f ≫ F.map g) (G.map f ≫ G.map g)

Tactic:
congr

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : HEq (F.map f) (G.map f)
hg : HEq (F.map g) (G.map g)
⊢ HEq (F.map (f ≫ g)) (G.map (f ≫ g))

Tactic:
rw [F.map_comp, G.map_comp]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : HEq (F.map f) (G.map f)
hg : HEq (F.map g) (G.map g)
⊢ HEq (F.map f ≫ F.map g) (G.map f ≫ G.map g)
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem edist_iterate_succ_le_geometric {f : α → α} (hf : LipschitzWith K f) (x n) :
    edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * (K : ℝ≥0∞) ^ n

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ edist (f^[n] x) ((f^[n] ∘ f) x) ≤ ↑K ^ n * edist x (f x)

Tactic:
simpa only [ENNReal.coe_pow] using (hf.iterate n) x (f x)

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * ↑K ^ n

Tactic:
rw [iterate_succ, mul_comm]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ edist (f^[n] x) ((f^[n] ∘ f) x) ≤ ↑K ^ n * edist x (f x)
-- Mathlib/Data/List/Enum.lean
theorem exists_mem_zipIdx {l : List α} {n : ℕ} {p : α × ℕ → Prop} :
    (∃ x ∈ l.zipIdx n, p x) ↔ ∃ (i : ℕ) (_ : i < length l), p (l[i], n + i)

Proof state:
α : Type u_1
l : List α
n : ℕ
p : α × ℕ → Prop
⊢ (∃ x, x ∈ l.zipIdx n ∧ p x) ↔ ∃ i x, p (l[i], n + i)

Tactic:
simp only [exists_mem_iff_getElem, getElem_zipIdx, length_zipIdx]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Vieta.lean
theorem prod_X_sub_C_coeff (s : Multiset R) {k : ℕ} (h : k ≤ Multiset.card s) :
    (s.map fun t => X - C t).prod.coeff k =
    (-1) ^ (Multiset.card s - k) * s.esymm (Multiset.card s - k)

Proof state:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (map (fun x => X + C (-x)) s).prod.coeff k = (map (fun r => X + C r) (map (fun t => -t) s)).prod.coeff ?convert_1

Tactic:
rw [map_map]

Result:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (map (fun x => X + C (-x)) s).prod.coeff k = (map ((fun r => X + C r) ∘ fun t => -t) s).prod.coeff ?convert_1

Proof state:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (map (fun x => X + C (-x)) s).prod.coeff k = (-1) ^ (s.card - k) * s.esymm (s.card - k)

Tactic:
convert prod_X_add_C_coeff (map (fun t => -t) s) _ using 1

Result:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (map (fun x => X + C (-x)) s).prod.coeff k = (map (fun r => X + C r) (map (fun t => -t) s)).prod.coeff ?convert_1

case h.e'_3
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (-1) ^ (s.card - k) * s.esymm (s.card - k) = (map (fun t => -t) s).esymm ((map (fun t => -t) s).card - ?convert_1)

case convert_1
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ ℕ

case convert_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ ?convert_1 ≤ (map (fun t => -t) s).card

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (-1) ^ (s.card - k) * s.esymm (s.card - k) = (map (fun t => -t) s).esymm ((map (fun t => -t) s).card - k)

Tactic:
rw [esymm_neg, card_map]

Result:
no goals

Proof state:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (map (fun x => X + C (-x)) s).prod.coeff k = (map ((fun r => X + C r) ∘ fun t => -t) s).prod.coeff ?convert_1

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (map (fun t => X - C t) s).prod.coeff k = (-1) ^ (s.card - k) * s.esymm (s.card - k)

Tactic:
conv_lhs =>
  congr
  congr
  congr
  ext x
  rw [sub_eq_add_neg]
  rw [← map_neg C x]

Result:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (map (fun x => X + C (-x)) s).prod.coeff k = (-1) ^ (s.card - k) * s.esymm (s.card - k)

Proof state:
case convert_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ k ≤ (map (fun t => -t) s).card

Tactic:
rwa [card_map]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem Antitone.cauchySeq_alternating_series_of_tendsto_zero (hfa : Antitone f)
    (hf0 : Tendsto f atTop (𝓝 0)) : CauchySeq fun n ↦ ∑ i ∈ range n, (-1) ^ i * f i

Proof state:
f : ℕ → ℝ
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ x ∈ Finset.range n, f x * (-1) ^ x

Tactic:
exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le

Result:
no goals

Proof state:
f : ℕ → ℝ
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i

Tactic:
simp_rw [mul_comm]

Result:
f : ℕ → ℝ
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ x ∈ Finset.range n, f x * (-1) ^ x
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive] lemma mabs_eq_mabs : |a|ₘ = |b|ₘ ↔ a = b ∨ a = b⁻¹

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
⊢ a = b ∨ a = b⁻¹ → mabs a = mabs b

Tactic:
rintro (h | h) <;> simp [h, abs_neg]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
h : mabs a = mabs b
⊢ a = b ∨ a = b⁻¹

Tactic:
obtain rfl | rfl := eq_or_eq_inv_of_mabs_eq h <;>
  simpa only [inv_eq_iff_eq_inv (a := |b|ₘ), inv_inv, inv_inj, or_comm] using mabs_choice b

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
⊢ mabs a = mabs b ↔ a = b ∨ a = b⁻¹

Tactic:
refine ⟨fun h ↦ ?_, by rintro (h | h) <;> simp [h, abs_neg]⟩

Result:
α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
h : mabs a = mabs b
⊢ a = b ∨ a = b⁻¹
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.ushiftRight_zero' (n : BitVec w) : n >>> 0#w' = n

Proof state:
w w' : Nat
n : BitVec w
⊢ n >>> 0#w' = n

Tactic:
ext i

Result:
case pred
w w' : Nat
n : BitVec w
i : Nat
a✝ : i < w
⊢ (n >>> 0#w').getLsbD i = n.getLsbD i

Proof state:
case pred
w w' : Nat
n : BitVec w
i : Nat
a✝ : i < w
⊢ (n.ushiftRight (0#w').toNat).getLsbD i = n.getLsbD i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map_map₂_distrib_left {g : γ → δ} {f' : α' → β → δ} {g' : α → α'}
    (h_distrib : ∀ a b, g (f a b) = f' (g' a) b) :
    (map₂ f a b).map g = map₂ f' (a.map g') b

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g' a) b

Tactic:
cases a <;> cases b <;> simp [h_distrib]

Result:
no goals
-- Mathlib/Order/JordanHolder.lean
theorem isMaximal_of_eq_inf (x b : X) {a y : X} (ha : x ⊓ y = a) (hxy : x ≠ y) (hxb : IsMaximal x b)
    (hyb : IsMaximal y b) : IsMaximal a y

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxy : x ≠ y
hxb : IsMaximal x (x ⊔ y)
hyb : IsMaximal y (x ⊔ y)
⊢ IsMaximal (x ⊓ y) y

Tactic:
exact isMaximal_inf_right_of_isMaximal_sup hxb hyb

Result:
no goals

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : IsMaximal x b
hyb : IsMaximal y b
⊢ IsMaximal a y

Tactic:
have hb : x ⊔ y = b := sup_eq_of_isMaximal hxb hyb hxy

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : IsMaximal x b
hyb : IsMaximal y b
hb : x ⊔ y = b
⊢ IsMaximal a y

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : IsMaximal x b
hyb : IsMaximal y b
hb : x ⊔ y = b
⊢ IsMaximal a y

Tactic:
substs a b

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxy : x ≠ y
hxb : IsMaximal x (x ⊔ y)
hyb : IsMaximal y (x ⊔ y)
⊢ IsMaximal (x ⊓ y) y
-- Mathlib/Data/Set/Card.lean
theorem encard_diff_singleton_add_one (h : a ∈ s) :
    (s \ {a}).encard + 1 = s.encard

Proof state:
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).encard + 1 = s.encard

Tactic:
rw [← encard_insert_of_not_mem (fun h ↦ h.2 rfl), insert_diff_singleton, insert_eq_of_mem h]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem eq_of_ge {a b : α} (h : b ≤ a) :
    variationOnFromTo f s a b = -(eVariationOn f (s ∩ Icc b a)).toReal

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
h : b ≤ a
⊢ variationOnFromTo f s a b = -(eVariationOn f (s ∩ Icc b a)).toReal

Tactic:
rw [variationOnFromTo.eq_neg_swap, neg_inj, variationOnFromTo.eq_of_le f s h]

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
/-- As `sInf s = 0` when `s` is an empty set of reals, it suffices to show that all elements of `s`
are at least some nonpositive number `a` to show that `a ≤ sInf s`.

See also `le_csInf`. -/
protected lemma le_sInf (hs : ∀ x ∈ s, a ≤ x) (ha : a ≤ 0) : a ≤ sInf s

Proof state:
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, a ≤ x
ha : a ≤ 0
⊢ a ≤ sInf s

Tactic:
obtain rfl | hs' := s.eq_empty_or_nonempty

Result:
case inl
a : ℝ
ha : a ≤ 0
hs : ∀ x ∈ ∅, a ≤ x
⊢ a ≤ sInf ∅

case inr
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, a ≤ x
ha : a ≤ 0
hs' : s.Nonempty
⊢ a ≤ sInf s

Proof state:
case inl
a : ℝ
ha : a ≤ 0
hs : ∀ x ∈ ∅, a ≤ x
⊢ a ≤ sInf ∅

case inr
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, a ≤ x
ha : a ≤ 0
hs' : s.Nonempty
⊢ a ≤ sInf s

Tactic:
exacts [ha.trans_eq sInf_empty.symm, le_csInf hs' hs]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.hasSum_sub (hf : HasFPowerSeriesOnBall f p x r) {y : E}
    (hy : y ∈ EMetric.ball x r) : HasSum (fun n : ℕ => p n fun _ => y - x) (f y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y : E
hy : y ∈ EMetric.ball x r
⊢ HasSum (fun n => (p n) fun x_1 => y - x) (f y)

Tactic:
have : y - x ∈ EMetric.ball (0 : E) r := by simpa [edist_eq_enorm_sub] using hy

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y : E
hy : y ∈ EMetric.ball x r
this : y - x ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p n) fun x_1 => y - x) (f y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y : E
hy : y ∈ EMetric.ball x r
this : y - x ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p n) fun x_1 => y - x) (f y)

Tactic:
simpa only [add_sub_cancel] using hf.hasSum this

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y : E
hy : y ∈ EMetric.ball x r
⊢ y - x ∈ EMetric.ball 0 r

Tactic:
simpa [edist_eq_enorm_sub] using hy

Result:
no goals
-- Mathlib/Algebra/Ring/Divisibility/Basic.lean
theorem neg_dvd : -a ∣ b ↔ a ∣ b :=
  (Equiv.neg _).exists_congr_left.trans <| by
    simp only [Equiv.neg_symm, Equiv.neg_apply, mul_neg, neg_mul, neg_neg, Dvd.dvd]

Proof state:
α : Type u_1
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b : α
⊢ (∃ b_1, b = -a * (Equiv.symm (Equiv.neg α)) b_1) ↔ a ∣ b

Tactic:
simp only [Equiv.neg_symm, Equiv.neg_apply, mul_neg, neg_mul, neg_neg, Dvd.dvd]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem toList_mapKey (f : α → δ) (l : AssocList α β) :
    (mapKey f l).toList = l.toList.map (fun (a, b) => (f a, b))

Proof state:
α : Type u_1
δ : Type u_2
β : Type u_3
f : α → δ
l : AssocList α β
⊢ (mapKey f l).toList =
    List.map
      (fun x =>
        match x with
        | (a, b) => (f a, b))
      l.toList

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
theorem Pi.π_comp_eqToHom {J : Type*} (f : J → C) [HasProduct f] {j j' : J} (w : j = j') :
    Pi.π f j ≫ eqToHom (by simp [w]) = Pi.π f j'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasProduct f
j j' : J
w : j = j'
⊢ π f j ≫ eqToHom ⋯ = π f j'

Tactic:
cases w

Result:
case refl
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasProduct f
j : J
⊢ π f j ≫ eqToHom ⋯ = π f j

Proof state:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasProduct f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]

Result:
no goals

Proof state:
case refl
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasProduct f
j : J
⊢ π f j ≫ eqToHom ⋯ = π f j

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
@[simp] lemma coe_nonZeroDivisorsRight_eq [NoZeroDivisors M₀] [Nontrivial M₀] :
    nonZeroDivisorsRight M₀ = {x : M₀ | x ≠ 0}

Proof state:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
hx : x ≠ 0
y : M₀
hx' : x = 0 ∨ y = 0
⊢ y = 0

Tactic:
aesop

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
⊢ ↑(nonZeroDivisorsRight M₀) = {x | x ≠ 0}

Tactic:
ext x

Result:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ x ∈ ↑(nonZeroDivisorsRight M₀) ↔ x ∈ {x | x ≠ 0}

Proof state:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : ∀ (y : M₀), x = 0 ∨ y = 0 → y = 0
⊢ x ≠ 0

Tactic:
contrapose! h

Result:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : x = 0
⊢ ∃ y, (x = 0 ∨ y = 0) ∧ y ≠ 0

Proof state:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ (∀ (y : M₀), x = 0 ∨ y = 0 → y = 0) ↔ x ≠ 0

Tactic:
refine ⟨fun h ↦ ?_, fun hx y hx' ↦ by aesop⟩

Result:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : ∀ (y : M₀), x = 0 ∨ y = 0 → y = 0
⊢ x ≠ 0

Proof state:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ x ∈ ↑(nonZeroDivisorsRight M₀) ↔ x ∈ {x | x ≠ 0}

Tactic:
simp only [SetLike.mem_coe, mem_nonZeroDivisorsRight_iff, mul_eq_zero, Set.mem_setOf_eq]

Result:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ (∀ (y : M₀), x = 0 ∨ y = 0 → y = 0) ↔ x ≠ 0

Proof state:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : x = 0
⊢ ∃ y, (x = 0 ∨ y = 0) ∧ y ≠ 0

Tactic:
exact ⟨1, Or.inl h, one_ne_zero⟩

Result:
no goals