harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftRight_sub_one_eq_shiftConcat (n : BitVec w) (hwn : 0 < wn) :
    n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1))

Proof state:
case pred
w wn : Nat
n : BitVec w
hwn : 0 < wn
i : Nat
h : i < w
⊢ n.getLsbD (wn - 1 + i) = if i = 0 then n.getLsbD (wn - 1) else n.getLsbD (wn + (i - 1))

Tactic:
split

Result:
case pred.isTrue
w wn : Nat
n : BitVec w
hwn : 0 < wn
i : Nat
h : i < w
h✝ : i = 0
⊢ n.getLsbD (wn - 1 + i) = n.getLsbD (wn - 1)

case pred.isFalse
w wn : Nat
n : BitVec w
hwn : 0 < wn
i : Nat
h : i < w
h✝ : ¬i = 0
⊢ n.getLsbD (wn - 1 + i) = n.getLsbD (wn + (i - 1))

Proof state:
case pred.isFalse
w wn : Nat
n : BitVec w
hwn : 0 < wn
i : Nat
h : i < w
h✝ : ¬i = 0
⊢ n.getLsbD (wn - 1 + i) = n.getLsbD (wn + (i - 1))

Tactic:
congr 1

Result:
case pred.isFalse.e_i
w wn : Nat
n : BitVec w
hwn : 0 < wn
i : Nat
h : i < w
h✝ : ¬i = 0
⊢ wn - 1 + i = wn + (i - 1)

Proof state:
w wn : Nat
n : BitVec w
hwn : 0 < wn
⊢ n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1))

Tactic:
ext i h

Result:
case pred
w wn : Nat
n : BitVec w
hwn : 0 < wn
i : Nat
h : i < w
⊢ (n >>> (wn - 1)).getLsbD i = ((n >>> wn).shiftConcat (n.getLsbD (wn - 1))).getLsbD i

Proof state:
case pred
w wn : Nat
n : BitVec w
hwn : 0 < wn
i : Nat
h : i < w
⊢ (n >>> (wn - 1)).getLsbD i = ((n >>> wn).shiftConcat (n.getLsbD (wn - 1))).getLsbD i

Tactic:
simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, h, decide_true, Bool.true_and]

Result:
case pred
w wn : Nat
n : BitVec w
hwn : 0 < wn
i : Nat
h : i < w
⊢ n.getLsbD (wn - 1 + i) = if i = 0 then n.getLsbD (wn - 1) else n.getLsbD (wn + (i - 1))

Proof state:
case pred.isTrue
w wn : Nat
n : BitVec w
hwn : 0 < wn
i : Nat
h : i < w
h✝ : i = 0
⊢ n.getLsbD (wn - 1 + i) = n.getLsbD (wn - 1)

Tactic:
simp [*]

Result:
no goals

Proof state:
case pred.isFalse.e_i
w wn : Nat
n : BitVec w
hwn : 0 < wn
i : Nat
h : i < w
h✝ : ¬i = 0
⊢ wn - 1 + i = wn + (i - 1)

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem finMulAntidiag_one {d : ℕ} :
    finMulAntidiag d 1 = {fun _ => 1}

Proof state:
d : ℕ
⊢ d.finMulAntidiag 1 = {fun x => 1}

Tactic:
ext f

Result:
case h
d : ℕ
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag 1 ↔ f ∈ {fun x => 1}

Proof state:
case h.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i

Tactic:
exact dvd_prod_of_mem f (mem_univ _)

Result:
no goals

Proof state:
case h
d : ℕ
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag 1 ↔ f ∈ {fun x => 1}

Tactic:
simp only [mem_finMulAntidiag, and_true, mem_singleton]

Result:
case h
d : ℕ
f : Fin d → ℕ
⊢ ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0 ↔ f = fun x => 1

Proof state:
case h.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i = 1

Tactic:
rw [← Nat.dvd_one, ← hf]

Result:
case h.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i

Proof state:
case h.mp
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
⊢ f = fun x => 1

Tactic:
ext i

Result:
case h.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i = 1

Proof state:
case h.mpr
d : ℕ
f : Fin d → ℕ
⊢ (f = fun x => 1) → ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0

Tactic:
rintro rfl

Result:
case h.mpr
d : ℕ
⊢ ∏ i : Fin d, (fun x => 1) i = 1 ∧ 1 ≠ 0

Proof state:
case h.mp
d : ℕ
f : Fin d → ℕ
⊢ ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0 → f = fun x => 1

Tactic:
intro ⟨hf, _⟩

Result:
case h.mp
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
⊢ f = fun x => 1

Proof state:
case h
d : ℕ
f : Fin d → ℕ
⊢ ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0 ↔ f = fun x => 1

Tactic:
constructor

Result:
case h.mp
d : ℕ
f : Fin d → ℕ
⊢ ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0 → f = fun x => 1

case h.mpr
d : ℕ
f : Fin d → ℕ
⊢ (f = fun x => 1) → ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0

Proof state:
case h.mpr
d : ℕ
⊢ ∏ i : Fin d, (fun x => 1) i = 1 ∧ 1 ≠ 0

Tactic:
simp only [prod_const_one, implies_true, ne_eq, one_ne_zero, not_false_eq_true, and_self]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem borel_eq_generateFrom_Iio_rat : borel ℝ = .generateFrom (⋃ a : ℚ, {Iio (a : ℝ)})

Proof state:
a : ℝ
⊢ IsLUB (range Rat.cast ∩ Iio a) a

Tactic:
simp [isLUB_iff_le_iff, mem_upperBounds, ← le_iff_forall_rat_lt_imp_le]

Result:
no goals

Proof state:
⊢ borel ℝ = generateFrom (⋃ a, {Iio ↑a})

Tactic:
rw [borel_eq_generateFrom_Iio]

Result:
⊢ generateFrom (range Iio) = generateFrom (⋃ a, {Iio ↑a})

Proof state:
⊢ generateFrom (range Iio) = generateFrom (⋃ a, {Iio ↑a})

Tactic:
refine le_antisymm
  (generateFrom_le ?_)
  (generateFrom_mono <| iUnion_subset fun q ↦ singleton_subset_iff.mpr <| mem_range_self _)

Result:
⊢ ∀ t ∈ range Iio, MeasurableSet t

Proof state:
a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
b : ℚ
x✝ : b ∈ Rat.cast ⁻¹' Iio a
⊢ Iio ↑b ∈ ⋃ a, {Iio ↑a}

Tactic:
simp

Result:
no goals

Proof state:
case intro
a : ℝ
⊢ MeasurableSet (Iio a)

Tactic:
have : IsLUB (range ((↑) : ℚ → ℝ) ∩ Iio a) a := by
  simp [isLUB_iff_le_iff, mem_upperBounds, ← le_iff_forall_rat_lt_imp_le]

Result:
case intro
a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
⊢ MeasurableSet (Iio a)

Proof state:
case intro
a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
⊢ MeasurableSet (Iio a)

Tactic:
rw [← this.biUnion_Iio_eq, ← image_univ, ← image_inter_preimage, univ_inter, biUnion_image]

Result:
case intro
a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
⊢ MeasurableSet (⋃ y ∈ Rat.cast ⁻¹' Iio a, Iio ↑y)

Proof state:
case intro
a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
⊢ MeasurableSet (⋃ y ∈ Rat.cast ⁻¹' Iio a, Iio ↑y)

Tactic:
exact MeasurableSet.biUnion (to_countable _)
  fun b _ => GenerateMeasurable.basic (Iio (b : ℝ)) (by simp)

Result:
no goals

Proof state:
⊢ ∀ t ∈ range Iio, MeasurableSet t

Tactic:
rintro _ ⟨a, rfl⟩

Result:
case intro
a : ℝ
⊢ MeasurableSet (Iio a)
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiff_iff_ftaylorSeries {n : ℕ∞} :
    ContDiff 𝕜 n f ↔ HasFTaylorSeriesUpTo n f (ftaylorSeries 𝕜 f)

Proof state:
case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ HasFTaylorSeriesUpTo (↑n) f (ftaylorSeries 𝕜 f) → ContDiff 𝕜 (↑n) f

Tactic:
exact fun h ↦ ⟨ftaylorSeries 𝕜 f, h⟩

Result:
no goals

Proof state:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ → HasFTaylorSeriesUpToOn (↑n) f (ftaylorSeriesWithin 𝕜 f univ) univ

Tactic:
exact fun h ↦ ContDiffOn.ftaylorSeriesWithin h uniqueDiffOn_univ

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiff 𝕜 (↑n) f ↔ HasFTaylorSeriesUpTo (↑n) f (ftaylorSeries 𝕜 f)

Tactic:
constructor

Result:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiff 𝕜 (↑n) f → HasFTaylorSeriesUpTo (↑n) f (ftaylorSeries 𝕜 f)

case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ HasFTaylorSeriesUpTo (↑n) f (ftaylorSeries 𝕜 f) → ContDiff 𝕜 (↑n) f

Proof state:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiff 𝕜 (↑n) f → HasFTaylorSeriesUpTo (↑n) f (ftaylorSeries 𝕜 f)

Tactic:
rw [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ]

Result:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ → HasFTaylorSeriesUpToOn (↑n) f (ftaylorSeriesWithin 𝕜 f univ) univ
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
/-- The image of `exteriorPower.ιMulti` spans `⋀[R]^n M`. -/
lemma ιMulti_span :
    Submodule.span R (Set.range (ιMulti R n)) = (⊤ : Submodule R (⋀[R]^n M))

Proof state:
case a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.map (⋀[R]^n M).subtype (Submodule.span R (Set.range ⇑(ιMulti R n))) = Submodule.map (⋀[R]^n M).subtype ⊤

Tactic:
rw [LinearMap.map_span, ← Set.image_univ, Set.image_image]

Result:
case a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.span R ((fun x => (⋀[R]^n M).subtype ((ιMulti R n) x)) '' Set.univ) = Submodule.map (⋀[R]^n M).subtype ⊤

Proof state:
case a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.span R ((fun x => (⋀[R]^n M).subtype ((ιMulti R n) x)) '' Set.univ) = Submodule.map (⋀[R]^n M).subtype ⊤

Tactic:
simp only [Submodule.coe_subtype, ιMulti_apply_coe, Set.image_univ, Submodule.map_top,
  Submodule.range_subtype]

Result:
case a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.span R (Set.range fun a => (ExteriorAlgebra.ιMulti R n) a) = ⋀[R]^n M

Proof state:
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.span R (Set.range ⇑(ιMulti R n)) = ⊤

Tactic:
apply LinearMap.map_injective (Submodule.ker_subtype (⋀[R]^n M))

Result:
case a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.map (⋀[R]^n M).subtype (Submodule.span R (Set.range ⇑(ιMulti R n))) = Submodule.map (⋀[R]^n M).subtype ⊤

Proof state:
case a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.span R (Set.range fun a => (ExteriorAlgebra.ιMulti R n) a) = ⋀[R]^n M

Tactic:
exact ExteriorAlgebra.ιMulti_span_fixedDegree R n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_induction
    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive as.size init) {f : α → β → β}
    (hf : ∀ i : Fin as.size, ∀ b, motive (i.1 + 1) b → motive i.1 (f as[i] b)) :
    motive 0 (as.foldr f init)

Proof state:
case h_1
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
b : β
x✝² : Nat
x✝¹ : x✝² ≤ as.size
x✝ : 0 ≤ as.size
H : motive 0 b
hi : ¬0 = 0
⊢ motive 0 b

case h_2
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
b : β
x✝¹ : Nat
x✝ : x✝¹ ≤ as.size
i✝ : Nat
h✝ : i✝ + 1 ≤ as.size
H : motive i✝.succ b
hi : ¬i✝.succ = 0
⊢ motive 0 (foldrM.fold f as 0 i✝ ⋯ (f as[i✝] b))

Tactic:
{simp at hi}

Result:
case h_2
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
b : β
x✝¹ : Nat
x✝ : x✝¹ ≤ as.size
i✝ : Nat
h✝ : i✝ + 1 ≤ as.size
H : motive i✝.succ b
hi : ¬i✝.succ = 0
⊢ motive 0 (foldrM.fold f as 0 i✝ ⋯ (f as[i✝] b))

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
b : β
x✝¹ : Nat
x✝ : x✝¹ ≤ as.size
i : Nat
hi' : i + 1 ≤ as.size
H : motive i.succ b
hi : ¬i.succ = 0
⊢ motive 0 (foldrM.fold f as 0 i ⋯ (f as[i] b))

Tactic:
exact go _ (hf ⟨i, hi'⟩ b H)

Result:
no goals

Proof state:
case isFalse
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
h✝ : ¬0 < as.size
⊢ motive 0 (Id.run init)

Tactic:
next h => exact (Nat.eq_zero_of_not_pos h ▸ h0)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
⊢ motive 0 (if 0 < as.size then foldrM.fold f as 0 as.size ⋯ init else init).run

Tactic:
split

Result:
case isTrue
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
h✝ : 0 < as.size
⊢ motive 0 (foldrM.fold f as 0 as.size ⋯ init).run

case isFalse
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
h✝ : ¬0 < as.size
⊢ motive 0 (Id.run init)
-- Mathlib/Data/Finset/Interval.lean
/-- A function `f` from `Finset α` is strictly monotone if and only if `f s < f (cons a s ha)` for
all `s` and `a ∉ s`. -/
lemma strictMono_iff_forall_lt_cons : StrictMono f ↔ ∀ s ⦃a⦄ ha, f s < f (cons a s ha)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f : Finset α → β
⊢ StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s < f (cons a s ha)

Tactic:
classical simp [strictMono_iff_forall_covBy, covBy_iff_exists_cons]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f : Finset α → β
⊢ StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s < f (cons a s ha)

Tactic:
simp [strictMono_iff_forall_covBy, covBy_iff_exists_cons]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem castNum_eq_bitwise {f : Num → Num → Num} {g : Bool → Bool → Bool}
    (p : PosNum → PosNum → Num)
    (gff : g false false = false) (f00 : f 0 0 = 0)
    (f0n : ∀ n, f 0 (pos n) = cond (g false true) (pos n) 0)
    (fn0 : ∀ n, f (pos n) 0 = cond (g true false) (pos n) 0)
    (fnn : ∀ m n, f (pos m) (pos n) = p m n) (p11 : p 1 1 = cond (g true true) 1 0)
    (p1b : ∀ b n, p 1 (PosNum.bit b n) = bit (g true b) (cond (g false true) (pos n) 0))
    (pb1 : ∀ a m, p (PosNum.bit a m) 1 = bit (g a true) (cond (g true false) (pos m) 0))
    (pbb : ∀ a b m n, p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)) :
    ∀ m n : Num, (f m n : ℕ) = Nat.bitwise g m n

Proof state:
case pos.pos.bit0.bit0
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit false n)) = Nat.bit (g false false) ↑(p m n)

Tactic:
rw [← bit_to_nat, pbb]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem toMul_multiset_sum (s : Multiset (Additive α)) : s.sum.toMul = (s.map toMul).prod

Proof state:
α : Type u_3
inst✝ : CommMonoid α
s : Multiset (Additive α)
⊢ s.sum = s.prod

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
inst✝ : CommMonoid α
s : Multiset (Additive α)
⊢ toMul s.sum = (Multiset.map (⇑toMul) s).prod

Tactic:
simp [toMul, ofMul]

Result:
α : Type u_3
inst✝ : CommMonoid α
s : Multiset (Additive α)
⊢ s.sum = s.prod
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem not_isReduced_alternatingWord (i i' : B) {m : ℕ} (hM : M i i' ≠ 0) (hm : m > M i i') :
    ¬cs.IsReduced (alternatingWord i i' m)

Proof state:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
⊢ cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1

Tactic:
have : M i i' + 1 ≤ M i i' * 2 := by linarith [Nat.one_le_iff_ne_zero.mpr hM]

Result:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1

Proof state:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
⊢ ¬cs.IsReduced (alternatingWord i i' (M.M i i').succ)

Tactic:
suffices h : ℓ (π (alternatingWord i i' (M i i' + 1))) < M i i' + 1 by
  unfold IsReduced
  rw [Nat.succ_eq_add_one, length_alternatingWord]
  omega

Result:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
⊢ cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
-- Mathlib/RingTheory/HopkinsLevitzki.lean
theorem induction
    {P : ∀ (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M], Prop}
    (h0 : ∀ (M) [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M]
      [IsSemisimpleModule R M], Module.IsTorsionBySet R M (Ring.jacobson R) → P M)
    (h1 : ∀ (M) [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M],
      let N := Ring.jacobson R • (⊤ : Submodule R M); P N → P (M ⧸ N) → P M) :
    P M

Proof state:
case succ.succ.refine_2
R₀ : Type u_1
R : Type u_2
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [inst_1 : Module R₀ M] → [inst : Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M]
    [inst_4 : IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    Jac ^ (n + 1) ≤ Module.annihilator R M → P M
hn : Jac ^ (n + 1 + 1) ≤ Module.annihilator R M
⊢ ∀ (x : M), ∀ r ∈ ↑(Jac ^ (n + 1)), r • x ∈ Jac • ⊤

Tactic:
exact fun m i hi ↦ Submodule.smul_mem_smul (Ideal.pow_le_self n.succ_ne_zero hi) trivial

Result:
no goals

Proof state:
case succ.zero
R₀ : Type u_1
R : Type u_2
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [inst_1 : Module R₀ M] → [inst : Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M]
    [inst_4 : IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
ih :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    Jac ^ 0 ≤ Module.annihilator R M → P M
hn : Jac ≤ Module.annihilator R M
⊢ P M

Tactic:
exact this hn

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_apply_ne_one (f : α → M) (a : α) : ∏ᶠ _ : f a ≠ 1, f a = f a

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
⊢ ∏ᶠ (_ : f a ≠ 1), f a = f a

Tactic:
rw [← mem_mulSupport, finprod_eq_mulIndicator_apply, mulIndicator_mulSupport]

Result:
no goals
-- Mathlib/RingTheory/Artinian/Algebra.lean
theorem isUnit_submonoid_eq_of_isIntegral [Algebra.IsIntegral R A] : IsUnit.submonoid A = A⁰

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsIntegral R A
⊢ IsUnit.submonoid A = A⁰

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsIntegral R A
x✝ : A
⊢ x✝ ∈ IsUnit.submonoid A ↔ x✝ ∈ A⁰

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsIntegral R A
x✝ : A
⊢ x✝ ∈ IsUnit.submonoid A ↔ x✝ ∈ A⁰

Tactic:
simpa [IsUnit.mem_submonoid_iff] using isUnit_iff_nonZeroDivisor_of_isIntegral' (R := R)

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
lemma inter_le_right : s ∩ t ≤ t

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
h : a ∈ t
⊢ (a ::ₘ s) ∩ t ≤ t

Tactic:
simpa [h] using cons_le_cons a (IH (t := t.erase a))

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t ≤ t

Tactic:
induction' s using Multiset.induction_on with a s IH generalizing t

Result:
case empty
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ 0 ∩ t ≤ t

case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
⊢ (a ::ₘ s) ∩ t ≤ t

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
⊢ (a ::ₘ s) ∩ t ≤ t

Tactic:
by_cases h : a ∈ t

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
h : a ∈ t
⊢ (a ::ₘ s) ∩ t ≤ t

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
h : a ∉ t
⊢ (a ::ₘ s) ∩ t ≤ t

Proof state:
case empty
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ 0 ∩ t ≤ t

Tactic:
exact (zero_inter t).symm ▸ zero_le _

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
h : a ∉ t
⊢ (a ::ₘ s) ∩ t ≤ t

Tactic:
simp [h, IH]

Result:
no goals