harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_of_append {l : Vector α n} {l₁ : Vector α m} {l₂ : Vector α k}
    (w : m + 1 + k = n) (eq : l = (l₁.push a ++ l₂).cast w) :
    l[m] = a := Option.some.inj <| by
  rw [← getElem?_eq_getElem, eq, getElem?_cast, getElem?_append_left (by simp)]
  simp

Proof state:
α : Type u_1
n m k : Nat
a : α
l : Vector α n
l₁ : Vector α m
l₂ : Vector α k
w : m + 1 + k = n
eq : l = Vector.cast w (l₁.push a ++ l₂)
⊢ m < m + 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n m k : Nat
a : α
l : Vector α n
l₁ : Vector α m
l₂ : Vector α k
w : m + 1 + k = n
eq : l = Vector.cast w (l₁.push a ++ l₂)
⊢ (l₁.push a)[m]? = some a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n m k : Nat
a : α
l : Vector α n
l₁ : Vector α m
l₂ : Vector α k
w : m + 1 + k = n
eq : l = Vector.cast w (l₁.push a ++ l₂)
⊢ some l[m] = some a

Tactic:
rw [← getElem?_eq_getElem, eq, getElem?_cast, getElem?_append_left (by simp)]

Result:
α : Type u_1
n m k : Nat
a : α
l : Vector α n
l₁ : Vector α m
l₂ : Vector α k
w : m + 1 + k = n
eq : l = Vector.cast w (l₁.push a ++ l₂)
⊢ (l₁.push a)[m]? = some a
-- Mathlib/Order/Filter/Cofinite.lean
theorem disjoint_cofinite_left : Disjoint cofinite l ↔ ∃ s ∈ l, Set.Finite s

Proof state:
α : Type u_2
l : Filter α
⊢ Disjoint cofinite l ↔ ∃ s ∈ l, s.Finite

Tactic:
simp [l.basis_sets.disjoint_iff_right]

Result:
no goals
-- Mathlib/Order/RelClasses.lean
theorem IsTrichotomous.swap (r) [IsTrichotomous α r] : IsTrichotomous α (swap r) :=
  ⟨fun a b => by simpa [Function.swap, or_comm, or_left_comm] using trichotomous_of r a b⟩

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsTrichotomous α r
a b : α
⊢ Function.swap r a b ∨ a = b ∨ Function.swap r b a

Tactic:
simpa [Function.swap, or_comm, or_left_comm] using trichotomous_of r a b

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem iff_or_not_self : ∀ {a b : Bool}, (b = (a || !b)) ↔ a ∧ b

Proof state:
⊢ ∀ {a b : Bool}, b = (a || !b) ↔ a = true ∧ b = true

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma lt_of_lt_pred (h : m < n - 1) : m < n

Proof state:
m n : ℕ
h : m < n - 1
⊢ m < n

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem derivWithin_of_mem_nhds (h : s ∈ 𝓝 x) : derivWithin f s x = deriv f x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 x
⊢ derivWithin f s x = deriv f x

Tactic:
simp only [derivWithin, deriv, fderivWithin_of_mem_nhds h]

Result:
no goals
-- Mathlib/Algebra/Divisibility/Basic.lean
theorem dvd_of_mul_left_dvd (h : a * b ∣ c) : b ∣ c :=
  Dvd.elim h fun d ceq => Dvd.intro (a * d) (by simp [ceq])

Proof state:
α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : a * b ∣ c
d : α
ceq : c = a * b * d
⊢ b * (a * d) = c

Tactic:
simp [ceq]

Result:
no goals
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem p_comm {P Q : Karoubi C} (f : Hom P Q) : P.p ≫ f.f = f.f ≫ Q.p

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : P.Hom Q
⊢ P.p ≫ f.f = f.f ≫ Q.p

Tactic:
rw [p_comp, comp_p]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_one_add_smoothingFn_nonneg : ∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 + ε n

Proof state:
case h
n : ℕ
hn : 0 < 1 + ε ↑n
⊢ 0 ≤ 1 + ε ↑n

Tactic:
exact le_of_lt hn

Result:
no goals

Proof state:
⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 + ε ↑n

Tactic:
filter_upwards [eventually_one_add_smoothingFn_pos] with n hn

Result:
case h
n : ℕ
hn : 0 < 1 + ε ↑n
⊢ 0 ≤ 1 + ε ↑n
-- Mathlib/Algebra/Lie/Submodule.lean
theorem comap_map_eq (h : ↑(map f I) = f '' I) : comap f (map f I) = I ⊔ f.ker

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : ↑(map f I) = ⇑f '' ↑I
⊢ comap f (map f I) = I ⊔ f.ker

Tactic:
rw [← LieSubmodule.toSubmodule_inj, comap_toSubmodule, I.map_toSubmodule f h,
  LieSubmodule.sup_toSubmodule, f.ker_toSubmodule, Submodule.comap_map_eq]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem postcomp_uniformContinuous [UniformSpace γ] {f : γ → β}
    (hf : UniformContinuous f) :
    UniformContinuous (ofFun ∘ (f ∘ ·) ∘ toFun : (α →ᵤ γ) → α →ᵤ β)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ ≤ UniformSpace.comap (⇑ofFun ∘ (fun x => f ∘ x) ∘ ⇑toFun) (uniformSpace α β)

Tactic:
exact (UniformFun.mono (uniformContinuous_iff.mp hf)).trans_eq UniformFun.comap_eq

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ UniformContinuous (⇑ofFun ∘ (fun x => f ∘ x) ∘ ⇑toFun)

Tactic:
refine uniformContinuous_iff.mpr ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ ≤ UniformSpace.comap (⇑ofFun ∘ (fun x => f ∘ x) ∘ ⇑toFun) (uniformSpace α β)
-- Mathlib/Order/Bounds/Basic.lean
theorem isGreatest_compl [HeytingAlgebra α] (a : α) :
    IsGreatest {w | Disjoint w a} (aᶜ)

Proof state:
α : Type u
inst✝ : HeytingAlgebra α
a : α
⊢ IsGreatest {w | Disjoint w a} aᶜ

Tactic:
simpa only [himp_bot, disjoint_iff_inf_le] using isGreatest_himp a ⊥

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict (hs : MeasurableSet s) :
    eLpNormEssSup (s.indicator f) μ = eLpNormEssSup f (μ.restrict s)

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
⊢ eLpNormEssSup (s.indicator f) μ = eLpNormEssSup f (μ.restrict s)

Tactic:
simp_rw [← eLpNorm_exponent_top, eLpNorm_indicator_eq_eLpNorm_restrict hs]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_add : cos (x + y) = cos x * cos y - sin x * sin y :=
  ofReal_injective <| by simp [cos_add]

Proof state:
x y : ℝ
⊢ ↑(cos (x + y)) = ↑(cos x * cos y - sin x * sin y)

Tactic:
simp [cos_add]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive]
lemma dist_one_left (a : E) : dist 1 a = ‖a‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ dist 1 a = ‖a‖

Tactic:
rw [dist_comm, dist_one_right]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_mulVec [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix n l α)
    (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (x : l ⊕ m → α) :
    (fromBlocks A B C D) *ᵥ x =
      Sum.elim (A *ᵥ (x ∘ Sum.inl) + B *ᵥ (x ∘ Sum.inr))
        (C *ᵥ (x ∘ Sum.inl) + D *ᵥ (x ∘ Sum.inr))

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
⊢ fromBlocks A B C D *ᵥ x = Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr)

Tactic:
ext i

Result:
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
i : n ⊕ o
⊢ (fromBlocks A B C D *ᵥ x) i = Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr) i

Proof state:
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
i : n ⊕ o
⊢ (fromBlocks A B C D *ᵥ x) i = Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr) i

Tactic:
cases i <;> simp [mulVec, dotProduct]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem hasseDeriv_single (k : ℕ) (n : ℤ) (x : V) :
    hasseDeriv R k (single n x) = single (n - k) ((Ring.choose n k) • x)

Proof state:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
n : ℤ
x : V
⊢ (hasseDeriv R k) ((single n) x) = (single (n - ↑k)) (Ring.choose n k • x)

Tactic:
rw [← Int.sub_add_cancel n k, hasseDeriv_single_add, Int.sub_add_cancel n k]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem eventually_nhdsSet_iUnion₂ {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {P : X → Prop} :
    (∀ᶠ x in 𝓝ˢ (⋃ (i) (_ : p i), s i), P x) ↔ ∀ i, p i → ∀ᶠ x in 𝓝ˢ (s i), P x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
P : X → Prop
⊢ (∀ᶠ (x : X) in 𝓝ˢ (⋃ i, ⋃ (_ : p i), s i), P x) ↔ ∀ (i : ι), p i → ∀ᶠ (x : X) in 𝓝ˢ (s i), P x

Tactic:
simp only [nhdsSet_iUnion, eventually_iSup]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma c_relation_of_char_three : W.c₄ ^ 3 = W.c₆ ^ 2

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.c₄ ^ 3 = W.c₆ ^ 2

Tactic:
linear_combination -W.c_relation + 576 * W.Δ * CharP.cast_eq_zero R 3

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
@[simp]
lemma le_smul_iff_one_le_left [SMulPosMono α β] [SMulPosReflectLE α β] (hb : 0 < b) :
    b ≤ a • b ↔ 1 ≤ a := Iff.trans (by rw [one_smul]) (smul_le_smul_iff_of_pos_right hb)

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Monoid α
inst✝⁵ : Zero β
inst✝⁴ : MulAction α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : SMulPosMono α β
inst✝ : SMulPosReflectLE α β
hb : 0 < b
⊢ b ≤ a • b ↔ 1 • b ≤ a • b

Tactic:
rw [one_smul]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem continuousOn_iff'_right [TopologicalSpace β] {f : β → α} {s : Set β} :
    ContinuousOn f s ↔ ∀ b ∈ s, Tendsto (fun x => (f b, f x)) (𝓝[s] b) (𝓤 α)

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ b ∈ s, Tendsto (fun x => (f b, f x)) (𝓝[s] b) (𝓤 α)

Tactic:
simp [ContinuousOn, continuousWithinAt_iff'_right]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem dist_self_mul_left (a b : E) : dist (a * b) a = ‖b‖

Proof state:
E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist (a * b) a = ‖b‖

Tactic:
rw [dist_comm, dist_self_mul_right]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
@[to_additive (attr := simp) existing nsmul_zmod_val_inv_nsmul]
lemma pow_zmod_val_inv_pow (hn : (Nat.card α).Coprime n) (a : α) :
    (a ^ (n⁻¹ : ZMod (Nat.card α)).val) ^ n = a

Proof state:
α : Type u_1
inst✝ : Group α
n : ℕ
hn : (Nat.card α).Coprime n
a : α
⊢ (a ^ (↑n)⁻¹.val) ^ n = a

Tactic:
rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
  ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem mem_vanishingIdeal (t : Set (PrimeSpectrum R)) (f : R) :
    f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asIdeal

Proof state:
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asIdeal

Tactic:
rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]

Result:
no goals
-- Mathlib/Topology/Compactness/SigmaCompact.lean
theorem find_shiftr (x : X) : K.shiftr.find x = K.find x + 1

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ K.shiftr.find x = K.find x + 1

Tactic:
exact Nat.find_comp_succ _ _ (not_mem_empty _)

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ K.shiftr.find x = K.find x + 1

Tactic:
classical
exact Nat.find_comp_succ _ _ (not_mem_empty _)

Result:
no goals
-- Mathlib/ModelTheory/Quotients.lean
theorem funMap_quotient_mk' {n : ℕ} (f : L.Functions n) (x : Fin n → M) :
    (funMap f fun i => (⟦x i⟧ : Quotient s)) = ⟦@funMap _ _ ps.toStructure _ f x⟧

Proof state:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ (funMap f fun i => ⟦x i⟧) = ⟦funMap f x⟧

Tactic:
change
  Quotient.map (@funMap L M ps.toStructure n f) Prestructure.fun_equiv (Quotient.finChoice _) =
    _

Result:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Quotient.map (funMap f) ⋯ (Quotient.finChoice fun i => ⟦x i⟧) = ⟦funMap f x⟧

Proof state:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Quotient.map (funMap f) ⋯ (Quotient.finChoice fun i => ⟦x i⟧) = ⟦funMap f x⟧

Tactic:
rw [Quotient.finChoice_eq, Quotient.map_mk]

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem one_div_mul_sub_mul_one_div_eq_one_div_add_one_div (ha : a ≠ 0) (hb : b ≠ 0) :
    1 / a * (b - a) * (1 / b) = 1 / a - 1 / b

Proof state:
K : Type u_1
inst✝ : DivisionRing K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a * (b - a) * (1 / b) = 1 / a - 1 / b

Tactic:
simpa only [one_div] using (inv_sub_inv' ha hb).symm

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem biSup_inf_biSup {ι ι' : Type*} {f : ι → α} {g : ι' → α} {s : Set ι} {t : Set ι'} :
    ((⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j) = ⨆ p ∈ s ×ˢ t, f (p : ι × ι').1 ⊓ g p.2

Proof state:
α : Type u
inst✝ : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ (⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j = ⨆ p ∈ s ×ˢ t, f p.1 ⊓ g p.2

Tactic:
simp only [iSup_subtype', iSup_inf_iSup]

Result:
α : Type u
inst✝ : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ ⨆ i, f ↑i.1 ⊓ g ↑i.2 = ⨆ x, f (↑x).1 ⊓ g (↑x).2

Proof state:
α : Type u
inst✝ : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ ⨆ i, f ↑i.1 ⊓ g ↑i.2 = ⨆ x, f (↑x).1 ⊓ g (↑x).2

Tactic:
exact (Equiv.surjective _).iSup_congr (Equiv.Set.prod s t).symm fun x => rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem limitCompWhiskeringLeftIsoCompLimit_inv_π (F : J ⥤ K ⥤ C) (G : D ⥤ K)
    [HasLimitsOfShape J C] (j : J) :
    (limitCompWhiskeringLeftIsoCompLimit F G).inv ≫ limit.π (F ⋙ (whiskeringLeft _ _ _).obj G) j =
      whiskerLeft G (limit.π F j)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasLimitsOfShape J C
j : J
⊢ (limitCompWhiskeringLeftIsoCompLimit F G).inv ≫ limit.π (F ⋙ (whiskeringLeft D K C).obj G) j =
    whiskerLeft G (limit.π F j)

Tactic:
simp [Iso.inv_comp_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_sUnion₀ {S : Set (Set α)} (hs : S.Countable) (hd : S.Pairwise (AEDisjoint μ))
    (h : ∀ s ∈ S, NullMeasurableSet s μ) : μ (⋃₀ S) = ∑' s : S, μ s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hs : S.Countable
hd : S.Pairwise (AEDisjoint μ)
h : ∀ s ∈ S, NullMeasurableSet s μ
⊢ μ (⋃₀ S) = ∑' (s : ↑S), μ ↑s

Tactic:
rw [sUnion_eq_biUnion, measure_biUnion₀ hs hd h]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_eq_mul_one_div (a b : G) : a / b = a * (1 / b)

Proof state:
G : Type u_3
inst✝ : DivInvMonoid G
a b : G
⊢ a / b = a * (1 / b)

Tactic:
rw [div_eq_mul_inv, one_div]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_smul_vsub_eq_affineCombination_vsub (w : ι → k) (p₁ p₂ : ι → P) :
    (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) =
      s.affineCombination k p₁ w -ᵥ s.affineCombination k p₂ w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ p₂ : ι → P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) =
    (s.weightedVSubOfPoint p₁ (Classical.choice ⋯)) w - (s.weightedVSubOfPoint p₂ (Classical.choice ⋯)) w

Tactic:
exact s.sum_smul_vsub_eq_weightedVSubOfPoint_sub _ _ _ _

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ p₂ : ι → P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = (affineCombination k s p₁) w -ᵥ (affineCombination k s p₂) w

Tactic:
simp_rw [affineCombination_apply, vadd_vsub_vadd_cancel_right]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ p₂ : ι → P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) =
    (s.weightedVSubOfPoint p₁ (Classical.choice ⋯)) w - (s.weightedVSubOfPoint p₂ (Classical.choice ⋯)) w
-- Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
@[simp] lemma T_univ [Fintype ι] [∀ i, SigmaFinite (μ i)] (f : (∀ i, A i) → ℝ≥0∞) (x : ∀ i, A i) :
    T μ p f univ x =
    ∫⁻ (x : ∀ i, A i), (f x ^ (1 - (#ι - 1 : ℝ) * p)
    * ∏ i : ι, (∫⁻ t : A i, f (update x i t) ∂(μ i)) ^ p) ∂(.pi μ)

Proof state:
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
f : ((i : ι) → A i) → ℝ≥0∞
x : (i : ι) → A i
⊢ T μ p f Finset.univ x =
    ∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (t : A i), f (update x i t) ∂μ i) ^ p ∂Measure.pi μ

Tactic:
simp [T, lmarginal_singleton]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exponential.lean
theorem hasStrictDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝕂}
    (hx : x ∈ EMetric.ball (0 : 𝕂) (expSeries 𝕂 𝕂).radius) :
    HasStrictDerivAt (exp 𝕂) (exp 𝕂 x) x

Proof state:
𝕂 : Type u_1
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : CompleteSpace 𝕂
inst✝ : CharZero 𝕂
x : 𝕂
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝕂).radius
⊢ HasStrictDerivAt (exp 𝕂) (exp 𝕂 x) x

Tactic:
simpa using (hasStrictFDerivAt_exp_of_mem_ball hx).hasStrictDerivAt

Result:
no goals
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
@[simp] lemma toUpperSet_specializes_toUpperSet {a b : α} :
    toUpperSet a ⤳ toUpperSet b ↔ b ≤ a

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ toUpperSet a ⤳ toUpperSet b ↔ b ≤ a

Tactic:
simp_rw [specializes_iff_closure_subset, IsUpperSet.closure_singleton, Iic_subset_Iic,
  toUpperSet_le_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a

Proof state:
α : Type u_1
a : α
l : List α
⊢ (l ++ [a]).getLast? = some a

Tactic:
simp [getLast?_eq_getElem?, Nat.succ_sub_succ]

Result:
no goals
-- Mathlib/RepresentationTheory/Rep.lean
theorem linearization_of (X : Action (Type u) G) (g : G) (x : X.V) :
    ((linearization k G).obj X).ρ g (Finsupp.single x (1 : k))
      = Finsupp.single (X.ρ g x) (1 : k)

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X : Action (Type u) G
g : G
x : X.V
⊢ (((linearization k G).obj X).ρ g) (Finsupp.single x 1) = Finsupp.single (X.ρ g x) 1

Tactic:
rw [linearization_obj_ρ, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem reflection_mem_subspace_orthogonalComplement_eq_neg [HasOrthogonalProjection K] {v : E}
    (hv : v ∈ Kᗮ) : reflection K v = -v

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
hv : v ∈ Kᗮ
⊢ (reflection K) v = -v

Tactic:
simp [reflection_apply, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero hv]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem conjugate_pos {a : R} (ha : 0 < a) {c : R} (hc : IsRegular c) : 0 < star c * a * c

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : 0 < a
c : R
hc : IsRegular c
⊢ 0 < star c * a * c

Tactic:
simpa only [mul_zero, zero_mul] using conjugate_lt_conjugate ha hc

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem tsum_measure_preimage_singleton {s : Set β} (hs : s.Countable) {f : α → β}
    (hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})) : (∑' b : s, μ (f ⁻¹' {↑b})) = μ (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
hs : s.Countable
f : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
⊢ ∑' (b : ↑s), μ (f ⁻¹' {↑b}) = μ (f ⁻¹' s)

Tactic:
rw [← Set.biUnion_preimage_singleton, measure_biUnion hs (pairwiseDisjoint_fiber f s) hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} {k : α} :
    (insertMany m l).contains k = (m.contains k || (l.map Prod.fst).contains k)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k : α
⊢ (insertMany m l).contains k = (m.contains k || (List.map Prod.fst l).contains k)

Tactic:
simp_to_raw using Raw₀.Const.contains_insertMany_list

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p → Array α} :
    (x ∈ if h : p then #[] else l h) ↔ ∃ h : ¬ p, x ∈ l h

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : ¬p → Array α
⊢ (x ∈ if h : p then #[] else l h) ↔ ∃ h, x ∈ l h

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem StrictConcaveOn.translate_left (hf : StrictConcaveOn 𝕜 s f) (c : E) :
    StrictConcaveOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCancelCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
hf : StrictConcaveOn 𝕜 s f
c : E
⊢ StrictConcaveOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)

Tactic:
simpa only [add_comm] using hf.translate_right c

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp] lemma one_lt_zpow_iff_right₀ (ha : 1 < a) : 1 < a ^ n ↔ 0 < n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha : 1 < a
⊢ 1 < a ^ n ↔ 0 < n

Tactic:
simp [← zpow_lt_zpow_iff_right₀ ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.eq_true_of_and_eq_true_right {a b : Bool} (h : (a && b) = true) : b = true

Proof state:
a b : Bool
h : (a && b) = true
⊢ b = true

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem not_le {i j : Fin n} : ¬ i ≤ j ↔ j < i

Proof state:
case mk
n : Nat
j : Fin n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ¬⟨val✝, isLt✝⟩ ≤ j ↔ j < ⟨val✝, isLt✝⟩

Tactic:
cases j

Result:
case mk.mk
n val✝¹ : Nat
isLt✝¹ : val✝¹ < n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ¬⟨val✝¹, isLt✝¹⟩ ≤ ⟨val✝, isLt✝⟩ ↔ ⟨val✝, isLt✝⟩ < ⟨val✝¹, isLt✝¹⟩

Proof state:
case mk.mk
n val✝¹ : Nat
isLt✝¹ : val✝¹ < n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ¬⟨val✝¹, isLt✝¹⟩ ≤ ⟨val✝, isLt✝⟩ ↔ ⟨val✝, isLt✝⟩ < ⟨val✝¹, isLt✝¹⟩

Tactic:
exact Nat.not_le

Result:
no goals

Proof state:
n : Nat
i j : Fin n
⊢ ¬i ≤ j ↔ j < i

Tactic:
cases i

Result:
case mk
n : Nat
j : Fin n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ¬⟨val✝, isLt✝⟩ ≤ j ↔ j < ⟨val✝, isLt✝⟩