harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
@[deprecated injOn_genEigenspace (since := "2024-10-23")]
lemma injOn_iSup_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) :
    InjOn (⨆ k : ℕ, f.genEigenspace · k) {μ | ⨆ k : ℕ, f.genEigenspace μ k ≠ ⊥}

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
⊢ InjOn (fun x => ⨆ k, (f.genEigenspace x) ↑k) {μ | ⨆ k, (f.genEigenspace μ) ↑k ≠ ⊥}

Tactic:
simp_rw [iSup_genEigenspace_eq]

Result:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
⊢ InjOn (fun x => f.maxGenEigenspace x) {μ | f.maxGenEigenspace μ ≠ ⊥}

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
⊢ InjOn (fun x => f.maxGenEigenspace x) {μ | f.maxGenEigenspace μ ≠ ⊥}

Tactic:
apply injOn_maxGenEigenspace

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem nim_one_moveLeft (x) : (nim 1).moveLeft x = nim 0

Proof state:
x : (nim 1).LeftMoves
⊢ (nim 1).moveLeft x = nim 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
@[reassoc (attr := simp)]
lemma limitIsoOfIsRightKanExtension_inv_π (i : C) :
    (F'.limitIsoOfIsRightKanExtension α).inv ≫ limit.π F' (L.obj i) ≫ α.app i = limit.π F i

Proof state:
C : Type u_1
H : Type u_3
D : Type u_4
inst✝⁵ : Category.{u_7, u_1} C
inst✝⁴ : Category.{u_6, u_3} H
inst✝³ : Category.{u_8, u_4} D
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝² : F'.IsRightKanExtension α
inst✝¹ : HasLimit F
inst✝ : HasLimit F'
i : C
⊢ (F'.limitIsoOfIsRightKanExtension α).inv ≫ limit.π F' (L.obj i) ≫ α.app i = limit.π F i

Tactic:
simp [limitIsoOfIsRightKanExtension]

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
lemma update_piecewise_of_not_mem [DecidableEq ι] {i : ι} (hi : i ∉ s) (v : π i) :
    update (s.piecewise f g) i v = s.piecewise f (update g i v)

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
j : ι
hj : j ∈ s
⊢ j ≠ i

Tactic:
exact fun h => hi (h ▸ hj)

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
⊢ update (s.piecewise f g) i v = s.piecewise f (update g i v)

Tactic:
rw [update_piecewise]

Result:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
⊢ s.piecewise (update f i v) (update g i v) = s.piecewise f (update g i v)

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
⊢ s.piecewise (update f i v) (update g i v) = s.piecewise f (update g i v)

Tactic:
refine s.piecewise_congr (fun j hj => update_of_ne ?_ ..) fun _ _ => rfl

Result:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
j : ι
hj : j ∈ s
⊢ j ≠ i
-- Mathlib/Order/Bounds/Lattice.lean
theorem isLUB_iUnion_iff_of_isLUB {u : ι → α} (hs : ∀ i, IsLUB (s i) (u i)) (c : α) :
    IsLUB (Set.range u) c ↔ IsLUB (⋃ i, s i) c

Proof state:
α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
⊢ upperBounds (range u) = upperBounds (⋃ i, s i)

Tactic:
simp_rw [range_eq_iUnion, upperBounds_iUnion, upperBounds_singleton, (hs _).upperBounds_eq]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
⊢ IsLUB (range u) c ↔ IsLUB (⋃ i, s i) c

Tactic:
refine isLUB_congr ?_

Result:
α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
⊢ upperBounds (range u) = upperBounds (⋃ i, s i)
-- Mathlib/Topology/Order/OrderClosed.lean
@[simp] lemma bddBelow_closure : BddBelow (closure s) ↔ BddBelow s

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIciTopology α
s : Set α
⊢ BddBelow (closure s) ↔ BddBelow s

Tactic:
simp_rw [BddBelow, lowerBounds_closure]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem mem_cyclicPermutations_self (l : List α) : l ∈ cyclicPermutations l

Proof state:
α : Type u
l : List α
⊢ l ∈ l.cyclicPermutations

Tactic:
simpa using head_mem (cyclicPermutations_ne_nil l)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reverse_trailingCoeff (f : R[X]) : f.reverse.trailingCoeff = f.leadingCoeff

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.trailingCoeff = f.leadingCoeff

Tactic:
rw [trailingCoeff, natTrailingDegree_reverse, coeff_zero_reverse]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearMap.lean
@[simp] lemma restrictScalarsRange_apply (m : M') (n : N') :
    k (restrictScalarsRange i j k hk B hB m n) = B (i m) (j n)

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : SMul S R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
inst✝¹² : Module S M
inst✝¹¹ : Module S N
inst✝¹⁰ : Module S P
inst✝⁹ : IsScalarTower S R M
inst✝⁸ : IsScalarTower S R N
inst✝⁷ : IsScalarTower S R P
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module S M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module S N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module S P'
inst✝ : SMulCommClass R S P
i : M' →ₗ[S] M
j : N' →ₗ[S] N
k : P' →ₗ[S] P
hk : Injective ⇑k
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ range k
m : M'
n : N'
⊢ k (((i.restrictScalarsRange j k hk B hB) m) n) = (B (i m)) (j n)

Tactic:
simp [restrictScalarsRange]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem not_true_eq_false : (¬ True) = False

Proof state:
⊢ (¬True) = False

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map_map₂ (f : α → β → γ) (g : γ → δ) :
    (map₂ f a b).map g = map₂ (fun a b => g (f a b)) a b

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
f : α → β → γ
g : γ → δ
⊢ Option.map g (map₂ f a b) = map₂ (fun a b => g (f a b)) a b

Tactic:
cases a <;> cases b <;> rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Asymptotics.lean
theorem LocallyIntegrable.integrable_of_isBigO_atBot [IsMeasurablyGenerated (atBot (α := α))]
    [OrderTop α] (hf : LocallyIntegrable f μ) (ho : f =O[atBot] g)
    (hg : IntegrableAtFilter g atBot μ) : Integrable f μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁷ : TopologicalSpace α
inst✝⁶ : SecondCountableTopology α
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedAddCommGroup F
inst✝³ : LinearOrder α
inst✝² : CompactIccSpace α
inst✝¹ : atBot.IsMeasurablyGenerated
inst✝ : OrderTop α
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ Integrable f μ

Tactic:
refine integrable_iff_integrableAtFilter_atBot.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁷ : TopologicalSpace α
inst✝⁶ : SecondCountableTopology α
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedAddCommGroup F
inst✝³ : LinearOrder α
inst✝² : CompactIccSpace α
inst✝¹ : atBot.IsMeasurablyGenerated
inst✝ : OrderTop α
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ StronglyMeasurableAtFilter f atBot μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁷ : TopologicalSpace α
inst✝⁶ : SecondCountableTopology α
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedAddCommGroup F
inst✝³ : LinearOrder α
inst✝² : CompactIccSpace α
inst✝¹ : atBot.IsMeasurablyGenerated
inst✝ : OrderTop α
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ StronglyMeasurableAtFilter f atBot μ

Tactic:
exact hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.isBase_of_maximal (hI : M.Indep I) (h : ∀ ⦃J⦄, M.Indep J → I ⊆ J → I = J) :
    M.IsBase I

Proof state:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
h : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → I = J
⊢ M.IsBase I

Tactic:
rwa [isBase_iff_maximal_indep, maximal_subset_iff, and_iff_right hI]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Canonical.lean
lemma Odd.pos [Semiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [Nontrivial α] {a : α} :
    Odd a → 0 < a

Proof state:
case intro
α : Type u
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : Nontrivial α
k : α
⊢ 0 < 2 * k + 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : Nontrivial α
a : α
⊢ Odd a → 0 < a

Tactic:
rintro ⟨k, rfl⟩

Result:
case intro
α : Type u
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : Nontrivial α
k : α
⊢ 0 < 2 * k + 1
-- Mathlib/Data/Finite/Defs.lean
theorem Equiv.set_finite_iff {s : Set α} {t : Set β} (hst : s ≃ t) : s.Finite ↔ t.Finite

Proof state:
α : Type u
β : Type v
s : Set α
t : Set β
hst : ↑s ≃ ↑t
⊢ s.Finite ↔ t.Finite

Tactic:
simp_rw [← Set.finite_coe_iff, hst.finite_iff]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem _root_.Orthonormal.linearIsometryEquiv_symm_apply_single_one [DecidableEq ι] (h i) :
    (hv.isHilbertSum h).linearIsometryEquiv.symm (lp.single 2 i 1) = v i

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
inst✝ : DecidableEq ι
h : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure
i : ι
⊢ ⋯.linearIsometryEquiv.symm (lp.single 2 i 1) = v i

Tactic:
rw [IsHilbertSum.linearIsometryEquiv_symm_apply_single, LinearIsometry.toSpanSingleton_apply,
  one_smul]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem not_eq_true_eq_eq_false (a : Bool) : (not a = true) = (a = false)

Proof state:
a : Bool
⊢ ((!a) = true) = (a = false)

Tactic:
cases a <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)} :
    (insertMany m l).1.1.isEmpty = (m.1.isEmpty && l.isEmpty)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
⊢ (insertMany m l).val.val.isEmpty = (m.val.isEmpty && l.isEmpty)

Tactic:
simp_to_model [Const.insertMany] using List.isEmpty_insertListConst

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem mrange_lift (f : M →* P) (g : N →* P) :
    MonoidHom.mrange (lift f g) = MonoidHom.mrange f ⊔ MonoidHom.mrange g

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : Monoid P
f : M →* P
g : N →* P
⊢ MonoidHom.mrange (lift f g) = MonoidHom.mrange f ⊔ MonoidHom.mrange g

Tactic:
simp [mrange_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst)
    {h'} :
    (insertMany empty l).1.getKey k' h' = k

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
h' : (empty.insertMany l).val.contains k' = true
⊢ (empty.insertMany l).val.getKey k' h' = k

Tactic:
rw [getKey_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_alter [LawfulBEq α] {k k' : α} (h : m.1.WF) [Inhabited (β k')]
    {f : Option (β k) → Option (β k)} :
    (m.alter k f).get! k' =
      if heq : k == k' then
        (f (m.get? k)).map (cast (congrArg β (eq_of_beq heq))) |>.get!
      else
        m.get! k'

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
k k' : α
h : m.val.WF
inst✝ : Inhabited (β k')
f : Option (β k) → Option (β k)
⊢ (m.alter k f).get! k' = if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).get! else m.get! k'

Tactic:
simp_to_model [alter] using List.getValueCast!_alterKey

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_succAbove [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) (x : Fin (n + 1)) :
    ∏ i, f i = f x * ∏ i : Fin n, f (x.succAbove i)

Proof state:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
f : Fin (n + 1) → β
x : Fin (n + 1)
⊢ ∏ i : Fin (n + 1), f i = f x * ∏ i : Fin n, f (x.succAbove i)

Tactic:
rw [univ_succAbove, prod_cons, Finset.prod_map _ x.succAboveEmb]

Result:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
f : Fin (n + 1) → β
x : Fin (n + 1)
⊢ f x * ∏ x_1 : Fin n, f (x.succAboveEmb x_1) = f x * ∏ i : Fin n, f (x.succAbove i)

Proof state:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
f : Fin (n + 1) → β
x : Fin (n + 1)
⊢ f x * ∏ x_1 : Fin n, f (x.succAboveEmb x_1) = f x * ∏ i : Fin n, f (x.succAbove i)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem derivWithin.neg : derivWithin (fun y => -f y) s x = -derivWithin f s x

Proof state:
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => -f y) s x = -derivWithin f s x

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => -f y) s x = -derivWithin f s x

Tactic:
simp only [derivWithin, fderivWithin_neg hxs, ContinuousLinearMap.neg_apply]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
⊢ derivWithin (fun y => -f y) s x = -derivWithin f s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => -f y) s x = -derivWithin f s x

case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => -f y) s x = -derivWithin f s x
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem Finset.measurable_prod (s : Finset ι) (hf : ∀ i ∈ s, Measurable (f i)) :
    Measurable fun a ↦ ∏ i ∈ s, f i a

Proof state:
M : Type u_2
ι : Type u_3
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun a => (∏ c ∈ s, f c) a

Tactic:
exact Finset.prod_induction _ _ (fun _ _ => Measurable.mul) (@measurable_one M _ _ _ _) hf

Result:
no goals

Proof state:
M : Type u_2
ι : Type u_3
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun a => ∏ i ∈ s, f i a

Tactic:
simp_rw [← Finset.prod_apply]

Result:
M : Type u_2
ι : Type u_3
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun a => (∏ c ∈ s, f c) a
-- Mathlib/Order/OrdContinuous.lean
theorem map_sSup (hf : LeftOrdContinuous f) (s : Set α) : f (sSup s) = ⨆ x ∈ s, f x

Proof state:
α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
s : Set α
⊢ f (sSup s) = ⨆ x ∈ s, f x

Tactic:
rw [hf.map_sSup', sSup_image]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
theorem cast_commute (r : ℚ) (a : α) : Commute (↑r) a

Proof state:
α : Type u_3
inst✝ : DivisionRing α
r : ℚ
a : α
⊢ Commute (↑r) a

Tactic:
simpa only [cast_def] using (r.1.cast_commute a).div_left (r.2.cast_commute a)

Result:
no goals
-- Mathlib/Algebra/Regular/SMul.lean
theorem isSMulRegular_of_group [MulAction G R] (g : G) : IsSMulRegular R g

Proof state:
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
⊢ IsSMulRegular R g

Tactic:
intro x y h

Result:
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x => g • x) x = (fun x => g • x) y
⊢ x = y
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem mkCoinductiveAux₃ (i j : ℕ) (h : i + 1 = j) :
    (P.xNextIso h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).2.1 =
      (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).1 ≫ (Q.xPrevIso h).hom

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
i j : ℕ
h : i + 1 = j
⊢ (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst ≫ (xPrevIso Q h).hom

Tactic:
subst j

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ (xNextIso P ⋯).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (i + 1)).fst ≫ (xPrevIso Q ⋯).hom

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ (xNextIso P ⋯).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (i + 1)).fst ≫ (xPrevIso Q ⋯).hom

Tactic:
rcases i with (_ | _ | i) <;> simp [mkCoinductiveAux₂]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/CardinalArrow.lean
lemma locallySmall_of_small_arrow (C : Type u) [Category.{v} C] [Small.{w} (Arrow C)] :
    LocallySmall.{w} C where
  hom_small X Y :=
    small_of_injective (f := fun f ↦ Arrow.mk f) (fun f g h ↦ by
      change (Arrow.mk f).hom = (Arrow.mk g).hom
      congr)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, max u v} (Arrow C)
X Y : C
f g : X ⟶ Y
h : (fun f => Arrow.mk f) f = (fun f => Arrow.mk f) g
⊢ f = g

Tactic:
change (Arrow.mk f).hom = (Arrow.mk g).hom

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, max u v} (Arrow C)
X Y : C
f g : X ⟶ Y
h : (fun f => Arrow.mk f) f = (fun f => Arrow.mk f) g
⊢ (Arrow.mk f).hom = (Arrow.mk g).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, max u v} (Arrow C)
X Y : C
f g : X ⟶ Y
h : (fun f => Arrow.mk f) f = (fun f => Arrow.mk f) g
⊢ (Arrow.mk f).hom = (Arrow.mk g).hom

Tactic:
congr

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean
theorem exists_dual_vector' [Nontrivial E] (x : E) : ∃ g : E →L[𝕜] 𝕜, ‖g‖ = 1 ∧ g x = ‖x‖

Proof state:
case pos
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
⊢ ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖

Tactic:
obtain ⟨y, hy⟩ := exists_ne (0 : E)

Result:
case pos.intro
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
⊢ ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖

Proof state:
case pos.intro.intro
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
g : E →L[𝕜] 𝕜
hg : ‖g‖ = 1 ∧ g y = ↑‖y‖
⊢ g x = ↑‖x‖

Tactic:
simp [hx]

Result:
no goals

Proof state:
case pos.intro.intro
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
g : E →L[𝕜] 𝕜
hg : ‖g‖ = 1 ∧ g y = ↑‖y‖
⊢ ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖

Tactic:
refine ⟨g, hg.left, ?_⟩

Result:
case pos.intro.intro
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
g : E →L[𝕜] 𝕜
hg : ‖g‖ = 1 ∧ g y = ↑‖y‖
⊢ g x = ↑‖x‖

Proof state:
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
⊢ ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖

Tactic:
by_cases hx : x = 0

Result:
case pos
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
⊢ ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖

case neg
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : ¬x = 0
⊢ ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖

Proof state:
case neg
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : ¬x = 0
⊢ ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖

Tactic:
exact exists_dual_vector 𝕜 x hx

Result:
no goals

Proof state:
case pos.intro
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
⊢ ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖

Tactic:
obtain ⟨g, hg⟩ : ∃ g : E →L[𝕜] 𝕜, ‖g‖ = 1 ∧ g y = ‖y‖ := exists_dual_vector 𝕜 y hy

Result:
case pos.intro.intro
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
g : E →L[𝕜] 𝕜
hg : ‖g‖ = 1 ∧ g y = ↑‖y‖
⊢ ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_mul_intCast (x : ℝ≥0) (y : ℝ) (n : ℤ) : x ^ (y * n) = (x ^ y) ^ n

Proof state:
x : ℝ≥0
y : ℝ
n : ℤ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
rw [rpow_mul, rpow_intCast]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma le_self_pow₀ (ha : 1 ≤ a) (hn : n ≠ 0) : a ≤ a ^ n

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
n : ℕ
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 ≤ a
hn : n ≠ 0
⊢ a ≤ a ^ n

Tactic:
simpa only [pow_one] using pow_le_pow_right₀ ha <| Nat.pos_iff_ne_zero.2 hn

Result:
no goals