harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Complement.lean
@[to_additive]
lemma isComplement_iff_existsUnique_inv_mul_mem :
    IsComplement S T ↔ ∀ g, ∃! s : S, (s : G)⁻¹ * g ∈ T

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S
hx : (↑x)⁻¹ * g ∈ T
hx' : ∀ (y : ↑S), (fun s => (↑s)⁻¹ * g ∈ T) y → y = x
⊢ ∀ (y : ↑S × ↑T), (fun x => ↑x.1 * ↑x.2 = g) y → y = (x, ⟨(↑x)⁻¹ * g, hx⟩)

Tactic:
aesop

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S
hx : (↑x)⁻¹ * g ∈ T
hx' : ∀ (y : ↑S), (fun s => (↑s)⁻¹ * g ∈ T) y → y = x
⊢ (fun x => ↑x.1 * ↑x.2 = g) (x, ⟨(↑x)⁻¹ * g, hx⟩)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.h.a
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! s, (↑s)⁻¹ * g ∈ T) ↔ ∃! x, ↑x.1 * ↑x.2 = g

Tactic:
constructor <;> rintro ⟨x, hx, hx'⟩

Result:
case h.e'_2.h.a.mp.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S
hx : (↑x)⁻¹ * g ∈ T
hx' : ∀ (y : ↑S), (fun s => (↑s)⁻¹ * g ∈ T) y → y = x
⊢ ∃! x, ↑x.1 * ↑x.2 = g

case h.e'_2.h.a.mpr.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S × ↑T
hx : ↑x.1 * ↑x.2 = g
hx' : ∀ (y : ↑S × ↑T), (fun x => ↑x.1 * ↑x.2 = g) y → y = x
⊢ ∃! s, (↑s)⁻¹ * g ∈ T

Proof state:
case h.e'_2.h.a.mp.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S
hx : (↑x)⁻¹ * g ∈ T
hx' : ∀ (y : ↑S), (fun s => (↑s)⁻¹ * g ∈ T) y → y = x
⊢ ∃! x, ↑x.1 * ↑x.2 = g

Tactic:
exact ⟨(x, ⟨_, hx⟩), by simp, by aesop⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S × ↑T
hx : ↑x.1 * ↑x.2 = g
hx' : ∀ (y : ↑S × ↑T), (fun x => ↑x.1 * ↑x.2 = g) y → y = x
⊢ (fun s => (↑s)⁻¹ * g ∈ T) x.1

Tactic:
simp [← hx]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S × ↑T
hx : ↑x.1 * ↑x.2 = g
hx' : ∀ (y : ↑S × ↑T), (fun x => ↑x.1 * ↑x.2 = g) y → y = x
y : ↑S
hy : (fun s => (↑s)⁻¹ * g ∈ T) y
⊢ ?m.65584 = ?m.65585

Tactic:
simpa using hx' (y, ⟨_, hy⟩)

Result:
no goals

Proof state:
case h.e'_2.h.a.mpr.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S × ↑T
hx : ↑x.1 * ↑x.2 = g
hx' : ∀ (y : ↑S × ↑T), (fun x => ↑x.1 * ↑x.2 = g) y → y = x
⊢ ∃! s, (↑s)⁻¹ * g ∈ T

Tactic:
exact ⟨x.1, by simp [← hx], fun y hy ↦ (Prod.ext_iff.1 <| by simpa using hx' (y, ⟨_, hy⟩)).1⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
⊢ IsComplement S T ↔ ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T

Tactic:
convert isComplement_iff_existsUnique with g

Result:
case h.e'_2.h.a
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! s, (↑s)⁻¹ * g ∈ T) ↔ ∃! x, ↑x.1 * ↑x.2 = g
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem uniformContinuous_restrict (h : s ∈ 𝔖) :
    UniformContinuous (UniformFun.ofFun ∘ (s.restrict : (α → β) → s → β) ∘ toFun 𝔖)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ map (fun x => ((⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) x.1, (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) x.2))
      (𝓤 (α →ᵤ[𝔖] β)) ≤
    𝓤 (↑s →ᵤ β)

Tactic:
simp only [UniformOnFun.uniformSpace, map_le_iff_le_comap, iInf_uniformity]

Result:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ ⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β) ≤
    comap
      (fun x => ((⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) x.1, (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) x.2))
      (𝓤 (↑s →ᵤ β))

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ ⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β) ≤
    comap
      (fun x => ((⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) x.1, (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) x.2))
      (𝓤 (↑s →ᵤ β))

Tactic:
exact iInf₂_le s h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ UniformContinuous (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖))

Tactic:
change _ ≤ _

Result:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ map (fun x => ((⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) x.1, (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) x.2))
      (𝓤 (α →ᵤ[𝔖] β)) ≤
    𝓤 (↑s →ᵤ β)
-- Mathlib/RingTheory/Ideal/Over.lean
theorem LiesOver.trans [𝔓.LiesOver P] [P.LiesOver p] : 𝔓.LiesOver p where
  over

Proof state:
A : Type u_2
inst✝⁸ : CommSemiring A
B : Type u_3
inst✝⁷ : CommSemiring B
C : Type u_4
inst✝⁶ : Semiring C
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra B C
inst✝³ : Algebra A C
inst✝² : IsScalarTower A B C
𝔓 : Ideal C
P : Ideal B
p : Ideal A
inst✝¹ : 𝔓.LiesOver P
inst✝ : P.LiesOver p
⊢ p = under A 𝔓

Tactic:
rw [P.over_def p, 𝔓.over_def P, under_under]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorRightHomEquiv_whiskerRight_comp_evaluation {X Y : C} [HasRightDual X] (f : Y ⟶ Xᘁ) :
    (tensorRightHomEquiv _ _ _ _) (f ▷ X ≫ ε_ X (Xᘁ)) = f ≫ (λ_ _).inv :=
  calc
    _ = 𝟙 _ ⊗≫ (Y ◁ η_ X Xᘁ ≫ f ▷ (X ⊗ Xᘁ)) ⊗≫ ε_ X Xᘁ ▷ Xᘁ

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ 𝟙 Y ⊗≫ (Y ◁ η_ X Xᘁ ≫ f ▷ (X ⊗ Xᘁ)) ⊗≫ ε_ X Xᘁ ▷ Xᘁ = f ⊗≫ Xᘁ ◁ η_ X Xᘁ ⊗≫ ε_ X Xᘁ ▷ Xᘁ

Tactic:
rw [whisker_exchange]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ 𝟙 Y ⊗≫ (f ▷ 𝟙_ C ≫ Xᘁ ◁ η_ X Xᘁ) ⊗≫ ε_ X Xᘁ ▷ Xᘁ = f ⊗≫ Xᘁ ◁ η_ X Xᘁ ⊗≫ ε_ X Xᘁ ▷ Xᘁ

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ (ρ_ Y).inv ≫ Y ◁ η_ X Xᘁ ≫ (α_ Y X Xᘁ).inv ≫ (f ▷ X ≫ ε_ X Xᘁ) ▷ Xᘁ =
    𝟙 Y ⊗≫ (Y ◁ η_ X Xᘁ ≫ f ▷ (X ⊗ Xᘁ)) ⊗≫ ε_ X Xᘁ ▷ Xᘁ

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ f ⊗≫ ⊗𝟙.hom = f ≫ (λ_ Xᘁ).inv

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ f ⊗≫ Xᘁ ◁ η_ X Xᘁ ⊗≫ ε_ X Xᘁ ▷ Xᘁ = f ≫ (λ_ Xᘁ).inv

Tactic:
rw [coevaluation_evaluation'']

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ f ⊗≫ ⊗𝟙.hom = f ≫ (λ_ Xᘁ).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ 𝟙 Y ⊗≫ (f ▷ 𝟙_ C ≫ Xᘁ ◁ η_ X Xᘁ) ⊗≫ ε_ X Xᘁ ▷ Xᘁ = f ⊗≫ Xᘁ ◁ η_ X Xᘁ ⊗≫ ε_ X Xᘁ ▷ Xᘁ

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ (tensorRightHomEquiv Y X Xᘁ (𝟙_ C)) (f ▷ X ≫ ε_ X Xᘁ) = 𝟙 Y ⊗≫ (Y ◁ η_ X Xᘁ ≫ f ▷ (X ⊗ Xᘁ)) ⊗≫ ε_ X Xᘁ ▷ Xᘁ

Tactic:
dsimp [tensorRightHomEquiv]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ (ρ_ Y).inv ≫ Y ◁ η_ X Xᘁ ≫ (α_ Y X Xᘁ).inv ≫ (f ▷ X ≫ ε_ X Xᘁ) ▷ Xᘁ =
    𝟙 Y ⊗≫ (Y ◁ η_ X Xᘁ ≫ f ▷ (X ⊗ Xᘁ)) ⊗≫ ε_ X Xᘁ ▷ Xᘁ
-- Mathlib/Data/Set/Finite/Basic.lean
/-- If a set `s` does not contain any triple of elements `x < y < z`, then `s` is finite. -/
lemma Set.finite_of_forall_not_lt_lt (h : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False) :
    Set.Finite s :=
  @Set.toFinite _ s <| Finite.of_forall_not_lt_lt <| by simpa only [SetCoe.forall'] using h

Proof state:
α : Type u
inst✝ : LinearOrder α
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False
⊢ ∀ ⦃x y z : ↑s⦄, x < y → y < z → False

Tactic:
simpa only [SetCoe.forall'] using h

Result:
no goals
-- Mathlib/Analysis/MellinTransform.lean
theorem MellinConvergent.div_const {f : ℝ → ℂ} {s : ℂ} (hf : MellinConvergent f s) (a : ℂ) :
    MellinConvergent (fun t => f t / a) s

Proof state:
f : ℝ → ℂ
s : ℂ
hf : MellinConvergent f s
a : ℂ
⊢ MellinConvergent (fun t => f t / a) s

Tactic:
simpa only [MellinConvergent, smul_eq_mul, ← mul_div_assoc] using hf.div_const a

Result:
no goals
-- Mathlib/Data/Finsupp/SMul.lean
theorem comapDomain_smul [AddMonoid M] [Monoid R] [DistribMulAction R M] {f : α → β} (r : R)
    (v : β →₀ M) (hfv : Set.InjOn f (f ⁻¹' ↑v.support))
    (hfrv : Set.InjOn f (f ⁻¹' ↑(r • v).support) :=
      hfv.mono <| Set.preimage_mono <| Finset.coe_subset.mpr support_smul) :
    comapDomain f (r • v) hfrv = r • comapDomain f v hfv

Proof state:
α : Type u_1
β : Type u_2
M : Type u_3
R : Type u_6
inst✝² : AddMonoid M
inst✝¹ : Monoid R
inst✝ : DistribMulAction R M
f : α → β
r : R
v : β →₀ M
hfv : Set.InjOn f (f ⁻¹' ↑v.support)
hfrv : optParam (Set.InjOn f (f ⁻¹' ↑(r • v).support)) ⋯
⊢ comapDomain f (r • v) hfrv = r • comapDomain f v hfv

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
M : Type u_3
R : Type u_6
inst✝² : AddMonoid M
inst✝¹ : Monoid R
inst✝ : DistribMulAction R M
f : α → β
r : R
v : β →₀ M
hfv : Set.InjOn f (f ⁻¹' ↑v.support)
hfrv : optParam (Set.InjOn f (f ⁻¹' ↑(r • v).support)) ⋯
a✝ : α
⊢ (comapDomain f (r • v) hfrv) a✝ = (r • comapDomain f v hfv) a✝

Proof state:
case h
α : Type u_1
β : Type u_2
M : Type u_3
R : Type u_6
inst✝² : AddMonoid M
inst✝¹ : Monoid R
inst✝ : DistribMulAction R M
f : α → β
r : R
v : β →₀ M
hfv : Set.InjOn f (f ⁻¹' ↑v.support)
hfrv : optParam (Set.InjOn f (f ⁻¹' ↑(r • v).support)) ⋯
a✝ : α
⊢ (comapDomain f (r • v) hfrv) a✝ = (r • comapDomain f v hfv) a✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma singleObjCyclesSelfIso_hom_naturality :
    cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom =
      (singleObjCyclesSelfIso c j A).hom ≫ f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j ≫ ((single C c j).obj B).iCycles j =
    ((singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjCyclesSelfIso c j B).inv) ≫ ((single C c j).obj B).iCycles j

Tactic:
simp only [cyclesMap_i, singleObjCyclesSelfIso, Iso.trans_hom, iCyclesIso_hom, Iso.trans_inv,
  assoc, iCyclesIso_inv_hom_id, comp_id, single_map_f_self]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom = (singleObjCyclesSelfIso c j A).hom ≫ f

Tactic:
rw [← cancel_mono (singleObjCyclesSelfIso c j B).inv, assoc, assoc, Iso.hom_inv_id, comp_id,
  ← cancel_mono (iCycles _ _)]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j ≫ ((single C c j).obj B).iCycles j =
    ((singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjCyclesSelfIso c j B).inv) ≫ ((single C c j).obj B).iCycles j
-- Mathlib/Order/Bounds/Image.lean
theorem BddAbove.image2 :
    BddAbove s → BddAbove t → BddAbove (image2 f s t)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddAbove s → BddAbove t → BddAbove (image2 f s t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Result:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (image2 f s t)

Proof state:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (image2 f s t)

Tactic:
exact ⟨f a b, mem_upperBounds_image2 h₀ h₁ ha hb⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffAt.comp_contDiffWithinAt_of_eq {y : F} (x : E) (hg : ContDiffAt 𝕜 n g y)
    (hf : ContDiffWithinAt 𝕜 n f s x) (hy : f x = y) : ContDiffWithinAt 𝕜 n (g ∘ f) s 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
s : Set E
f : E → F
g : F → G
n : WithTop ℕ∞
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffAt 𝕜 n g (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
exact hg.comp_contDiffWithinAt x hf

Result:
no goals

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
s : Set E
f : E → F
g : F → G
n : WithTop ℕ∞
y : F
x : E
hg : ContDiffAt 𝕜 n g y
hf : ContDiffWithinAt 𝕜 n f s x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
subst hy

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
s : Set E
f : E → F
g : F → G
n : WithTop ℕ∞
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffAt 𝕜 n g (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x
-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem isOpen_iff : IsOpen s ↔ ∀ o ∈ s, IsLimit o → ∃ a < o, Set.Ioo a o ⊆ s

Proof state:
case pos
s : Set Ordinal.{u}
o : Ordinal.{u}
ho : o ∈ s
ho' : o.IsLimit
a : Ordinal.{u}
ha : a < o
⊢ Set.Ioc a o ⊆ s ↔ Set.Ioo a o ⊆ s

Tactic:
simp only [← Set.Ioo_insert_right ha, Set.insert_subset_iff, ho, true_and]

Result:
no goals

Proof state:
s : Set Ordinal.{u}
o : Ordinal.{u}
ho : o ∈ s
⊢ s ∈ 𝓝 o ↔ o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s

Tactic:
by_cases ho' : IsLimit o

Result:
case pos
s : Set Ordinal.{u}
o : Ordinal.{u}
ho : o ∈ s
ho' : o.IsLimit
⊢ s ∈ 𝓝 o ↔ o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s

case neg
s : Set Ordinal.{u}
o : Ordinal.{u}
ho : o ∈ s
ho' : ¬o.IsLimit
⊢ s ∈ 𝓝 o ↔ o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s

Proof state:
case pos
s : Set Ordinal.{u}
o : Ordinal.{u}
ho : o ∈ s
ho' : o.IsLimit
⊢ s ∈ 𝓝 o ↔ o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s

Tactic:
simp only [(SuccOrder.hasBasis_nhds_Ioc_of_exists_lt ⟨0, ho'.pos⟩).mem_iff, ho', true_implies]

Result:
case pos
s : Set Ordinal.{u}
o : Ordinal.{u}
ho : o ∈ s
ho' : o.IsLimit
⊢ (∃ i < o, Set.Ioc i o ⊆ s) ↔ ∃ a < o, Set.Ioo a o ⊆ s

Proof state:
case neg
s : Set Ordinal.{u}
o : Ordinal.{u}
ho : o ∈ s
ho' : ¬o.IsLimit
⊢ s ∈ 𝓝 o ↔ o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s

Tactic:
simp [nhds_eq_pure.2 ho', ho, ho']

Result:
no goals

Proof state:
s : Set Ordinal.{u}
⊢ IsOpen s ↔ ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s

Tactic:
refine isOpen_iff_mem_nhds.trans <| forall₂_congr fun o ho => ?_

Result:
s : Set Ordinal.{u}
o : Ordinal.{u}
ho : o ∈ s
⊢ s ∈ 𝓝 o ↔ o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s

Proof state:
case pos
s : Set Ordinal.{u}
o : Ordinal.{u}
ho : o ∈ s
ho' : o.IsLimit
⊢ (∃ i < o, Set.Ioc i o ⊆ s) ↔ ∃ a < o, Set.Ioo a o ⊆ s

Tactic:
refine exists_congr fun a => and_congr_right fun ha => ?_

Result:
case pos
s : Set Ordinal.{u}
o : Ordinal.{u}
ho : o ∈ s
ho' : o.IsLimit
a : Ordinal.{u}
ha : a < o
⊢ Set.Ioc a o ⊆ s ↔ Set.Ioo a o ⊆ s
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_map_le {mβ : MeasurableSpace β} (f : β → ℝ≥0∞) {g : α → β} (hg : Measurable g) :
    ∫⁻ a, f a ∂Measure.map g μ ≤ ∫⁻ a, f (g a) ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
i : β → ℝ≥0∞
hi : Measurable i
h'i : i ≤ f
⊢ ∫⁻ (a : β), i a ∂Measure.map g μ ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ fun a => f (g a)), ∫⁻ (a : α), g_1 a ∂μ

Tactic:
refine le_iSup₂_of_le (i ∘ g) (hi.comp hg) ?_

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
i : β → ℝ≥0∞
hi : Measurable i
h'i : i ≤ f
⊢ ∫⁻ (a : β), i a ∂Measure.map g μ ≤ ⨆ (_ : i ∘ g ≤ fun a => f (g a)), ∫⁻ (a : α), (i ∘ g) a ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
⊢ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f), ∫⁻ (a : β), g_1 a ∂Measure.map g μ ≤
    ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ fun a => f (g a)), ∫⁻ (a : α), g_1 a ∂μ

Tactic:
refine iSup₂_le fun i hi => iSup_le fun h'i => ?_

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
i : β → ℝ≥0∞
hi : Measurable i
h'i : i ≤ f
⊢ ∫⁻ (a : β), i a ∂Measure.map g μ ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ fun a => f (g a)), ∫⁻ (a : α), g_1 a ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ

Tactic:
rw [← iSup_lintegral_measurable_le_eq_lintegral, ← iSup_lintegral_measurable_le_eq_lintegral]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
⊢ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f), ∫⁻ (a : β), g_1 a ∂Measure.map g μ ≤
    ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ fun a => f (g a)), ∫⁻ (a : α), g_1 a ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
i : β → ℝ≥0∞
hi : Measurable i
h'i : i ≤ f
⊢ ∫⁻ (a : β), i a ∂Measure.map g μ ≤ ⨆ (_ : i ∘ g ≤ fun a => f (g a)), ∫⁻ (a : α), (i ∘ g) a ∂μ

Tactic:
exact le_iSup_of_le (fun x => h'i (g x)) (le_of_eq (lintegral_map hi hg))

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
@[simp] lemma pair_zip_pair (a₁ a₂ : α) (b₁ b₂ : β) (ha hb) :
    (pair a₁ a₂ ha).zip (pair b₁ b₂ hb) = pair (a₁, b₁) (a₂, b₂) (Prod.le_def.2 ⟨ha, hb⟩)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ (pair a₁ a₂ ha).zip (pair b₁ b₂ hb) = pair (a₁, b₁) (a₂, b₂) ⋯

Tactic:
ext n : 2

Result:
case h.h
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n : ℕ
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) n = (pair (a₁, b₁) (a₂, b₂) ⋯) n

Proof state:
case h.h
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n : ℕ
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) n = (pair (a₁, b₁) (a₂, b₂) ⋯) n

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_zsmul_eq_zero_iff {θ : Angle} : (2 : ℤ) • θ = 0 ↔ θ = 0 ∨ θ = π

Proof state:
θ : Angle
⊢ 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
simp_rw [two_zsmul, ← two_nsmul, two_nsmul_eq_zero_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
@[simp]
lemma comp_mk₀_id {a : M} (f : ShiftedHom X Y a) (m₀ : M) (hm₀ : m₀ = 0) :
    f.comp (mk₀ m₀ hm₀ (𝟙 Y)) (by rw [hm₀, zero_add]) = f

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y : C
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
⊢ f.comp (mk₀ m₀ hm₀ (𝟙 Y)) ⋯ = f

Tactic:
simp [comp_mk₀]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁶ : Category.{?u.24148, u_1} C
D : Type u_2
inst✝⁵ : Category.{?u.24155, u_2} D
E : Type u_3
inst✝⁴ : Category.{?u.24162, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
⊢ m₀ + a = a

Tactic:
rw [hm₀, zero_add]

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem card_finMulAntidiag_pi (d n : ℕ) (hn : Squarefree n) :
    #(n.primeFactors.pi fun _ => (univ : Finset <| Fin d)) =
      #(finMulAntidiag d n)

Proof state:
d n : ℕ
hn : Squarefree n
⊢ #(n.primeFactors.pi fun x => univ) = #(d.finMulAntidiag n)

Tactic:
apply Finset.card_bij (Nat.primeFactorsPiBij d n) (primeFactorsPiBij_img d n hn)
  (primeFactorsPiBij_inj d n) (primeFactorsPiBij_surj d n hn)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_pow_le_of_le {a : WithBot ℕ} (b : ℕ) (hp : degree p ≤ a) :
    degree (p ^ b) ≤ b * a

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
a : WithBot ℕ
b : ℕ
hp : p.degree ≤ a
⊢ (p ^ b).degree ≤ ↑b * a

Tactic:
induction b with
| zero => simp [degree_one_le]
| succ n hn =>
    rw [Nat.cast_succ, add_mul, one_mul, pow_succ]
    exact degree_mul_le_of_le hn hp

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
a : WithBot ℕ
hp : p.degree ≤ a
⊢ (p ^ 0).degree ≤ ↑0 * a

Tactic:
simp [degree_one_le]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
a : WithBot ℕ
hp : p.degree ≤ a
n : ℕ
hn : (p ^ n).degree ≤ ↑n * a
⊢ (p ^ (n + 1)).degree ≤ ↑(n + 1) * a

Tactic:
rw [Nat.cast_succ, add_mul, one_mul, pow_succ]

Result:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
a : WithBot ℕ
hp : p.degree ≤ a
n : ℕ
hn : (p ^ n).degree ≤ ↑n * a
⊢ (p ^ n * p).degree ≤ ↑n * a + a

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
a : WithBot ℕ
hp : p.degree ≤ a
n : ℕ
hn : (p ^ n).degree ≤ ↑n * a
⊢ (p ^ n * p).degree ≤ ↑n * a + a

Tactic:
exact degree_mul_le_of_le hn hp

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem isLindelof_iff_isLindelof_univ : IsLindelof s ↔ IsLindelof (univ : Set s)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsLindelof s ↔ IsLindelof univ

Tactic:
rw [Subtype.isLindelof_iff, image_univ, Subtype.range_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem getElem_zipIdx (l : List α) (n) (i : Nat) (h : i < (l.zipIdx n).length) :
    (l.zipIdx n)[i] = (l[i]'(by simpa [length_zipIdx] using h), n + i)

Proof state:
α : Type u_1
l : List α
n i : Nat
h✝ : i < (l.zipIdx n).length
h : i < l.length
⊢ (Option.map (fun a => (a, n + i)) (some l[i])).get ⋯ = (l[i], n + i)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
n i : Nat
h✝ : i < (l.zipIdx n).length
h : i < l.length
⊢ (l.zipIdx n)[i]?.get ⋯ = (l[i], n + i)

Tactic:
simp only [getElem?_zipIdx, getElem?_eq_getElem h]

Result:
α : Type u_1
l : List α
n i : Nat
h✝ : i < (l.zipIdx n).length
h : i < l.length
⊢ (Option.map (fun a => (a, n + i)) (some l[i])).get ⋯ = (l[i], n + i)

Proof state:
α : Type u_1
l : List α
n i : Nat
h✝ : i < (l.zipIdx n).length
h : i < l.length
⊢ (l.zipIdx n)[i] = (l[i], n + i)

Tactic:
rw [getElem_eq_getElem?_get]

Result:
α : Type u_1
l : List α
n i : Nat
h✝ : i < (l.zipIdx n).length
h : i < l.length
⊢ (l.zipIdx n)[i]?.get ⋯ = (l[i], n + i)

Proof state:
α : Type ?u.22618
l : List α
n i : Nat
h : i < (l.zipIdx n).length
⊢ i < l.length

Tactic:
simpa [length_zipIdx] using h

Result:
no goals

Proof state:
α : Type u_1
l : List α
n i : Nat
h : i < (l.zipIdx n).length
⊢ (l.zipIdx n)[i] = (l[i], n + i)

Tactic:
simp only [length_zipIdx] at h

Result:
α : Type u_1
l : List α
n i : Nat
h✝ : i < (l.zipIdx n).length
h : i < l.length
⊢ (l.zipIdx n)[i] = (l[i], n + i)
-- Mathlib/CategoryTheory/Abelian/Opposite.lean
theorem imageUnopOp_hom_comp_image_ι :
    (imageUnopOp g).hom ≫ image.ι g = (factorThruImage g.unop).op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ (imageUnopOp g).hom ≫ image.ι g = (factorThruImage g.unop).op

Tactic:
simp only [← cancel_epi (image.ι g.unop).op, ← Category.assoc, image_ι_op_comp_imageUnopOp_hom,
  ← op_comp, image.fac, Quiver.Hom.op_unop]

Result:
no goals