mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case zero.f.f
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
z : F.M
a✝¹ : F.A
f✝¹ : F.B a✝¹ → F.M
hx : Agree' 0 z (M.mk ⟨a✝¹, f✝¹⟩)
a✝ : F.A
f✝ : F.B a✝ → F.M
hy : Agree' 0 z (M.mk ⟨a✝, f✝⟩)
hrec : a✝¹ = a✝
⊢ (M.mk ⟨a✝¹, f✝¹⟩).approx (0 + 1) = (M.mk ⟨a✝, f✝⟩).approx (0 + 1)

Tactic:
subst hrec

Goal state after:
case zero.f.f
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
z : F.M
a✝ : F.A
f✝¹ : F.B a✝ → F.M
hx : Agree' 0 z (M.mk ⟨a✝, f✝¹⟩)
f✝ : F.B a✝ → F.M
hy : Agree' 0 z (M.mk ⟨a✝, f✝⟩)
⊢ (M.mk ⟨a✝, f✝¹⟩).approx (0 + 1) = (M.mk ⟨a✝, f✝⟩).approx (0 + 1)
Module: Mathlib.Data.Ordmap.Ordset

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

pp: case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : l.size > delta * r.size
⊢ Valid' o₁ (l.rotateR x r) o₂

pp: case neg
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : ¬l.size > delta * r.size
⊢ Valid' o₁ (l.node' x r) o₂

Tactic:
· exact hl.rotateL hr h h_1 H₁

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : l.size > delta * r.size
⊢ Valid' o₁ (l.rotateR x r) o₂

case neg
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : ¬l.size > delta * r.size
⊢ Valid' o₁ (l.node' x r) o₂
Module: Mathlib.Data.PFunctor.Univariate.M

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

Tactic:
simp only [dest_mk] at h₀ h₁

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk a f) ⟹ α
i : Fin2 n
x : P.WPath (WType.mk a f) i
⊢ P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) i x = h i x

Tactic:
cases x <;> rfl

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
x : P.WPath (WType.mk a f) i
⊢ (h ⊚ P.wPathCasesOn g' g) i x = P.wPathCasesOn (h ⊚ g') (fun i ↦ h ⊚ g i) i x

Tactic:
cases x <;> rfl

Goal state after:
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₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a, f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)

Tactic:
simp only [dest_mk] at h₀ h₁

Goal state after:
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)
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
⊢ ∃ b, ⟨i, a⟩ < b

Tactic:
obtain ⟨b⟩ : Nonempty (α j) := inferInstance

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
b : α j
⊢ ∃ b, ⟨i, a⟩ < b
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : j < i
⊢ ∃ b, b < ⟨i, a⟩

Tactic:
obtain ⟨b⟩ : Nonempty (α j) := inferInstance

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : j < i
b : α j
⊢ ∃ b, b < ⟨i, a⟩
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case right.left
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ a = a' * d

Tactic:
exact eq ha''

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

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ) → u ∈ f i✝ '' univ

pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ u ∈ f i✝ '' univ → ∀ (a_2 : (P F).A) (f_1 : (P F).B a_2 ⟹ α), abs ⟨a_2, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ

Tactic:
· intro h'
    apply h' _ _ rfl

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ u ∈ f i✝ '' univ → ∀ (a_2 : (P F).A) (f_1 : (P F).B a_2 ⟹ α), abs ⟨a_2, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv ((P F).wMk a (dropFun (splitFun f' (wrepr ∘ f))) (lastFun (splitFun f' (wrepr ∘ f)))) ((P F).wMk a f' f)

Tactic:
apply WEquiv.ind

Goal state after:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), WEquiv (wrepr (f i)) (f i)
⊢ ∀ (x : (P F).last.B a), WEquiv (lastFun (splitFun f' (wrepr ∘ f)) x) (f x)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case ind
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ WEquiv ((P F).wMk a (g ⊚ f') fun i ↦ g <$$> f₀ i) ((P F).wMk a (g ⊚ f') fun i ↦ g <$$> f₁ i)

Tactic:
apply WEquiv.ind

Goal state after:
case ind
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ ∀ (x : (P F).last.B a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
t : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ t a₂
h_mem : x ∈ t
⊢ (erase x t).size = t.size - 1

Tactic:
by
  induction t generalizing a₁ a₂ with
  | nil =>
    contradiction
  | node _ t_l t_x t_r 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
    dsimp only [Membership.mem, mem] at h_mem
    unfold erase
    revert h_mem; cases cmpLE x t_x <;> intro h_mem <;> dsimp only at h_mem ⊢
    · have t_ih_l := t_ih_l' h_mem
      clear t_ih_l' t_ih_r'
      have t_l_h := Valid'.erase_aux x h.left
      obtain ⟨t_l_valid, t_l_size⟩ := t_l_h
      rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz
          (Or.inl (Exists.intro t_l.size (And.intro t_l_size h.bal.1)))]
      rw [t_ih_l, h.sz.1]
      have h_pos_t_l_size := pos_size_of_mem h.left.sz h_mem
      revert h_pos_t_l_size; rcases t_l.size with - | t_l_size <;> intro h_pos_t_l_size
      · cases h_pos_t_l_size
      · simp [Nat.add_right_comm]
    · rw [(Valid'.glue h.left h.right h.bal.1).2, h.sz.1]; rfl
    · have t_ih_r := t_ih_r' h_mem
      clear t_ih_l' t_ih_r'
      have t_r_h := Valid'.erase_aux x h.right
      obtain ⟨t_r_valid, t_r_size⟩ := t_r_h
      rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz
          (Or.inr (Exists.intro t_r.size (And.intro t_r_size h.bal.1)))]
      rw [t_ih_r, h.sz.1]
      have h_pos_t_r_size := pos_size_of_mem h.right.sz h_mem
      revert h_pos_t_r_size; rcases t_r.size with - | t_r_size <;> intro h_pos_t_r_size
      · cases h_pos_t_r_size
      · simp [Nat.add_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
t : Ordset α
h_mem : x ∈ t
⊢ 0 < t.size

Tactic:
by
  simp only [Membership.mem, mem, Bool.decide_eq_true] at h_mem
  apply Ordnode.pos_size_of_mem t.property.sz h_mem

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
x : Cofix F α
⊢ mk x.dest = x

Tactic:
apply Cofix.bisim_rel (fun x y : Cofix F α => x = Cofix.mk (Cofix.dest y)) _ _ _ rfl
  intro x y h
  rw [h]
  conv =>
    lhs
    congr
    rfl
    rw [Cofix.mk]
    rw [Cofix.dest_corec]
  rw [← comp_map, ← appendFun_comp, id_comp]
  rw [← comp_map, ← appendFun_comp, id_comp, ← Cofix.mk]
  congr 1
  apply congrArg
  funext x
  apply Quot.sound
  rfl

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
x : F (α ::: Cofix F α)
⊢ (mk x).dest = x

Tactic:
have : Cofix.mk ∘ Cofix.dest = @_root_.id (Cofix F α) := funext Cofix.mk_dest
  rw [Cofix.mk, Cofix.dest_corec, ← comp_map, ← Cofix.mk, ← appendFun_comp, this, id_comp,
    appendFun_id_id, MvFunctor.id_map]

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Tactic:
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
  · exact Or.inl <| sign_of_neg hn
  · exact Or.inr <| Or.inl <| sign_zero
  · exact Or.inr <| Or.inr <| sign_of_pos hp

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

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ) → u ∈ f '' univ

pp: case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
⊢ u ∈ f '' univ → ∀ (a_2 : (P F).A) (f_1 : (P F).B a_2 → α), abs ⟨a_2, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ

Tactic:
· intro h'
    apply h' _ _ rfl

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
⊢ u ∈ f '' univ → ∀ (a_2 : (P F).A) (f_1 : (P F).B a_2 → α), abs ⟨a_2, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
s' : Seq (Option α)
⊢ ∀ ⦃s₂ : Seq (Option α)⦄,
    (fun s1 s2 ↦ flatten (Computation.pure s2) = s1) s' s₂ →
      Seq.BisimO (fun s1 s2 ↦ flatten (Computation.pure s2) = s1) s'.destruct s₂.destruct

Tactic:
s

Goal state after:
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
⊢ (fun s1 s2 ↦ flatten (Computation.pure s2) = s1) s' s →
    Seq.BisimO (fun s1 s2 ↦ flatten (Computation.pure s2) = s1) s'.destruct s.destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
S : WSeq (WSeq α)
⊢ S.think.join = S.join.think

Tactic:
simp only [join, think]

Goal state after:
α : Type u
S : WSeq (WSeq α)
⊢ ((fun o ↦
          match o with
          | none => Seq1.ret none
          | some s => (none, s)) <$>
        Seq.cons none S).join =
    Seq.cons none
      ((fun o ↦
            match o with
            | none => Seq1.ret none
            | some s => (none, s)) <$>
          S).join
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
S : WSeq (WSeq α)
⊢ (cons s S).join = (s.append S.join).think

Tactic:
simp only [join, think]

Goal state after:
α : Type u
s : WSeq α
S : WSeq (WSeq α)
⊢ ((fun o ↦
          match o with
          | none => Seq1.ret none
          | some s => (none, s)) <$>
        cons s S).join =
    Seq.cons none
      (s.append
        ((fun o ↦
              match o with
              | none => Seq1.ret none
              | some s => (none, s)) <$>
            S).join)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ (↑(s.drop n)).tail = ↑(s.drop n).tail

Tactic:
tail_ofSeq

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ ↑(s.drop n).tail = ↑(s.drop n).tail
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
⊢ ∃ b, ⟨i, a⟩ < b

Tactic:
obtain ⟨b⟩ : Nonempty (α j) := inferInstance

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
b : α j
⊢ ∃ b, ⟨i, a⟩ < b
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : j < i
⊢ ∃ b, b < ⟨i, a⟩

Tactic:
obtain ⟨b⟩ : Nonempty (α j) := inferInstance

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : j < i
b : α j
⊢ ∃ b, b < ⟨i, a⟩
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h1
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
have e' := congr_arg destruct e

Goal state after:
case h1
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
e' : (corec parallel.aux1 (l, S)).destruct = (pure a).destruct
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h2
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
have e' := congr_arg destruct e

Goal state after:
case h2
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
e' : (corec parallel.aux1 (l, S)).destruct = C'.think.destruct
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
⊢ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s

Tactic:
s

Goal state after:
case h1
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s : WSeq α
⊢ ∀ (S : WSeq (WSeq α)), s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
⊢ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss.think → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s

Tactic:
s

Goal state after:
case h2
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s : WSeq α
⊢ ∀ (S : WSeq (WSeq α)), s.append S.join = ss.think → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)), corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
apply memRecOn aC <;> [skip; intro C' IH] <;> intro l S e <;> have e' := congr_arg destruct e <;>
    have := lem1 l <;> simp only [parallel.aux1, corec_eq, destruct_pure, destruct_think] at e' <;>
    revert this e' <;> rcases parallel.aux2 l with a' | l' <;> intro this e' <;>
    [injection e' with h'; injection e'; injection e'; injection e' with h']

Goal state after:
case h1.inl
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
a' : α
this : F l (Sum.inl a')
h' : a' = a
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

case h2.inr
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
h' :
  corec parallel.aux1
      ((fun l' ↦
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        l') =
    C'
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.String.Basic

Goal state before:
pp: c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
this :
  ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ } { s := ofList (c₁ :: cs₂), i := 0 + c₁ } =
    ltb { s := ofList cs₁, i := 0 } { s := ofList cs₂, i := 0 }
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ } { s := ofList (c₁ :: cs₂), i := 0 + c₁ } = true ↔ c₁ :: cs₁ < c₁ :: cs₂

Tactic:
rw [this]; exact (ih cs₂).trans List.lex_cons_iff.symm

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

Goal state before:
pp: α : Type u
s s' : WSeq α
⊢ ∀ {t : WSeq α},
    (fun s1 s2 ↦ (map ret s2).join = s1) s' t →
      Computation.LiftRel (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1) s'.destruct t.destruct

Tactic:
s

Goal state after:
α : Type u
s✝ s' s : WSeq α
⊢ (fun s1 s2 ↦ (map ret s2).join = s1) s' s →
    Computation.LiftRel (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1) s'.destruct s.destruct
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: α : Type u_1
k : ℕ
⊢ Nat.card (Sym α k) = (Nat.card α + k - 1).choose k

Tactic:
natCard_sym_eq_multichoose,

Goal state after:
α : Type u_1
k : ℕ
⊢ (Nat.card α).multichoose k = (Nat.card α + k - 1).choose k
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (map ret (map f s)).join ~ʷ map f s

Tactic:
apply join_map_ret

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

Goal state before:
pp: α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
h1 : s1 = s.append (S.append SS.join).join
h2 : s2 = s.append (S.join.append (map join SS).join)
⊢ s2.destruct = (s.append (S.join.append (map join SS).join)).destruct

Tactic:
simp [h2]

Goal state after:
Module: Mathlib.Data.ZMod.Coprime

Goal state before:
pp: a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ ¬(↑p).gcd a = 1

Tactic:
← Int.isCoprime_iff_gcd_eq_one,

Goal state after:
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ ¬IsCoprime (↑p) a
Module: Mathlib.Dynamics.Ergodic.Action.Basic

Goal state before:
pp: case refine_2
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h : Ergodic f μ
⊢ ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)

Tactic:
intro s hm hs
    exact h.quasiErgodic.aeconst_set₀ hm.nullMeasurableSet <| hs (.mk 1)

Goal state after: