harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem Measurable.biSup {ι} (s : Set ι) {f : ι → δ → α} (hs : s.Countable)
    (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun b => ⨆ i ∈ s, f i b

Proof state:
case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this✝ : Encodable ↑s
H : ¬∀ (i : ι), i ∈ s
this : ∀ (b : δ), ⨆ i ∈ s, f i b = (⨆ i, f (↑i) b) ⊔ sSup ∅
⊢ Measurable fun b => ⨆ i ∈ s, f i b

Tactic:
simp only [this]

Result:
case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this✝ : Encodable ↑s
H : ¬∀ (i : ι), i ∈ s
this : ∀ (b : δ), ⨆ i ∈ s, f i b = (⨆ i, f (↑i) b) ⊔ sSup ∅
⊢ Measurable fun b => (⨆ i, f (↑i) b) ⊔ sSup ∅
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem exists_pos_preimage_ball [PseudoMetricSpace δ] (f : α → δ) (x : δ) (hμ : μ ≠ 0) :
    ∃ n : ℕ, 0 < μ (f ⁻¹' Metric.ball x n) :=
  exists_pos_measure_of_cover (by rw [← preimage_iUnion, Metric.iUnion_ball_nat, preimage_univ]) hμ

Proof state:
α : Type u_1
δ : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetricSpace δ
f : α → δ
x : δ
hμ : μ ≠ 0
⊢ ⋃ i, f ⁻¹' Metric.ball x ↑i = univ

Tactic:
rw [← preimage_iUnion, Metric.iUnion_ball_nat, preimage_univ]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsNormal.bsup {f : Ordinal.{max u v} → Ordinal.{max u w}} (H : IsNormal f)
    {o : Ordinal.{u}} :
    ∀ (g : ∀ a < o, Ordinal), o ≠ 0 → f (bsup.{_, v} o g) = bsup.{_, w} o fun a h => f (g a h) :=
  inductionOn o fun α r _ g h => by
    haveI := type_ne_zero_iff_nonempty.1 h
    rw [← sup_eq_bsup' r, IsNormal.sup.{_, v, w} H, ← sup_eq_bsup' r] <;> rfl

Proof state:
f : Ordinal.{max u v} → Ordinal.{max u w}
H : IsNormal f
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
h : type r ≠ 0
this : Nonempty α
⊢ f ((type r).bsup g) = (type r).bsup fun a h => f (g a h)

Tactic:
rw [← sup_eq_bsup' r, IsNormal.sup.{_, v, w} H, ← sup_eq_bsup' r] <;> rfl

Result:
no goals

Proof state:
f : Ordinal.{max u v} → Ordinal.{max u w}
H : IsNormal f
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
h : type r ≠ 0
⊢ f ((type r).bsup g) = (type r).bsup fun a h => f (g a h)

Tactic:
haveI := type_ne_zero_iff_nonempty.1 h

Result:
f : Ordinal.{max u v} → Ordinal.{max u w}
H : IsNormal f
o : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
h : type r ≠ 0
this : Nonempty α
⊢ f ((type r).bsup g) = (type r).bsup fun a h => f (g a h)
-- Mathlib/Tactic/Ring/Basic.lean
theorem inv_add {a₁ a₂ : ℕ} (_ : ((a₁ : ℕ) : R) = b₁) (_ : ((a₂ : ℕ) : R) = b₂) :
    ((a₁ + a₂ : ℕ) : R) = b₁ + b₂

Proof state:
R : Type u_1
inst✝ : CommSemiring R
b₁ b₂ : R
a₁ a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ : ℕ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ : ℕ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem tensor_inv_hom_id {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
    (g ⊗ f.inv) ≫ (h ⊗ f.hom) = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ g ≫ h ⊗ 𝟙 W = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)

Tactic:
simp [tensorHom_id]

Result:
no goals

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ (g ⊗ f.inv) ≫ (h ⊗ f.hom) = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)

Tactic:
rw [← tensor_comp, f.inv_hom_id]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ g ≫ h ⊗ 𝟙 W = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem countable_leftLim_ne (f : StieltjesFunction) : Set.Countable { x | leftLim f x ≠ f x }

Proof state:
f : StieltjesFunction
x : ℝ
hx : x ∈ {x | leftLim (↑f) x ≠ ↑f x}
h'x : ContinuousAt (↑f) x
⊢ leftLim (↑f) x = ↑f x

Tactic:
exact tendsto_nhds_unique (f.mono.tendsto_leftLim x) (h'x.tendsto.mono_left nhdsWithin_le_nhds)

Result:
no goals

Proof state:
f : StieltjesFunction
⊢ {x | leftLim (↑f) x ≠ ↑f x}.Countable

Tactic:
refine Countable.mono ?_ f.mono.countable_not_continuousAt

Result:
f : StieltjesFunction
⊢ {x | leftLim (↑f) x ≠ ↑f x} ⊆ {x | ¬ContinuousAt (↑f) x}

Proof state:
f : StieltjesFunction
x : ℝ
hx : x ∈ {x | leftLim (↑f) x ≠ ↑f x}
h'x : ContinuousAt (↑f) x
⊢ False

Tactic:
apply hx

Result:
f : StieltjesFunction
x : ℝ
hx : x ∈ {x | leftLim (↑f) x ≠ ↑f x}
h'x : ContinuousAt (↑f) x
⊢ leftLim (↑f) x = ↑f x

Proof state:
f : StieltjesFunction
⊢ {x | leftLim (↑f) x ≠ ↑f x} ⊆ {x | ¬ContinuousAt (↑f) x}

Tactic:
intro x hx h'x

Result:
f : StieltjesFunction
x : ℝ
hx : x ∈ {x | leftLim (↑f) x ≠ ↑f x}
h'x : ContinuousAt (↑f) x
⊢ False
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma exists_smul_basis_eq (x : W.CoordinateRing) :
    ∃ p q : R[X], p • (1 : W.CoordinateRing) + q • mk W Y = x

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x : W.CoordinateRing
⊢ ∃ p q, p • 1 + q • (mk W) Y = x

Tactic:
have h := (CoordinateRing.basis W).sum_equivFun x

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
x : W.CoordinateRing
h : ∑ i : Fin 2, (CoordinateRing.basis W).equivFun x i • (CoordinateRing.basis W) i = x
⊢ ∃ p q, p • 1 + q • (mk W) Y = x

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x : W.CoordinateRing
h : (CoordinateRing.basis W).equivFun x 0 • 1 + (CoordinateRing.basis W).equivFun x 1 • (mk W) Y = x
⊢ ∃ p q, p • 1 + q • (mk W) Y = x

Tactic:
exact ⟨_, _, h⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x : W.CoordinateRing
h : ∑ i : Fin 2, (CoordinateRing.basis W).equivFun x i • (CoordinateRing.basis W) i = x
⊢ ∃ p q, p • 1 + q • (mk W) Y = x

Tactic:
rw [Fin.sum_univ_succ, Fin.sum_univ_one, basis_zero, Fin.succ_zero_eq_one, basis_one] at h

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
x : W.CoordinateRing
h : (CoordinateRing.basis W).equivFun x 0 • 1 + (CoordinateRing.basis W).equivFun x 1 • (mk W) Y = x
⊢ ∃ p q, p • 1 + q • (mk W) Y = x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_eq_singleton_iff {a b : Array α} {x : α} :
    a ++ b = #[x] ↔ (a = #[] ∧ b = #[x]) ∨ (a = #[x] ∧ b = #[])

Proof state:
α : Type u_1
a b : Array α
x : α
⊢ a ++ b = #[x] ↔ a = #[] ∧ b = #[x] ∨ a = #[x] ∧ b = #[]

Tactic:
rcases a with ⟨a⟩

Result:
case mk
α : Type u_1
b : Array α
x : α
a : List α
⊢ { toList := a } ++ b = #[x] ↔ { toList := a } = #[] ∧ b = #[x] ∨ { toList := a } = #[x] ∧ b = #[]

Proof state:
case mk.mk
α : Type u_1
x : α
a b : List α
⊢ { toList := a } ++ { toList := b } = #[x] ↔
    { toList := a } = #[] ∧ { toList := b } = #[x] ∨ { toList := a } = #[x] ∧ { toList := b } = #[]

Tactic:
simp only [List.append_toArray, mk.injEq, List.append_eq_singleton_iff, toArray_eq_append_iff]

Result:
no goals

Proof state:
case mk
α : Type u_1
b : Array α
x : α
a : List α
⊢ { toList := a } ++ b = #[x] ↔ { toList := a } = #[] ∧ b = #[x] ∨ { toList := a } = #[x] ∧ b = #[]

Tactic:
rcases b with ⟨b⟩

Result:
case mk.mk
α : Type u_1
x : α
a b : List α
⊢ { toList := a } ++ { toList := b } = #[x] ↔
    { toList := a } = #[] ∧ { toList := b } = #[x] ∨ { toList := a } = #[x] ∧ { toList := b } = #[]
-- Mathlib/Data/Nat/Init.lean
lemma dvd_div_of_mul_dvd (h : a * b ∣ c) : b ∣ c / a :=
  if ha : a = 0 then by simp [ha]
  else
    have ha : 0 < a := Nat.pos_of_ne_zero ha
    have h1 : ∃ d, c = a * b * d := h
    let ⟨d, hd⟩ := h1
    have h2 : c / a = b * d := Nat.div_eq_of_eq_mul_right ha (by simpa [Nat.mul_assoc] using hd)
    show ∃ d, c / a = b * d from ⟨d, h2⟩

Proof state:
a b c : ℕ
h : a * b ∣ c
ha✝ : ¬a = 0
ha : 0 < a
h1 : ∃ d, c = a * b * d
d : ℕ
hd : c = a * b * d
⊢ c = a * (b * d)

Tactic:
simpa [Nat.mul_assoc] using hd

Result:
no goals

Proof state:
a b c : ℕ
h : a * b ∣ c
ha : a = 0
⊢ b ∣ c / a

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem killCompl_comp_rename : (killCompl hf).comp (rename f) = AlgHom.id R _ :=
  algHom_ext fun i => by
    dsimp
    rw [rename, killCompl, aeval_X, comp_apply, aeval_X, dif_pos, Equiv.ofInjective_symm_apply]

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
⊢ ((killCompl hf).comp (rename f)) (X i) = (AlgHom.id R (MvPolynomial σ R)) (X i)

Tactic:
dsimp

Result:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
⊢ (killCompl hf) ((rename f) (X i)) = X i

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
⊢ (killCompl hf) ((rename f) (X i)) = X i

Tactic:
rw [rename, killCompl, aeval_X, comp_apply, aeval_X, dif_pos, Equiv.ofInjective_symm_apply]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma lieBracket_smul_left {c : 𝕜} (hV : DifferentiableAt 𝕜 V x) :
    lieBracket 𝕜 (c • V) W x = c • lieBracket 𝕜 V W x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
c : 𝕜
hV : DifferentiableAt 𝕜 V x
⊢ lieBracket 𝕜 (c • V) W x = c • lieBracket 𝕜 V W x

Tactic:
simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ] at hV ⊢

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
c : 𝕜
hV : DifferentiableWithinAt 𝕜 V univ x
⊢ lieBracketWithin 𝕜 (c • V) W univ x = c • lieBracketWithin 𝕜 V W univ x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
c : 𝕜
hV : DifferentiableWithinAt 𝕜 V univ x
⊢ lieBracketWithin 𝕜 (c • V) W univ x = c • lieBracketWithin 𝕜 V W univ x

Tactic:
exact lieBracketWithin_smul_left hV uniqueDiffWithinAt_univ

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.odd_zsmul_antiperiodic [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c)
    (n : ℤ) : Antiperiodic f ((2 * n + 1) • c)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ f (x + (2 * n + 1) • c) = -f x

Tactic:
rw [add_zsmul, one_zsmul, ← add_assoc, h, h.even_zsmul_periodic]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Antiperiodic f ((2 * n + 1) • c)

Tactic:
intro x

Result:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ f (x + (2 * n + 1) • c) = -f x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem alter_eq_alterₘ [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun _ => β)) (a : α)
    (f : Option β → Option β) : Const.alter m a f = Const.alterₘ m a f

Proof state:
case isFalse
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : Option β → Option β
h✝ : ¬AssocList.contains a (bucket m.1.buckets ⋯ a) = true
⊢ (match f none with
    | none => m
    | some b =>
      expandIfNecessary
        ⟨{ size := m.1.size + 1,
            buckets :=
              m.1.buckets.uset (mkIdx m.1.buckets.size ⋯ (hash a)).val (AssocList.cons a b (bucket m.1.buckets ⋯ a))
                ⋯ },
          ⋯⟩) =
    match f none with
    | none => m
    | some b => (m.consₘ a b).expandIfNecessary

Tactic:
congr

Result:
no goals

Proof state:
case isTrue.e_val.e_buckets
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : Option β → Option β
h✝ : AssocList.contains a (bucket m.1.buckets ⋯ a) = true
⊢ (m.1.buckets.uset (mkIdx m.1.buckets.size ⋯ (hash a)).val AssocList.nil ⋯).uset
      (mkIdx m.1.buckets.size ⋯ (hash a)).val (AssocList.Const.alter a f (bucket m.1.buckets ⋯ a)) ⋯ =
    updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l

Tactic:
simp only [Array.uset, bucket, Array.ugetElem_eq_getElem, Array.set_set, updateBucket]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem not_dvd_ordCompl {n p : ℕ} (hp : Prime p) (hn : n ≠ 0) : ¬p ∣ ordCompl[p] n

Proof state:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ (n.factorization - (p ^ n.factorization p).factorization) p

Tactic:
simp [hp.factorization]

Result:
no goals

Proof state:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ (n / p ^ n.factorization p).factorization p

Tactic:
rw [Nat.factorization_div (Nat.ordProj_dvd n p)]

Result:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ (n.factorization - (p ^ n.factorization p).factorization) p

Proof state:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬p ∣ n / p ^ n.factorization p

Tactic:
rw [Nat.Prime.dvd_iff_one_le_factorization hp (ordCompl_pos p hn).ne']

Result:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ (n / p ^ n.factorization p).factorization p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) : setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y

Proof state:
case pred.isFalse
v w' v' : Nat
x : BitVec v
y : BitVec w'
i : Nat
h : i < v' + w'
h✝ : ¬i < w'
⊢ x.getLsbD (i - w') = (decide (i - w' < v') && x.getLsbD (i - w'))

Tactic:
simp_all only [Bool.iff_and_self, decide_eq_true_eq]

Result:
case pred.isFalse
v w' v' : Nat
x : BitVec v
y : BitVec w'
i : Nat
h : i < v' + w'
h✝ : ¬i < w'
⊢ x.getLsbD (i - w') = true → i - w' < v'

Proof state:
case pred
v w' v' : Nat
x : BitVec v
y : BitVec w'
i : Nat
h : i < v' + w'
⊢ (if i < w' then y.getLsbD i else x.getLsbD (i - w')) =
    if i < w' then y.getLsbD i else decide (i - w' < v') && x.getLsbD (i - w')

Tactic:
split

Result:
case pred.isTrue
v w' v' : Nat
x : BitVec v
y : BitVec w'
i : Nat
h : i < v' + w'
h✝ : i < w'
⊢ y.getLsbD i = y.getLsbD i

case pred.isFalse
v w' v' : Nat
x : BitVec v
y : BitVec w'
i : Nat
h : i < v' + w'
h✝ : ¬i < w'
⊢ x.getLsbD (i - w') = (decide (i - w' < v') && x.getLsbD (i - w'))

Proof state:
v w w' v' : Nat
x : BitVec v
y : BitVec w
h : w' = w
⊢ setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y

Tactic:
subst h

Result:
v w' v' : Nat
x : BitVec v
y : BitVec w'
⊢ setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y

Proof state:
case pred.isFalse
v w' v' : Nat
x : BitVec v
y : BitVec w'
i : Nat
h✝¹ : i < v' + w'
h✝ : ¬i < w'
h : x.getLsbD (i - w') = true
⊢ i - w' < v'

Tactic:
omega

Result:
no goals

Proof state:
v w' v' : Nat
x : BitVec v
y : BitVec w'
⊢ setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y

Tactic:
ext i h

Result:
case pred
v w' v' : Nat
x : BitVec v
y : BitVec w'
i : Nat
h : i < v' + w'
⊢ (setWidth (v' + w') (x ++ y)).getLsbD i = (setWidth v' x ++ setWidth w' y).getLsbD i

Proof state:
case pred.isFalse
v w' v' : Nat
x : BitVec v
y : BitVec w'
i : Nat
h : i < v' + w'
h✝ : ¬i < w'
⊢ x.getLsbD (i - w') = true → i - w' < v'

Tactic:
intro h

Result:
case pred.isFalse
v w' v' : Nat
x : BitVec v
y : BitVec w'
i : Nat
h✝¹ : i < v' + w'
h✝ : ¬i < w'
h : x.getLsbD (i - w') = true
⊢ i - w' < v'

Proof state:
case pred
v w' v' : Nat
x : BitVec v
y : BitVec w'
i : Nat
h : i < v' + w'
⊢ (setWidth (v' + w') (x ++ y)).getLsbD i = (setWidth v' x ++ setWidth w' y).getLsbD i

Tactic:
simp only [getLsbD_setWidth, h, decide_true, getLsbD_append, cond_eq_if,
  decide_eq_true_eq, Bool.true_and, setWidth_eq]

Result:
case pred
v w' v' : Nat
x : BitVec v
y : BitVec w'
i : Nat
h : i < v' + w'
⊢ (if i < w' then y.getLsbD i else x.getLsbD (i - w')) =
    if i < w' then y.getLsbD i else decide (i - w' < v') && x.getLsbD (i - w')

Proof state:
case pred.isTrue
v w' v' : Nat
x : BitVec v
y : BitVec w'
i : Nat
h : i < v' + w'
h✝ : i < w'
⊢ y.getLsbD i = y.getLsbD i

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_eq_mkArray_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} {b : β} :
    l.mapFinIdx f = mkArray l.size b ↔ ∀ (i : Nat) (h : i < l.size), f i l[i] h = b

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : (i : Nat) → α → i < l.size → β
b : β
⊢ l.mapFinIdx f = mkArray l.size b ↔ ∀ (i : Nat) (h : i < l.size), f i l[i] h = b

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
⊢ { toList := l }.mapFinIdx f = mkArray { toList := l }.size b ↔
    ∀ (i : Nat) (h : i < { toList := l }.size), f i { toList := l }[i] h = b

Proof state:
case mk
α : Type u_1
β : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
⊢ ({ toList := l }.mapFinIdx f).toList = (mkArray { toList := l }.size b).toList ↔
    ∀ (i : Nat) (h : i < { toList := l }.size), f i { toList := l }[i] h = b

Tactic:
simp [List.mapFinIdx_eq_replicate_iff]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
⊢ { toList := l }.mapFinIdx f = mkArray { toList := l }.size b ↔
    ∀ (i : Nat) (h : i < { toList := l }.size), f i { toList := l }[i] h = b

Tactic:
rw [← toList_inj]

Result:
case mk
α : Type u_1
β : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
⊢ ({ toList := l }.mapFinIdx f).toList = (mkArray { toList := l }.size b).toList ↔
    ∀ (i : Nat) (h : i < { toList := l }.size), f i { toList := l }[i] h = b
-- Mathlib/Analysis/Fourier/ZMod.lean
/-- The discrete Fourier transform of `Φ` is odd if and only if `Φ` itself is. -/
lemma dft_odd_iff {Φ : ZMod N → ℂ} : (𝓕 Φ).Odd ↔ Φ.Odd

Proof state:
N : ℕ
inst✝ : NeZero N
Φ f : ZMod N → ℂ
hf : Function.Odd f
⊢ Function.Odd (𝓕 f)

Tactic:
simp only [Function.Odd, ← congr_fun (dft_comp_neg f), funext hf, ← Pi.neg_apply, map_neg,
  implies_true]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Function.Odd (𝓕 Φ) ↔ Function.Odd Φ

Tactic:
have h {f : ZMod N → ℂ} (hf : f.Odd) : (𝓕 f).Odd := by
  simp only [Function.Odd, ← congr_fun (dft_comp_neg f), funext hf, ← Pi.neg_apply, map_neg,
    implies_true]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Odd f → Function.Odd (𝓕 f)
⊢ Function.Odd (𝓕 Φ) ↔ Function.Odd Φ

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Odd f → Function.Odd (𝓕 f)
⊢ Function.Odd (𝓕 Φ) ↔ Function.Odd Φ

Tactic:
refine ⟨fun hΦ x ↦ ?_, h⟩

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Odd f → Function.Odd (𝓕 f)
hΦ : Function.Odd (𝓕 Φ)
x : ZMod N
⊢ Φ (-x) = -Φ x

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Odd f → Function.Odd (𝓕 f)
hΦ : Function.Odd (𝓕 Φ)
x : ZMod N
⊢ Φ (-x) = -Φ x

Tactic:
simpa only [neg_neg, dft_dft, ← smul_neg, smul_right_inj (NeZero.ne (N : ℂ))] using h hΦ (-x)

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValNat_mul_div_factorial (n : ℕ) [hp : Fact p.Prime] :
    padicValNat p (p * (n / p))! = padicValNat p n !

Proof state:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValNat p (p * (n / p))! = padicValNat p (p * (n / p) + n % p)!

Tactic:
exact (padicValNat_factorial_mul_add (n / p) <| mod_lt n hp.out.pos).symm

Result:
no goals

Proof state:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValNat p (p * (n / p))! = padicValNat p n !

Tactic:
nth_rw 2 [← div_add_mod n p]

Result:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValNat p (p * (n / p))! = padicValNat p (p * (n / p) + n % p)!
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem map_roots_le_of_injective [IsDomain A] [IsDomain B] (p : A[X]) {f : A →+* B}
    (hf : Function.Injective f) : p.roots.map f ≤ (p.map f).roots

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
⊢ Multiset.map (⇑f) p.roots ≤ (map f p).roots

Tactic:
by_cases hp0 : p = 0

Result:
case pos
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hp0 : p = 0
⊢ Multiset.map (⇑f) p.roots ≤ (map f p).roots

case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hp0 : ¬p = 0
⊢ Multiset.map (⇑f) p.roots ≤ (map f p).roots

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hp0 : ¬p = 0
⊢ Multiset.map (⇑f) p.roots ≤ (map f p).roots

Tactic:
exact map_roots_le ((Polynomial.map_ne_zero_iff hf).mpr hp0)

Result:
no goals

Proof state:
case pos
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hp0 : p = 0
⊢ Multiset.map (⇑f) p.roots ≤ (map f p).roots

Tactic:
simp only [hp0, roots_zero, Multiset.map_zero, Polynomial.map_zero, le_rfl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toFin_setWidth {x : BitVec w} :
    (x.setWidth v).toFin = Fin.ofNat' (2^v) x.toNat

Proof state:
w v : Nat
x : BitVec w
⊢ (setWidth v x).toFin = Fin.ofNat' (2 ^ v) x.toNat

Tactic:
ext

Result:
case h
w v : Nat
x : BitVec w
⊢ ↑(setWidth v x).toFin = ↑(Fin.ofNat' (2 ^ v) x.toNat)

Proof state:
case h
w v : Nat
x : BitVec w
⊢ ↑(setWidth v x).toFin = ↑(Fin.ofNat' (2 ^ v) x.toNat)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma liftCochain_snd :
    (liftCochain φ α β h).comp (snd φ) (add_zero n) = β

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
⊢ (liftCochain φ α β h).comp (snd φ) ⋯ = β

Tactic:
simp [liftCochain]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem inv_eq_empty : s⁻¹ = ∅ ↔ s = ∅

Proof state:
α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ s⁻¹ = ∅ ↔ s = ∅

Tactic:
rw [← image_inv_eq_inv, image_eq_empty]

Result:
no goals