mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
x✝ :
  (fun X ↦ X)
    ↑{x |
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
          (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
a : C(↑(G.obj Z), X)
ha✝ :
  a ∈
    {x |
      (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
ha : ⇑a ∘ ⇑(TopCat.Hom.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(TopCat.Hom.hom (G.map (pullback.snd π π)))
⊢ ∃ a_1, { toFun := ⇑a_1 ∘ ⇑(TopCat.Hom.hom (G.map π)), continuous_toFun := ⋯ } = a

Tactic:
refine ⟨(hq Z B π).lift a (factorsThrough_of_pullbackCondition G X ha), ?_⟩

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
x✝ :
  (fun X ↦ X)
    ↑{x |
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
          (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
a : C(↑(G.obj Z), X)
ha✝ :
  a ∈
    {x |
      (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
ha : ⇑a ∘ ⇑(TopCat.Hom.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(TopCat.Hom.hom (G.map (pullback.snd π π)))
⊢ { toFun := ⇑(⋯.lift a ⋯) ∘ ⇑(TopCat.Hom.hom (G.map π)), continuous_toFun := ⋯ } = a
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h :
  codeSupp' f (Cont'.cons₁ fs k) ∪
      (trStmts₁
          (move₂ (fun x ↦ false) main aux
            (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
              (move₂ (fun x ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
        (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
⊢ Supports
    (trStmts₁
        (move₂ (fun x ↦ false) main aux
          (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main (move₂ (fun x ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
      (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k))))
    S

Tactic:
refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun h => ?_

Goal state after:
case cons.refine_1
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h :
  codeSupp' f (Cont'.cons₁ fs k) ∪
      (trStmts₁
          (move₂ (fun x ↦ false) main aux
            (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
              (move₂ (fun x ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
        (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
⊢ codeSupp fs k.cons₂ ⊆ S

case cons.refine_2
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h✝ :
  codeSupp' f (Cont'.cons₁ fs k) ∪
      (trStmts₁
          (move₂ (fun x ↦ false) main aux
            (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
              (move₂ (fun x ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
        (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
⊢ Supports (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k))) S
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f✝ : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
f : ℕ → ↑X
p : ↑X
h : Filter.Tendsto f Filter.atTop (nhds p)
⊢ Filter.Tendsto ((topCatAdjunctionCounitEquiv X).invFun ∘ f) Filter.atTop
    (nhds ((topCatAdjunctionCounitEquiv X).invFun p))

Tactic:
let g := (topCatAdjunctionCounitEquiv X).invFun ∘ (OnePoint.continuousMapMkNat f p h)

Goal state after:
X✝ Y : LightCondSet
f✝ : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
f : ℕ → ↑X
p : ↑X
h : Filter.Tendsto f Filter.atTop (nhds p)
g : OnePoint ℕ → ↑X.toLightCondSet.toTopCat :=
  (topCatAdjunctionCounitEquiv X).invFun ∘ ⇑(OnePoint.continuousMapMkNat f p h)
⊢ Filter.Tendsto ((topCatAdjunctionCounitEquiv X).invFun ∘ f) Filter.atTop
    (nhds ((topCatAdjunctionCounitEquiv X).invFun p))
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝² : PreservesFiniteProducts F
X Y : Profinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))
g : X ⟶ Y
⊢ (ConcreteCategory.hom (isoFinYonedaComponents F X).inv) (f ∘ ⇑(ConcreteCategory.hom g)) =
    (ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f)

Tactic:
by
  apply injective_of_mono (isoFinYonedaComponents F X).hom
  simp only [Iso.inv_hom_id_apply]
  ext x
  rw [isoFinYonedaComponents_hom_apply]
  simp only [← Functor.map_comp_apply, ← op_comp, CompHausLike.const_comp,
    ← isoFinYonedaComponents_hom_apply, Iso.inv_hom_id_apply, Function.comp_apply]

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
⊢ (ConcreteCategory.hom (isoFinYonedaComponents F X).inv) (f ∘ ⇑(ConcreteCategory.hom g)) =
    (ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f)

Tactic:
by
  apply injective_of_mono (isoFinYonedaComponents F X).hom
  simp only [Iso.inv_hom_id_apply]
  ext x
  rw [isoFinYonedaComponents_hom_apply]
  simp only [← Functor.map_comp_apply, ← op_comp, CompHausLike.const_comp,
    ← isoFinYonedaComponents_hom_apply, Iso.inv_hom_id_apply, Function.comp_apply]

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
⊢ ∃ h, f ≫ h = g

Tactic:
have (n : ℕ) : Epi (S.transitionMap n) := (LightProfinite.epi_iff_surjective _).mpr
      (S.surjective_transitionMap n)

Goal state after:
S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
⊢ ∃ h, f ≫ h = g
Module: Mathlib.Data.Nat.Upto

Goal state before:
pp: p : ℕ → Prop
x : ℕ
h : p x
⊢ Upto.GT p = InvImage (fun x1 x2 ↦ x1 < x2) fun y ↦ x - ↑y

Tactic:
ext ⟨a, ha⟩ ⟨b, _⟩

Goal state after:
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property✝ : ∀ (j : ℕ), j < b → ¬p j
⊢ Upto.GT p ⟨a, ha⟩ ⟨b, property✝⟩ ↔ InvImage (fun x1 x2 ↦ x1 < x2) (fun y ↦ x - ↑y) ⟨a, ha⟩ ⟨b, property✝⟩
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
⊢ ∀ {α β : Type u_1} (x : α) (f : α → ContT r m β), pure x >>= f = f x

Tactic:
intros; ext; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
⊢ ∀ {α β γ : Type u_1} (x : ContT r m α) (f : α → ContT r m β) (g : β → ContT r m γ),
    x >>= f >>= g = x >>= fun x ↦ f x >>= g

Tactic:
intros; ext; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
⊢ ∀ {α ω γ : Type u_1} (cmd : ContT r m α) (next : Label ω (ContT r m) γ → α → ContT r m ω),
    (callCC fun f ↦ cmd >>= next f) = do
      let x ← cmd
      callCC fun f ↦ next f x

Tactic:
intros; ext; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
⊢ ∀ {α : Type u_1} (β : Type u_1) (x : α) (dead : Label α (ContT r m) β → β → ContT r m α),
    (callCC fun f ↦ goto f x >>= dead f) = pure x

Tactic:
intros; ext; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
⊢ ∀ {α β : Type u_1} (dummy : ContT r m α), (callCC fun x ↦ dummy) = dummy

Tactic:
intros; ext; rfl

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : Option.some i = ↑n
h : σ (Option.some i) s = x
⊢ σ (Option.some n) s = σ (Option.some i) s

Tactic:
Option.some_injective _ hn'.symm

Goal state after:
case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : Option.some i = ↑n
h : σ (Option.some i) s = x
⊢ σ (Option.some i) s = σ (Option.some i) s
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u} n
⊢ subtypeVal α.repeatEq ⊚ diagSub = prod.diag

Tactic:
ext i x
  induction i with
  | fz => simp only [comp, subtypeVal, diagSub, prod.diag]
  | fs _ i_ih => apply @i_ih (drop α)

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
⊢ (a ∉ s → ∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s

Tactic:
have := Classical.propDecidable

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (a ∉ s → ∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
b : α
h' : f a = some b
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

Tactic:
simp [lookmap_cons_some _ _ h', h _ _ h']

Goal state after:
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
b : α
h' : f a = some b
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

Tactic:
· simp [lookmap_cons_some _ _ h', h _ _ h']

Goal state after:
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a ^^^ b ^^^ b = a

Tactic:
by
  rw [xor_assoc, LawfulXor.xor_self, xor_zero]

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
⊢ map₂Left' f as [] = (map (fun a ↦ f a none) as, [])

Tactic:
cases as <;> rfl

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
⊢ as.zipLeft' [] = (map (fun a ↦ (a, none)) as, [])

Tactic:
cases as <;> rfl

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
⊢ as.zipLeft' [] = (map (fun a ↦ (a, none)) as, [])

Tactic:
by
  cases as <;> rfl

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
⊢ map₂Left f as [] = map (fun a ↦ f a none) as

Tactic:
cases as <;> rfl

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
⊢ as.zipLeft [] = map (fun a ↦ (a, none)) as

Tactic:
cases as <;> rfl

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
⊢ as.zipLeft [] = map (fun a ↦ (a, none)) as

Tactic:
by
  cases as <;> rfl

Goal state after:
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
drop : List.drop p w <+: w
⊢ w <+: take p w ++ w

Tactic:
rw [← prefix_append_right_inj (w.take p)] at drop

Goal state after:
case mpr
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
drop : take p w ++ List.drop p w <+: take p w ++ w
⊢ w <+: take p w ++ w
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
head✝ : α
tail✝ : List α
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r (head✝ :: tail✝))

Tactic:
| cons _ _ =>

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m n A
b : Matrix n o A
⊢ mulRightLinearMap l R (a * b) = mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a

Tactic:
ext
  simp only [mulRightLinearMap_apply, LinearMap.comp_apply, Matrix.mul_assoc]

Goal state after:
Module: Mathlib.Data.NNRat.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(f x).toNNRat

Tactic:
rw [Rat.coe_toNNRat _ (hf x hxs)]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ ofDigits b' (b'.digits n) % b = 0 ↔ ofDigits 1 (b'.digits n) % b = 0

Tactic:
ofDigits_mod,

Goal state after:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ ofDigits (b' % b) (b'.digits n) % b = 0 ↔ ofDigits 1 (b'.digits n) % b = 0
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ (b'.digits n).sum

Tactic:
rw [← ofDigits_one]
  conv_lhs => rw [← ofDigits_digits b' n]
  rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, ofDigits_mod, h]

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
⊢ nth p n = 0 ↔ p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ n

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · simp only [or_iff_not_imp_right, not_exists, not_le]
    exact fun hn => ⟨h ▸ nth_mem _ hn, nonpos_iff_eq_zero.1 <| h ▸ le_nth hn⟩
  · rintro (⟨h₀, rfl⟩ | ⟨hf, hle⟩)
    exacts [nth_zero_of_zero h₀, nth_of_card_le hf hle]

Goal state after:
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case refine_2
n : PosNum
⊢ ↑n.bit0 = ↑n.bit0.minFac ↔ n = 1

Tactic:
to_nat_inj

Goal state after:
case refine_2
n : PosNum
⊢ n.bit0 = n.bit0.minFac ↔ n = 1
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case refine_2
n : PosNum
⊢ ↑n.bit1.minFac = ↑n.bit1 ↔ n.bit1.minFacAux (↑n) 1 = n.bit1

Tactic:
to_nat_inj

Goal state after:
case refine_2
n : PosNum
⊢ n.bit1.minFac = n.bit1 ↔ n.bit1.minFacAux (↑n) 1 = n.bit1
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

pp: case nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· rcases lr with _ | ⟨_, _, lrx⟩
        · exact node 2 l x nil
        · exact node 3 (ι lx) lrx ι x

Goal state after:
case nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

pp: case node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· exact nil

Goal state after:
case node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

pp: case node.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α

Tactic:
· exact nil

Goal state after:
case node.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

pp: case node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· exact nil

Goal state after:
case node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

pp: case node.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α

Tactic:
· exact nil

Goal state after:
case node.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

pp: case node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· rcases lr with _ | ⟨_, _, lrx⟩
        · exact node 2 l x nil
        · exact node 3 (ι lx) lrx ι x

Goal state after:
case node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.node.refine_1.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

pp: case node.node.refine_1.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α

Tactic:
· exact nil

Goal state after:
case node.node.refine_1.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.node.refine_1.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α

pp: case node.node.refine_1.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· exact nil

Goal state after:
case node.node.refine_1.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.node.refine_2.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

pp: case node.node.refine_2.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· exact nil

Goal state after:
case node.node.refine_2.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.node.refine_2.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

pp: case node.node.refine_2.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α

Tactic:
· exact nil

Goal state after:
case node.node.refine_2.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α