harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma powerset_union (s t : Finset α) : (s ∪ t).powerset = s.powerset ⊻ t.powerset

Proof state:
case h.refine_2
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ (∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u) → u ⊆ s ∪ t

Tactic:
rintro ⟨v, hv, w, hw, rfl⟩

Result:
case h.refine_2.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
s t v : Finset α
hv : v ⊆ s
w : Finset α
hw : w ⊆ t
⊢ v ∪ w ⊆ s ∪ t

Proof state:
case h
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ u ∈ (s ∪ t).powerset ↔ u ∈ s.powerset ⊻ t.powerset

Tactic:
simp only [mem_sups, mem_powerset, le_eq_subset, sup_eq_union]

Result:
case h
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ u ⊆ s ∪ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u

Proof state:
case h
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ u ⊆ s ∪ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u

Tactic:
refine ⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩

Result:
case h.refine_1
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
h : u ⊆ s ∪ t
⊢ s ∩ u ∪ t ∩ u = u

case h.refine_2
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ (∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u) → u ⊆ s ∪ t

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∪ t).powerset = s.powerset ⊻ t.powerset

Tactic:
ext u

Result:
case h
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ u ∈ (s ∪ t).powerset ↔ u ∈ s.powerset ⊻ t.powerset

Proof state:
case h.refine_2.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
s t v : Finset α
hv : v ⊆ s
w : Finset α
hw : w ⊆ t
⊢ v ∪ w ⊆ s ∪ t

Tactic:
exact union_subset_union hv hw

Result:
no goals

Proof state:
case h.refine_1
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
h : u ⊆ s ∪ t
⊢ s ∩ u ∪ t ∩ u = u

Tactic:
rwa [← union_inter_distrib_right, inter_eq_right]

Result:
no goals
-- Mathlib/RingTheory/IntegralDomain.lean
theorem sum_hom_units (f : G →* R) [Decidable (f = 1)] :
    ∑ g : G, f g = if f = 1 then Fintype.card G else 0

Proof state:
case pos
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : f = 1
⊢ ∑ g : G, f g = ↑(Fintype.card G)

Tactic:
simp [h, card_univ]

Result:
no goals

Proof state:
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
⊢ ∑ g : G, f g = ↑(if f = 1 then Fintype.card G else 0)

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : f = 1
⊢ ∑ g : G, f g = ↑(Fintype.card G)

case neg
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g : G, f g = ↑0

Proof state:
case neg
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g : G, f g = 0

Tactic:
exact sum_hom_units_eq_zero f h

Result:
no goals

Proof state:
case neg
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g : G, f g = ↑0

Tactic:
rw [cast_zero]

Result:
case neg
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g : G, f g = 0
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem Associated.irreducible [Monoid M] {p q : M} (h : p ~ᵤ q) (hp : Irreducible p) :
    Irreducible q :=
  ⟨mt h.symm.isUnit hp.1,
    let ⟨u, hu⟩ := h
    fun a b hab =>
    have hpab : p = a * (b * (u⁻¹ : Mˣ)) :=
      calc
        p = p * u * (u⁻¹ : Mˣ)

Proof state:
M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ q * ↑u⁻¹ = a * (b * ↑u⁻¹)

Tactic:
simp [hab, mul_assoc]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ p = p * ↑u * ↑u⁻¹

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
hpab : p = a * (b * ↑u⁻¹)
x✝ : IsUnit (b * ↑u⁻¹)
v : Mˣ
hv : ↑v = b * ↑u⁻¹
⊢ ↑(v * u) = b

Tactic:
simp [hv]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ p * ↑u * ↑u⁻¹ = a * (b * ↑u⁻¹)

Tactic:
rw [hu]

Result:
M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ q * ↑u⁻¹ = a * (b * ↑u⁻¹)
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
lemma integrable_integral_norm_of_integrable_comp (h_int : Integrable f (κ ∘ₘ μ)) :
    Integrable (fun x ↦ ∫ y, ‖f y‖ ∂κ x) μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
E : Type u_4
inst✝ : NormedAddCommGroup E
f : β → E
h_int : Integrable f (⇑κ ∘ₘ μ)
⊢ Integrable (fun x => ∫ (y : β), ‖f y‖ ∂κ x) μ

Tactic:
rw [comp_eq_comp_const_apply, integrable_comp_iff h_int.1] at h_int

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
E : Type u_4
inst✝ : NormedAddCommGroup E
f : β → E
h_int :
  (∀ᵐ (y : α) ∂(Kernel.const Unit μ) (), Integrable f (κ y)) ∧
    Integrable (fun y => ∫ (z : β), ‖f z‖ ∂κ y) ((Kernel.const Unit μ) ())
⊢ Integrable (fun x => ∫ (y : β), ‖f y‖ ∂κ x) μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
E : Type u_4
inst✝ : NormedAddCommGroup E
f : β → E
h_int :
  (∀ᵐ (y : α) ∂(Kernel.const Unit μ) (), Integrable f (κ y)) ∧
    Integrable (fun y => ∫ (z : β), ‖f z‖ ∂κ y) ((Kernel.const Unit μ) ())
⊢ Integrable (fun x => ∫ (y : β), ‖f y‖ ∂κ x) μ

Tactic:
exact h_int.2

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem IsSeparable.exists_countable_dense_subset
    {s : Set α} (hs : IsSeparable s) : ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsSeparable s
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε

Tactic:
rcases hs with ⟨t, htc, hst⟩

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0∞
ε0 : ε > 0
t : Set α
htc : t.Countable
hst : s ⊆ closure t
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsSeparable s
this : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

Tactic:
exact subset_countable_closure_of_almost_dense_set _ this

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0∞
ε0 : ε > 0
t : Set α
htc : t.Countable
hst : s ⊆ closure t
x : α
hx : x ∈ closure t
y : α
hyt : y ∈ t
hxy : edist x y < ε
⊢ x ∈ ⋃ x ∈ t, closedBall x ε

Tactic:
exact mem_iUnion₂.2 ⟨y, hyt, mem_closedBall.2 hxy.le⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0∞
ε0 : ε > 0
t : Set α
htc : t.Countable
hst : s ⊆ closure t
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε

Tactic:
refine ⟨t, htc, hst.trans fun x hx => ?_⟩

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0∞
ε0 : ε > 0
t : Set α
htc : t.Countable
hst : s ⊆ closure t
x : α
hx : x ∈ closure t
⊢ x ∈ ⋃ x ∈ t, closedBall x ε

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0∞
ε0 : ε > 0
t : Set α
htc : t.Countable
hst : s ⊆ closure t
x : α
hx : x ∈ closure t
⊢ x ∈ ⋃ x ∈ t, closedBall x ε

Tactic:
rcases mem_closure_iff.1 hx ε ε0 with ⟨y, hyt, hxy⟩

Result:
case intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0∞
ε0 : ε > 0
t : Set α
htc : t.Countable
hst : s ⊆ closure t
x : α
hx : x ∈ closure t
y : α
hyt : y ∈ t
hxy : edist x y < ε
⊢ x ∈ ⋃ x ∈ t, closedBall x ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsSeparable s
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

Tactic:
have : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε := fun ε ε0 => by
  rcases hs with ⟨t, htc, hst⟩
  refine ⟨t, htc, hst.trans fun x hx => ?_⟩
  rcases mem_closure_iff.1 hx ε ε0 with ⟨y, hyt, hxy⟩
  exact mem_iUnion₂.2 ⟨y, hyt, mem_closedBall.2 hxy.le⟩

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsSeparable s
this : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullbackWithin_eq_pullbackWithin {f : E → E'} {V : E' → E'} {s : Set E} :
    mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s = pullbackWithin 𝕜 f V s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_6
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
V : E' → E'
s : Set E
⊢ mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s = pullbackWithin 𝕜 f V s

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_6
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
V : E' → E'
s : Set E
x : E
⊢ mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s x = pullbackWithin 𝕜 f V s x

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_6
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
V : E' → E'
s : Set E
x : E
⊢ (fderivWithin 𝕜 f s x).inverse (V (f x)) = (fderivWithin 𝕜 f s x).inverse (V (f x))

Tactic:
rfl

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_6
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
V : E' → E'
s : Set E
x : E
⊢ mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s x = pullbackWithin 𝕜 f V s x

Tactic:
simp only [mpullbackWithin, mfderivWithin_eq_fderivWithin, pullbackWithin]

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_6
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
V : E' → E'
s : Set E
x : E
⊢ (fderivWithin 𝕜 f s x).inverse (V (f x)) = (fderivWithin 𝕜 f s x).inverse (V (f x))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_rotateRight {r w : Nat} {x : BitVec w} :
    (x.rotateRight r).msb = x.getMsbD ((w - r % w) % w)

Proof state:
case pos
r w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : r % w = 0
⊢ x.getMsbD 0 = x.getMsbD ((w - r % w) % w)

Tactic:
simp [h₁]

Result:
no goals

Proof state:
case pos
r w : Nat
x : BitVec w
h₀ : 0 < w
⊢ (decide (0 < w) && if 0 < r % w then x.getMsbD ((w + 0 - r % w) % w) else x.getMsbD (0 - r % w)) =
    x.getMsbD ((w - r % w) % w)

Tactic:
simp only [h₀, decide_true, Nat.add_zero, Nat.zero_le, Nat.sub_eq_zero_of_le, Bool.true_and,
ite_eq_left_iff, Nat.not_lt, Nat.le_zero_eq]

Result:
case pos
r w : Nat
x : BitVec w
h₀ : 0 < w
⊢ r % w = 0 → x.getMsbD 0 = x.getMsbD ((w - r % w) % w)

Proof state:
r w : Nat
x : BitVec w
h₀ : ¬0 < w
⊢ w = 0

Tactic:
omega

Result:
no goals

Proof state:
r w : Nat
x : BitVec w
⊢ (x.rotateRight r).msb = x.getMsbD ((w - r % w) % w)

Tactic:
simp only [BitVec.msb, getMsbD_rotateRight]

Result:
r w : Nat
x : BitVec w
⊢ (decide (0 < w) && if 0 < r % w then x.getMsbD ((w + 0 - r % w) % w) else x.getMsbD (0 - r % w)) =
    x.getMsbD ((w - r % w) % w)

Proof state:
case neg
r w : Nat
x : BitVec w
h₀ : ¬0 < w
⊢ (decide (0 < w) && if 0 < r % w then x.getMsbD ((w + 0 - r % w) % w) else x.getMsbD (0 - r % w)) =
    x.getMsbD ((w - r % w) % w)

Tactic:
simp [show w = 0 by omega]

Result:
no goals

Proof state:
case pos
r w : Nat
x : BitVec w
h₀ : 0 < w
⊢ r % w = 0 → x.getMsbD 0 = x.getMsbD ((w - r % w) % w)

Tactic:
intro h₁

Result:
case pos
r w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : r % w = 0
⊢ x.getMsbD 0 = x.getMsbD ((w - r % w) % w)

Proof state:
r w : Nat
x : BitVec w
⊢ (decide (0 < w) && if 0 < r % w then x.getMsbD ((w + 0 - r % w) % w) else x.getMsbD (0 - r % w)) =
    x.getMsbD ((w - r % w) % w)

Tactic:
by_cases h₀ : 0 < w

Result:
case pos
r w : Nat
x : BitVec w
h₀ : 0 < w
⊢ (decide (0 < w) && if 0 < r % w then x.getMsbD ((w + 0 - r % w) % w) else x.getMsbD (0 - r % w)) =
    x.getMsbD ((w - r % w) % w)

case neg
r w : Nat
x : BitVec w
h₀ : ¬0 < w
⊢ (decide (0 < w) && if 0 < r % w then x.getMsbD ((w + 0 - r % w) % w) else x.getMsbD (0 - r % w)) =
    x.getMsbD ((w - r % w) % w)
-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
lemma map_smul :
    A.val.map π (smul α φ r m) = smul α φ (R.val.map π r) (A.val.map π m)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y✝ : Cᵒᵖ
π : X ⟶ Y✝
r : ↑(R.val.obj X)
m : ↑(A.val.obj X)
S : Sieve (Opposite.unop Y✝) :=
  Presheaf.imageSieve α ((ConcreteCategory.hom (R.val.map π)) r) ⊓
    Presheaf.imageSieve φ ((ConcreteCategory.hom (A.val.map π)) m)
hS : S ∈ J (Opposite.unop Y✝)
Y : C
f : Y ⟶ Opposite.unop Y✝
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ :
  (RingCat.Hom.hom (α.app (Opposite.op Y))) r₀ = (RingCat.Hom.hom (R.val.map f.op)) ((RingCat.Hom.hom (R.val.map π)) r)
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ :
  (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ =
    (ConcreteCategory.hom (A.val.map f.op)) ((ConcreteCategory.hom (A.val.map π)) m)
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.val.map (π ≫ f.op))) m

Tactic:
rw [hm₀, Functor.map_comp, ConcreteCategory.comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldrM_start_stop {m} [Monad m] (l : Array α) (f : α → β → m β) (b) (start stop : Nat) :
    l.foldrM f b start stop = (l.extract stop start).foldrM f b

Proof state:
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : α → β → m β
start stop : Nat
⊢ ∀ (b : β),
    stop ≤ min start l.size →
      foldrM.fold f l stop (min start l.size) ⋯ b = foldrM.fold f (l.extract stop start) 0 (min start l.size - stop) ⋯ b

Tactic:
suffices ∀ (b : β) (i) (w : stop + i ≤ min start l.size),
    foldrM.fold f l stop (stop + i) (by omega) b =
      foldrM.fold f (l.extract stop start) 0 i (by simp; omega) b by
  intro b w
  specialize this b (min start l.size - stop)
  have h : stop + (min start l.size - stop) = min start l.size := by omega
  simp_all

Result:
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : α → β → m β
start stop : Nat
⊢ ∀ (b : β) (i : Nat) (w : stop + i ≤ min start l.size),
    foldrM.fold f l stop (stop + i) ⋯ b = foldrM.fold f (l.extract stop start) 0 i ⋯ b

Proof state:
case succ
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : α → β → m β
start stop i : Nat
ih :
  ∀ (b : β) (w : stop + i ≤ min start l.size),
    foldrM.fold f l stop (stop + i) ⋯ b = foldrM.fold f (l.extract stop start) 0 i ⋯ b
b : β
w : stop + (i + 1) ≤ min start l.size
⊢ (if (stop + (i + 1) == stop) = true then pure b
    else
      match stop + (i + 1), ⋯ with
      | 0, x => pure b
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f l[i] b
        foldrM.fold f l stop i ⋯ __do_lift) =
    if (i + 1 == 0) = true then pure b
    else
      match i + 1, ⋯ with
      | 0, x => pure b
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f (l.extract stop start)[i] b
        foldrM.fold f (l.extract stop start) 0 i ⋯ __do_lift

Tactic:
simp only [beq_iff_eq, Nat.add_right_eq_self, Nat.add_one_ne_zero, ↓reduceIte, Nat.add_eq,
  getElem_extract]

Result:
case succ
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : α → β → m β
start stop i : Nat
ih :
  ∀ (b : β) (w : stop + i ≤ min start l.size),
    foldrM.fold f l stop (stop + i) ⋯ b = foldrM.fold f (l.extract stop start) 0 i ⋯ b
b : β
w : stop + (i + 1) ≤ min start l.size
⊢ (do
      let __do_lift ← f l[stop + i] b
      foldrM.fold f l stop (stop + i) ⋯ __do_lift) =
    do
    let __do_lift ← f l[stop + i] b
    foldrM.fold f (l.extract stop start) 0 i ⋯ __do_lift
-- Mathlib/Algebra/Order/Star/Basic.lean
/-- When `R` is a non-unital ring, to construct a `StarOrderedRing` instance it suffices to
show that the nonnegative elements are precisely those elements of the form `star s * s`
for `s : R`.

This is provided for convenience because it holds in many common scenarios (e.g.,`ℝ`, `ℂ`, or
any C⋆-algebra), and obviates the hassle of `AddSubmonoid.closure_induction` when creating those
instances. -/
lemma of_nonneg_iff' [NonUnitalRing R] [PartialOrder R] [StarRing R]
    (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
    (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ ∃ s, x = star s * s) : StarOrderedRing R :=
  of_le_iff <| by
    have : AddLeftMono R := ⟨fun _ _ _ h => h_add h _⟩
    simpa [sub_eq_iff_eq_add', sub_nonneg] using fun x y => h_nonneg_iff (y - x)

Proof state:
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ ∃ s, x = star s * s
⊢ ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s

Tactic:
have : AddLeftMono R := ⟨fun _ _ _ h => h_add h _⟩

Result:
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ ∃ s, x = star s * s
this : AddLeftMono R
⊢ ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s

Proof state:
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ ∃ s, x = star s * s
this : AddLeftMono R
⊢ ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s

Tactic:
simpa [sub_eq_iff_eq_add', sub_nonneg] using fun x y => h_nonneg_iff (y - x)

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma lieBracketWithin_add_left (hV : DifferentiableWithinAt 𝕜 V s x)
    (hV₁ : DifferentiableWithinAt 𝕜 V₁ s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
    lieBracketWithin 𝕜 (V + V₁) W s x =
      lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V₁ W s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
s : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hV₁ : DifferentiableWithinAt 𝕜 V₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 W s x) (V x) + (fderivWithin 𝕜 W s x) (V₁ x) - (fderivWithin 𝕜 (V + V₁) s x) (W x) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W s x) (V₁ x) - (fderivWithin 𝕜 V₁ s x) (W x))

Tactic:
rw [fderivWithin_add' hs hV hV₁, ContinuousLinearMap.add_apply]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
s : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hV₁ : DifferentiableWithinAt 𝕜 V₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 W s x) (V x) + (fderivWithin 𝕜 W s x) (V₁ x) -
      ((fderivWithin 𝕜 V s x) (W x) + (fderivWithin 𝕜 V₁ s x) (W x)) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W s x) (V₁ x) - (fderivWithin 𝕜 V₁ s x) (W x))

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
s : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hV₁ : DifferentiableWithinAt 𝕜 V₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ lieBracketWithin 𝕜 (V + V₁) W s x = lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V₁ W s x

Tactic:
simp only [lieBracketWithin, Pi.add_apply, map_add]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
s : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hV₁ : DifferentiableWithinAt 𝕜 V₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 W s x) (V x) + (fderivWithin 𝕜 W s x) (V₁ x) - (fderivWithin 𝕜 (V + V₁) s x) (W x) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W s x) (V₁ x) - (fderivWithin 𝕜 V₁ s x) (W x))

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
s : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hV₁ : DifferentiableWithinAt 𝕜 V₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 W s x) (V x) + (fderivWithin 𝕜 W s x) (V₁ x) -
      ((fderivWithin 𝕜 V s x) (W x) + (fderivWithin 𝕜 V₁ s x) (W x)) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W s x) (V₁ x) - (fderivWithin 𝕜 V₁ s x) (W x))

Tactic:
abel

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_eq_nil_iff {p : α → Prop} {f : ∀ a, p a → β} {l H} : pmap f l H = [] ↔ l = []

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
⊢ pmap f l H = [] ↔ l = []

Tactic:
rw [← length_eq_zero, length_pmap, length_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_twoPow {i j w: Nat} :
    (twoPow w i).getMsbD j = (decide (i < w) && decide (j = w - i - 1))

Proof state:
i j w : Nat
⊢ (twoPow w i).getMsbD j = (decide (i < w) && decide (j = w - i - 1))

Tactic:
simp only [getMsbD_eq_getLsbD, getLsbD_twoPow]

Result:
i j w : Nat
⊢ (decide (j < w) && (decide (i < w) && decide (i = w - 1 - j))) = (decide (i < w) && decide (j = w - i - 1))

Proof state:
i j w : Nat
⊢ (decide (j < w) && (decide (i < w) && decide (i = w - 1 - j))) = (decide (i < w) && decide (j = w - i - 1))

Tactic:
by_cases h₀ : i < w <;> by_cases h₁ : j < w <;>
simp [h₀, h₁] <;> omega

Result:
no goals