harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
theorem set_smul_span [SMulCommClass S R M] (s : Set S) (t : Set M) :
    s • span R t = span R (s • t)

Proof state:
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : Set S
t : Set M
⊢ s • span R t = span R (s • t)

Tactic:
simp_rw [set_smul_eq_iSup, smul_span, iSup_span, Set.iUnion_smul_set]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_eq_toNat_of_msb {x : BitVec w} (h : x.msb = false) :
    x.toInt = x.toNat

Proof state:
w : Nat
x : BitVec w
h : x.msb = false
⊢ x.toInt = ↑x.toNat

Tactic:
simp [toInt_eq_msb_cond, h]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma mul_le_mul_of_nonpos_right {a b c : EReal} (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c

Proof state:
a b c : EReal
h : b ≤ a
hc : 0 ≤ -c
⊢ -c * b ≤ -c * a

Tactic:
exact mul_le_mul_of_nonneg_left h hc

Result:
no goals

Proof state:
a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ a * c ≤ b * c

Tactic:
rw [mul_comm a c, mul_comm b c, ← neg_le_neg_iff, ← neg_mul c b, ← neg_mul c a]

Result:
a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ -c * b ≤ -c * a

Proof state:
a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ -c * b ≤ -c * a

Tactic:
rw [← neg_zero, EReal.le_neg] at hc

Result:
a b c : EReal
h : b ≤ a
hc : 0 ≤ -c
⊢ -c * b ≤ -c * a
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_update_of_ne_one [DecidableEq α] (f : α → M) (x : α) {y : M} (hy : y ≠ 1) :
    mulSupport (update f x y) = insert x (mulSupport f)

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : One M
inst✝ : DecidableEq α
f : α → M
x : α
y : M
hy : y ≠ 1
⊢ mulSupport (update f x y) = insert x (mulSupport f)

Tactic:
ext a

Result:
case h
α : Type u_1
M : Type u_5
inst✝¹ : One M
inst✝ : DecidableEq α
f : α → M
x : α
y : M
hy : y ≠ 1
a : α
⊢ a ∈ mulSupport (update f x y) ↔ a ∈ insert x (mulSupport f)

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝¹ : One M
inst✝ : DecidableEq α
f : α → M
x : α
y : M
hy : y ≠ 1
a : α
⊢ a ∈ mulSupport (update f x y) ↔ a ∈ insert x (mulSupport f)

Tactic:
rcases eq_or_ne a x with rfl | hne <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_pow_odd :
    (∫ x in (0)..π, sin x ^ (2 * n + 1)) = 2 * ∏ i ∈ range n, (2 * (i : ℝ) + 2) / (2 * i + 3)

Proof state:
case zero
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * 0 + 1) = 2 * ∏ i ∈ Finset.range 0, (2 * ↑i + 2) / (2 * ↑i + 3)

Tactic:
norm_num

Result:
no goals

Proof state:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * (k + 1) + 1) = 2 * ∏ i ∈ Finset.range (k + 1), (2 * ↑i + 2) / (2 * ↑i + 3)

Tactic:
rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow]

Result:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ (sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π) / (↑(2 * k + 1) + 2) +
      (↑(2 * k + 1) + 1) / (↑(2 * k + 1) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) =
    (2 * ↑k + 2) / (2 * ↑k + 3) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)

Proof state:
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * n + 1) = 2 * ∏ i ∈ Finset.range n, (2 * ↑i + 2) / (2 * ↑i + 3)

Tactic:
induction' n with k ih

Result:
case zero
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * 0 + 1) = 2 * ∏ i ∈ Finset.range 0, (2 * ↑i + 2) / (2 * ↑i + 3)

case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * (k + 1) + 1) = 2 * ∏ i ∈ Finset.range (k + 1), (2 * ↑i + 2) / (2 * ↑i + 3)

Proof state:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ (sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π) / (↑(2 * k + 1) + 2) +
      (↑(2 * k + 1) + 1) / (↑(2 * k + 1) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) =
    (2 * ↑k + 2) / (2 * ↑k + 3) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)

Tactic:
norm_cast

Result:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ (sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π) / ↑(2 * k + 1 + 2) +
      ↑(2 * k + 1 + 1) / ↑(2 * k + 1 + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) =
    ↑(2 * k + 2) / ↑(2 * k + 3) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)

Proof state:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ (sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π) / ↑(2 * k + 1 + 2) +
      ↑(2 * k + 1 + 1) / ↑(2 * k + 1 + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) =
    ↑(2 * k + 2) / ↑(2 * k + 3) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)

Tactic:
simp [-cast_add, field_simps]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem weightedSMul_null {s : Set α} (h_zero : μ s = 0) : (weightedSMul μ s : F →L[ℝ] F) = 0

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
h_zero : μ s = 0
x : F
⊢ (weightedSMul μ s) x = 0 x

Tactic:
rw [weightedSMul_apply, h_zero]

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
h_zero : μ s = 0
x : F
⊢ ENNReal.toReal 0 • x = 0 x

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
h_zero : μ s = 0
⊢ weightedSMul μ s = 0

Tactic:
ext1 x

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
h_zero : μ s = 0
x : F
⊢ (weightedSMul μ s) x = 0 x

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
h_zero : μ s = 0
x : F
⊢ ENNReal.toReal 0 • x = 0 x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem image2_iInter₂_subset_left (s : ∀ i, κ i → Set α) (t : Set β) :
    image2 f (⋂ (i) (j), s i j) t ⊆ ⋂ (i) (j), image2 f (s i j) t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ image2 f (⋂ i, ⋂ j, s i j) t ⊆ ⋂ i, ⋂ j, image2 f (s i j) t

Tactic:
simp_rw [image2_subset_iff, mem_iInter]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι) (i_1 : κ i), x ∈ s i i_1) → ∀ y ∈ t, ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f (s i i_1) t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι) (i_1 : κ i), x ∈ s i i_1) → ∀ y ∈ t, ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f (s i i_1) t

Tactic:
exact fun x hx y hy i j => mem_image2_of_mem (hx _ _) hy

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iInf_nat_gt_zero_eq (f : ℕ → α) : ⨅ i > 0, f i = ⨅ i, f (i + 1)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
⊢ ⨅ i, ⨅ (_ : i > 0), f i = ⨅ b ∈ {i | 0 < i}, f b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
⊢ ⨅ i, ⨅ (_ : i > 0), f i = ⨅ i, f (i + 1)

Tactic:
rw [← iInf_range, Nat.range_succ]

Result:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
⊢ ⨅ i, ⨅ (_ : i > 0), f i = ⨅ b ∈ {i | 0 < i}, f b
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem mem_perpBisector_pointReflection_iff_inner_eq_zero :
    c ∈ perpBisector p₁ (Equiv.pointReflection p₂ p₁) ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ c ∈ perpBisector p₁ ((Equiv.pointReflection p₂) p₁) ↔ inner (c -ᵥ p₂) (p₁ -ᵥ p₂) = 0

Tactic:
rw [mem_perpBisector_iff_inner_eq_zero, midpoint_pointReflection_right,
  Equiv.pointReflection_apply, vadd_vsub_assoc, inner_add_right, add_self_eq_zero,
  ← neg_eq_zero, ← inner_neg_right, neg_vsub_eq_vsub_rev]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem concat_or_concat (x y : BitVec w) (a b : Bool) :
    (concat x a) ||| (concat y b) = concat (x ||| y) (a || b)

Proof state:
w : Nat
x y : BitVec w
a b : Bool
⊢ x.concat a ||| y.concat b = (x ||| y).concat (a || b)

Tactic:
ext (_ | i) h <;> simp [getLsbD_concat]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem map₂_map_right (f₁ : α → γ → ζ) (f₂ : β → γ) :
    map₂ f₁ xs (map f₂ ys) = map₂ (fun x y => f₁ x (f₂ y)) xs ys

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → γ → ζ
f₂ : β → γ
⊢ map₂ f₁ xs (map f₂ ys) = map₂ (fun x y => f₁ x (f₂ y)) xs ys

Tactic:
induction xs, ys using Vector.revInductionOn₂ <;> simp_all

Result:
no goals
-- Mathlib/Topology/UniformSpace/Compact.lean
theorem Disjoint.exists_uniform_thickening_of_basis {p : ι → Prop} {s : ι → Set (α × α)}
    (hU : (𝓤 α).HasBasis p s) {A B : Set α} (hA : IsCompact A) (hB : IsClosed B)
    (h : Disjoint A B) : ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))

Proof state:
case intro.intro
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
⊢ ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))

Tactic:
rcases hU.mem_iff.1 hV with ⟨i, hi, hiV⟩

Result:
case intro.intro.intro.intro
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
i : ι
hi : p i
hiV : s i ⊆ V
⊢ ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))

Proof state:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
⊢ ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))

Tactic:
rcases h.exists_uniform_thickening hA hB with ⟨V, hV, hVAB⟩

Result:
case intro.intro
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
⊢ ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))

Proof state:
case intro.intro.intro.intro
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
i : ι
hi : p i
hiV : s i ⊆ V
⊢ ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))

Tactic:
exact ⟨i, hi, hVAB.mono (iUnion₂_mono fun a _ => ball_mono hiV a)
  (iUnion₂_mono fun b _ => ball_mono hiV b)⟩

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem map {F : Type*} [NormedAddCommGroup F] [NormedSpace K F] (f : E ≃ₗ[K] F) :
    Submodule.map (f.restrictScalars ℤ) (span ℤ (Set.range b)) = span ℤ (Set.range (b.map f))

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
f : E ≃ₗ[K] F
⊢ Submodule.map (LinearEquiv.restrictScalars ℤ f) (span ℤ (Set.range ⇑b)) = span ℤ (Set.range ⇑(b.map f))

Tactic:
simp_rw [Submodule.map_span, LinearEquiv.restrictScalars_apply, Basis.coe_map, Set.range_comp]

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Defs.lean
theorem gcdB_zero_left {s : R} : gcdB 0 s = 1

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ gcdB 0 s = 1

Tactic:
unfold gcdB

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcd 0 s).snd = 1

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcd 0 s).snd = 1

Tactic:
rw [xgcd, xgcd_zero_left]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/CompatiblePlus.lean
theorem plusCompIso_inv_eq_plusLift (hP : Presheaf.IsSheaf J (J.plusObj P ⋙ F)) :
    (J.plusCompIso F P).inv = J.plusLift (whiskerRight (J.toPlus _) _) hP

Proof state:
case hγ
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
hP : Presheaf.IsSheaf J (J.plusObj P ⋙ F)
⊢ J.toPlus (P ⋙ F) ≫ (J.plusCompIso F P).inv = whiskerRight (J.toPlus P) F

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
hP : Presheaf.IsSheaf J (J.plusObj P ⋙ F)
⊢ (J.plusCompIso F P).inv = J.plusLift (whiskerRight (J.toPlus P) F) hP

Tactic:
apply J.plusLift_unique

Result:
case hγ
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
hP : Presheaf.IsSheaf J (J.plusObj P ⋙ F)
⊢ J.toPlus (P ⋙ F) ≫ (J.plusCompIso F P).inv = whiskerRight (J.toPlus P) F
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mfderivWithin_eq_mfderiv (hs : UniqueMDiffWithinAt I s x) (h : MDifferentiableAt I I' f x) :
    mfderivWithin I I' f s x = mfderiv I I' f x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
hs : UniqueMDiffWithinAt I s x
h : MDifferentiableAt I I' f x
⊢ mfderivWithin I I' f s x = mfderiv I I' f x

Tactic:
rw [← mfderivWithin_univ]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
hs : UniqueMDiffWithinAt I s x
h : MDifferentiableAt I I' f x
⊢ mfderivWithin I I' f s x = mfderivWithin I I' f univ x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
hs : UniqueMDiffWithinAt I s x
h : MDifferentiableAt I I' f x
⊢ mfderivWithin I I' f s x = mfderivWithin I I' f univ x

Tactic:
exact mfderivWithin_subset (subset_univ _) hs h.mdifferentiableWithinAt

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem pow_sub_lt_descFactorial {n : ℕ} :
    ∀ {k : ℕ}, 2 ≤ k → k ≤ n → (n + 1 - k) ^ k < n.descFactorial k
  | 0 => by rintro ⟨⟩
  | 1 => by intro; contradiction
  | k + 2 => fun _ h => by
    rw [succ_sub_succ]
    exact pow_sub_lt_descFactorial' h

Proof state:
n : ℕ
⊢ 2 ≤ 1 → 1 ≤ n → (n + 1 - 1) ^ 1 < n.descFactorial 1

Tactic:
intro

Result:
n : ℕ
a✝ : 2 ≤ 1
⊢ 1 ≤ n → (n + 1 - 1) ^ 1 < n.descFactorial 1

Proof state:
n k : ℕ
x✝ : 2 ≤ k + 2
h : k + 2 ≤ n
⊢ (n + 1 - (k + 2)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
rw [succ_sub_succ]

Result:
n k : ℕ
x✝ : 2 ≤ k + 2
h : k + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Proof state:
n k : ℕ
x✝ : 2 ≤ k + 2
h : k + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
exact pow_sub_lt_descFactorial' h

Result:
no goals

Proof state:
n : ℕ
a✝ : 2 ≤ 1
⊢ 1 ≤ n → (n + 1 - 1) ^ 1 < n.descFactorial 1

Tactic:
contradiction

Result:
no goals

Proof state:
n : ℕ
⊢ 2 ≤ 0 → 0 ≤ n → (n + 1 - 0) ^ 0 < n.descFactorial 0

Tactic:
rintro ⟨⟩

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem Finsupp.inner_sum {ι : Type*} (l : ι →₀ 𝕜) (v : ι → E) (x : E) :
    ⟪x, l.sum fun (i : ι) (a : 𝕜) => a • v i⟫ = l.sum fun (i : ι) (a : 𝕜) => a • ⟪x, v i⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
l : ι →₀ 𝕜
v : ι → E
x : E
⊢ ⟪x, l.sum fun i a => a • v i⟫_𝕜 = l.sum fun i a => a • ⟪x, v i⟫_𝕜

Tactic:
convert inner_sum (𝕜 := 𝕜) l.support (fun a => l a • v a) x

Result:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
l : ι →₀ 𝕜
v : ι → E
x : E
⊢ (l.sum fun i a => a • ⟪x, v i⟫_𝕜) = ∑ i ∈ l.support, ⟪x, l i • v i⟫_𝕜

Proof state:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
l : ι →₀ 𝕜
v : ι → E
x : E
⊢ (l.sum fun i a => a • ⟪x, v i⟫_𝕜) = ∑ i ∈ l.support, ⟪x, l i • v i⟫_𝕜

Tactic:
simp only [inner_smul_right, Finsupp.sum, smul_eq_mul]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_div_lt_neg_one (h1 : a < 0) (h2 : -1 < a) : 1 / a < -1 :=
  suffices 1 / a < 1 / -1 by rwa [one_div_neg_one_eq_neg_one] at this
  one_div_lt_one_div_of_neg_of_lt h1 h2

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
h1 : a < 0
h2 : -1 < a
this : 1 / a < 1 / -1
⊢ 1 / a < -1

Tactic:
rwa [one_div_neg_one_eq_neg_one] at this

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_eq_iff : toIocMod hp a b = c ↔ c ∈ Set.Ioc a (a + p) ∧ ∃ z : ℤ, b = c + z • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocMod hp a b = c ↔ c ∈ Set.Ioc a (a + p) ∧ ∃ z, b = c + z • p

Tactic:
refine
  ⟨fun h =>
    ⟨h ▸ toIocMod_mem_Ioc hp a b, toIocDiv hp a b, h ▸ (toIocMod_add_toIocDiv_zsmul hp _ _).symm⟩,
    ?_⟩

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (c ∈ Set.Ioc a (a + p) ∧ ∃ z, b = c + z • p) → toIocMod hp a b = c

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (c ∈ Set.Ioc a (a + p) ∧ ∃ z, b = c + z • p) → toIocMod hp a b = c

Tactic:
simp_rw [← @sub_eq_iff_eq_add]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (c ∈ Set.Ioc a (a + p) ∧ ∃ z, b - z • p = c) → toIocMod hp a b = c

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (c ∈ Set.Ioc a (a + p) ∧ ∃ z, b - z • p = c) → toIocMod hp a b = c

Tactic:
rintro ⟨hc, n, rfl⟩

Result:
case intro.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
n : ℤ
hc : b - n • p ∈ Set.Ioc a (a + p)
⊢ toIocMod hp a b = b - n • p

Proof state:
case intro.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
n : ℤ
hc : b - n • p ∈ Set.Ioc a (a + p)
⊢ toIocMod hp a b = b - n • p

Tactic:
rw [← toIocDiv_eq_of_sub_zsmul_mem_Ioc hp hc, toIocMod]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_set (a b : α) (l : Vector α n) (i : Nat) (h : i < n) :
    (l.set i a).count b = l.count b - (if l[i] == b then 1 else 0) + (if a == b then 1 else 0)

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
i : Nat
l : Array α
h : i < l.size
⊢ count b ({ toArray := l, size_toArray := ⋯ }.set i a h) =
    (count b { toArray := l, size_toArray := ⋯ } -
        if ({ toArray := l, size_toArray := ⋯ }[i] == b) = true then 1 else 0) +
      if (a == b) = true then 1 else 0

Tactic:
simp [Array.count_set, h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
n : Nat
a b : α
l : Vector α n
i : Nat
h : i < n
⊢ count b (l.set i a h) = (count b l - if (l[i] == b) = true then 1 else 0) + if (a == b) = true then 1 else 0

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
i : Nat
l : Array α
h : i < l.size
⊢ count b ({ toArray := l, size_toArray := ⋯ }.set i a h) =
    (count b { toArray := l, size_toArray := ⋯ } -
        if ({ toArray := l, size_toArray := ⋯ }[i] == b) = true then 1 else 0) +
      if (a == b) = true then 1 else 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_add_of_pos_right (a : Int) {b : Int} (h : 0 < b) : a < a + b

Proof state:
a b : Int
h : 0 < b
⊢ a < a + b

Tactic:
have : a + 0 < a + b := Int.add_lt_add_left h a

Result:
a b : Int
h : 0 < b
this : a + 0 < a + b
⊢ a < a + b

Proof state:
a b : Int
h : 0 < b
this : a + 0 < a + b
⊢ a < a + b

Tactic:
rwa [Int.add_zero] at this

Result:
no goals
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem sup_comm (a b : α) : a ⊔ b = b ⊔ a

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + b + a * b = b + a + b * a

Tactic:
ring

Result:
no goals