mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * l.size < r.size
H3 : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
⊢ Valid' o₁ (l.rotateL x r) o₂

Tactic:
obtain - | ⟨rs, rl, rx, rr⟩ := r; · cases H2
  rw [hr.2.size_eq, Nat.lt_succ_iff] at H2
  rw [hr.2.size_eq] at H3
  replace H3 : 2 * (size rl + size rr) ≤ 9 * size l + 3 ∨ size rl + size rr ≤ 2 :=
    H3.imp (@Nat.le_of_add_le_add_right _ 2 _) Nat.le_of_succ_le_succ
  have H3_0 (l0 : size l = 0) : size rl + size rr ≤ 2 := by lia
  have H3p : size l > 0 → 2 * (size rl + size rr) ≤ 9 * size l + 3 := fun l0 : 1 ≤ size l =>
    (or_iff_left_of_imp <| by lia).1 H3
  have ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1 := by lia
  have hlp : size l > 0 → ¬size rl + size rr ≤ 1 := fun l0 hb =>
    absurd (le_trans (le_trans (Nat.mul_le_mul_left _ l0) H2) hb) (by decide)
  rw [Ordnode.rotateL_node]; split_ifs with h
  · have rr0 : size rr > 0 :=
      (mul_lt_mul_iff_right₀ (by decide)).1 (lt_of_le_of_lt (Nat.zero_le _) h : ratio * 0 < _)
    suffices BalancedSz (size l) (size rl) ∧ BalancedSz (size l + size rl + 1) (size rr) by
      exact hl.node3L hr.left hr.right this.1 this.2
    rcases Nat.eq_zero_or_pos (size l) with l0 | l0
    · rw [l0]; replace H3 := H3_0 l0
      have := hr.3.1
      rcases Nat.eq_zero_or_pos (size rl) with rl0 | rl0
      · rw [rl0] at this ⊢
        rw [le_antisymm (balancedSz_zero.1 this.symm) rr0]
        decide
      have rr1 : size rr = 1 := le_antisymm (ablem rl0 H3) rr0
      rw [add_comm] at H3
      rw [rr1, show size rl = 1 from le_antisymm (ablem rr0 H3) rl0]
      decide
    replace H3 := H3p l0
    rcases hr.3.1.resolve_left (hlp l0) with ⟨_, hb₂⟩
    refine ⟨Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩⟩
    · exact Valid'.rotateL_lemma₁ H2 hb₂
    · exact Nat.le_of_lt_succ (Valid'.rotateL_lemma₂ H3 h)
    · exact Valid'.rotateL_lemma₃ H2 h
    · exact
        le_trans hb₂
          (Nat.mul_le_mul_left _ <| le_trans (Nat.le_add_left _ _) (Nat.le_add_right _ _))
  · rcases Nat.eq_zero_or_pos (size rl) with rl0 | rl0
    · rw [rl0, not_lt, Nat.le_zero, Nat.mul_eq_zero] at h
      replace h := h.resolve_left (by decide)
      rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2
      rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1
      cases H1 (by decide)
    refine hl.node4L hr.left hr.right rl0 ?_
    rcases Nat.eq_zero_or_pos (size l) with l0 | l0
    · replace H3 := H3_0 l0
      rcases Nat.eq_zero_or_pos (size rr) with rr0 | rr0
      · have := hr.3.1
        rw [rr0] at this
        exact Or.inl ⟨l0, le_antisymm (balancedSz_zero.1 this) rl0, rr0.symm ▸ zero_le_one⟩
      exact Or.inl ⟨l0, le_antisymm (ablem rr0 <| by rwa [add_comm]) rl0, ablem rl0 H3⟩
    exact
      Or.inr ⟨l0, not_lt.1 h, H2, Valid'.rotateL_lemma₄ (H3p l0), (hr.3.1.resolve_left (hlp l0)).1⟩

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

Goal state before:
pp: α : Type u_1
t : Ordnode α
⊢ t.eraseMax.dual = t.dual.eraseMin.dual.dual

Tactic:
dual_eraseMin,

Goal state after:
α : Type u_1
t : Ordnode α
⊢ t.eraseMax.dual = t.dual.dual.eraseMax.dual
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ Multiset.pmap (fun a h ↦ ↑⟨a, h⟩) v h = v

Tactic:
Multiset.pmap_eq_map,

Goal state after:
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ Multiset.map (fun a ↦ a) v = v
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
this : (fun p h ↦ ↑⟨↑p, h⟩) = fun p x ↦ id p
⊢ Multiset.pmap (fun p x ↦ id p) v h = v

Tactic:
Multiset.pmap_eq_map,

Goal state after:
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
this : (fun p h ↦ ↑⟨↑p, h⟩) = fun p x ↦ id p
⊢ Multiset.map id v = v
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
⊢ PNat.find h = PNat.find h₂ + 1

Tactic:
refine (find_eq_iff _).2 ⟨PNat.find_spec h₂, fun n ↦ ?_⟩

Goal state after:
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
n : ℕ+
⊢ n < PNat.find h₂ + 1 → ¬p n
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case fst
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * u.q + ↑u.z) * ↑u.b + u.y * (u.r - 1 + 1) = u.y * (u.r + ↑u.b * u.q) + ↑u.z * ↑u.b

Tactic:
hr

Goal state after:
case fst
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * u.q + ↑u.z) * ↑u.b + u.y * u.r = u.y * (u.r + ↑u.b * u.q) + ↑u.z * ↑u.b
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case snd
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑u.w * u.q + u.x) * ↑u.b + ↑u.w * (u.r - 1 + 1) = ↑u.w * (u.r + ↑u.b * u.q) + u.x * ↑u.b

Tactic:
hr

Goal state after:
case snd
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑u.w * u.q + u.x) * ↑u.b + ↑u.w * u.r = ↑u.w * (u.r + ↑u.b * u.q) + u.x * ↑u.b
Module: Mathlib.Data.Pi.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b x : (i : ι) → α i
⊢ (∀ (a_1 : ι), x a_1 ∈ Icc (a a_1) (b a_1)) ↔ a ≤ x ∧ x ≤ b

Tactic:
mem_Icc,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b x : (i : ι) → α i
⊢ (∀ (a_1 : ι), a a_1 ≤ x a_1 ∧ x a_1 ≤ b a_1) ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

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

Tactic:
clear y

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
t : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ t a₂
⊢ Valid' (Option.map f a₁) (map f t) (Option.map f a₂) ∧ (map f t).size = t.size

Tactic:
by
  induction t generalizing a₁ a₂ with
  | nil =>
    simp only [map, size_nil, and_true]; apply valid'_nil
    cases a₁; · trivial
    cases a₂; · trivial
    simp only [Option.map, Bounded]
    exact f_strict_mono h.ord
  | node _ _ _ _ t_ih_l t_ih_r =>
    have t_ih_l' := t_ih_l h.left
    have t_ih_r' := t_ih_r h.right
    clear t_ih_l t_ih_r
    obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
    obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
    simp only [map, size_node, and_true]
    constructor
    · exact And.intro t_l_valid.ord t_r_valid.ord
    · constructor
      · rw [t_l_size, t_r_size]; exact h.sz.1
      · constructor
        · exact t_l_valid.sz
        · exact t_r_valid.sz
    · constructor
      · rw [t_l_size, t_r_size]; exact h.bal.1
      · constructor
        · exact t_l_valid.bal
        · exact t_r_valid.bal

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Quot

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u
q : MvQPF F
G : TypeVec.{u} n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec.{u} n} → F α → G α
FG_repr : {α : TypeVec.{u} n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec.{u} n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ : TypeVec.{u} n
x : G α✝
⊢ FG_abs (abs (repr (FG_repr x))) = x

Tactic:
rw [abs_repr, FG_abs_repr]

Goal state after:
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
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
⊢ ∀ (x y : Cofix F α), r x y → x = y

Tactic:
by
  apply Cofix.bisim_rel
  intro x y rxy
  rcases (liftR_iff (fun a b => RelLast α r b) (dest x) (dest y)).mp (h x y rxy)
    with ⟨a, f₀, f₁, dxeq, dyeq, h'⟩
  rw [dxeq, dyeq, ← abs_map, ← abs_map, MvPFunctor.map_eq, MvPFunctor.map_eq]
  rw [← split_dropFun_lastFun f₀, ← split_dropFun_lastFun f₁]
  rw [appendFun_comp_splitFun, appendFun_comp_splitFun]
  rw [id_comp, id_comp]
  congr 2 with (i j); rcases i with - | i
  · apply Quot.sound
    apply h' _ j
  · change f₀ _ j = f₁ _ j
    apply h' _ j

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
G : Type u → Type u
inst✝ : Functor G
FG_abs : {α : Type u} → F α → G α
FG_repr : {α : Type u} → G α → F α
FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x
α : Type u
x : G α
⊢ FG_abs (abs (repr (FG_repr x))) = x

Tactic:
rw [abs_repr, FG_abs_repr]

Goal state after:
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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
⊢ corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) = Sum.elim _root_.id (corec' g)

Tactic:
ext (i | i) <;> erw [corec_roll]

Goal state after:
case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : Cofix F α
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) val) fun val ↦ g val)
      (Sum.inl i) =
    Sum.elim _root_.id (corec' g) (Sum.inl i)

case inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) val) fun val ↦ g val)
      (Sum.inr i) =
    Sum.elim _root_.id (corec' g) (Sum.inr i)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
n : ℕ
⊢ s.tail.drop n = s.drop (n + 1)

Tactic:
Nat.add_comm

Goal state after:
α : Type u
s : WSeq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝¹ t✝¹ u✝¹ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝¹
s✝ u✝ t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t✝.destruct u✝.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t✝.destruct
c : α
u : WSeq α
hc : some (c, u) ∈ u✝.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
ab : R a b
st : LiftRel R s t
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))

Tactic:
obtain ⟨bc, tu⟩ := t2

Goal state after:
case some.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝¹ t✝¹ u✝¹ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝¹
s✝ u✝ t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t✝.destruct u✝.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t✝.destruct
c : α
u : WSeq α
hc : some (c, u) ∈ u✝.destruct
ab : R a b
st : LiftRel R s t
bc : R b c
tu : LiftRel R t u
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
⊢ ∀ (s : Computation (Option (α × WSeq α))),
    (∀ {s_1 : WSeq α}, s_1.destruct = s → (a ∈ s_1 ↔ a = a' ∨ a ∈ s')) →
      ∀ {s_1 : WSeq α}, s_1.destruct = s.think → (a ∈ s_1 ↔ a = a' ∨ a ∈ s')

Tactic:
intro c IH

Goal state after:
case h2
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
⊢ ∀ {s : WSeq α}, s.destruct = c.think → (a ∈ s ↔ a = a' ∨ a ∈ s')
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
this : x✝ = a' ∧ s✝ = s'
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

Tactic:
obtain ⟨i1, i2⟩ := this

Goal state after:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
b : (i : ι) × α i
i : ι
a : α i
⊢ (∃ h, h ▸ ⟨i, a⟩.snd ≤ b.snd) → ⟨i, a⟩ ≤ b

Tactic:
obtain ⟨j, b⟩ := b

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
i : ι
a : α i
j : ι
b : α j
⊢ (∃ h, h ▸ ⟨i, a⟩.snd ≤ ⟨j, b⟩.snd) → ⟨i, a⟩ ≤ ⟨j, b⟩
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
b : (i : ι) × α i
i : ι
a : α i
⊢ (∃ h, h ▸ ⟨i, a⟩.snd < b.snd) → ⟨i, a⟩ < b

Tactic:
obtain ⟨j, b⟩ := b

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
i : ι
a : α i
j : ι
b : α j
⊢ (∃ h, h ▸ ⟨i, a⟩.snd < ⟨j, b⟩.snd) → ⟨i, a⟩ < ⟨j, b⟩
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k) (h_1 : j = k), c ∈ Icc (⋯ ▸ a) (⋯ ▸ b)) ↔ (∃ (h : i = k), ⋯ ▸ a ≤ c) ∧ ∃ (h : k = j), ⋯ ▸ c ≤ b

Tactic:
mem_Icc,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k) (h_1 : j = k), ⋯ ▸ a ≤ c ∧ c ≤ ⋯ ▸ b) ↔ (∃ (h : i = k), ⋯ ▸ a ≤ c) ∧ ∃ (h : k = j), ⋯ ▸ c ≤ b
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case nil.cons
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList [], i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔ [] < head✝ :: tail✝

pp: case cons.nil
head✝ : Char
tail✝ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝ < s₂
⊢ ltb { s := ofList (head✝ :: tail✝), i := 0 } { s := ofList [], i := 0 } = true ↔ head✝ :: tail✝ < []

pp: case cons.cons
head✝¹ : Char
tail✝¹ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝¹, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝¹ < s₂
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList (head✝¹ :: tail✝¹), i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔
    head✝¹ :: tail✝¹ < head✝ :: tail✝

Tactic:
· rename_i c₂ cs₂; apply iff_of_true
    · unfold ltb
      simp [Legacy.Iterator.hasNext, Char.utf8Size_pos]
    · apply List.nil_lt_cons

Goal state after:
case cons.nil
head✝ : Char
tail✝ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝ < s₂
⊢ ltb { s := ofList (head✝ :: tail✝), i := 0 } { s := ofList [], i := 0 } = true ↔ head✝ :: tail✝ < []

case cons.cons
head✝¹ : Char
tail✝¹ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝¹, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝¹ < s₂
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList (head✝¹ :: tail✝¹), i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔
    head✝¹ :: tail✝¹ < head✝ :: tail✝
Module: Mathlib.Data.SubtypeNeLift

Goal state before:
pp: case neg
ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
φ : (i : ι) → M i
i₀ i : ι
h : ¬i = i₀
⊢ subtypeNeLift i₀ (fun i ↦ φ ↑i) (φ i₀) i = φ i

Tactic:
rw [subtypeNeLift_of_neq _ _ _ _ h]

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

Goal state before:
pp: case bisim.nil
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (nil.append (map f S.join))) (Seq.destruct (nil.append (map (map f) S).join))

pp: case bisim.cons
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
x✝ : β
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct ((cons x✝ s✝).append (map f S.join))) (Seq.destruct ((cons x✝ s✝).append (map (map f) S).join))

pp: case bisim.think
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (s✝.think.append (map f S.join))) (Seq.destruct (s✝.think.append (map (map f) S).join))

Tactic:
· induction S using WSeq.recOn with
      | nil => simp
      | cons s S => simpa using ⟨map f s, S, rfl, rfl⟩
      | think S => simpa using ⟨nil, S, by simp, by simp⟩

Goal state after:
case bisim.cons
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
x✝ : β
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct ((cons x✝ s✝).append (map f S.join))) (Seq.destruct ((cons x✝ s✝).append (map (map f) S).join))

case bisim.think
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (s✝.think.append (map f S.join))) (Seq.destruct (s✝.think.append (map (map f) S).join))
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
⊢ map₂ f (xs.snoc x) (ys.snoc y) = (map₂ f xs ys).snoc (f x y)

Tactic:
induction xs, ys using Vector.inductionOn₂

Goal state after:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
⊢ map₂ f (nil.snoc x) (nil.snoc y) = (map₂ f nil nil).snoc (f x y)

case cons
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : map₂ f (x✝.snoc x) (y✝.snoc y) = (map₂ f x✝ y✝).snoc (f x y)
⊢ map₂ f ((a✝¹ ::ᵥ x✝).snoc x) ((b✝ ::ᵥ y✝).snoc y) = (map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝)).snoc (f x y)
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
x : α
y : β
⊢ mapAccumr₂ f (xs.snoc x) (ys.snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f xs ys q.1;
    (r.1, r.2.snoc q.2)

Tactic:
induction xs, ys using Vector.inductionOn₂

Goal state after:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
x : α
y : β
⊢ mapAccumr₂ f (nil.snoc x) (nil.snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f nil nil q.1;
    (r.1, r.2.snoc q.2)

case cons
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
x : α
y : β
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ :
  mapAccumr₂ f (x✝.snoc x) (y✝.snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f x✝ y✝ q.1;
    (r.1, r.2.snoc q.2)
⊢ mapAccumr₂ f ((a✝¹ ::ᵥ x✝).snoc x) ((b✝ ::ᵥ y✝).snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) q.1;
    (r.1, r.2.snoc q.2)
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α (n + 1)
f : α → β
⊢ b = (map f v).head ∨ b ∈ (map f v).tail.toList ↔ f v.head = b ∨ ∃ a, a ∈ v.tail.toList ∧ f a = b

Tactic:
head_map,

Goal state after:
α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α (n + 1)
f : α → β
⊢ b = f v.head ∨ b ∈ (map f v).tail.toList ↔ f v.head = b ∨ ∃ a, a ∈ v.tail.toList ∧ f a = b
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
f' : α → β
s✝ : σ
h : ∀ (a : α) (s : σ), (f a s).2 = f' a
a : α
s s' : σ
x✝¹ : s ∈ Set.univ
x✝ : s' ∈ Set.univ
⊢ (f a s).2 = (f a s').2

Tactic:
by rw [h, h]

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
f' : α → β → γ
s✝ : σ
h : ∀ (a : α) (b : β) (s : σ), (f a b s).2 = f' a b
a : α
b : β
s s' : σ
x✝¹ : s ∈ Set.univ
x✝ : s' ∈ Set.univ
⊢ (f a b s).2 = (f a b s').2

Tactic:
by rw [h, h]

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
xs ys : Vector α n
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
⊢ map₂ f xs ys = map₂ f ys xs

Tactic:
induction xs, ys using Vector.inductionOn₂

Goal state after:
case nil
α : Type u_1
β : Type u_2
n : ℕ
xs ys : Vector α n
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
⊢ map₂ f nil nil = map₂ f nil nil

case cons
α : Type u_1
β : Type u_2
n : ℕ
xs ys : Vector α n
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
n✝ : ℕ
a✝¹ b✝ : α
x✝ y✝ : Vector α n✝
a✝ : map₂ f x✝ y✝ = map₂ f y✝ x✝
⊢ map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) = map₂ f (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝)
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
⊢ map₂ f xs ys = map₂ (flip f) ys xs

Tactic:
induction xs, ys using Vector.inductionOn₂

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
⊢ map₂ f nil nil = map₂ (flip f) nil nil

case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : map₂ f x✝ y✝ = map₂ (flip f) y✝ x✝
⊢ map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) = map₂ (flip f) (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝)
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
⊢ mapAccumr₂ f xs ys s = mapAccumr₂ (flip f) ys xs s

Tactic:
induction xs, ys using Vector.inductionOn₂

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
⊢ mapAccumr₂ f nil nil s = mapAccumr₂ (flip f) nil nil s

case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : mapAccumr₂ f x✝ y✝ s = mapAccumr₂ (flip f) y✝ x✝ s
⊢ mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) s = mapAccumr₂ (flip f) (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝) s