harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_restrict₀' (ht : NullMeasurableSet t μ) :
    (μ.restrict t).restrict s = μ.restrict (s ∩ t) :=
  ext fun u hu => by simp only [restrict_apply hu, restrict_apply₀' ht, inter_assoc]

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
u : Set α
hu : MeasurableSet u
⊢ ((μ.restrict t).restrict s) u = (μ.restrict (s ∩ t)) u

Tactic:
simp only [restrict_apply hu, restrict_apply₀' ht, inter_assoc]

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
@[simp] lemma max_self (a : α) : max a a = a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ max a a = a

Tactic:
simp [max_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
    {a : α} :
    m.getKey! a = m.getKeyD a default

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
a : α
⊢ m.getKey! a = m.getKeyD a default

Tactic:
simp_to_raw using Raw₀.getKey!_eq_getKeyD_default

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Support.lean
theorem support_mul_single_eq_image [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k}
    (hr : ∀ y, y * r = 0 ↔ y = 0) {x : G} (rx : IsRightRegular x) :
    (f * single x r).support = Finset.image (· * x) f.support

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
hy : y ∈ image (fun x_1 => x_1 * x) f.support
⊢ ∃ a ∈ f.support, a * x = y

Tactic:
simpa only [Finset.mem_image, exists_prop] using hy

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
⊢ (f * single x r).support = image (fun x_1 => x_1 * x) f.support

Tactic:
refine subset_antisymm (support_mul_single_subset f _ _) fun y hy => ?_

Result:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
hy : y ∈ image (fun x_1 => x_1 * x) f.support
⊢ y ∈ (f * single x r).support

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
hy : y ∈ image (fun x_1 => x_1 * x) f.support
⊢ y ∈ (f * single x r).support

Tactic:
obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ a * x = y := by
  simpa only [Finset.mem_image, exists_prop] using hy

Result:
case intro.intro
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
yf : y ∈ f.support
hy : y * x ∈ image (fun x_1 => x_1 * x) f.support
⊢ y * x ∈ (f * single x r).support

Proof state:
case intro.intro
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
yf : y ∈ f.support
hy : y * x ∈ image (fun x_1 => x_1 * x) f.support
⊢ y * x ∈ (f * single x r).support

Tactic:
simp only [mul_apply, mem_support_iff.mp yf, hr, mem_support_iff, sum_single_index,
  Finsupp.sum_ite_eq', Ne, not_false_iff, if_true, mul_zero, ite_self, sum_zero, rx.eq_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem Fintype.range_linearCombination :
    LinearMap.range (Fintype.linearCombination R S v) = Submodule.span R (Set.range v)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
⊢ LinearMap.range ((Fintype.linearCombination R S) v) = span R (Set.range v)

Tactic:
rw [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearMap.range_comp,
    LinearEquiv.range, Submodule.map_top, Finsupp.range_linearCombination]

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
theorem toMatrix_conjAe :
    LinearMap.toMatrix basisOneI basisOneI conjAe.toLinearMap = !![1, 0; 0, -1]

Proof state:
⊢ (LinearMap.toMatrix basisOneI basisOneI) conjAe.toLinearMap = !![1, 0; 0, -1]

Tactic:
ext i j

Result:
case a
i j : Fin 2
⊢ (LinearMap.toMatrix basisOneI basisOneI) conjAe.toLinearMap i j = !![1, 0; 0, -1] i j

Proof state:
case a
i j : Fin 2
⊢ (LinearMap.toMatrix basisOneI basisOneI) conjAe.toLinearMap i j = !![1, 0; 0, -1] i j

Tactic:
fin_cases i <;> fin_cases j <;> simp [LinearMap.toMatrix_apply]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean
lemma le_opENorm : ‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ ‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ

Tactic:
dsimp [enorm]

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ ↑‖f x‖₊ ≤ ↑‖f‖₊ * ↑‖x‖₊

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ ↑‖f x‖₊ ≤ ↑‖f‖₊ * ↑‖x‖₊

Tactic:
exact mod_cast le_opNNNorm ..

Result:
no goals
-- Mathlib/Data/List/Indexes.lean
theorem findIdxs_eq_map_indexesValues (p : α → Prop) [DecidablePred p] (as : List α) :
    findIdxs p as = map Prod.fst (indexesValues p as)

Proof state:
α : Type u
p : α → Prop
inst✝ : DecidablePred p
as : List α
⊢ findIdxs (fun b => decide (p b)) as = map Prod.fst (indexesValues (fun b => decide (p b)) as)

Tactic:
simp (config := { unfoldPartialApp := true }) only [indexesValues_eq_filter_enum,
  map_filter_eq_foldr, findIdxs, uncurry, foldrIdx_eq_foldr_enum, decide_eq_true_eq, comp_apply,
  Bool.cond_decide]

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem trans_refl : e.trans (PartialEquiv.refl β) = e :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) (by simp [trans_source])

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ (e.trans (PartialEquiv.refl β)).source = e.source

Tactic:
simp [trans_source]

Result:
no goals
-- Mathlib/Order/Hom/Basic.lean
theorem fst_prod_snd : (fst : α × β →o α).prod snd = id

Proof state:
case h.h.mk
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x : α
y : β
⊢ (fst.prod snd) (x, y) = id (x, y)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ fst.prod snd = id

Tactic:
ext ⟨x, y⟩ : 2

Result:
case h.h.mk
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x : α
y : β
⊢ (fst.prod snd) (x, y) = id (x, y)
-- Mathlib/Data/Finsupp/Single.lean
theorem card_support_eq_one' {f : α →₀ M} :
    #f.support = 1 ↔ ∃ a, ∃ b ≠ 0, f = single a b

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
⊢ #f.support = 1 ↔ ∃ a b, b ≠ 0 ∧ f = single a b

Tactic:
simp only [card_eq_one, support_eq_singleton']

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean
theorem contMDiff_iff_contDiff {f : E → E'} : ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f ↔ ContDiff 𝕜 n f

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
⊢ ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f ↔ ContDiff 𝕜 n f

Tactic:
rw [← contDiffOn_univ, ← contMDiffOn_univ, contMDiffOn_iff_contDiffOn]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem injectiveSeminorm_apply (x : ⨂[𝕜] i, E i) :
    injectiveSeminorm x = ⨆ p : {p | ∃ (G : Type (max uι u𝕜 uE))
    (_ : SeminormedAddCommGroup G) (_ : NormedSpace 𝕜 G), p = Seminorm.comp (normSeminorm 𝕜
    (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
    (toDualContinuousMultilinearMap G (𝕜 := 𝕜) (E := E))}, p.1 x

Proof state:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
⊢ injectiveSeminorm x = ⨆ p, ↑p x

Tactic:
simpa only [injectiveSeminorm, Set.coe_setOf, Set.mem_setOf_eq]
  using Seminorm.sSup_apply dualSeminorms_bounded

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Rank.lean
theorem rank_lt_of_rel (hb : Acc r b) (h : r a b) : (hb.inv h).rank < hb.rank :=
  (Order.lt_succ _).trans_le <| by
    rw [hb.rank_eq]
    exact Ordinal.le_iSup _ (⟨a, h⟩ : {a // r a b})

Proof state:
α : Type u
a b : α
r : α → α → Prop
hb : Acc r b
h : r a b
⊢ Order.succ ⋯.rank ≤ ⨆ b_1, Order.succ ⋯.rank

Tactic:
exact Ordinal.le_iSup _ (⟨a, h⟩ : {a // r a b})

Result:
no goals

Proof state:
α : Type u
a b : α
r : α → α → Prop
hb : Acc r b
h : r a b
⊢ Order.succ ⋯.rank ≤ hb.rank

Tactic:
rw [hb.rank_eq]

Result:
α : Type u
a b : α
r : α → α → Prop
hb : Acc r b
h : r a b
⊢ Order.succ ⋯.rank ≤ ⨆ b_1, Order.succ ⋯.rank
-- Mathlib/Data/Int/Log.lean
theorem log_one_right (b : ℕ) : log b (1 : R) = 0

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ log b 1 = 0

Tactic:
rw [log_of_one_le_right _ le_rfl, Nat.floor_one, Nat.log_one_right, Int.ofNat_zero]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem ofENat_toWithTop (x : PartENat) {_ : Decidable (x : PartENat).Dom} : toWithTop x = x

Proof state:
x : PartENat
x✝ : Decidable x.Dom
⊢ ↑x.toWithTop = x

Tactic:
induction x using PartENat.casesOn <;> simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem cons_isCycle {u v : V} (p : G.Path v u) (h : G.Adj u v)
    (he : ¬s(u, v) ∈ (p : G.Walk v u).edges) : (Walk.cons h ↑p).IsCycle

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Path v u
h : G.Adj u v
he : s(u, v) ∉ (↑p).edges
⊢ (Walk.cons h ↑p).IsCycle

Tactic:
simp [Walk.isCycle_def, Walk.cons_isTrail_iff, he]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.isBasis_insert_iff (hI : M.Indep I) :
    M.IsBasis I (insert e I) ↔ M.Dep (insert e I) ∨ e ∈ I

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ M.IsBasis I (insert e I) ↔ M.Dep (insert e I) ∨ e ∈ I

Tactic:
simp_rw [hI.isBasis_iff_forall_insert_dep (subset_insert _ _), dep_iff, insert_subset_iff,
  and_iff_left hI.subset_ground, mem_diff, mem_insert_iff, or_and_right, and_not_self,
  or_false, and_imp, forall_eq]

Result:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
-- Mathlib/Topology/Algebra/Algebra.lean
theorem continuous_algebraMap [ContinuousSMul R A] : Continuous (algebraMap R A)

Proof state:
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ Continuous fun r => r • 1

Tactic:
exact continuous_id.smul continuous_const

Result:
no goals

Proof state:
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ Continuous ⇑(algebraMap R A)

Tactic:
rw [algebraMap_eq_smul_one']

Result:
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ Continuous fun r => r • 1
-- Mathlib/Algebra/Order/Group/Finset.lean
lemma sup_add_sup (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → M) (g : κ → M) :
    s.sup f + t.sup g = (s ×ˢ t).sup fun ij ↦ f ij.1 + g ij.2

Proof state:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝⁴ : LinearOrderedAddCommMonoid M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → M
g : κ → M
⊢ s.sup f + t.sup g = (s ×ˢ t).sup fun ij => f ij.1 + g ij.2

Tactic:
simp only [Finset.sup_add hs, Finset.add_sup ht, Finset.sup_product_left]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sin_neg (θ : Angle) : sin (-θ) = -sin θ

Proof state:
case h
x✝ : ℝ
⊢ (-↑x✝).sin = -(↑x✝).sin

Tactic:
exact Real.sin_neg _

Result:
no goals

Proof state:
θ : Angle
⊢ (-θ).sin = -θ.sin

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (-↑x✝).sin = -(↑x✝).sin
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem add_assoc {X Y : C} (a b c : X ⟶ Y) : a + b + c = a + (b + c)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a + b + c = a + (b + c)

Tactic:
conv_lhs =>
  congr; rw [add_def]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a - -b + c = a + (b + c)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a - -b + c = a + (b + c)

Tactic:
rw [sub_add, ← add_neg, neg_sub', neg_neg]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem mem_keys_kinsert {a a'} {b' : β a'} {l : List (Sigma β)} :
    a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
⊢ a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys

Tactic:
by_cases h : a = a' <;> simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem append_singleton {a : α} {as : Vector α n} : as ++ #v[a] = as.push a

Proof state:
case mk
α : Type u_1
n : Nat
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ } ++ { toArray := #[a], size_toArray := ⋯ } =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.push a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
as : Vector α n
⊢ as ++ { toArray := #[a], size_toArray := ⋯ } = as.push a

Tactic:
cases as

Result:
case mk
α : Type u_1
n : Nat
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ } ++ { toArray := #[a], size_toArray := ⋯ } =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.push a
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
lemma edist_top_of_ne (h : u ≠ v) : (⊤ : SimpleGraph V).edist u v = 1

Proof state:
V : Type u_1
u v : V
h : u ≠ v
⊢ ⊤.edist u v = 1

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem mem_closure {s : Set (Filter α)} {l : Filter α} :
    l ∈ closure s ↔ ∀ t ∈ l, ∃ l' ∈ s, t ∈ l'

Proof state:
α : Type u_2
s : Set (Filter α)
l : Filter α
⊢ l ∈ closure s ↔ ∀ t ∈ l, ∃ l' ∈ s, t ∈ l'

Tactic:
simp only [closure_eq_compl_interior_compl, Filter.mem_interior, mem_compl_iff, not_exists,
  not_forall, Classical.not_not, exists_prop, not_and, and_comm, subset_def, mem_Iic,
  le_principal_iff]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem one_le_prod' (h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i :=
  le_trans (by rw [prod_const_one]) (prod_le_prod' h)

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s : Finset ι
h : ∀ i ∈ s, 1 ≤ f i
⊢ 1 ≤ ∏ i ∈ s, 1

Tactic:
rw [prod_const_one]

Result:
no goals
-- Mathlib/RingTheory/Bialgebra/TensorProduct.lean
lemma counit_eq_algHom_toLinearMap :
    Coalgebra.counit (R := R) (A := A ⊗[R] B) =
      ((Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map
      (Bialgebra.counitAlgHom R A) (Bialgebra.counitAlgHom R B))).toLinearMap

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
⊢ CoalgebraStruct.counit =
    ((Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map (counitAlgHom R A) (counitAlgHom R B))).toLinearMap

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem exists_bucket [BEq α] [Hashable α]
    (m : Array (AssocList α β)) (h : 0 < m.size) (k : α) :
    ∃ l : List ((a : α) × β a), Perm (toListModel m) ((bucket m h k).toList ++ l) ∧
      (∀ [LawfulHashable α], IsHashSelf m → ∀ k', hash k = hash k' → containsKey k' l = false)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
h : 0 < m.size
k : α
⊢ ∃ l,
    (toListModel m).Perm ((bucket m h k).toList ++ l) ∧
      ∀ [inst : LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → containsKey k' l = false

Tactic:
obtain ⟨l, h₁, -, h₂⟩ := exists_bucket_of_update m h k (fun _ => .nil)

Result:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
h : 0 < m.size
k : α
l : List ((a : α) × β a)
h₁ : (toListModel m).Perm ((bucket m h k).toList ++ l)
h₂ : ∀ [inst : LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → containsKey k' l = false
⊢ ∃ l,
    (toListModel m).Perm ((bucket m h k).toList ++ l) ∧
      ∀ [inst : LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → containsKey k' l = false

Proof state:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
h : 0 < m.size
k : α
l : List ((a : α) × β a)
h₁ : (toListModel m).Perm ((bucket m h k).toList ++ l)
h₂ : ∀ [inst : LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → containsKey k' l = false
⊢ ∃ l,
    (toListModel m).Perm ((bucket m h k).toList ++ l) ∧
      ∀ [inst : LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → containsKey k' l = false

Tactic:
exact ⟨l, h₁, h₂⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContinuousLinearMap.iteratedFDeriv_comp_left {f : E → F} (g : F →L[𝕜] G)
    (hf : ContDiffAt 𝕜 n f x) {i : ℕ} (hi : i ≤ n) :
    iteratedFDeriv 𝕜 i (g ∘ f) x = g.compContinuousMultilinearMap (iteratedFDeriv 𝕜 i f x)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E
n : WithTop ℕ∞
f : E → F
g : F →L[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDeriv 𝕜 i (⇑g ∘ f) x = g.compContinuousMultilinearMap (iteratedFDeriv 𝕜 i f x)

Tactic:
simp only [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E
n : WithTop ℕ∞
f : E → F
g : F →L[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDerivWithin 𝕜 i (⇑g ∘ f) univ x = g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f univ x)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E
n : WithTop ℕ∞
f : E → F
g : F →L[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDerivWithin 𝕜 i (⇑g ∘ f) univ x = g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f univ x)

Tactic:
exact g.iteratedFDerivWithin_comp_left hf.contDiffWithinAt uniqueDiffOn_univ (mem_univ x) hi

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineSpace.lean
@[simp]
lemma map_id : map n (𝟙 S) = 𝟙 𝔸(n; S)

Proof state:
n : Type v
S : Scheme
⊢ map n (𝟙 S) = 𝟙 𝔸(n; S)

Tactic:
ext1 <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
lemma map_apply_of_aemeasurable (ν : FiniteMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν)
    {A : Set Ω'} (A_mble : MeasurableSet A) :
    ν.map f A = ν (f ⁻¹' A)

Proof state:
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
ν : FiniteMeasure Ω
f : Ω → Ω'
f_aemble : AEMeasurable f ↑ν
A : Set Ω'
A_mble : MeasurableSet A
key : ↑(ν.map f) A = ↑ν (f ⁻¹' A)
⊢ (ν.map f) A = ν (f ⁻¹' A)

Tactic:
exact (ENNReal.toNNReal_eq_toNNReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mpr key

Result:
no goals

Proof state:
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
ν : FiniteMeasure Ω
f : Ω → Ω'
f_aemble : AEMeasurable f ↑ν
A : Set Ω'
A_mble : MeasurableSet A
⊢ (ν.map f) A = ν (f ⁻¹' A)

Tactic:
have key := ν.map_apply' f_aemble A_mble

Result:
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
ν : FiniteMeasure Ω
f : Ω → Ω'
f_aemble : AEMeasurable f ↑ν
A : Set Ω'
A_mble : MeasurableSet A
key : ↑(ν.map f) A = ↑ν (f ⁻¹' A)
⊢ (ν.map f) A = ν (f ⁻¹' A)
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem setAverage_congr (h : s =ᵐ[μ] t) : ⨍ x in s, f x ∂μ = ⨍ x in t, f x ∂μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
s t : Set α
f : α → E
h : s =ᶠ[ae μ] t
⊢ ⨍ (x : α) in s, f x ∂μ = ⨍ (x : α) in t, f x ∂μ

Tactic:
simp only [setAverage_eq, setIntegral_congr_set h, measure_congr h]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeriesSummable.smul {f : ℕ → ℂ} (c : ℂ) {s : ℂ} (hf : LSeriesSummable f s) :
    LSeriesSummable (c • f) s

Proof state:
f : ℕ → ℂ
c s : ℂ
hf : LSeriesSummable f s
⊢ LSeriesSummable (c • f) s

Tactic:
simpa [LSeriesSummable, term_smul] using hf.const_smul c

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
theorem tprod_eq_one_of_not_multipliable (h : ¬Multipliable f) : ∏' b, f b = 1

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
h : ¬Multipliable f
⊢ ∏' (b : β), f b = 1

Tactic:
simp [tprod_def, h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem ext (h : ∀ s, MeasurableSet s → μ₁ s = μ₂ s) : μ₁ = μ₂ :=
  toOuterMeasure_injective <| by
  rw [← trimmed, OuterMeasure.trim_congr (h _), trimmed]

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
h : ∀ (s : Set α), MeasurableSet s → μ₁ s = μ₂ s
⊢ μ₁.toOuterMeasure = μ₂.toOuterMeasure

Tactic:
rw [← trimmed, OuterMeasure.trim_congr (h _), trimmed]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem le_sdiff_sup : a ≤ a \ b ⊔ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b

Tactic:
rw [sup_comm, ← sdiff_le_iff]

Result:
no goals