harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma real_iff [Algebra ℂ A] {a : A} :
    SpectrumRestricts a Complex.reCLM ↔ ∀ x ∈ spectrum ℂ a, x = x.re

Proof state:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℂ A
a : A
⊢ SpectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ spectrum ℂ a, x = ↑x.re

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℂ A
a : A
h : SpectrumRestricts a ⇑Complex.reCLM
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ x = ↑x.re

case refine_2
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℂ A
a : A
h : ∀ x ∈ spectrum ℂ a, x = ↑x.re
⊢ SpectrumRestricts a ⇑Complex.reCLM

Proof state:
case refine_1.intro.intro
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℂ A
a : A
h : SpectrumRestricts a ⇑Complex.reCLM
x : ℝ
hx : (algebraMap ℝ ℂ) x ∈ spectrum ℂ a
⊢ (algebraMap ℝ ℂ) x = ↑((algebraMap ℝ ℂ) x).re

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℂ A
a : A
h : ∀ x ∈ spectrum ℂ a, x = ↑x.re
⊢ SpectrumRestricts a ⇑Complex.reCLM

Tactic:
exact .of_subset_range_algebraMap Complex.ofReal_re fun x hx ↦ ⟨x.re, (h x hx).symm⟩

Result:
no goals

Proof state:
case refine_1
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℂ A
a : A
h : SpectrumRestricts a ⇑Complex.reCLM
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ x = ↑x.re

Tactic:
obtain ⟨x, -, rfl⟩ := h.algebraMap_image.symm ▸ hx

Result:
case refine_1.intro.intro
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℂ A
a : A
h : SpectrumRestricts a ⇑Complex.reCLM
x : ℝ
hx : (algebraMap ℝ ℂ) x ∈ spectrum ℂ a
⊢ (algebraMap ℝ ℂ) x = ↑((algebraMap ℝ ℂ) x).re
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[reassoc]
lemma mapHomologyIso'_hom_naturality [S₁.HasHomology] [S₂.HasHomology]
    [(S₁.map F).HasHomology] [(S₂.map F).HasHomology]
    [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
    @homologyMap _ _ _ (S₁.map F) (S₂.map F) (F.mapShortComplex.map φ) _ _ ≫
      (S₂.mapHomologyIso' F).hom = (S₁.mapHomologyIso' F).hom ≫ F.map (homologyMap φ)

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} C
inst✝⁹ : Category.{u_4, u_2} D
inst✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫
      (S₂.homologyData.right.map F).homologyIso.hom ≫ F.map S₂.homologyData.right.homologyIso.inv =
    ((S₁.homologyData.right.map F).homologyIso.hom ≫ F.map S₁.homologyData.right.homologyIso.inv) ≫
      F.map (homologyMap φ)

Tactic:
simp only [← RightHomologyData.rightHomologyIso_hom_naturality_assoc _
  ((homologyData S₁).right.map F) ((homologyData S₂).right.map F), assoc,
  ← RightHomologyData.map_rightHomologyMap', ← F.map_comp,
  RightHomologyData.rightHomologyIso_inv_naturality _
    (homologyData S₁).right (homologyData S₂).right]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} C
inst✝⁹ : Category.{u_4, u_2} D
inst✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapHomologyIso' F).hom =
    (S₁.mapHomologyIso' F).hom ≫ F.map (homologyMap φ)

Tactic:
dsimp only [Iso.trans, Iso.symm, Functor.mapIso, mapHomologyIso']

Result:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} C
inst✝⁹ : Category.{u_4, u_2} D
inst✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫
      (S₂.homologyData.right.map F).homologyIso.hom ≫ F.map S₂.homologyData.right.homologyIso.inv =
    ((S₁.homologyData.right.map F).homologyIso.hom ≫ F.map S₁.homologyData.right.homologyIso.inv) ≫
      F.map (homologyMap φ)
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin :
    ‖iteratedFDerivWithin 𝕜 n f s x‖ = ‖iteratedDerivWithin n f s x‖

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ ‖iteratedFDerivWithin 𝕜 n f s x‖ = ‖iteratedDerivWithin n f s x‖

Tactic:
rw [iteratedDerivWithin_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_compl : x \ yᶜ = x ⊓ y

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x \ yᶜ = x ⊓ y

Tactic:
rw [sdiff_eq, compl_compl]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem add_tsub_add_le_tsub_add_tsub : a + b - (c + d) ≤ a - c + (b - d)

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + b - d - c ≤ a - c + (b - d)

Tactic:
refine (tsub_le_tsub_right add_tsub_le_assoc c).trans ?_

Result:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + (b - d) - c ≤ a - c + (b - d)

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + (b - d) - c ≤ a - c + (b - d)

Tactic:
rw [add_comm a, add_comm (a - c)]

Result:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ b - d + a - c ≤ b - d + (a - c)

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ b - d + a - c ≤ b - d + (a - c)

Tactic:
exact add_tsub_le_assoc

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + b - (c + d) ≤ a - c + (b - d)

Tactic:
rw [add_comm c, tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]

Result:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + b - d - c ≤ a - c + (b - d)
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem nonUnitalSubsemiringClosure_eq_closure :
    M.nonUnitalSubsemiringClosure = NonUnitalSubsemiring.closure (M : Set R)

Proof state:
case h.refine_1.intro.intro
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ M.nonUnitalSubsemiringClosure
H1 : NonUnitalSubsemiring R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ x✝ ∈ (fun h => ↑H1) H2

Tactic:
exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2

Result:
no goals

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
⊢ M.nonUnitalSubsemiringClosure = NonUnitalSubsemiring.closure ↑M

Tactic:
ext

Result:
case h
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
⊢ x✝ ∈ M.nonUnitalSubsemiringClosure ↔ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Proof state:
case h
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
⊢ x✝ ∈ M.nonUnitalSubsemiringClosure ↔ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
refine ⟨fun hx => ?_,
  fun hx => (NonUnitalSubsemiring.mem_closure.mp hx) M.nonUnitalSubsemiringClosure fun s sM => ?_⟩
<;> rintro - ⟨H1, rfl⟩
<;> rintro - ⟨H2, rfl⟩

Result:
case h.refine_1.intro.intro
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ M.nonUnitalSubsemiringClosure
H1 : NonUnitalSubsemiring R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ x✝ ∈ (fun h => ↑H1) H2

case h.refine_2.intro.intro
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h => ↑H1) H2

Proof state:
case h.refine_2.intro.intro
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h => ↑H1) H2

Tactic:
exact H2 sM

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
lemma basicOpenToSpec_app_top :
    (basicOpenToSpec 𝒜 f).app ⊤ = (Scheme.ΓSpecIso _).hom ≫ awayToSection 𝒜 f ≫
      (basicOpen 𝒜 f).topIso.inv

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
⊢ Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤ =
    (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).hom ≫ awayToSection 𝒜 f ≫ (basicOpen 𝒜 f).topIso.inv

Tactic:
rw [basicOpenToSpec]

Result:
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
⊢ Scheme.Hom.app ((basicOpen 𝒜 f).toSpecΓ ≫ Spec.map (awayToSection 𝒜 f)) ⊤ =
    (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).hom ≫ awayToSection 𝒜 f ≫ (basicOpen 𝒜 f).topIso.inv

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
⊢ Scheme.Hom.app (Spec.map (awayToSection 𝒜 f)) ⊤ ≫ Scheme.Hom.app (basicOpen 𝒜 f).toSpecΓ ⊤ =
    (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).hom ≫ awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (eqToHom ⋯)

Tactic:
erw [Scheme.comp_app]

Result:
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
⊢ Scheme.Hom.app (Spec.map (awayToSection 𝒜 f)) ⊤ ≫
      Scheme.Hom.app (Spec.map (basicOpen 𝒜 f).topIso.inv) ⊤ ≫
        Scheme.Hom.app (↑(basicOpen 𝒜 f)).toSpecΓ (Spec.map (basicOpen 𝒜 f).topIso.inv ⁻¹ᵁ ⊤) =
    (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).hom ≫ awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (eqToHom ⋯)

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
⊢ Scheme.Hom.app ((basicOpen 𝒜 f).toSpecΓ ≫ Spec.map (awayToSection 𝒜 f)) ⊤ =
    (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).hom ≫ awayToSection 𝒜 f ≫ (basicOpen 𝒜 f).topIso.inv

Tactic:
simp only [Scheme.comp_coeBase, TopologicalSpace.Opens.map_comp_obj,
  TopologicalSpace.Opens.map_top, Scheme.comp_app, Scheme.Opens.topIso_inv, eqToHom_op]

Result:
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
⊢ Scheme.Hom.app (Spec.map (awayToSection 𝒜 f)) ⊤ ≫ Scheme.Hom.app (basicOpen 𝒜 f).toSpecΓ ⊤ =
    (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).hom ≫ awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (eqToHom ⋯)

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
⊢ Scheme.Hom.app (Spec.map (awayToSection 𝒜 f)) ⊤ ≫
      Scheme.Hom.app (Spec.map (basicOpen 𝒜 f).topIso.inv) ⊤ ≫
        Scheme.Hom.app (↑(basicOpen 𝒜 f)).toSpecΓ (Spec.map (basicOpen 𝒜 f).topIso.inv ⁻¹ᵁ ⊤) =
    (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).hom ≫ awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (eqToHom ⋯)

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Function/ULift.lean
theorem PLift.down_inj {a b : PLift α} : a.down = b.down ↔ a = b :=
  ⟨fun h ↦ PLift.down_injective h, fun h ↦ by rw [h]⟩

Proof state:
α : Sort u_1
a b : PLift α
h : a = b
⊢ a.down = b.down

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Topology/LocallyConstant/Basic.lean
theorem apply_eq_of_isPreconnected {f : X → Y} (hf : IsLocallyConstant f) {s : Set X}
    (hs : IsPreconnected s) {x y : X} (hx : x ∈ s) (hy : y ∈ s) : f x = f y

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y

Tactic:
let U := f ⁻¹' {f y}

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ f x = f y

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
hs : (s ∩ (U ∩ Uᶜ)).Nonempty
⊢ False

Tactic:
simp only [inter_empty, Set.not_nonempty_empty, inter_compl_self] at hs

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ f x = f y

Tactic:
suffices x ∉ Uᶜ from Classical.not_not.1 this

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ x ∉ Uᶜ

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
⊢ s ⊆ U ∪ Uᶜ

Tactic:
simp only [union_compl_self, subset_univ]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
⊢ False

Tactic:
specialize hs U Uᶜ (hf {f y}) (hf {f y}ᶜ) _ ⟨y, ⟨hy, rfl⟩⟩ ⟨x, ⟨hx, hxV⟩⟩

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
⊢ s ⊆ U ∪ Uᶜ

X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
hs : (s ∩ (U ∩ Uᶜ)).Nonempty
⊢ False

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ x ∉ Uᶜ

Tactic:
intro hxV

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
⊢ False
-- Mathlib/Data/Nat/ModEq.lean
theorem le_of_lt_add (h1 : a ≡ b [MOD m]) (h2 : a < b + m) : a ≤ b :=
  (le_total a b).elim id fun h3 =>
    Nat.le_of_sub_eq_zero
      (eq_zero_of_dvd_of_lt ((modEq_iff_dvd' h3).mp h1.symm) (by omega))

Proof state:
m a b : ℕ
h1 : a ≡ b [MOD m]
h2 : a < b + m
h3 : b ≤ a
⊢ a - b < m

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem contDiff_rpow_const_of_le {p : ℝ} {n : ℕ} (h : ↑n ≤ p) :
    ContDiff ℝ n fun x : ℝ => x ^ p

Proof state:
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(n + 1) ≤ p
⊢ 1 ≤ ↑(n + 1)

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ ContDiff ℝ ↑(n + 1) fun x => x ^ p

Tactic:
rw [show ((n + 1 : ℕ) : WithTop ℕ∞) = n + 1 from rfl,
  contDiff_succ_iff_deriv, deriv_rpow_const' h1]

Result:
case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ fun x => x ^ p) ∧
    (↑n = ⊤ → AnalyticOn ℝ (fun x => x ^ p) Set.univ) ∧ ContDiff ℝ ↑n fun x => p * x ^ (p - 1)

Proof state:
p : ℝ
h : ↑0 ≤ p
x : ℝ
⊢ 0 ≤ p

Tactic:
simpa using h

Result:
no goals

Proof state:
case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ fun x => x ^ p) ∧ ContDiff ℝ ↑n fun x => p * x ^ (p - 1)

Tactic:
exact ⟨differentiable_rpow_const h1, contDiff_const.mul (ihn h)⟩

Result:
no goals

Proof state:
case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ fun x => x ^ p) ∧
    (↑n = ⊤ → AnalyticOn ℝ (fun x => x ^ p) Set.univ) ∧ ContDiff ℝ ↑n fun x => p * x ^ (p - 1)

Tactic:
simp only [WithTop.natCast_ne_top, analyticOn_univ, IsEmpty.forall_iff, true_and]

Result:
case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ fun x => x ^ p) ∧ ContDiff ℝ ↑n fun x => p * x ^ (p - 1)

Proof state:
case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(n + 1) ≤ p
h1 : 1 ≤ p
⊢ ContDiff ℝ ↑(n + 1) fun x => x ^ p

Tactic:
rw [Nat.cast_succ, ← le_sub_iff_add_le] at h

Result:
case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ ContDiff ℝ ↑(n + 1) fun x => x ^ p

Proof state:
case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(n + 1) ≤ p
⊢ ContDiff ℝ ↑(n + 1) fun x => x ^ p

Tactic:
have h1 : 1 ≤ p := le_trans (by simp) h

Result:
case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(n + 1) ≤ p
h1 : 1 ≤ p
⊢ ContDiff ℝ ↑(n + 1) fun x => x ^ p

Proof state:
case zero
p : ℝ
h : ↑0 ≤ p
⊢ ContDiff ℝ ↑0 fun x => x ^ p

Tactic:
exact contDiff_zero.2 (continuous_id.rpow_const fun x => Or.inr <| by simpa using h)

Result:
no goals

Proof state:
p : ℝ
n : ℕ
h : ↑n ≤ p
⊢ ContDiff ℝ ↑n fun x => x ^ p

Tactic:
induction' n with n ihn generalizing p

Result:
case zero
p : ℝ
h : ↑0 ≤ p
⊢ ContDiff ℝ ↑0 fun x => x ^ p

case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(n + 1) ≤ p
⊢ ContDiff ℝ ↑(n + 1) fun x => x ^ p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Basic.lean
theorem shrink_eq_take (v : Vector α n) (m : Nat) : v.shrink m = v.take m

Proof state:
α : Type u_1
n : Nat
v : Vector α n
m : Nat
⊢ v.shrink m = v.take m

Tactic:
simp [shrink, take]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem sum_cycleType (σ : Perm α) : σ.cycleType.sum = σ.support.card

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.cycleType.sum = σ.support.card

Tactic:
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => rw [hσ.cycleType, sum_coe, List.sum_singleton]
| induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType, sum_add, hσ, hτ, hd.card_support_mul]

Result:
no goals

Proof state:
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : σ.cycleType.sum = σ.support.card
hτ : τ.cycleType.sum = τ.support.card
⊢ (σ * τ).cycleType.sum = (σ * τ).support.card

Tactic:
rw [hd.cycleType, sum_add, hσ, hτ, hd.card_support_mul]

Result:
no goals

Proof state:
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ (cycleType 1).sum = (support 1).card

Tactic:
simp

Result:
no goals

Proof state:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
⊢ σ.cycleType.sum = σ.support.card

Tactic:
rw [hσ.cycleType, sum_coe, List.sum_singleton]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Differentials.lean
lemma hom₁_single (r : pres.rels) :
    hom₁ pres (Finsupp.single r 1) = Extension.Cotangent.mk ⟨pres.relation r, by simp⟩

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
⊢ (hom₁ pres) (Finsupp.single r 1) = Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩

Tactic:
simp [hom₁]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
⊢ pres.relation r ∈ pres.toExtension.ker

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousOn_finite [Finite ι] {F : ι → X → α} {S : Set X} :
    EquicontinuousOn F S ↔ ∀ i, ContinuousOn (F i) S

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst✝ : Finite ι
F : ι → X → α
S : Set X
⊢ EquicontinuousOn F S ↔ ∀ (i : ι), ContinuousOn (F i) S

Tactic:
simp only [EquicontinuousOn, equicontinuousWithinAt_finite, ContinuousOn, @forall_swap ι]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem map_zero (f : α → β) : (0 : VectorMeasure α M).map f = 0

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
f : α → β
hf : Measurable f
⊢ map 0 f = 0

Tactic:
ext i hi

Result:
case pos.h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ ↑(map 0 f) i = ↑0 i

Proof state:
case pos.h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ ↑(map 0 f) i = ↑0 i

Tactic:
rw [map_apply _ hf hi, zero_apply, zero_apply]

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
f : α → β
hf : ¬Measurable f
⊢ map 0 f = 0

Tactic:
exact dif_neg hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
f : α → β
⊢ map 0 f = 0

Tactic:
by_cases hf : Measurable f

Result:
case pos
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
f : α → β
hf : Measurable f
⊢ map 0 f = 0

case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
f : α → β
hf : ¬Measurable f
⊢ map 0 f = 0
-- Mathlib/Data/Nat/Choose/Mul.lean
theorem choose_mul_right {m n : ℕ} (hn : n ≠ 0) :
    (m * n).choose n = m * (m * n - 1).choose (n - 1)

Proof state:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
have hp : m = p + 1 := (succ_pred_eq_of_ne_zero hm).symm

Result:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Proof state:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
simp only [hm, zero_mul, choose_eq_zero_iff]

Result:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ 0 < n

Proof state:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
simp only [hp]

Result:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
⊢ ((p + 1) * n).choose n = (p + 1) * ((p + 1) * n - 1).choose (n - 1)

Proof state:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ 0 < n

Tactic:
exact Nat.pos_of_ne_zero hn

Result:
no goals

Proof state:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
⊢ ((p + 1) * n).choose n = (p + 1) * ((p + 1) * n - 1).choose (n - 1)

Tactic:
rw [add_mul, one_mul, choose_mul_add hn]

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
by_cases hm : m = 0

Result:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Proof state:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
set p := m - 1

Result:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)