harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean
@[simp]
lemma linearDeriv_apply : f.linearDeriv x y = ∑ i, f (Function.update x i (y i))

Proof state:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst✝⁹ : Semiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : ι) → Module R (M₁ i)
inst✝⁵ : Module R M₂
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : TopologicalSpace M₂
f : ContinuousMultilinearMap R M₁ M₂
inst✝² : ContinuousAdd M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x y : (i : ι) → M₁ i
⊢ (∑ i : ι,
        (let __src := f.toLinearMap x i;
            { toLinearMap := __src, cont := ⋯ }).comp
          (ContinuousLinearMap.proj i))
      y =
    ∑ i : ι, f (update x i (y i))

Tactic:
simp only [ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_comp',
  ContinuousLinearMap.coe_mk', LinearMap.coe_mk, LinearMap.coe_toAddHom, Finset.sum_apply]

Result:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst✝⁹ : Semiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : ι) → Module R (M₁ i)
inst✝⁵ : Module R M₂
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : TopologicalSpace M₂
f : ContinuousMultilinearMap R M₁ M₂
inst✝² : ContinuousAdd M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x y : (i : ι) → M₁ i
⊢ ∑ c : ι, (⇑(f.toLinearMap x c) ∘ ⇑(ContinuousLinearMap.proj c)) y = ∑ i : ι, f (update x i (y i))

Proof state:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst✝⁹ : Semiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : ι) → Module R (M₁ i)
inst✝⁵ : Module R M₂
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : TopologicalSpace M₂
f : ContinuousMultilinearMap R M₁ M₂
inst✝² : ContinuousAdd M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x y : (i : ι) → M₁ i
⊢ (f.linearDeriv x) y = ∑ i : ι, f (update x i (y i))

Tactic:
unfold linearDeriv toContinuousLinearMap

Result:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst✝⁹ : Semiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : ι) → Module R (M₁ i)
inst✝⁵ : Module R M₂
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : TopologicalSpace M₂
f : ContinuousMultilinearMap R M₁ M₂
inst✝² : ContinuousAdd M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x y : (i : ι) → M₁ i
⊢ (∑ i : ι,
        (let __src := f.toLinearMap x i;
            { toLinearMap := __src, cont := ⋯ }).comp
          (ContinuousLinearMap.proj i))
      y =
    ∑ i : ι, f (update x i (y i))

Proof state:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst✝⁹ : Semiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : ι) → Module R (M₁ i)
inst✝⁵ : Module R M₂
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : TopologicalSpace M₂
f : ContinuousMultilinearMap R M₁ M₂
inst✝² : ContinuousAdd M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x y : (i : ι) → M₁ i
⊢ ∑ c : ι, (⇑(f.toLinearMap x c) ∘ ⇑(ContinuousLinearMap.proj c)) y = ∑ i : ι, f (update x i (y i))

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.insertManyIfNewUnit_eq {ρ : Type w} [ForIn Id ρ α] [BEq α] [Hashable α]
    {m : Raw α (fun _ => Unit)} {l : ρ} (h : m.WF):
    Raw.Const.insertManyIfNewUnit m l = Raw₀.Const.insertManyIfNewUnit ⟨m, h.size_buckets_pos⟩ l

Proof state:
α : Type u
ρ : Type w
inst✝² : ForIn Id ρ α
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => Unit
l : ρ
h : m.WF
⊢ Raw.Const.insertManyIfNewUnit m l = (Raw₀.Const.insertManyIfNewUnit ⟨m, ⋯⟩ l).val.val

Tactic:
simp [Raw.Const.insertManyIfNewUnit, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem le_one_div (ha : 0 < a) (hb : 0 < b) : a ≤ 1 / b ↔ b ≤ 1 / a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
ha : 0 < a
hb : 0 < b
⊢ a ≤ 1 / b ↔ b ≤ 1 / a

Tactic:
simpa using le_inv_comm₀ ha hb

Result:
no goals
-- Mathlib/Analysis/Complex/OperatorNorm.lean
theorem reCLM_norm : ‖reCLM‖ = 1 :=
  le_antisymm (LinearMap.mkContinuous_norm_le _ zero_le_one _) <|
    calc
      1 = ‖reCLM 1‖

Proof state:
⊢ 1 = ‖reCLM 1‖

Tactic:
simp

Result:
no goals

Proof state:
⊢ ‖1‖ ≤ 1

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Distributions/Geometric.lean
lemma geometricPMFReal_nonneg {n : ℕ} (hp_pos : 0 < p) (hp_le_one : p ≤ 1) :
    0 ≤ geometricPMFReal p n

Proof state:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ 0 ≤ (1 - p) ^ n * p

Tactic:
have : 0 ≤ 1 - p := sub_nonneg.mpr hp_le_one

Result:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : 0 ≤ 1 - p
⊢ 0 ≤ (1 - p) ^ n * p

Proof state:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : 0 ≤ 1 - p
⊢ 0 ≤ (1 - p) ^ n * p

Tactic:
positivity

Result:
no goals

Proof state:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ 0 ≤ geometricPMFReal p n

Tactic:
rw [geometricPMFReal]

Result:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ 0 ≤ (1 - p) ^ n * p
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem le_outerMeasure_compacts (K : Compacts G) : μ K ≤ μ.outerMeasure K

Proof state:
case m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ → μ.innerContent { carrier := s₁, is_open' := hs₁ } ≤ μ.innerContent { carrier := s₂, is_open' := hs₂ }

Tactic:
exact μ.innerContent_mono

Result:
no goals

Proof state:
case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    μ.innerContent { carrier := ⋃ i, f i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := f i, is_open' := ⋯ }

Tactic:
exact μ.innerContent_iUnion_nat

Result:
no goals

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ μ K ≤ μ.outerMeasure ↑K

Tactic:
rw [Content.outerMeasure, inducedOuterMeasure_eq_iInf]

Result:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ μ K ≤ ⨅ t, ⨅ (ht : IsOpen t), ⨅ (_ : ↑K ⊆ t), μ.innerContent { carrier := t, is_open' := ht }

case PU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄, (∀ (i : ℕ), IsOpen (f i)) → IsOpen (⋃ i, f i)

case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    μ.innerContent { carrier := ⋃ i, f i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := f i, is_open' := ⋯ }

case m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ → μ.innerContent { carrier := s₁, is_open' := hs₁ } ≤ μ.innerContent { carrier := s₂, is_open' := hs₂ }

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ μ K ≤ ⨅ t, ⨅ (ht : IsOpen t), ⨅ (_ : ↑K ⊆ t), μ.innerContent { carrier := t, is_open' := ht }

Tactic:
exact le_iInf fun U => le_iInf fun hU => le_iInf <| μ.le_innerContent K ⟨U, hU⟩

Result:
no goals

Proof state:
case PU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄, (∀ (i : ℕ), IsOpen (f i)) → IsOpen (⋃ i, f i)

Tactic:
exact fun U hU => isOpen_iUnion hU

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
lemma H2π_eq_zero_iff (x : twoCocycles A) : H2π A x = 0 ↔ ⇑x ∈ twoCoboundaries A

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(twoCocycles A)
⊢ (LinearMap.range (LinearMap.codRestrict (twoCocycles A) (dOne A) ⋯)).mkQ x = 0 ↔ ⇑x ∈ twoCoboundaries A

Tactic:
simp [LinearMap.range_codRestrict, twoCoboundaries]

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(twoCocycles A)
⊢ (ConcreteCategory.hom (H2π A)) x = 0 ↔ ⇑x ∈ twoCoboundaries A

Tactic:
show (LinearMap.range ((dOne A).codRestrict (twoCocycles A) _)).mkQ _ = 0 ↔ _

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(twoCocycles A)
⊢ (LinearMap.range (LinearMap.codRestrict (twoCocycles A) (dOne A) ⋯)).mkQ x = 0 ↔ ⇑x ∈ twoCoboundaries A
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Iio : (some : α → WithTop α) '' Iio a = Iio (a : WithTop α)

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Iio a = Iio ↑a

Tactic:
rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Iio_subset_Iio le_top)]

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Colimits.lean
theorem cocone_naturality {j j' : J} (f : j ⟶ j') :
    F.map f ≫ coconeMorphism F j' = coconeMorphism F j

Proof state:
case hf.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (Hom.hom (F.map f ≫ coconeMorphism F j')) x✝ = (Hom.hom (coconeMorphism F j)) x✝

Tactic:
apply Quot.sound

Result:
case hf.a.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (colimitSetoid F) (Prequotient.of j' ((F.map f).hom' x✝)) (Prequotient.of j x✝)

Proof state:
case hf.a.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (colimitSetoid F) (Prequotient.of j' ((F.map f).hom' x✝)) (Prequotient.of j x✝)

Tactic:
apply Relation.map

Result:
no goals

Proof state:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j

Tactic:
ext

Result:
case hf.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (Hom.hom (F.map f ≫ coconeMorphism F j')) x✝ = (Hom.hom (coconeMorphism F j)) x✝
-- Mathlib/Data/Finsupp/Single.lean
theorem single_eq_set_indicator : ⇑(single a b) = Set.indicator {a} fun _ => b

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ ⇑(single a b) = {a}.indicator fun x => b

Tactic:
classical
ext
simp [single_apply, Set.indicator, @eq_comm _ a]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ ⇑(single a b) = {a}.indicator fun x => b

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
x✝ : α
⊢ (single a b) x✝ = {a}.indicator (fun x => b) x✝

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
x✝ : α
⊢ (single a b) x✝ = {a}.indicator (fun x => b) x✝

Tactic:
simp [single_apply, Set.indicator, @eq_comm _ a]

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem isStoppingTime_const [Preorder ι] (f : Filtration ι m) (i : ι) :
    IsStoppingTime f fun _ => i := fun j => by simp only [MeasurableSet.const]

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i j : ι
⊢ MeasurableSet {ω | (fun x => i) ω ≤ j}

Tactic:
simp only [MeasurableSet.const]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem PseudoMetricSpace.replaceTopology_eq {γ} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ)
    (H : U = m.toUniformSpace.toTopologicalSpace) : m.replaceTopology H = m

Proof state:
γ : Type u_3
U : TopologicalSpace γ
m : PseudoMetricSpace γ
H : U = UniformSpace.toTopologicalSpace
⊢ m.replaceTopology H = m

Tactic:
ext

Result:
case h.dist.h.h
γ : Type u_3
U : TopologicalSpace γ
m : PseudoMetricSpace γ
H : U = UniformSpace.toTopologicalSpace
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Proof state:
case h.dist.h.h
γ : Type u_3
U : TopologicalSpace γ
m : PseudoMetricSpace γ
H : U = UniformSpace.toTopologicalSpace
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem sort_nodup (s : Finset α) : (sort r s).Nodup :=
  (by rw [sort_eq]; exact s.2 : @Multiset.Nodup α (sort r s))

Proof state:
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ s.val.Nodup

Tactic:
exact s.2

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ (↑(sort r s)).Nodup

Tactic:
rw [sort_eq]

Result:
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ s.val.Nodup
-- Mathlib/AlgebraicGeometry/Scheme.lean
@[simp]
lemma stalkMap_hom_inv_apply (e : X ≅ Y) (y : Y) (z) :
    e.inv.stalkMap y (e.hom.stalkMap (e.inv.base y) z) =
      (Y.presheaf.stalkCongr (.of_eq (by simp))).hom z :=
  DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkMap_hom_inv e y)) z

Proof state:
X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
y : ↑↑Y.toPresheafedSpace
z : ↑(Y.presheaf.stalk ((ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y)))
⊢ (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y) = y

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem neg_smul : -s • t = -(s • t)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
s : Set α
t : Set β
⊢ (fun x => -x) '' s • t = (fun x => -x) '' (s • t)

Tactic:
exact image2_image_left_comm neg_smul

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
s : Set α
t : Set β
⊢ -s • t = -(s • t)

Tactic:
simp_rw [← image_neg_eq_neg]

Result:
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
s : Set α
t : Set β
⊢ (fun x => -x) '' s • t = (fun x => -x) '' (s • t)
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem HasStrictDerivAt.neg (h : HasStrictDerivAt f f' x) :
    HasStrictDerivAt (fun x => -f x) (-f') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
h : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun x => -f x) (-f') x

Tactic:
simpa using h.neg.hasStrictDerivAt

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem mul_eq_mul_left_iff : a * b = a * c ↔ b = c ∨ a = 0

Proof state:
M₀ : Type u_1
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
⊢ a * b = a * c ↔ b = c ∨ a = 0

Tactic:
by_cases ha : a = 0 <;> [simp only [ha, zero_mul, or_true]; simp [mul_right_inj', ha]]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem card_support_trinomial {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0)
    (hy : y ≠ 0) (hz : z ≠ 0) : #(support (C x * X ^ k + C y * X ^ m + C z * X ^ n)) = 3

Proof state:
R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ #(C x * X ^ k + C y * X ^ m + C z * X ^ n).support = 3

Tactic:
rw [support_trinomial hkm hmn hx hy hz,
  card_insert_of_not_mem
    (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
  card_insert_of_not_mem (mt mem_singleton.mp hmn.ne), card_singleton]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem himp_le_himp_himp_himp : b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ c ⊓ (b ⊓ a) ≤ c

Tactic:
exact inf_le_left

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c

Tactic:
rw [le_himp_iff, le_himp_iff, inf_assoc, himp_inf_self, ← inf_assoc, himp_inf_self, inf_assoc]

Result:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ c ⊓ (b ⊓ a) ≤ c
-- Mathlib/Algebra/Lie/SkewAdjoint.lean
theorem skewAdjointLieSubalgebraEquiv_symm_apply (f : skewAdjointLieSubalgebra B) :
    ↑((skewAdjointLieSubalgebraEquiv B e).symm f) = e.symm.lieConj f

Proof state:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
f : ↥(skewAdjointLieSubalgebra B)
⊢ ↑((skewAdjointLieSubalgebraEquiv B e).symm f) = e.symm.lieConj ↑f

Tactic:
simp [skewAdjointLieSubalgebraEquiv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueD_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
    {k a : α} {fallback v : β} : getValueD a (insertEntry k v l) fallback =
      if k == a then v else getValueD a l fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
fallback v : β
⊢ getValueD a (insertEntry k v l) fallback = if (k == a) = true then v else getValueD a l fallback

Tactic:
simp [getValueD_eq_getValue?, getValue?_insertEntry, apply_ite (fun x => Option.getD x fallback)]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean
theorem mkPiRing_eq_zero_iff (z : M) : ContinuousMultilinearMap.mkPiRing R ι z = 0 ↔ z = 0

Proof state:
R : Type u
ι : Type v
M : Type u_1
inst✝⁷ : Fintype ι
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousMul R
inst✝ : ContinuousSMul R M
z : M
⊢ ContinuousMultilinearMap.mkPiRing R ι z = 0 ↔ z = 0

Tactic:
rw [← mkPiRing_zero, mkPiRing_eq_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean
theorem aux2 {a b c : Nat} (hidx1 : b < c * a) : b % c < c

Proof state:
case a
a b c : Nat
hidx1 : b < c * a
⊢ c > 0

Tactic:
apply aux1

Result:
case a.h
a b c : Nat
hidx1 : b < c * a
⊢ ?a.b✝ < c * ?a.c✝

case a.b
a b c : Nat
hidx1 : b < c * a
⊢ Nat

case a.c
a b c : Nat
hidx1 : b < c * a
⊢ Nat

Proof state:
case a.h
a b c : Nat
hidx1 : b < c * a
⊢ ?a.b✝ < c * ?a.c✝

case a.b
a b c : Nat
hidx1 : b < c * a
⊢ Nat

case a.c
a b c : Nat
hidx1 : b < c * a
⊢ Nat

Tactic:
assumption

Result:
no goals

Proof state:
a b c : Nat
hidx1 : b < c * a
⊢ b % c < c

Tactic:
apply Nat.mod_lt

Result:
case a
a b c : Nat
hidx1 : b < c * a
⊢ c > 0
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
lemma generateFrom_iUnion_memPartition_le [m : MeasurableSpace α] {t : ℕ → Set α}
    (ht : ∀ n, MeasurableSet (t n)) :
    generateFrom (⋃ n, memPartition t n) ≤ m

Proof state:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ ∀ t_1 ∈ range t, MeasurableSet t_1

Tactic:
rintro s ⟨i, rfl⟩

Result:
case intro
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
i : ℕ
⊢ MeasurableSet (t i)

Proof state:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ generateFrom (⋃ n, memPartition t n) ≤ m

Tactic:
refine (generateFrom_iUnion_memPartition t).trans_le (generateFrom_le ?_)

Result:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ ∀ t_1 ∈ range t, MeasurableSet t_1

Proof state:
case intro
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
i : ℕ
⊢ MeasurableSet (t i)

Tactic:
exact ht i

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
/-- `EReal.toENNReal` is multiplicative. For the version with the nonnegativity
hypothesis on the first variable, see `EReal.toENNReal_mul`. -/
lemma toENNReal_mul' {x y : EReal} (hy : 0 ≤ y) :
    (x * y).toENNReal = x.toENNReal * y.toENNReal

Proof state:
x y : EReal
hy : 0 ≤ y
⊢ (x * y).toENNReal = x.toENNReal * y.toENNReal

Tactic:
rw [EReal.mul_comm, toENNReal_mul hy, mul_comm]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/FunctionSeries.lean
theorem tendstoUniformly_tsum_of_cofinite_eventually {ι : Type*} {f : ι → β → F} {u : ι → ℝ}
    (hu : Summable u) (hfu : ∀ᶠ (n : ι) in cofinite, ∀ x : β, ‖f n x‖ ≤ u n) :
    TendstoUniformly (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' n, f n x) atTop

Proof state:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
⊢ ∀ᶠ (n : ι) in cofinite, ∀ x ∈ univ, ‖f n x‖ ≤ u n

Tactic:
simpa using hfu

Result:
no goals

Proof state:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformly (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : ι), f n x) atTop

Tactic:
rw [← tendstoUniformlyOn_univ]

Result:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : ι), f n x) atTop univ

Proof state:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : ι), f n x) atTop univ

Tactic:
apply tendstoUniformlyOn_tsum_of_cofinite_eventually hu

Result:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
⊢ ∀ᶠ (n : ι) in cofinite, ∀ x ∈ univ, ‖f n x‖ ≤ u n
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivWithinAt.scomp_of_eq (hg : HasDerivWithinAt g₁ g₁' t' y)
    (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s t') (hy : y = h x) :
    HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' t' y
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Tactic:
rw [hy] at hg

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' t' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' t' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Tactic:
exact hg.scomp x hh hst

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem le_count_iff_replicate_sublist {l : List α} : n ≤ count a l ↔ replicate n a <+ l

Proof state:
case refine_2
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a : α
l : List α
h : replicate n a <+ l
⊢ n ≤ count a l

Tactic:
simpa only [count_replicate_self] using h.count_le a

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a : α
l : List α
⊢ n ≤ count a l ↔ replicate n a <+ l

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a : α
l : List α
h : n ≤ count a l
⊢ replicate n a <+ l

case refine_2
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a : α
l : List α
h : replicate n a <+ l
⊢ n ≤ count a l

Proof state:
case refine_1
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a : α
l : List α
h : n ≤ count a l
⊢ replicate n a <+ l

Tactic:
exact ((replicate_sublist_replicate a).2 h).trans <| filter_beq l a ▸ filter_sublist _

Result:
no goals