harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma HasFPowerSeriesWithinOnBall.restrictScalars (hf : HasFPowerSeriesWithinOnBall f p s x r) :
    HasFPowerSeriesWithinOnBall f (p.restrictScalars 𝕜) s x r :=
  ⟨hf.r_le.trans (FormalMultilinearSeries.radius_le_of_le (fun n ↦ by simp)), hf.r_pos, hf.hasSum⟩

Proof state:
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
s : Set E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
n : ℕ
⊢ ‖FormalMultilinearSeries.restrictScalars 𝕜 p n‖ ≤ ‖p n‖

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_mul_C (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) :
    coeff R n (φ * C σ R a) = coeff R n φ * a

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff R n) (φ * (C σ R) a) = (coeff R n) φ * a

Tactic:
simpa using coeff_add_mul_monomial n 0 φ a

Result:
no goals
-- Mathlib/Order/SuccPred/CompleteLinearOrder.lean
theorem Order.IsSuccPrelimit.iSup_Iio (h : IsSuccPrelimit x) : ⨆ a : Iio x, a.1 = x

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
⊢ ⨆ a, ↑a = x

Tactic:
rw [← sSup_eq_iSup', h.sSup_Iio]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem mod_two_eq_one_iff_testBit_zero : (x % 2 = 1) ↔ x.testBit 0 = true

Proof state:
x : Nat
⊢ x % 2 = 1 ↔ x.testBit 0 = true

Tactic:
cases mod_two_eq_zero_or_one x <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_eq_ite (p : Prop) {h h' : Decidable p} (x y : α) :
    (@ite _ p h x y = @ite _ p h' x y) ↔ True

Proof state:
α : Sort u_1
p : Prop
h h' : Decidable p
x y : α
⊢ (if p then x else y) = if p then x else y

Tactic:
congr

Result:
no goals

Proof state:
α : Sort u_1
p : Prop
h h' : Decidable p
x y : α
⊢ ((if p then x else y) = if p then x else y) ↔ True

Tactic:
simp

Result:
α : Sort u_1
p : Prop
h h' : Decidable p
x y : α
⊢ (if p then x else y) = if p then x else y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem length_mapIdx {l : List α} : (l.mapIdx f).length = l.length

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
⊢ (mapIdx f l).length = l.length

Tactic:
simp [mapIdx, length_mapIdx_go]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
lemma coeff_rTensorAlgHom_monomial_tmul
    (e : σ →₀ ℕ) (s : S) (n : N) (d : σ →₀ ℕ) :
    coeff d (rTensorAlgHom (monomial e s ⊗ₜ[R] n)) =
      if e = d then s ⊗ₜ[R] n else 0

Proof state:
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
e : σ →₀ ℕ
s : S
n : N
d : σ →₀ ℕ
⊢ coeff d (rTensorAlgHom ((monomial e) s ⊗ₜ[R] n)) = if e = d then s ⊗ₜ[R] n else 0

Tactic:
simp [ite_tmul]

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

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

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.sub_isLittleO (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) :
    IsBigOWith c₂ l (fun x => f₁ x - f₂ x) g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : f₂ =o[l] g
hc : c₁ < c₂
⊢ IsBigOWith c₂ l (fun x => f₁ x - f₂ x) g

Tactic:
simpa only [sub_eq_add_neg] using h₁.add_isLittleO h₂.neg_left hc

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_ult : eval .ult = (BitVec.ult : BitVec w → BitVec w → Bool)

Proof state:
w : Nat
⊢ ult.eval = BitVec.ult

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_or_inj_left_iff :
    ∀ {m x y : Bool}, (m && x) = (m && y) ∧ (m || x) = (m || y) ↔ x = y

Proof state:
⊢ ∀ {m x y : Bool}, (m && x) = (m && y) ∧ (m || x) = (m || y) ↔ x = y

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Complex/UnitDisc/Basic.lean
theorem coe_ne_neg_one (z : 𝔻) : (z : ℂ) ≠ -1 :=
  ne_of_apply_ne (‖·‖) <| by simpa [norm_neg] using z.norm_ne_one

Proof state:
z : 𝔻
⊢ (fun x => ‖x‖) ↑z ≠ (fun x => ‖x‖) (-1)

Tactic:
simpa [norm_neg] using z.norm_ne_one

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem verts_iInf {f : ι → G.Subgraph} : (⨅ i, f i).verts = ⋂ i, (f i).verts

Proof state:
ι : Sort u_1
V : Type u
G : SimpleGraph V
f : ι → G.Subgraph
⊢ (⨅ i, f i).verts = ⋂ i, (f i).verts

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem take_modifyHead {f : α → α} {l : List α} {n} :
    (l.modifyHead f).take n = (l.take n).modifyHead f

Proof state:
α : Type u_1
f : α → α
l : List α
n : Nat
⊢ take n (modifyHead f l) = modifyHead f (take n l)

Tactic:
cases l <;> cases n <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_hasBinaryCoproduct [HasBinaryCoproduct X Y] [HasZeroObject C] [HasZeroMorphisms C] :
    IsPushout (0 : 0 ⟶ X) (0 : 0 ⟶ Y) coprod.inl coprod.inr

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
inst✝² : HasBinaryCoproduct X Y
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
⊢ IsPushout 0 0 coprod.inl coprod.inr

Tactic:
convert @of_is_coproduct _ _ 0 X Y _ (colimit.isColimit _) HasZeroObject.zeroIsInitial
  <;> subsingleton

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_algebraMap (p : K[X]) : num (algebraMap _ _ p) = p

Proof state:
K : Type u
inst✝ : Field K
p : K[X]
⊢ ((algebraMap K[X] (RatFunc K)) p).num = p

Tactic:
convert num_div p 1 <;> simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
/-- The δ-thickening of the complement of the δ-thickening of a set is contained in the complement
of the set. -/
lemma thickening_compl_thickening_self_subset_compl (δ : ℝ) (E : Set α) :
    thickening δ (thickening δ E)ᶜ ⊆ Eᶜ

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ thickening δ (thickening δ E)ᶜ ⊆ Eᶜ

Tactic:
apply compl_subset_compl.mp

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ Eᶜᶜ ⊆ (thickening δ (thickening δ E)ᶜ)ᶜ

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ Eᶜᶜ ⊆ (thickening δ (thickening δ E)ᶜ)ᶜ

Tactic:
simpa only [compl_compl] using subset_compl_thickening_compl_thickening_self δ E

Result:
no goals
-- Mathlib/CategoryTheory/Dialectica/Monoidal.lean
theorem braiding_naturality_right (X : Dial C) {Y Z : Dial C} (f : Y ⟶ Z) :
    tensorHom (𝟙 X) f ≫ (braiding X Z).hom = (braiding X Y).hom ≫ tensorHom f (𝟙 X)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
f : Y ⟶ Z
⊢ tensorHom (𝟙 X) f ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ tensorHom f (𝟙 X)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_prod_Icc (a₁ a₂ : α) (b₁ b₂ : β) : Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
⊢ Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂)

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
x : α
y : β
⊢ (x, y) ∈ Icc a₁ a₂ ×ˢ Icc b₁ b₂ ↔ (x, y) ∈ Icc (a₁, b₁) (a₂, b₂)

Proof state:
case h.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
x : α
y : β
⊢ (x, y) ∈ Icc a₁ a₂ ×ˢ Icc b₁ b₂ ↔ (x, y) ∈ Icc (a₁, b₁) (a₂, b₂)

Tactic:
simp [and_assoc, and_comm, and_left_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem Fintype.linearIndependent_iff'ₛ [Fintype ι] [DecidableEq ι] :
    LinearIndependent R v ↔
      Injective (LinearMap.lsum R (fun _ ↦ R) ℕ fun i ↦ LinearMap.id.smulRight (v i))

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ LinearIndependent R v ↔ Injective ⇑((LinearMap.lsum R (fun x => R) ℕ) fun i => LinearMap.id.smulRight (v i))

Tactic:
simp [Fintype.linearIndependent_iffₛ, Injective, funext_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_tensorProduct' :
    Module.rank R (M ⊗[S] M₁) = Module.rank R M * Module.rank S M₁

Proof state:
R : Type u
S : Type u'
M M₁ : Type v
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : StrongRankCondition S
inst✝⁵ : Module S M
inst✝⁴ : Module S M₁
inst✝³ : Free S M₁
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : Free R M
⊢ Module.rank R (M ⊗[S] M₁) = Module.rank R M * Module.rank S M₁

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Finite.lean
@[simp]
lemma IsRkFinite.diff_singleton_iff : M.IsRkFinite (X \ {e}) ↔ M.IsRkFinite X

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
⊢ M.IsRkFinite (X \ {e}) ↔ M.IsRkFinite X

Tactic:
rw [isRkFinite_singleton.isRkFinite_diff_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem le_kernelSubobject (A : Subobject X) (h : A.arrow ≫ f = 0) : A ≤ kernelSubobject f :=
  Subobject.le_mk_of_comm (kernel.lift f A.arrow h) (by simp)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
A : Subobject X
h : A.arrow ≫ f = 0
⊢ kernel.lift f A.arrow h ≫ kernel.ι f = A.arrow

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Constructions.lean
@[simp]
lemma Topology.isInducing_const_prod {x : X} {f : Y → Z} :
    IsInducing (fun x' => (x, f x')) ↔ IsInducing f

Proof state:
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
x : X
f : Y → Z
⊢ (IsInducing fun x' => (x, f x')) ↔ IsInducing f

Tactic:
simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
  Function.comp_def, induced_const, top_inf_eq]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem map_subset_map {s₁ s₂ : Finset α} : s₁.map f ⊆ s₂.map f ↔ s₁ ⊆ s₂ :=
  ⟨fun h _ xs => (mem_map' _).1 <| h <| (mem_map' f).2 xs,
   fun h => by simp [subset_def, Multiset.map_subset_map h]⟩

Proof state:
α : Type u_1
β : Type u_2
f : α ↪ β
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ map f s₁ ⊆ map f s₂

Tactic:
simp [subset_def, Multiset.map_subset_map h]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem mapRange_id (h : ∀ i, id (0 : β₁ i) = 0 := fun _ => rfl) (g : Π₀ i : ι, β₁ i) :
    mapRange (fun i => (id : β₁ i → β₁ i)) h g = g

Proof state:
case h
ι : Type u
β₁ : ι → Type v₁
inst✝ : (i : ι) → Zero (β₁ i)
h : optParam (∀ (i : ι), id 0 = 0) ⋯
g : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ (mapRange (fun i => id) h g) i✝ = g i✝

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u
β₁ : ι → Type v₁
inst✝ : (i : ι) → Zero (β₁ i)
h : optParam (∀ (i : ι), id 0 = 0) ⋯
g : Π₀ (i : ι), β₁ i
⊢ mapRange (fun i => id) h g = g

Tactic:
ext

Result:
case h
ι : Type u
β₁ : ι → Type v₁
inst✝ : (i : ι) → Zero (β₁ i)
h : optParam (∀ (i : ι), id 0 = 0) ⋯
g : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ (mapRange (fun i => id) h g) i✝ = g i✝
-- Mathlib/Algebra/Ring/Invertible.lean
theorem invOf_add_invOf [Semiring α] (a b : α) [Invertible a] [Invertible b] :
    ⅟a + ⅟b = ⅟a * (a + b) * ⅟b

Proof state:
α : Type u
inst✝² : Semiring α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟a + ⅟b = ⅟a * (a + b) * ⅟b

Tactic:
rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem bex_ne_none {p : Option α → Prop} : (∃ x, ∃ (_ : x ≠ none), p x) ↔ ∃ x, p (some x) :=
  ⟨fun ⟨x, hx, hp⟩ => ⟨x.get <| ne_none_iff_isSome.1 hx, by rwa [some_get]⟩,
    fun ⟨x, hx⟩ => ⟨some x, some_ne_none x, hx⟩⟩

Proof state:
α : Type u_1
p : Option α → Prop
x✝ : ∃ x x_1, p x
x : Option α
hx : x ≠ none
hp : p x
⊢ p (some (x.get ⋯))

Tactic:
rwa [some_get]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF)
    {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) :
    (m.insertMany l).1.getKey! k' = k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
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
⊢ (m.insertMany l).val.getKey! k' = k

Tactic:
simp_to_model [insertMany] using List.getKey!_insertList_of_mem

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
@[simp]
lemma eqToHom_comp_lift_iff {R S : 𝒮} {a b b' : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : b = b') :
    p.IsHomLift f (φ ≫ eqToHom h) ↔ p.IsHomLift f φ where
  mp hφ'

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
hφ' : p.IsHomLift f (φ ≫ eqToHom ⋯)
⊢ p.IsHomLift f φ

Tactic:
simpa using hφ'

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b b' : 𝒳
f : R ⟶ S
φ : a ⟶ b
h : b = b'
hφ' : p.IsHomLift f (φ ≫ eqToHom h)
⊢ p.IsHomLift f φ

Tactic:
subst h

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
hφ' : p.IsHomLift f (φ ≫ eqToHom ⋯)
⊢ p.IsHomLift f φ
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem exp_zero : exp 𝕂 (0 : 𝔸) = 1

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ exp 𝕂 0 = 1

Tactic:
simp_rw [exp_eq_tsum, ← expSeries_apply_eq, expSeries_apply_zero, tsum_pi_single]

Result:
no goals
-- Mathlib/Logic/Equiv/Fintype.lean
theorem Equiv.Perm.viaFintypeEmbedding_apply_not_mem_range {b : β} (h : b ∉ Set.range f) :
    e.viaFintypeEmbedding f b = b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∉ Set.range ⇑f
⊢ (e.viaFintypeEmbedding f) b = b

Tactic:
rwa [Equiv.Perm.viaFintypeEmbedding, Equiv.Perm.extendDomain_apply_not_subtype]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[simp, reassoc]
lemma left_unitality (X : C) :
    (λ_ (F.obj X)).hom = ε F ▷ F.obj X ≫ μ F (𝟙_ C) X ≫ F.map (λ_ X).hom

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
⊢ (λ_ (F.obj X)).hom = ε F ▷ F.obj X ≫ μ F (𝟙_ C) X ≫ F.map (λ_ X).hom

Tactic:
apply left_unitality'

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem normalize_eq {num den} (den_nz) : normalize num den den_nz =
    { num := num / num.natAbs.gcd den
      den := den / num.natAbs.gcd den
      den_nz := normalize.den_nz den_nz rfl
      reduced := normalize.reduced' den_nz rfl }

Proof state:
num : Int
den : Nat
den_nz : den ≠ 0
⊢ normalize num den den_nz =
    { num := num / ↑(num.natAbs.gcd den), den := den / num.natAbs.gcd den, den_nz := ⋯, reduced := ⋯ }

Tactic:
simp only [normalize, maybeNormalize_eq,
  Int.tdiv_eq_ediv_of_dvd (Int.ofNat_dvd_left.2 (Nat.gcd_dvd_left ..))]

Result:
no goals
-- Mathlib/RingTheory/Derivation/Basic.lean
theorem map_natCast (n : ℕ) : D (n : A) = 0

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
n : ℕ
⊢ D ↑n = 0

Tactic:
rw [← nsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_div {x m n : Nat} (h : n ≤ m) (hx : 0 < x) : x ^ m / x ^ n = x ^ (m - n)

Proof state:
x m n : Nat
h : n ≤ m
hx : 0 < x
⊢ x ^ m / x ^ n = x ^ (m - n)

Tactic:
rw [Nat.div_eq_iff_eq_mul_left (Nat.pow_pos hx) (Nat.pow_dvd_pow _ h), Nat.pow_sub_mul_pow _ h]

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

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'
⊢ ((i.restrictScalarsRange j k hk B hB) m) n = 0 ↔ (B (i m)) (j n) = 0

Tactic:
rw [← hk.eq_iff, restrictScalarsRange_apply, map_zero]

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma mem_toRight {x : β} : x ∈ u.toRight ↔ inr x ∈ u

Proof state:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : β
⊢ x ∈ u.toRight ↔ inr x ∈ u

Tactic:
simp [toRight]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
@[to_additive]
lemma map_comp_zpow [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ι → G)
    (n : ℤ) : f ∘ (g ^ n) = f ∘ g ^ n

Proof state:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
n : ℤ
⊢ ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem isInitial_natCast (n : ℕ) : IsInitial n

Proof state:
n : ℕ
⊢ (↑n).IsInitial

Tactic:
rw [IsInitial, card_nat, ord_nat]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasStrictDerivAt.iterate {f : 𝕜 → 𝕜} {f' : 𝕜}
    (hf : HasStrictDerivAt f f' x) (hx : f x = x) (n : ℕ) :
    HasStrictDerivAt f^[n] (f' ^ n) x

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasStrictDerivAt f f' x
hx : f x = x
n : ℕ
⊢ HasStrictDerivAt f^[n] (f' ^ n) x

Tactic:
have := hf.iterate hx n

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasStrictDerivAt f f' x
hx : f x = x
n : ℕ
this : HasStrictFDerivAt f^[n] (smulRight 1 f' ^ n) x
⊢ HasStrictDerivAt f^[n] (f' ^ n) x

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasStrictDerivAt f f' x
hx : f x = x
n : ℕ
this : HasStrictFDerivAt f^[n] (smulRight 1 f' ^ n) x
⊢ HasStrictDerivAt f^[n] (f' ^ n) x

Tactic:
rwa [ContinuousLinearMap.smulRight_one_pow] at this

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem map_comp_lTensor (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) :
    (map f g).comp (g'.lTensor _) = map f (g.comp g')

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R Q
inst✝¹ : Module R S
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
g' : S →ₗ[R] N
⊢ map f g ∘ₗ lTensor M g' = map f (g ∘ₗ g')

Tactic:
simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem covBy_iff_Ioo_eq : a ⋖ b ↔ a < b ∧ Ioo a b = ∅ :=
  and_congr_right' <| by simp [eq_empty_iff_forall_not_mem]

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (∀ ⦃c : α⦄, a < c → ¬c < b) ↔ Ioo a b = ∅

Tactic:
simp [eq_empty_iff_forall_not_mem]

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean
theorem hasDerivAt_sqrt_mul_log {x : ℝ} (hx : x ≠ 0) :
    HasDerivAt (fun x => √x * log x) ((2 + log x) / (2 * √x)) x

Proof state:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt (fun x => √x * log x) ((2 + log x) / (2 * √x)) x

Tactic:
convert (hasDerivAt_sqrt hx).mul (hasDerivAt_log hx) using 1

Result:
case h.e'_9
x : ℝ
hx : x ≠ 0
⊢ (2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹

Proof state:
case h.e'_9
x : ℝ
hx : x ≠ 0
⊢ (2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹

Tactic:
rw [add_div, div_mul_cancel_left₀ two_ne_zero, ← div_eq_mul_inv, sqrt_div_self', add_comm,
  one_div, one_div, ← div_eq_inv_mul]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
theorem pow_count [DecidableEq α] (a : α) : a ^ s.count a = (s.filter (Eq a)).prod

Proof state:
α : Type u_3
inst✝¹ : CommMonoid α
s : Multiset α
inst✝ : DecidableEq α
a : α
⊢ a ^ count a s = (filter (Eq a) s).prod

Tactic:
rw [filter_eq, prod_replicate]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubVSubWeights_apply_right [DecidableEq ι] {i j : ι} (h : i ≠ j) :
    weightedVSubVSubWeights k i j j = -1

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
⊢ weightedVSubVSubWeights k i j j = -1

Tactic:
simp [weightedVSubVSubWeights, h.symm]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Sigma.lean
theorem prod_sigma {σ : α → Type*} (s : Finset α) (t : ∀ a, Finset (σ a)) (f : Sigma σ → β) :
    ∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
σ : α → Type u_6
s : Finset α
t : (a : α) → Finset (σ a)
f : Sigma σ → β
⊢ ∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩

Tactic:
simp_rw [← disjiUnion_map_sigma_mk, prod_disjiUnion, prod_map, Function.Embedding.sigmaMk_apply]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
lemma iSup_unique [Unique ι] (f : ι → α) : ⨆ i, f i = f default

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Unique ι
f : ι → α
⊢ ⨆ i, f i = f default

Tactic:
simp only [congr_arg f (Unique.eq_default _), iSup_const]

Result:
no goals