harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_add_le_iff_left {n : ℕ} (p q : R[X]) (qn : q.natDegree ≤ n) :
    (p + q).natDegree ≤ n ↔ p.natDegree ≤ n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
⊢ (p + q).natDegree ≤ n ↔ p.natDegree ≤ n

Tactic:
refine ⟨fun h => ?_, fun h => natDegree_add_le_of_degree_le h qn⟩

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
⊢ p.natDegree ≤ n

Proof state:
case h.e'_2
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
⊢ p.coeff m = (p + q).coeff m

Tactic:
rw [coeff_add, natDegree_le_iff_coeff_eq_zero.mp qn _ hm, add_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
⊢ p.coeff m = 0

Tactic:
convert natDegree_le_iff_coeff_eq_zero.mp h m hm using 1

Result:
case h.e'_2
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
⊢ p.coeff m = (p + q).coeff m

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
⊢ p.natDegree ≤ n

Tactic:
refine natDegree_le_iff_coeff_eq_zero.mpr fun m hm => ?_

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
⊢ p.coeff m = 0
-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem mem_closedBall (t : Icc v.tMin v.tMax) : f t ∈ closedBall v.x₀ v.R :=
  calc
    dist (f t) v.x₀ = dist (f t) (f.toFun v.t₀)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
t : ↑(Icc v.tMin v.tMax)
⊢ dist (f.toFun t) v.x₀ = dist (f.toFun t) (f.toFun v.t₀)

Tactic:
rw [f.map_t₀']

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem map_map [Semiring T] (g : S →+* T) (p : R[X]) : (p.map f).map g = p.map (g.comp f) :=
  ext (by simp [coeff_map])

Proof state:
R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
p : R[X]
⊢ ∀ (n : ℕ), (map g (map f p)).coeff n = (map (g.comp f) p).coeff n

Tactic:
simp [coeff_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem eq_swap_iff_eq_eq {o : Ordering} : o = o.swap ↔ o = .eq

Proof state:
o : Ordering
⊢ o = o.swap ↔ o = eq

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Order/SuccPred/WithBot.lean
lemma pred_mono : Monotone (pred : WithTop α → α)
  | _, ⊤, _ => by simp
  | ⊤, (a : α), hab => by simp at hab
  | (a : α), (b : α), hab => Order.pred_le_pred (by simpa using hab)

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : α
hab : ⊤ ≤ ↑a
⊢ ⊤.pred ≤ (↑a).pred

Tactic:
simp at hab

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
x✝¹ : WithTop α
x✝ : x✝¹ ≤ ⊤
⊢ x✝¹.pred ≤ ⊤.pred

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a b : α
hab : ↑a ≤ ↑b
⊢ a ≤ b

Tactic:
simpa using hab

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWithAll_map_left (l₁ : Array α) (l₂ : Array β) (f : α → α') (g : Option α' → Option β → γ) :
    zipWithAll g (l₁.map f) l₂ = zipWithAll (fun a b => g (f <$> a) b) l₁ l₂

Proof state:
α : Type u_1
β : Type u_2
α' : Type u_1
γ : Type u_3
l₁ : Array α
l₂ : Array β
f : α → α'
g : Option α' → Option β → γ
⊢ zipWithAll g (map f l₁) l₂ = zipWithAll (fun a b => g (f <$> a) b) l₁ l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
α' : Type u_1
γ : Type u_3
l₂ : Array β
f : α → α'
g : Option α' → Option β → γ
toList✝ : List α
⊢ zipWithAll g (map f { toList := toList✝ }) l₂ = zipWithAll (fun a b => g (f <$> a) b) { toList := toList✝ } l₂

Proof state:
case mk
α : Type u_1
β : Type u_2
α' : Type u_1
γ : Type u_3
l₂ : Array β
f : α → α'
g : Option α' → Option β → γ
toList✝ : List α
⊢ zipWithAll g (map f { toList := toList✝ }) l₂ = zipWithAll (fun a b => g (f <$> a) b) { toList := toList✝ } l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
α' : Type u_1
γ : Type u_3
f : α → α'
g : Option α' → Option β → γ
toList✝¹ : List α
toList✝ : List β
⊢ zipWithAll g (map f { toList := toList✝¹ }) { toList := toList✝ } =
    zipWithAll (fun a b => g (f <$> a) b) { toList := toList✝¹ } { toList := toList✝ }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
α' : Type u_1
γ : Type u_3
f : α → α'
g : Option α' → Option β → γ
toList✝¹ : List α
toList✝ : List β
⊢ zipWithAll g (map f { toList := toList✝¹ }) { toList := toList✝ } =
    zipWithAll (fun a b => g (f <$> a) b) { toList := toList✝¹ } { toList := toList✝ }

Tactic:
simp [List.zipWithAll_map_left]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem uniformEquicontinuousOn_iff_uniformContinuousOn {F : ι → β → α} {S : Set β} :
    UniformEquicontinuousOn F S ↔ UniformContinuousOn (ofFun ∘ Function.swap F : β → ι →ᵤ α) S

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔
    ∀ i ∈ 𝓤 α, ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ UniformFun.gen ι α i

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔ UniformContinuousOn (⇑ofFun ∘ swap F) S

Tactic:
rw [UniformContinuousOn, (UniformFun.hasBasis_uniformity ι α).tendsto_right_iff]

Result:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔
    ∀ i ∈ 𝓤 α, ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ UniformFun.gen ι α i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reverseAux_reverseAux_nil (as bs : List α) : reverseAux (reverseAux as bs) [] = reverseAux bs as

Proof state:
case cons
α : Type u_1
a : α
as : List α
ih : ∀ (bs : List α), (as.reverseAux bs).reverseAux [] = bs.reverseAux as
bs : List α
⊢ ((a :: as).reverseAux bs).reverseAux [] = bs.reverseAux (a :: as)

Tactic:
simp [reverseAux, ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
bs : List α
⊢ ([].reverseAux bs).reverseAux [] = bs.reverseAux []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
as bs : List α
⊢ (as.reverseAux bs).reverseAux [] = bs.reverseAux as

Tactic:
induction as generalizing bs with
| nil => rfl
| cons a as ih => simp [reverseAux, ih]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
@[to_additive]
lemma IsComplement.nonempty_right (hst : IsComplement S T) : T.Nonempty

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hst : T = ∅
⊢ ¬IsComplement S T

Tactic:
simp [hst]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hst : IsComplement S T
⊢ T.Nonempty

Tactic:
contrapose! hst

Result:
G : Type u_1
inst✝ : Group G
S T : Set G
hst : T = ∅
⊢ ¬IsComplement S T
-- Mathlib/Order/WithBot.lean
lemma WithTop.toDual_le_iff {x : WithTop α} {y : WithBot αᵒᵈ} :
    x.toDual ≤ y ↔ WithBot.ofDual y ≤ x

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

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

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem forall_mem_filterMap {f : α → Option β} {l : List α} {P : β → Prop} :
    (∀ (i) (_ : i ∈ filterMap f l), P i) ↔ ∀ (j) (_ : j ∈ l) (b), f j = some b → P b

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
P : β → Prop
⊢ (∀ (i : β), i ∈ filterMap f l → P i) ↔ ∀ (j : α), j ∈ l → ∀ (b : β), f j = some b → P b

Tactic:
simp only [mem_filterMap, forall_exists_index, and_imp]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
P : β → Prop
⊢ (∀ (i : β) (x : α), x ∈ l → f x = some i → P i) ↔ ∀ (j : α), j ∈ l → ∀ (b : β), f j = some b → P b

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
P : β → Prop
⊢ (∀ (b : α) (a : β), b ∈ l → f b = some a → P a) ↔ ∀ (j : α), j ∈ l → ∀ (b : β), f j = some b → P b

Tactic:
apply forall_congr'

Result:
case h
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
P : β → Prop
⊢ ∀ (a : α), (∀ (a_1 : β), a ∈ l → f a = some a_1 → P a_1) ↔ a ∈ l → ∀ (b : β), f a = some b → P b

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
P : β → Prop
a : α
⊢ (∀ (a_1 : β), a ∈ l → f a = some a_1 → P a_1) ↔ a ∈ l → ∀ (b : β), f a = some b → P b

Tactic:
rw [forall_comm]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
P : β → Prop
⊢ ∀ (a : α), (∀ (a_1 : β), a ∈ l → f a = some a_1 → P a_1) ↔ a ∈ l → ∀ (b : β), f a = some b → P b

Tactic:
intro a

Result:
case h
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
P : β → Prop
a : α
⊢ (∀ (a_1 : β), a ∈ l → f a = some a_1 → P a_1) ↔ a ∈ l → ∀ (b : β), f a = some b → P b

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
P : β → Prop
⊢ (∀ (i : β) (x : α), x ∈ l → f x = some i → P i) ↔ ∀ (j : α), j ∈ l → ∀ (b : β), f j = some b → P b

Tactic:
rw [forall_comm]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
P : β → Prop
⊢ (∀ (b : α) (a : β), b ∈ l → f b = some a → P a) ↔ ∀ (j : α), j ∈ l → ∀ (b : β), f j = some b → P b
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem summable_of_ratio_test_tendsto_lt_one {α : Type*} [NormedAddCommGroup α] [CompleteSpace α]
    {f : ℕ → α} {l : ℝ} (hl₁ : l < 1) (hf : ∀ᶠ n in atTop, f n ≠ 0)
    (h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)) : Summable f

Proof state:
case h
α : Type u_2
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
a✝¹ : ℕ
a✝ : ‖f (a✝¹ + 1)‖ / ‖f a✝¹‖ ≤ r
h₁ : f a✝¹ ≠ 0
⊢ ‖f (a✝¹ + 1)‖ ≤ r * ‖f a✝¹‖

Tactic:
rwa [← div_le_iff₀ (norm_pos_iff.mpr h₁)]

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
⊢ Summable f

Tactic:
refine summable_of_ratio_norm_eventually_le hr₁ ?_

Result:
case intro.intro
α : Type u_2
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
⊢ ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
⊢ ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖

Tactic:
filter_upwards [h.eventually_le_const hr₀, hf] with _ _ h₁

Result:
case h
α : Type u_2
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
a✝¹ : ℕ
a✝ : ‖f (a✝¹ + 1)‖ / ‖f a✝¹‖ ≤ r
h₁ : f a✝¹ ≠ 0
⊢ ‖f (a✝¹ + 1)‖ ≤ r * ‖f a✝¹‖

Proof state:
α : Type u_2
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
⊢ Summable f

Tactic:
rcases exists_between hl₁ with ⟨r, hr₀, hr₁⟩

Result:
case intro.intro
α : Type u_2
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
⊢ Summable f
-- Mathlib/Topology/Sets/Opens.lean
theorem coe_iSup {ι} (s : ι → Opens α) : ((⨆ i, s i : Opens α) : Set α) = ⋃ i, s i

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_5
s : ι → Opens α
⊢ ↑(⨆ i, s i) = ⋃ i, ↑(s i)

Tactic:
simp [iSup]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem degree_cyclotomic (n : ℕ) (R : Type*) [Ring R] [Nontrivial R] :
    (cyclotomic n R).degree = Nat.totient n

Proof state:
case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
k : ℕ
⊢ (cyclotomic (k + 1) ℤ).degree = ↑(k + 1).totient

Tactic:
rw [← degree_cyclotomic' (Complex.isPrimitiveRoot_exp k.succ (Nat.succ_ne_zero k))]

Result:
case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
k : ℕ
⊢ (cyclotomic (k + 1) ℤ).degree = (cyclotomic' k.succ ℂ).degree

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic n ℤ).degree = ↑n.totient

Tactic:
rcases n with - | k

Result:
case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic 0 ℤ).degree = ↑(Nat.totient 0)

case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
k : ℕ
⊢ (cyclotomic (k + 1) ℤ).degree = ↑(k + 1).totient

Proof state:
case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic 0 ℤ).degree = ↑(Nat.totient 0)

Tactic:
simp only [cyclotomic, degree_one, dif_pos, Nat.totient_zero, CharP.cast_eq_zero]

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (map (Int.castRingHom R) (cyclotomic n ℤ)).degree = ↑n.totient

Tactic:
rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom R) _]

Result:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic n ℤ).degree = ↑n.totient

n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (Int.castRingHom R) (cyclotomic n ℤ).leadingCoeff ≠ 0

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic n R).degree = ↑n.totient

Tactic:
rw [← map_cyclotomic_int]

Result:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (map (Int.castRingHom R) (cyclotomic n ℤ)).degree = ↑n.totient

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (Int.castRingHom R) (cyclotomic n ℤ).leadingCoeff ≠ 0

Tactic:
simp only [(int_cyclotomic_spec n).right.right, eq_intCast, Monic.leadingCoeff, Int.cast_one,
  Ne, not_false_iff, one_ne_zero]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
k : ℕ
⊢ (cyclotomic (k + 1) ℤ).degree = (cyclotomic' k.succ ℂ).degree

Tactic:
exact (int_cyclotomic_spec k.succ).2.1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sshiftRight_and_distrib (x y : BitVec w) (n : Nat) :
    (x &&& y).sshiftRight n = (x.sshiftRight n) &&& (y.sshiftRight n)

Proof state:
case pred
w : Nat
x y : BitVec w
n i : Nat
a✝ : i < w
⊢ (!decide (w ≤ i) && if n + i < w then x.getLsbD (n + i) && y.getLsbD (n + i) else x.msb && y.msb) =
    ((!decide (w ≤ i) && if n + i < w then x.getLsbD (n + i) else x.msb) &&
      (!decide (w ≤ i) && if n + i < w then y.getLsbD (n + i) else y.msb))

Tactic:
split
  <;> by_cases w ≤ i
  <;> simp [*]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
n : Nat
⊢ (x &&& y).sshiftRight n = x.sshiftRight n &&& y.sshiftRight n

Tactic:
ext i

Result:
case pred
w : Nat
x y : BitVec w
n i : Nat
a✝ : i < w
⊢ ((x &&& y).sshiftRight n).getLsbD i = (x.sshiftRight n &&& y.sshiftRight n).getLsbD i

Proof state:
case pred
w : Nat
x y : BitVec w
n i : Nat
a✝ : i < w
⊢ ((x &&& y).sshiftRight n).getLsbD i = (x.sshiftRight n &&& y.sshiftRight n).getLsbD i

Tactic:
simp only [getLsbD_sshiftRight, getLsbD_and, msb_and]

Result:
case pred
w : Nat
x y : BitVec w
n i : Nat
a✝ : i < w
⊢ (!decide (w ≤ i) && if n + i < w then x.getLsbD (n + i) && y.getLsbD (n + i) else x.msb && y.msb) =
    ((!decide (w ≤ i) && if n + i < w then x.getLsbD (n + i) else x.msb) &&
      (!decide (w ≤ i) && if n + i < w then y.getLsbD (n + i) else y.msb))
-- Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean
@[simp]
lemma const_comp {X Y Z : SSet.{u}} (y : Y _⦋0⦌) (g : Y ⟶ Z) :
    const (X := X) y ≫ g = const (g.app _ y)

Proof state:
X Y Z : SSet
y : Y _⦋0⦌
g : Y ⟶ Z
⊢ const y ≫ g = const (g.app (Opposite.op ⦋0⦌) y)

Tactic:
ext m x

Result:
case w.h
X Y Z : SSet
y : Y _⦋0⦌
g : Y ⟶ Z
m : SimplexCategoryᵒᵖ
x : X.obj m
⊢ (const y ≫ g).app m x = (const (g.app (Opposite.op ⦋0⦌) y)).app m x

Proof state:
case w.h
X Y Z : SSet
y : Y _⦋0⦌
g : Y ⟶ Z
m : SimplexCategoryᵒᵖ
x : X.obj m
⊢ (const y ≫ g).app m x = (const (g.app (Opposite.op ⦋0⦌) y)).app m x

Tactic:
simp [FunctorToTypes.naturality]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
@[simp]
lemma toMeasure_map (p : PMF α) (hf : Measurable f) : p.toMeasure.map f = (p.map f).toMeasure

Proof state:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
mβ : MeasurableSpace β
p : PMF α
hf : Measurable f
⊢ Measure.map f p.toMeasure = (map f p).toMeasure

Tactic:
ext s hs : 1

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
mβ : MeasurableSpace β
p : PMF α
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (Measure.map f p.toMeasure) s = (map f p).toMeasure s

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
mβ : MeasurableSpace β
p : PMF α
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (Measure.map f p.toMeasure) s = (map f p).toMeasure s

Tactic:
rw [PMF.toMeasure_map_apply _ _ _ hf hs, Measure.map_apply hf hs]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem repeat_add (a : Fin n → α) (m₁ m₂ : ℕ) : Fin.repeat (m₁ + m₂) a =
    append (Fin.repeat m₁ a) (Fin.repeat m₂ a) ∘ Fin.cast (Nat.add_mul ..)

Proof state:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ ∀ (x : Fin ((m₁ + m₂) * n)), «repeat» (m₁ + m₂) a x = (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) x

Tactic:
rw [(Fin.rightInverse_cast h.symm).surjective.forall]

Result:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ ∀ (x : Fin (m₁ * n + m₂ * n)),
    «repeat» (m₁ + m₂) a (Fin.cast ⋯ x) = (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ x)

Proof state:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ «repeat» (m₁ + m₂) a = append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h

Tactic:
apply funext

Result:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ ∀ (x : Fin ((m₁ + m₂) * n)), «repeat» (m₁ + m₂) a x = (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) x

Proof state:
case h.refine_2
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
r : Fin (m₂ * n)
⊢ «repeat» (m₁ + m₂) a (Fin.cast ⋯ (natAdd (m₁ * n) r)) =
    (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd (m₁ * n) r))

Tactic:
simp [modNat, Nat.add_mod]

Result:
no goals

Proof state:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ ∀ (x : Fin (m₁ * n + m₂ * n)),
    «repeat» (m₁ + m₂) a (Fin.cast ⋯ x) = (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ x)

Tactic:
refine Fin.addCases (fun l => ?_) fun r => ?_

Result:
case h.refine_1
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
l : Fin (m₁ * n)
⊢ «repeat» (m₁ + m₂) a (Fin.cast ⋯ (castAdd (m₂ * n) l)) =
    (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ (castAdd (m₂ * n) l))

case h.refine_2
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
r : Fin (m₂ * n)
⊢ «repeat» (m₁ + m₂) a (Fin.cast ⋯ (natAdd (m₁ * n) r)) =
    (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd (m₁ * n) r))

Proof state:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
⊢ «repeat» (m₁ + m₂) a = append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast ⋯

Tactic:
generalize_proofs h

Result:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ «repeat» (m₁ + m₂) a = append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h

Proof state:
case h.refine_1
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
l : Fin (m₁ * n)
⊢ «repeat» (m₁ + m₂) a (Fin.cast ⋯ (castAdd (m₂ * n) l)) =
    (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ (castAdd (m₂ * n) l))

Tactic:
simp [modNat, Nat.mod_eq_of_lt l.is_lt]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp]
lemma adj_penultimate {p : G.Walk v w} (hp : ¬ p.Nil) :
    G.Adj p.penultimate w

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.length = 0
⊢ G.Adj p.penultimate (p.getVert p.length)

Tactic:
convert adj_getVert_succ _ _ <;> omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.Nil
⊢ G.Adj p.penultimate w

Tactic:
conv => rhs; rw [← getVert_length p]

Result:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.Nil
⊢ G.Adj p.penultimate (p.getVert p.length)

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.Nil
⊢ G.Adj p.penultimate (p.getVert p.length)

Tactic:
rw [nil_iff_length_eq] at hp

Result:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.length = 0
⊢ G.Adj p.penultimate (p.getVert p.length)
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem measurableSet_toMeasurable (μ : Measure α) (s : Set α) :
    MeasurableSet (toMeasurable μ s)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ MeasurableSet
    (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then h.choose
    else
      if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u) then h'.choose
      else ⋯.choose)

Tactic:
split_ifs with hs h's

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ MeasurableSet hs.choose

case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ MeasurableSet h's.choose

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's : ¬∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ MeasurableSet ⋯.choose

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ MeasurableSet (toMeasurable μ s)

Tactic:
rw [toMeasurable_def]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ MeasurableSet
    (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then h.choose
    else
      if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u) then h'.choose
      else ⋯.choose)

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ MeasurableSet hs.choose

case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ MeasurableSet h's.choose

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's : ¬∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ MeasurableSet ⋯.choose

Tactic:
exacts [hs.choose_spec.2.1, h's.choose_spec.2.1,
        (exists_measurable_superset μ s).choose_spec.2.1]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_of_zero_length (h : w = 0) (x : BitVec w) : x.msb = false

Proof state:
x : BitVec 0
⊢ x.msb = false

Tactic:
simp [msb_zero_length]

Result:
no goals

Proof state:
w : Nat
h : w = 0
x : BitVec w
⊢ x.msb = false

Tactic:
subst h

Result:
x : BitVec 0
⊢ x.msb = false
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftLeft_zero' {x : BitVec w₁} : x <<< 0#w₂ = x

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
⊢ x <<< 0#w₂ = x

Tactic:
simp

Result:
no goals