harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Oscillation.lean
theorem uniform_oscillationWithin (comp : IsCompact K) (hK : ∀ x ∈ K, oscillationWithin f D x < ε) :
    ∃ δ > 0, ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε

Proof state:
case right.intro
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : T.Nonempty
x : E
hx : x ∈ K
r : ℝ
hr : x ∈ ⋃ (_ : r ∈ T), S r
⊢ x ∈ S (⋯.min T_nonempty)

Tactic:
simp only [mem_iUnion, exists_prop] at hr

Result:
case right.intro
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : T.Nonempty
x : E
hx : x ∈ K
r : ℝ
hr : r ∈ T ∧ x ∈ S r
⊢ x ∈ S (⋯.min T_nonempty)
-- Mathlib/Topology/LocallyFinite.lean
theorem nhdsWithin_iUnion (hf : LocallyFinite f) (a : X) :
    𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : {i | (f i ∩ U).Nonempty}.Finite
⊢ 𝓝[⋃ i, f i ∩ U] a = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, f i ∩ U] a

Tactic:
simp only [mem_setOf_eq, iUnion_nonempty_self]

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
⊢ 𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a

Tactic:
rcases hf a with ⟨U, haU, hfin⟩

Result:
case intro.intro
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : {i | (f i ∩ U).Nonempty}.Finite
⊢ 𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a

Proof state:
case intro.intro
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : {i | (f i ∩ U).Nonempty}.Finite
⊢ 𝓝[⋃ i, f i] a ≤ ⨆ i, 𝓝[f i] a

Tactic:
calc
  𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a := by
    rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
  _ = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, (f i ∩ U)] a := by
    simp only [mem_setOf_eq, iUnion_nonempty_self]
  _ = ⨆ i ∈ {j | (f j ∩ U).Nonempty}, 𝓝[f i ∩ U] a := nhdsWithin_biUnion hfin _ _
  _ ≤ ⨆ i, 𝓝[f i ∩ U] a := iSup₂_le_iSup _ _
  _ ≤ ⨆ i, 𝓝[f i] a := iSup_mono fun i ↦ nhdsWithin_mono _ inter_subset_left

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : {i | (f i ∩ U).Nonempty}.Finite
⊢ 𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a

Tactic:
rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]

Result:
no goals

Proof state:
case intro.intro
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : {i | (f i ∩ U).Nonempty}.Finite
⊢ 𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a

Tactic:
refine le_antisymm ?_ (Monotone.le_map_iSup fun _ _ ↦ nhdsWithin_mono _)

Result:
case intro.intro
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : {i | (f i ∩ U).Nonempty}.Finite
⊢ 𝓝[⋃ i, f i] a ≤ ⨆ i, 𝓝[f i] a
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma deriv2_mul_log (x : ℝ) : deriv^[2] (fun x ↦ x * log x) x = x⁻¹

Proof state:
x : ℝ
hx : ¬x = 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun x => x * log x) y = log y + 1
⊢ deriv (deriv fun x => x * log x) x = x⁻¹

Tactic:
refine (Filter.EventuallyEq.deriv_eq this).trans ?_

Result:
x : ℝ
hx : ¬x = 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun x => x * log x) y = log y + 1
⊢ deriv (fun x => log x + 1) x = x⁻¹

Proof state:
case neg
x : ℝ
hx : ¬x = 0
⊢ deriv (deriv fun x => x * log x) x = x⁻¹

Tactic:
suffices ∀ᶠ y in (𝓝 x), deriv (fun x ↦ x * log x) y = log y + 1 by
  refine (Filter.EventuallyEq.deriv_eq this).trans ?_
  rw [deriv_add_const, deriv_log x]

Result:
case neg
x : ℝ
hx : ¬x = 0
⊢ ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun x => x * log x) y = log y + 1

Proof state:
x : ℝ
hx : ¬x = 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun x => x * log x) y = log y + 1
⊢ deriv (fun x => log x + 1) x = x⁻¹

Tactic:
rw [deriv_add_const, deriv_log x]

Result:
no goals

Proof state:
x : ℝ
⊢ deriv (deriv fun x => x * log x) x = x⁻¹

Tactic:
by_cases hx : x = 0

Result:
case pos
x : ℝ
hx : x = 0
⊢ deriv (deriv fun x => x * log x) x = x⁻¹

case neg
x : ℝ
hx : ¬x = 0
⊢ deriv (deriv fun x => x * log x) x = x⁻¹

Proof state:
x : ℝ
⊢ deriv^[2] (fun x => x * log x) x = x⁻¹

Tactic:
simp only [Function.iterate_succ, Function.iterate_zero, Function.id_comp, Function.comp_apply]

Result:
x : ℝ
⊢ deriv (deriv fun x => x * log x) x = x⁻¹

Proof state:
case neg
x : ℝ
hx : ¬x = 0
⊢ ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun x => x * log x) y = log y + 1

Tactic:
filter_upwards [eventually_ne_nhds hx] with y hy using deriv_mul_log hy

Result:
no goals

Proof state:
case pos
x : ℝ
hx : x = 0
⊢ deriv (deriv fun x => x * log x) x = x⁻¹

Tactic:
rw [hx, inv_zero]

Result:
case pos
x : ℝ
hx : x = 0
⊢ deriv (deriv fun x => x * log x) 0 = 0

Proof state:
case pos
x : ℝ
hx : x = 0
⊢ deriv (deriv fun x => x * log x) 0 = 0

Tactic:
exact deriv_zero_of_not_differentiableAt
  (fun h ↦ not_continuousAt_deriv_mul_log_zero h.continuousAt)

Result:
no goals
-- Mathlib/RingTheory/Artinian/Module.lean
@[stacks 00J7]
lemma setOf_isMaximal_finite : {I : Ideal R | I.IsMaximal}.Finite

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsArtinianRing R
s : Finset { I // I.IsMaximal }
H : ∀ (a : { I // I.IsMaximal }), s.inf Subtype.val ≤ ↑a
p : ↑{I | I.IsMaximal}
q : { I // I.IsMaximal }
hq1 : q ∈ s
hq2 : ↑q ≤ ↑p
⊢ p ∈ s

Tactic:
rwa [← Subtype.ext <| q.2.eq_of_le p.2.ne_top hq2]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsArtinianRing R
⊢ {I | I.IsMaximal}.Finite

Tactic:
have ⟨s, H⟩ := Finset.exists_inf_le (Subtype.val (p := fun I : Ideal R ↦ I.IsMaximal))

Result:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsArtinianRing R
s : Finset { I // I.IsMaximal }
H : ∀ (a : { I // I.IsMaximal }), s.inf Subtype.val ≤ ↑a
⊢ {I | I.IsMaximal}.Finite

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsArtinianRing R
s : Finset { I // I.IsMaximal }
H : ∀ (a : { I // I.IsMaximal }), s.inf Subtype.val ≤ ↑a
⊢ {I | I.IsMaximal}.Finite

Tactic:
refine Set.finite_def.2 ⟨s, fun p ↦ ?_⟩

Result:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsArtinianRing R
s : Finset { I // I.IsMaximal }
H : ∀ (a : { I // I.IsMaximal }), s.inf Subtype.val ≤ ↑a
p : ↑{I | I.IsMaximal}
⊢ p ∈ s

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsArtinianRing R
s : Finset { I // I.IsMaximal }
H : ∀ (a : { I // I.IsMaximal }), s.inf Subtype.val ≤ ↑a
p : ↑{I | I.IsMaximal}
⊢ p ∈ s

Tactic:
have ⟨q, hq1, hq2⟩ := p.2.isPrime.inf_le'.mp (H p)

Result:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsArtinianRing R
s : Finset { I // I.IsMaximal }
H : ∀ (a : { I // I.IsMaximal }), s.inf Subtype.val ≤ ↑a
p : ↑{I | I.IsMaximal}
q : { I // I.IsMaximal }
hq1 : q ∈ s
hq2 : ↑q ≤ ↑p
⊢ p ∈ s
-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem isMaximal_of_toPiLocalization_surjective (surj : Function.Surjective (toPiLocalization R))
    (I : PrimeSpectrum R) : I.1.IsMaximal

Proof state:
case intro.h
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI : 1 = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ I ≠ { asIdeal := J, isPrime := ⋯ }

Tactic:
intro eq

Result:
case intro.h
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI : 1 = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
eq : I = { asIdeal := J, isPrime := ⋯ }
⊢ False

Proof state:
case intro
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
⊢ False

Tactic:
have hJ : algebraMap _ _ r = _ := (congr_fun hr _).trans (Function.update_self ..)

Result:
case intro
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
⊢ False
-- Mathlib/Data/Set/Lattice.lean
theorem nonempty_biUnion {t : Set α} {s : α → Set β} :
    (⋃ i ∈ t, s i).Nonempty ↔ ∃ i ∈ t, (s i).Nonempty

Proof state:
α : Type u_1
β : Type u_2
t : Set α
s : α → Set β
⊢ (⋃ i ∈ t, s i).Nonempty ↔ ∃ i ∈ t, (s i).Nonempty

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsUniversalColimit.whiskerEquivalence_iff {K : Type*} [Category K] (e : J ≌ K)
    {F : K ⥤ C} {c : Cocone F} :
    IsUniversalColimit (c.whisker e.functor) ↔ IsUniversalColimit c :=
  ⟨fun hc ↦ ((hc.whiskerEquivalence e.symm).precompose_isIso (e.invFunIdAssoc F).inv).of_iso
      (Cocones.ext (Iso.refl _) (by simp)), IsUniversalColimit.whiskerEquivalence e⟩

Proof state:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit (Cocone.whisker e.functor c)
⊢ ∀ (j : K),
    ((Cocones.precompose (e.invFunIdAssoc F).inv).obj
                (Cocone.whisker e.symm.functor (Cocone.whisker e.functor c))).ι.app
          j ≫
        (Iso.refl
            ((Cocones.precompose (e.invFunIdAssoc F).inv).obj
                (Cocone.whisker e.symm.functor (Cocone.whisker e.functor c))).pt).hom =
      c.ι.app j

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem balance1_All {l : RBNode α} {v : α} {r : RBNode α} :
    (balance1 l v r).All p ↔ p v ∧ l.All p ∧ r.All p

Proof state:
α : Type u_1
p : α → Prop
l : RBNode α
v : α
r : RBNode α
⊢ All p
      (match l, v, r with
      | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d)
      | node red a x (node red b y c), z, d => node red (node black a x b) y (node black c z d)
      | a, x, b => node black a x b) ↔
    p v ∧ All p l ∧ All p r

Tactic:
split <;> simp [and_assoc, and_left_comm]

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : RBNode α
v : α
r : RBNode α
⊢ All p (l.balance1 v r) ↔ p v ∧ All p l ∧ All p r

Tactic:
unfold balance1

Result:
α : Type u_1
p : α → Prop
l : RBNode α
v : α
r : RBNode α
⊢ All p
      (match l, v, r with
      | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d)
      | node red a x (node red b y c), z, d => node red (node black a x b) y (node black c z d)
      | a, x, b => node black a x b) ↔
    p v ∧ All p l ∧ All p r
-- Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean
theorem limit_π_isIso_of_is_strict_terminal (F : J ⥤ C) [HasLimit F] (i : J)
    (H : ∀ (j) (_ : j ≠ i), IsTerminal (F.obj j)) [Subsingleton (i ⟶ i)] : IsIso (limit.π F i)

Proof state:
case refine_4
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.lift F
        { pt := F.toPrefunctor.1 i,
          π :=
            {
              app := fun j =>
                if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j),
              naturality := ⋯ } } ≫
      limit.π F i =
    𝟙 (F.obj i)

Tactic:
rw [limit.lift_π]

Result:
case refine_4
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ { pt := F.toPrefunctor.1 i,
            π :=
              {
                app := fun j =>
                  if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j),
                naturality := ⋯ } }.π.app
      i =
    𝟙 (F.obj i)

Proof state:
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
k : J
h : ¬k = i
f : i ⟶ k
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      (H k h).from (((Functor.const J).obj (F.toPrefunctor.1 i)).obj k) =
    eqToHom ⋯ ≫ F.map f

Tactic:
apply (H _ h).hom_ext

Result:
no goals

Proof state:
case pos.refl.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map (𝟙 i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ F.map (𝟙 i)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Balanced.insert {t : RBNode α} (h : t.Balanced c n) :
    ∃ c' n', (insert cmp t v).Balanced c' n'

Proof state:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
h : t.Balanced c n
a✝¹ : RBNode α
c₁✝ : RBColor
b✝ : RBNode α
c₂✝ : RBColor
x✝ : α
a✝ : t.isRed = red
ha : a✝¹.Balanced c₁✝ n
hb : b✝.Balanced c₂✝ n
⊢ ∃ c' n',
    (match t.isRed with
        | red => (node red a✝¹ x✝ b✝).setBlack
        | black => node red a✝¹ x✝ b✝).Balanced
      c' n'

Tactic:
have .node red .. := t

Result:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t a✝¹ : RBNode α
c₁✝ : RBColor
b✝ : RBNode α
c₂✝ : RBColor
x✝ : α
ha : a✝¹.Balanced c₁✝ n
hb : b✝.Balanced c₂✝ n
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
h : (node red l✝ v✝ r✝).Balanced c n
a✝ : (node red l✝ v✝ r✝).isRed = red
⊢ ∃ c' n',
    (match (node red l✝ v✝ r✝).isRed with
        | red => (node red a✝¹ x✝ b✝).setBlack
        | black => node red a✝¹ x✝ b✝).Balanced
      c' n'

Proof state:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
h : t.Balanced c n
⊢ ∃ c' n', (RBNode.insert cmp t v).Balanced c' n'

Tactic:
unfold RBNode.insert

Result:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
h : t.Balanced c n
⊢ ∃ c' n',
    (match t.isRed with
        | red => (ins cmp v t).setBlack
        | black => ins cmp v t).Balanced
      c' n'

Proof state:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
h : t.Balanced c n
⊢ ∃ c' n',
    (match t.isRed with
        | red => (ins cmp v t).setBlack
        | black => ins cmp v t).Balanced
      c' n'

Tactic:
match ins cmp v t, h.ins cmp v with
| _, .balanced h => split <;> [exact ⟨_, h.setBlack⟩; exact ⟨_, _, h⟩]
| _, .redred _ ha hb => have .node red .. := t; exact ⟨_, _, .black ha hb⟩

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
h✝ : t.Balanced c n
x✝ : RBNode α
c✝ : RBColor
h : x✝.Balanced c✝ n
⊢ ∃ c' n',
    (match t.isRed with
        | red => x✝.setBlack
        | black => x✝).Balanced
      c' n'

Tactic:
split <;> [exact ⟨_, h.setBlack⟩; exact ⟨_, _, h⟩]

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t a✝¹ : RBNode α
c₁✝ : RBColor
b✝ : RBNode α
c₂✝ : RBColor
x✝ : α
ha : a✝¹.Balanced c₁✝ n
hb : b✝.Balanced c₂✝ n
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
h : (node red l✝ v✝ r✝).Balanced c n
a✝ : (node red l✝ v✝ r✝).isRed = red
⊢ ∃ c' n',
    (match (node red l✝ v✝ r✝).isRed with
        | red => (node red a✝¹ x✝ b✝).setBlack
        | black => node red a✝¹ x✝ b✝).Balanced
      c' n'

Tactic:
exact ⟨_, _, .black ha hb⟩

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_eq_add_one_iff {k : ℕ∞} :
    s.encard = k + 1 ↔ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ t.encard = k)

Proof state:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ insert a (s \ {a}) = s

Tactic:
rwa [insert_diff_singleton, insert_eq_of_mem]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k

Tactic:
obtain ⟨a, ha⟩ := nonempty_of_encard_ne_zero (s := s) (by simp [h])

Result:
case refine_1.intro
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k

Proof state:
case refine_1.intro
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k

Tactic:
refine ⟨a, s \ {a}, fun h ↦ h.2 rfl, by rwa [insert_diff_singleton, insert_eq_of_mem], ?_⟩

Result:
case refine_1.intro
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ (s \ {a}).encard = k

Proof state:
case refine_2.intro.intro.intro.intro
α : Type u_1
a : α
t : Set α
h : a ∉ t
⊢ (insert a t).encard = t.encard + 1

Tactic:
rw [encard_insert_of_not_mem h]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
⊢ s.encard ≠ 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case refine_1.intro
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ (s \ {a}).encard = k

Tactic:
rw [← WithTop.add_right_inj WithTop.one_ne_top, ← h,
  encard_diff_singleton_add_one ha]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
k : ℕ∞
⊢ s.encard = k + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k

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

Result:
case refine_1
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k

case refine_2
α : Type u_1
s : Set α
k : ℕ∞
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k) → s.encard = k + 1

Proof state:
case refine_2
α : Type u_1
s : Set α
k : ℕ∞
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k) → s.encard = k + 1

Tactic:
rintro ⟨a, t, h, rfl, rfl⟩

Result:
case refine_2.intro.intro.intro.intro
α : Type u_1
a : α
t : Set α
h : a ∉ t
⊢ (insert a t).encard = t.encard + 1
-- Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
@[ext]
lemma hom_ext {f g : M₁ ⟶ M₂} (h : ∀ (X : Cᵒᵖ), f.app X = g.app X) :
    f = g := Hom.ext (by ext1; apply h)

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f g : M₁ ⟶ M₂
h : ∀ (X : Cᵒᵖ), f.app X = g.app X
x✝ : Cᵒᵖ
⊢ f.app x✝ = g.app x✝

Tactic:
apply h

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f g : M₁ ⟶ M₂
h : ∀ (X : Cᵒᵖ), f.app X = g.app X
⊢ f.app = g.app

Tactic:
ext1

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f g : M₁ ⟶ M₂
h : ∀ (X : Cᵒᵖ), f.app X = g.app X
x✝ : Cᵒᵖ
⊢ f.app x✝ = g.app x✝
-- Mathlib/Data/Prod/Basic.lean
theorem map_leftInverse [Nonempty β] [Nonempty δ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α}
    {g₂ : δ → γ} : LeftInverse (map f₁ g₁) (map f₂ g₂) ↔ LeftInverse f₁ f₂ ∧ LeftInverse g₁ g₂ :=
  ⟨fun h =>
    ⟨fun b => by
      inhabit δ
      exact congr_arg Prod.fst (h (b, default)),
      fun d => by
      inhabit β
      exact congr_arg Prod.snd (h (default, d))⟩,
    fun h => h.1.prodMap h.2 ⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
inhabited_h : Inhabited β
⊢ g₁ (g₂ d) = d

Tactic:
exact congr_arg Prod.snd (h (default, d))

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
⊢ g₁ (g₂ d) = d

Tactic:
inhabit β

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
inhabited_h : Inhabited β
⊢ g₁ (g₂ d) = d

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
⊢ f₁ (f₂ b) = b

Tactic:
inhabit δ

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
inhabited_h : Inhabited δ
⊢ f₁ (f₂ b) = b

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
inhabited_h : Inhabited δ
⊢ f₁ (f₂ b) = b

Tactic:
exact congr_arg Prod.fst (h (b, default))

Result:
no goals