harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Set.Finite.ciSup_mem_image {s : Set ι} (hs : s.Finite) (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
    ⨆ i ∈ s, f i ∈ f '' s

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Set ι
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i ∈ f '' s

Tactic:
lift s to Finset ι using hs

Result:
case intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ ↑s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ ↑s, f i ∈ f '' ↑s

Proof state:
case intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ ↑s, f i ∈ f '' ↑s

Tactic:
simpa using Finset.ciSup_mem_image f h

Result:
no goals

Proof state:
case intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ ↑s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ ↑s, f i ∈ f '' ↑s

Tactic:
simp only [Finset.mem_coe] at h

Result:
case intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ ↑s, f i ∈ f '' ↑s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem back?_mapIdx {l : Array α} {f : Nat → α → β} :
    (mapIdx f l).back? = (l.back?).map (f (l.size - 1))

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : Nat → α → β
⊢ (mapIdx f l).back? = Option.map (f (l.size - 1)) l.back?

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : List α
⊢ (mapIdx f { toList := l }).back? = Option.map (f ({ toList := l }.size - 1)) { toList := l }.back?

Proof state:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : List α
⊢ (mapIdx f { toList := l }).back? = Option.map (f ({ toList := l }.size - 1)) { toList := l }.back?

Tactic:
simp [List.getLast?_mapIdx]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem nonempty_inter_of_measure_lt_add' {m : MeasurableSpace α} (μ : Measure α) {s t u : Set α}
    (hs : MeasurableSet s) (h's : s ⊆ u) (h't : t ⊆ u) (h : μ u < μ s + μ t) :
    (s ∩ t).Nonempty

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ t + μ s
⊢ (s ∩ t).Nonempty

Tactic:
rw [inter_comm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ t + μ s
⊢ (t ∩ s).Nonempty

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ s + μ t
⊢ (s ∩ t).Nonempty

Tactic:
rw [add_comm] at h

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ t + μ s
⊢ (s ∩ t).Nonempty

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ t + μ s
⊢ (t ∩ s).Nonempty

Tactic:
exact nonempty_inter_of_measure_lt_add μ hs h't h's h

Result:
no goals
-- Mathlib/Data/Matrix/Diagonal.lean
theorem diagonal_injective [Zero α] : Function.Injective (diagonal : (n → α) → Matrix n n α) :=
  fun d₁ d₂ h => funext fun i => by simpa using Matrix.ext_iff.mpr h i i

Proof state:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
d₁ d₂ : n → α
h : diagonal d₁ = diagonal d₂
i : n
⊢ d₁ i = d₂ i

Tactic:
simpa using Matrix.ext_iff.mpr h i i

Result:
no goals
-- Mathlib/Algebra/Lie/OfAssociative.lean
@[simp]
lemma toEnd_eq_zero_iff [IsFaithful R L M] {x : L} :
    toEnd R L M x = 0 ↔ x = 0

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsFaithful R L M
x : L
⊢ (toEnd R L M) x = 0 ↔ x = 0

Tactic:
simp [- LieHom.map_zero, ← (toEnd R L M).map_zero]

Result:
no goals
-- Mathlib/Topology/NoetherianSpace.lean
theorem noetherianSpace_iff_opens : NoetherianSpace α ↔ ∀ s : Opens α, IsCompact (s : Set α)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s

Tactic:
rw [NoetherianSpace, CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact,
  CompleteLattice.isSupFiniteCompact_iff_all_elements_compact]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ (∀ (k : Opens α), CompleteLattice.IsCompactElement k) ↔ ∀ (s : Opens α), IsCompact ↑s

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ (∀ (k : Opens α), CompleteLattice.IsCompactElement k) ↔ ∀ (s : Opens α), IsCompact ↑s

Tactic:
exact forall_congr' Opens.isCompactElement_iff

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem List.Nodup.length_le_card {α : Type*} [Fintype α] {l : List α} (h : l.Nodup) :
    l.length ≤ Fintype.card α

Proof state:
α : Type u_4
inst✝ : Fintype α
l : List α
h : l.Nodup
⊢ l.length ≤ Fintype.card α

Tactic:
classical exact List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ

Result:
no goals

Proof state:
α : Type u_4
inst✝ : Fintype α
l : List α
h : l.Nodup
⊢ l.length ≤ Fintype.card α

Tactic:
exact List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
    m.keys.Pairwise (fun a b => (a == b) = false)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ List.Pairwise (fun a b => (a == b) = false) m.keys

Tactic:
simp_to_raw using Raw₀.distinct_keys ⟨m, h.size_buckets_pos⟩ h

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem isoRestrict_inv_ofRestrict : (isoRestrict f).inv ≫ f = Y.ofRestrict _

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (isoRestrict f).inv ≫ f = Y.ofRestrict ⋯

Tactic:
simp only [← isoRestrict_hom_ofRestrict f, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem moveRight_nim_hEq (o : Ordinal) :
    HEq (nim o).moveRight fun i : o.toType => nim ((enumIsoToType o).symm i)

Proof state:
o : Ordinal.{u_1}
⊢ HEq (mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)).moveRight
    fun i => nim ↑(o.enumIsoToType.symm i)

Tactic:
rfl

Result:
no goals

Proof state:
o : Ordinal.{u_1}
⊢ HEq (nim o).moveRight fun i => nim ↑(o.enumIsoToType.symm i)

Tactic:
rw [nim]

Result:
o : Ordinal.{u_1}
⊢ HEq (mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)).moveRight
    fun i => nim ↑(o.enumIsoToType.symm i)
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Bisect.lean
theorem avg_lt_right (h : a < b) : avg a b < b

Proof state:
case h
a b : Nat
h : a < b
⊢ a + b < 2 * b

Tactic:
omega

Result:
no goals

Proof state:
a b : Nat
h : a < b
⊢ a.avg b < b

Tactic:
apply Nat.div_lt_of_lt_mul

Result:
case h
a b : Nat
h : a < b
⊢ a + b < 2 * b
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem infsep_zero : s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ⊤

Tactic:
rw [infsep, ENNReal.toReal_eq_zero_iff]

Result:
no goals
-- Mathlib/NumberTheory/KummerDedekind.lean
theorem conductor_subset_adjoin : (conductor R x : Set S) ⊆ R<x> := fun y hy => by
  simpa only [mul_one] using hy 1

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S
hy : y ∈ ↑(conductor R x)
⊢ y ∈ ↑(adjoin R {x})

Tactic:
simpa only [mul_one] using hy 1

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem Metric.emetric_closedBall_nnreal {x : α} {ε : ℝ≥0} :
    EMetric.closedBall x ε = closedBall x ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ EMetric.closedBall x ↑ε = closedBall x ↑ε

Tactic:
rw [← Metric.emetric_closedBall ε.coe_nonneg, ENNReal.ofReal_coe_nnreal]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
lemma SupClosed.insert_upperBounds {s : Set α} {a : α} (hs : SupClosed s) (ha : a ∈ upperBounds s) :
    SupClosed (insert a s)

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
hs : SupClosed s
ha : a ∈ upperBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
hs : SupClosed s
ha : a ∈ upperBounds s
⊢ SupClosed (insert a s)

Tactic:
rw [SupClosed]

Result:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
hs : SupClosed s
ha : a ∈ upperBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_zero' : mgf X μ 0 = (μ Set.univ).toReal

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ mgf X μ 0 = (μ Set.univ).toReal

Tactic:
simp only [mgf, zero_mul, exp_zero, integral_const, smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
@[simp]
lemma localized'_bot : (⊥ : Submodule R M).localized' S p f = ⊥ :=
  SetLike.ext' (by apply SetLike.ext'_iff.mp <| Submodule.localized₀_bot p f)

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ ↑(localized' S p f ⊥) = ↑⊥

Tactic:
apply SetLike.ext'_iff.mp <| Submodule.localized₀_bot p f

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem IsBasis'.cardinalMk_eq_cRk (hIX : M.IsBasis' I X) : #I = M.cRk X

Proof state:
α : Type u
M : Matroid α
I X : Set α
inst✝ : M.InvariantCardinalRank
hIX : M.IsBasis' I X
⊢ #↑I = M.cRk X

Tactic:
rw [cRk, (isBase_restrict_iff'.2 hIX).cardinalMk_eq_cRank]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
lemma toSpec_preimage_basicOpen {f}
    (t : NumDenSameDeg 𝒜 (.powers f)) :
    (Opens.map (toSpec 𝒜 f).base).obj (sbo (HomogeneousLocalization.mk t)) =
      Opens.comap ⟨_, continuous_subtype_val⟩ (pbo t.num.1) :=
  Opens.ext <| Opens.map_coe _ _ ▸ by
  convert (ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen f t)
  exact funext fun _ => toSpec_base_apply_eq _ _

Proof state:
case h.e'_2.h.e'_3
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
t : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ⇑(ConcreteCategory.hom (toSpec 𝒜 f).base) = ProjIsoSpecTopComponent.ToSpec.toFun f

Tactic:
exact funext fun _ => toSpec_base_apply_eq _ _

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
t : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ⇑(ConcreteCategory.hom (toSpec 𝒜 f).base) ⁻¹' ↑(sbo HomogeneousLocalization.mk t) =
    ↑((Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (pbo ↑t.num))

Tactic:
convert (ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen f t)

Result:
case h.e'_2.h.e'_3
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
t : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ⇑(ConcreteCategory.hom (toSpec 𝒜 f).base) = ProjIsoSpecTopComponent.ToSpec.toFun f
-- Mathlib/Algebra/Group/Fin/Tuple.lean
@[simp] lemma sub_cons (v : Fin n.succ → α) (y : α) (w : Fin n → α) :
    v - vecCons y w = vecCons (vecHead v - y) (vecTail v - w)

Proof state:
α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
⊢ v - vecCons y w = vecCons (vecHead v - y) (vecTail v - w)

Tactic:
ext i

Result:
case h
α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v - vecCons y w) i = vecCons (vecHead v - y) (vecTail v - w) i

Proof state:
case h
α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v - vecCons y w) i = vecCons (vecHead v - y) (vecTail v - w) i

Tactic:
refine i.cases ?_ ?_ <;> simp [vecHead, vecTail]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
@[simp] lemma prod_eq_univ [Nonempty α] [Nonempty β] : s ×ˢ t = univ ↔ s = univ ∧ t = univ

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ s ×ˢ t = univ ↔ s = univ ∧ t = univ

Tactic:
simp [eq_univ_iff_forall, forall_and]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ideal.lean
lemma asIdeal_jacobson (I : TwoSidedIdeal R) : asIdeal I.jacobson = (asIdeal I).jacobson

Proof state:
R : Type u
inst✝ : Ring R
I : TwoSidedIdeal R
⊢ asIdeal I.jacobson = (asIdeal I).jacobson

Tactic:
ext

Result:
case h
R : Type u
inst✝ : Ring R
I : TwoSidedIdeal R
x✝ : R
⊢ x✝ ∈ asIdeal I.jacobson ↔ x✝ ∈ (asIdeal I).jacobson

Proof state:
case h
R : Type u
inst✝ : Ring R
I : TwoSidedIdeal R
x✝ : R
⊢ x✝ ∈ asIdeal I.jacobson ↔ x✝ ∈ (asIdeal I).jacobson

Tactic:
simp [jacobson]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Grothendieck.lean
lemma Hom.ext_iff (f g : a ⟶ b) :
    f = g ↔ ∃ (hfg : f.base = g.base), f.fiber = g.fiber ≫ eqToHom (hfg ▸ rfl) where
  mp hfg := ⟨by rw [hfg], by simp [hfg]⟩
  mpr := fun ⟨hfg₁, hfg₂⟩ => Hom.ext f g hfg₁ hfg₂

Proof state:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
f g : a ⟶ b
hfg : f = g
⊢ f.fiber = g.fiber ≫ eqToHom ⋯

Tactic:
simp [hfg]

Result:
no goals

Proof state:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
f g : a ⟶ b
hfg : f = g
⊢ f.base = g.base

Tactic:
rw [hfg]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem exists_lt_add_of_not_principal_add (ha : ¬ Principal (· + ·) a) :
    ∃ b < a, ∃ c < a, b + c = a

Proof state:
a : Ordinal.{u}
ha : ∃ a_1 < a, ∃ b < a, a ≤ a_1 + b
⊢ ∃ b < a, ∃ c < a, b + c = a

Tactic:
rcases ha with ⟨b, hb, c, hc, H⟩

Result:
case intro.intro.intro.intro
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ b + c
⊢ ∃ b < a, ∃ c < a, b + c = a

Proof state:
a : Ordinal.{u}
ha : ¬Principal (fun x1 x2 => x1 + x2) a
⊢ ∃ b < a, ∃ c < a, b + c = a

Tactic:
rw [not_principal_iff] at ha

Result:
a : Ordinal.{u}
ha : ∃ a_1 < a, ∃ b < a, a ≤ a_1 + b
⊢ ∃ b < a, ∃ c < a, b + c = a

Proof state:
case intro.intro.intro.intro
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ b + c
hab : a - b = a
⊢ False

Tactic:
rw [← sub_le, hab] at H

Result:
case intro.intro.intro.intro
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ c
hab : a - b = a
⊢ False

Proof state:
case intro.intro.intro.intro
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ b + c
⊢ ∃ b < a, ∃ c < a, b + c = a

Tactic:
refine
  ⟨b, hb, _, lt_of_le_of_ne (sub_le_self a b) fun hab => ?_, Ordinal.add_sub_cancel_of_le hb.le⟩

Result:
case intro.intro.intro.intro
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ b + c
hab : a - b = a
⊢ False

Proof state:
case intro.intro.intro.intro
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ c
hab : a - b = a
⊢ False

Tactic:
exact H.not_lt hc

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
lemma pentagon : tensorHom (associator X₁ X₂ X₃).hom (𝟙 X₄) ≫
    (associator X₁ (tensorObj X₂ X₃) X₄).hom ≫ tensorHom (𝟙 X₁) (associator X₂ X₃ X₄).hom =
    (associator (tensorObj X₁ X₂) X₃ X₄).hom ≫ (associator X₁ X₂ (tensorObj X₃ X₄)).hom

Proof state:
I : Type u
inst✝²⁵ : AddMonoid I
C : Type u_1
inst✝²⁴ : Category.{u_2, u_1} C
inst✝²³ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝²² : X₁.HasTensor X₂
inst✝²¹ : X₂.HasTensor X₃
inst✝²⁰ : X₃.HasTensor X₄
inst✝¹⁹ : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹⁸ : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹⁷ : (tensorObj X₂ X₃).HasTensor X₄
inst✝¹⁶ : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹⁵ : (tensorObj (tensorObj X₁ X₂) X₃).HasTensor X₄
inst✝¹⁴ : (tensorObj X₁ (tensorObj X₂ X₃)).HasTensor X₄
inst✝¹³ : X₁.HasTensor (tensorObj (tensorObj X₂ X₃) X₄)
inst✝¹² : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
inst✝¹¹ : (tensorObj X₁ X₂).HasTensor (tensorObj X₃ X₄)
inst✝¹⁰ : X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝⁹ : X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝⁸ : X₁.HasGoodTensor₁₂Tensor (tensorObj X₂ X₃) X₄
inst✝⁷ : X₁.HasGoodTensorTensor₂₃ (tensorObj X₂ X₃) X₄
inst✝⁶ : X₂.HasGoodTensor₁₂Tensor X₃ X₄
inst✝⁵ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
inst✝⁴ : (tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄
inst✝³ : (tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄
inst✝² : X₁.HasGoodTensor₁₂Tensor X₂ (tensorObj X₃ X₄)
inst✝¹ : X₁.HasGoodTensorTensor₂₃ X₂ (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor₄ObjExt X₂ X₃ X₄
⊢ tensorHom (associator X₁ X₂ X₃).hom (𝟙 X₄) ≫
      (associator X₁ (tensorObj X₂ X₃) X₄).hom ≫ tensorHom (𝟙 X₁) (associator X₂ X₃ X₄).hom =
    (associator (tensorObj X₁ X₂) X₃ X₄).hom ≫ (associator X₁ X₂ (tensorObj X₃ X₄)).hom

Tactic:
rw [← cancel_epi (associator (tensorObj X₁ X₂) X₃ X₄).inv,
  ← cancel_epi (associator X₁ X₂ (tensorObj X₃ X₄)).inv, Iso.inv_hom_id_assoc,
  Iso.inv_hom_id, ← pentagon_inv_assoc, ← tensor_comp_assoc, id_comp, Iso.inv_hom_id,
  tensor_id, id_comp, Iso.inv_hom_id_assoc, ← tensor_comp, id_comp, Iso.inv_hom_id,
  tensor_id]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma isDiameter_iff_ofDiameter_eq : s.IsDiameter p₁ p₂ ↔ .ofDiameter p₁ p₂ = s :=
  ⟨IsDiameter.ofDiameter_eq, by rintro rfl; exact isDiameter_ofDiameter _ _⟩

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ (Sphere.ofDiameter p₁ p₂).IsDiameter p₁ p₂

Tactic:
exact isDiameter_ofDiameter _ _

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
⊢ Sphere.ofDiameter p₁ p₂ = s → s.IsDiameter p₁ p₂

Tactic:
rintro rfl

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ (Sphere.ofDiameter p₁ p₂).IsDiameter p₁ p₂
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem hasLineDerivAt_smul_iff {c : 𝕜} (hc : c ≠ 0) :
    HasLineDerivAt 𝕜 f (c • f') x (c • v) ↔ HasLineDerivAt 𝕜 f f' x v :=
  ⟨fun h ↦ by simpa [smul_smul, inv_mul_cancel₀ hc] using h.smul (c ⁻¹), fun h ↦ h.smul c⟩

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
f' : F
c : 𝕜
hc : c ≠ 0
h : HasLineDerivAt 𝕜 f (c • f') x (c • v)
⊢ HasLineDerivAt 𝕜 f f' x v

Tactic:
simpa [smul_smul, inv_mul_cancel₀ hc] using h.smul (c ⁻¹)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem continuousWithinAt_iff' [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} :
    ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ x in 𝓝[s] b, dist (f x) (f b) < ε

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε

Tactic:
rw [ContinuousWithinAt, tendsto_nhds]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal
    (hf : HasFPowerSeriesOnBall f p x r) (hr : r' < r) :
    (fun y : E × E => f y.1 - f y.2 - p 1 fun _ => y.1 - y.2)
      =O[𝓟 (EMetric.ball (x, x) r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
hr : r' < r
⊢ (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
simpa using hf.isBigO_image_sub_image_sub_deriv_principal hr

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hr : r' < r
⊢ (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
hr : r' < r
⊢ (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
-- Mathlib/MeasureTheory/Measure/Trim.lean
theorem trim_eq_self [MeasurableSpace α] {μ : Measure α} : μ.trim le_rfl = μ

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
⊢ μ.trim ⋯ = μ

Tactic:
simp [Measure.trim]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem mirror_monomial (n : ℕ) (a : R) : (monomial n a).mirror = monomial n a

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : a = 0
⊢ ((monomial n) a).mirror = (monomial n) a

Tactic:
rw [ha, monomial_zero_right, mirror_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).mirror = (monomial n) a

Tactic:
by_cases ha : a = 0

Result:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : a = 0
⊢ ((monomial n) a).mirror = (monomial n) a

case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ ((monomial n) a).mirror = (monomial n) a

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ ((monomial n) a).mirror = (monomial n) a

Tactic:
rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
  C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
  mul_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.pre_eq (s : LimitCone (E ⋙ F)) (t : LimitCone F) :
    limit.pre F E = (limit.isoLimitCone t).hom ≫ s.isLimit.lift (t.cone.whisker E) ≫
      (limit.isoLimitCone s).inv

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
s : LimitCone (E ⋙ F)
t : LimitCone F
⊢ pre F E = (isoLimitCone t).hom ≫ s.isLimit.lift (Cone.whisker E t.cone) ≫ (isoLimitCone s).inv

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
lemma iSup₂_eq_top (f : ∀ i, κ i → α) : ⨆ i, ⨆ j, f i j = ⊤ ↔ ∀ b < ⊤, ∃ i j, b < f i j

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLinearOrder α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j = ⊤ ↔ ∀ b < ⊤, ∃ i j, b < f i j

Tactic:
simp_rw [iSup_psigma', iSup_eq_top, PSigma.exists]

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem l_biInf_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x}
    {p : ι → Prop} (f : ∀ (i) (_ : p i), β) : l (⨅ (i) (hi), u (f i hi)) = ⨅ (i) (hi), f i hi

Proof state:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → β
⊢ l (⨅ i, ⨅ (hi : p i), u (f i hi)) = ⨅ i, ⨅ (hi : p i), f i hi

Tactic:
simp only [iInf_subtype', gi.l_iInf_u]

Result:
no goals