mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ (sz.splitLengths l)[i].length ≤ sz[i]

Tactic:
induction sz generalizing l i
  · simp at hi
  case cons head tail tail_ih =>
    simp only [splitLengths_cons]
    cases i
    · simp
    · simp only [getElem_cons_succ, tail_ih]

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

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
⊢ (∀ i < w.length - p, w[i]? = w[i + p]?) → w.HasPeriod p

Tactic:
intro lhs
    rw [HasPeriod]
    have drop : drop p w <+: w := by
      simp only [prefix_iff_getElem?, length_drop, getElem_drop]
      intro i leni
      have len : i + p < w.length := by lia
      simp_all only [getElem?_pos, add_comm p i]
    rw [← prefix_append_right_inj (w.take p)] at drop
    simp_all

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

Goal state before:
pp: case h_2
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
h : m = g.reverse ++ [a] ∨ m ∈ splitBy.loop r l b [] []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
obtain rfl | hm := h

Goal state after:
case h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α},
    (∀ (b : α), b ∈ g_1.head? → r b a_1 = true) →
      IsChain (fun y x ↦ r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])

case h_2.inr
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
hm : m ∈ splitBy.loop r l b [] []
⊢ IsChain (fun x y ↦ r x y = true) m
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (of fun i j ↦ fst (diagonal (fun i ↦ (algebraMap R (DualNumber R)) r) i j),
      of fun i j ↦ snd (diagonal (fun i ↦ (algebraMap R (DualNumber R)) r) i j)) =
    inl (diagonal fun i ↦ r)

Tactic:
algebraMap_eq_inl,

Goal state after:
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (of fun i j ↦ fst (diagonal (fun i ↦ inl r) i j), of fun i j ↦ snd (diagonal (fun i ↦ inl r) i j)) =
    inl (diagonal fun i ↦ r)
Module: Mathlib.Data.Nat.Cast.SetInterval

Goal state before:
pp: a : ℕ
⊢ IsUpperSet (range ⇑castOrderEmbedding)

Tactic:
simp [isUpperSet_Ici]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
hx : x₁ < n % p + 1 ∧ x₂ < n / p + 1
h' : x₁ < p
⊢ (x₁, x₂).1 % p = x₁ ∧ (x₁, x₂).1 / p + (x₁, x₂).2 = x₂

Tactic:
eq_comm (b := x₂)

Goal state after:
case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
hx : x₁ < n % p + 1 ∧ x₂ < n / p + 1
h' : x₁ < p
⊢ (x₁, x₂).1 % p = x₁ ∧ x₂ = (x₁, x₂).1 / p + (x₁, x₂).2
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
m : ℕ
hm : m < #hf.toFinset
n : ℕ
hn : n < #hf.toFinset
h : m < n
⊢ nth p m < nth p n

Tactic:
simp only [nth_eq_orderEmbOfFin, *]

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Finite
m : ℕ
hm : m < #hf.toFinset
n : ℕ
hn : n < #hf.toFinset
h : m < n
⊢ (hf.toFinset.orderEmbOfFin ⋯) ⟨m, hm⟩ < (hf.toFinset.orderEmbOfFin ⋯) ⟨n, hn⟩
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

Tactic:
by
  rcases id r with _ | rs
  · rcases id l with _ | ⟨ls, ll, lx, lr⟩
    · exact ι x
    · rcases id ll with _ | lls
      · rcases lr with _ | ⟨_, _, lrx⟩
        · exact node 2 l x nil
        · exact node 3 (ι lx) lrx ι x
      · rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)
  · rcases id l with _ | ⟨ls, ll, lx, lr⟩
    · exact node (rs + 1) nil x r
    · refine if ls > delta * rs then ?_ else node (ls + rs + 1) l x r
      rcases id ll with _ | lls
      · exact nil
      --should not happen
      rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
      · exact nil
      --should not happen
      exact
        if lrs < ratio * lls then node (ls + rs + 1) ll lx (node (rs + lrs + 1) lr x r)
        else
          node (ls + rs + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
            (node (size lrr + rs + 1) lrr x r)

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

Goal state before:
pp: p : ℕ → Prop
n n' : ℕ
hn' : n' ∈ Set.ofPred p
hp : n' ∉ ↑(range n)
⊢ ∃ n' ≥ n, p n'

Tactic:
exact ⟨n', by simpa using hp, Set.mem_ofPred.mp hn'⟩

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.inl.succ.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
n✝ : ℕ
⊢ n✝ + 1 + 1 ≤ 1 → BalancedSz 0 0 ∧ BalancedSz 0 (n✝ + 1 + 1) ∧ BalancedSz (0 + 0 + 1) (0 + (n✝ + 1 + 1) + 1)

Tactic:
intro r0; unfold BalancedSz delta; lia

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

Goal state before:
pp: a : PosNum
⊢ ofInt' ↑↑a = pos a

Tactic:
← Num.ofInt'_toZNum,

Goal state after:
a : PosNum
⊢ (↑↑a).toZNum = pos a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a : PosNum
⊢ -ofInt' ↑↑a = neg a

Tactic:
← Num.ofInt'_toZNum,

Goal state after:
a : PosNum
⊢ -(↑↑a).toZNum = neg a
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case intro
F : PFunctor.{uA, uB}
n✝ n : ℕ
a✝ : F.A
x✝ : F.B a✝ → CofixA F n✝
x'✝ : F.B a✝ → CofixA F (n✝ + 1)
hagree : ∀ (i : F.B a✝), Agree (x✝ i) (x'✝ i)
i : F.B (head' (CofixA.intro a✝ x✝))
j : F.B (head' (CofixA.intro a✝ x'✝))
h₀ : i ≍ j
⊢ Agree (children' (CofixA.intro a✝ x✝) i) (children' (CofixA.intro a✝ x'✝) j)

Tactic:
cases h₀

Goal state after:
case intro.refl
F : PFunctor.{uA, uB}
n✝ n : ℕ
a✝ : F.A
x✝ : F.B a✝ → CofixA F n✝
x'✝ : F.B a✝ → CofixA F (n✝ + 1)
hagree : ∀ (i : F.B a✝), Agree (x✝ i) (x'✝ i)
i : F.B (head' (CofixA.intro a✝ x✝))
⊢ Agree (children' (CofixA.intro a✝ x✝) i) (children' (CofixA.intro a✝ x'✝) i)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ
F : PFunctor.{uA, uB}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
⊢ (CofixA.intro (f x₀).fst fun i ↦ sCorec f ((f x₀).snd i) n) =
    CofixA.intro (F.map (M.corec f) (f x₀)).fst fun i ↦ ((F.map (M.corec f) (f x₀)).snd i).approx n

Tactic:
cases f x₀

Goal state after:
case succ.mk
F : PFunctor.{uA, uB}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
fst✝ : F.A
snd✝ : F.B fst✝ → X
⊢ (CofixA.intro ⟨fst✝, snd✝⟩.fst fun i ↦ sCorec f (⟨fst✝, snd✝⟩.snd i) n) =
    CofixA.intro (F.map (M.corec f) ⟨fst✝, snd✝⟩).fst fun i ↦ ((F.map (M.corec f) ⟨fst✝, snd✝⟩).snd i).approx n
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
h✝ : l✝.size < ratio * r✝.size
⊢ (l.node3L x l✝ x✝ r✝).Sized

pp: case neg
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
h✝ : ¬l✝.size < ratio * r✝.size
⊢ (l.node4L x l✝ x✝ r✝).Sized

Tactic:
· exact hl.node3L hr.2.1 hr.2.2

Goal state after:
case neg
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
h✝ : ¬l✝.size < ratio * r✝.size
⊢ (l.node4L x l✝ x✝ r✝).Sized
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
a'' : P.A
g g' : P.B a'' → P.M
h₀ : ⟨a, f⟩ = ⟨a'', g⟩
h₁ : ⟨a, f'⟩ = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)

Tactic:
cases h₀

Goal state after:
case tail.refl
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
g' : P.B a → P.M
h₁ : ⟨a, f'⟩ = ⟨a, g'⟩
h₂ : ∀ (i : P.B a), R (f i) (g' i)
⊢ R (f i) (f' i)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩
i : P.B a
⊢ ∃ x', True ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'

Tactic:
exact ⟨f' i, trivial, rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → p.Prime
⊢ (ofPNatList l h).prod = l.prod

Tactic:
have := prod_ofPNatMultiset (l : Multiset ℕ+) h

Goal state after:
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → p.Prime
this : (ofPNatMultiset (↑l) h).prod = (↑l).prod
⊢ (ofPNatList l h).prod = l.prod
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ ⟨a₁, b₁⟩ ≤ ⟨a₃, b₃⟩

Tactic:
left

Goal state after:
case left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ a₁ < a₃
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a✝¹ : a₁ < a₂
b₂✝ : α a₂
a✝ : b₂ ≤ b₂✝
⊢ ⟨a₁, b₁⟩ ≤ ⟨a₂, b₂✝⟩

Tactic:
left

Goal state after:
case left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a✝¹ : a₁ < a₂
b₂✝ : α a₂
a✝ : b₂ ≤ b₂✝
⊢ a₁ < a₂
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₃ : ι
b₃ : α a₃
b₂✝ : α a₁
a✝¹ : b₁ ≤ b₂✝
a✝ : a₁ < a₃
⊢ ⟨a₁, b₁⟩ ≤ ⟨a₃, b₃⟩

Tactic:
left

Goal state after:
case right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₃ : ι
b₃ : α a₃
b₂✝ : α a₁
a✝¹ : b₁ ≤ b₂✝
a✝ : a₁ < a₃
⊢ a₁ < a₃
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i ↦ Subtype p
h : repr y = ⟨a, f⟩
i : Fin2 n
j : (P F).B a i
⊢ p ↑(f i j)

Tactic:
apply (f i j).property

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.nil.refl.refl
α : Type u_1
x : α
rs : ℕ
rx : α
sl : nil.Sized
sr : (node rs nil rx nil).Sized
H1 : nil.size = 0 → (node rs nil rx nil).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs nil rx nil).size → (node rs nil rx nil).size ≤ delta * nil.size
this : nil.size = 0 ∧ nil.size = 0
⊢ nil.balanceL x (node rs nil rx nil) = nil.balance x (node rs nil rx nil)

Tactic:
rw [sr.eq_node']

Goal state after:
case node.nil.refl.refl
α : Type u_1
x : α
rs : ℕ
rx : α
sl : nil.Sized
sr : (node rs nil rx nil).Sized
H1 : nil.size = 0 → (node rs nil rx nil).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs nil rx nil).size → (node rs nil rx nil).size ≤ delta * nil.size
this : nil.size = 0 ∧ nil.size = 0
⊢ nil.balanceL x (nil.node' rx nil) = nil.balance x (nil.node' rx nil)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case H2.inr.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
H : l.size + r' ≤ 1
⊢ r.size ≤ delta * l.size

Tactic:
cases raised_iff.1 e

Goal state after:
case H2.inr.inl.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
H : l.size + r' ≤ 1
left✝ : r.size ≤ r'
right✝ : r' ≤ r.size + 1
⊢ r.size ≤ delta * l.size
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
⊢ Mcongr (g <$$> aa₁) (g <$$> aa₂)

Tactic:
use r'

Goal state after:
case h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := ⋯
⊢ IsPrecongr r' ∧ r' (g <$$> aa₁) (g <$$> aa₂)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr x y
⊢ (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) x) = (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) y)

Tactic:
rw [← Quot.factor_mk_eq _ _ this]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr x y
⊢ (TypeVec.id ::: Quot.factor r Mcongr this ∘ Quot.mk r) <$$> abs (M.dest (P F) x) =
    (TypeVec.id ::: Quot.factor r Mcongr this ∘ Quot.mk r) <$$> abs (M.dest (P F) y)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ (∃ l', Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size) ∨
    ∃ r', Raised r' t_r.size ∧ BalancedSz (erase x t_l).size r'

Tactic:
left

Goal state after:
case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ ∃ l', Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ recF g ∘ fixToW = rec g

Tactic:
apply funext

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ ∀ (x : Fix F α), (recF g ∘ fixToW) x = rec g x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h'
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x✝ y : Cofix F α
rxy : r x✝ y
x : Cofix F α
⊢ r' x x

Tactic:
left

Goal state after:
case h'
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := ⋯
x✝ y : Cofix F α
rxy : r x✝ y
x : Cofix F α
⊢ x = x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ (TypeVec.id ::: Quot.mk r') <$$> x.dest = (TypeVec.id ::: Quot.mk r') <$$> y.dest

Tactic:
rw [← Quot.factor_mk_eq _ _ this]

Goal state after:
case h.inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ (TypeVec.id ::: Quot.factor r r' this ∘ Quot.mk r) <$$> x.dest =
    (TypeVec.id ::: Quot.factor r r' this ∘ Quot.mk r) <$$> y.dest
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ (TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) <$$> (TypeVec.id ::: Quot.mk r) <$$> x.dest =
    (TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) <$$> (TypeVec.id ::: Quot.mk r) <$$> y.dest

Tactic:
rw [h _ _ r'xy]

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : true = true
⊢ (t_l.glue t_r).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
(Valid'.glue h.left h.right h.bal.1).2,

Goal state after:
case node.eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : true = true
⊢ t_l.size + t_r.size = (node size✝ t_l t_x t_r).size - 1
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
⊢ ∀ (x : Fix F), g₁ x = g₂ x

Tactic:
rintro ⟨x⟩

Goal state after:
case mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
x : (P F).W
⊢ g₁ (Quot.mk (⇑Wsetoid) x) = g₂ (Quot.mk (⇑Wsetoid) x)
Module: Mathlib.Data.Rat.Cast.OfScientific

Goal state before:
pp: K : Type u_1
inst✝¹ : _root_.Field K
inst✝ : CharZero K
m : ℕ
s : Bool
e : ℕ
⊢ OfScientific.ofScientific m s e = if s = true then ↑m / 10 ^ e else ↑m * 10 ^ e

Tactic:
rw [← NNRat.cast_ofScientific, NNRatCast.toOfScientific_def]

Goal state after:
K : Type u_1
inst✝¹ : _root_.Field K
inst✝ : CharZero K
m : ℕ
s : Bool
e : ℕ
⊢ ↑↑⟨OfScientific.ofScientific m s e, ⋯⟩ = if s = true then ↑m / 10 ^ e else ↑m * 10 ^ e
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
⊢ ∀ (x : Fix F), p x

Tactic:
rintro ⟨x⟩

Goal state after:
case mk
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x✝ : Fix F
x : (P F).W
⊢ p (Quot.mk (⇑Wsetoid) x)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
⊢ Quot.mk Mcongr <$> abs x.dest = Quot.mk Mcongr <$> abs y.dest

Tactic:
rw [← Quot.factor_mk_eq _ _ this]

Goal state after:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
⊢ (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest