mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)

Tactic:
by
  ext (_ | _) _ <;> simp [mul_apply]

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

Goal state before:
pp: p a b : ℕ
hp : Prime p
hb : b < p
ha : a ≤ b
⊢ p.Coprime (b.choose a)

Tactic:
by
  rw [Nat.choose_eq_descFactorial_div_factorial]
  exact (hp.coprime_descFactorial_of_lt_of_le hb ha).coprime_div_right
    (Nat.factorial_dvd_descFactorial b a)

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
k : ℕ × ℕ
hm : IsUnit ↑(k.1 + k.2)!
⊢ ↑((k.1 + k.2).choose k.1) = ↑(k.1 + k.2)! * (↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ

Tactic:
rw [eq_mul_inverse_iff_mul_eq, eq_mul_inverse_iff_mul_eq, ← Nat.cast_mul, ← Nat.cast_mul,
    add_comm, Nat.add_choose_mul_factorial_mul_factorial] <;>
    apply hm.natCast_factorial_of_le

Goal state after:
case h
A : Type u_1
inst✝ : CommSemiring A
k : ℕ × ℕ
hm : IsUnit ↑(k.1 + k.2)!
⊢ k.1 ≤ k.1 + k.2

case h
A : Type u_1
inst✝ : CommSemiring A
k : ℕ × ℕ
hm : IsUnit ↑(k.1 + k.2)!
⊢ k.2 ≤ k.1 + k.2
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ↑n.divisors = {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

Tactic:
refine Set.ext fun k ↦ ⟨fun h ↦ ?_, fun ⟨f, hle, h⟩ ↦ mem_divisors.mpr ⟨?_, hn⟩⟩

Goal state after:
case refine_1
n : ℕ
hn : n ≠ 0
k : ℕ
h : k ∈ ↑n.divisors
⊢ k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

case refine_2
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∣ n
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.floorRoot 1 = 1

Tactic:
simp [floorRoot, hn]

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

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
⊢ (∑ x ∈ range (n % p + 1),
      ∑ x_1 ∈ range (n / p + 1), if k = x + p * x_1 then 1 * ↑((n % p).choose x * (n / p).choose x_1) else 0) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
← sum_product',

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
⊢ (∑ x ∈ range (n % p + 1) ×ˢ range (n / p + 1),
      if k = x.1 + p * x.2 then 1 * ↑((n % p).choose x.1 * (n / p).choose x.2) else 0) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
⊢ (map fib n.zeckendorf).sum = n

Tactic:
induction n using zeckendorf.induct <;> simp_all [fib_greatestFib_le]

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

Goal state before:
pp: k a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (p ^ k * a).choose (p ^ k * b) ≡ a.choose b [MOD p]

Tactic:
rw [← Int.natCast_modEq_iff]
  exact_mod_cast choose_pow_mul_pow_mul_modEq_choose

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

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Infinite
⊢ StrictMono (nth p)

Tactic:
by
  rw [nth_eq_orderIsoOfNat hf]
  exact (Subtype.strictMono_coe _).comp (OrderIso.strictMono _)

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

Goal state before:
pp: p : PosNum
this : (↑p).bit0 = (ZNum.pos p).bit0
⊢ ↑p.bit0 = ZNum.pos p.bit0

Tactic:
← ZNum.bit0_of_bit0

Goal state after:
p : PosNum
this : ↑p + ↑p = (ZNum.pos p).bit0
⊢ ↑p.bit0 = ZNum.pos p.bit0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑m = ↑n ↔ m = n

Tactic:
rw [← cast_to_int m, ← cast_to_int n, Int.cast_inj (α := α), to_int_inj]

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

Goal state before:
pp: ⊢ ↑(-0) = -↑0

Tactic:
by rw [Int.cast_neg]

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

Goal state before:
pp: case bit1
d n : PosNum
⊢ ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d →
    ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit1).2 +
          ↑d *
            ↑(match d.divMod n with
                | (q, r₁) => d.divModAux q r₁.bit1).1 =
        ↑n.bit1 ∧
      ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit1).2 <
        ↑d

Tactic:
obtain ⟨q, r⟩ := divMod d n

Goal state after:
case bit1
d n : PosNum
q r : Num
⊢ ↑(q, r).2 + ↑d * ↑(q, r).1 = ↑n ∧ ↑(q, r).2 < ↑d →
    ↑(match (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit1).2 +
          ↑d *
            ↑(match (q, r) with
                | (q, r₁) => d.divModAux q r₁.bit1).1 =
        ↑n.bit1 ∧
      ↑(match (q, r) with
            | (q, r₁) => d.divModAux q r₁.bit1).2 <
        ↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (x.approx n.succ) = head' (x.approx (succ 0))
n : ℕ
P' : Agree (x.approx n.succ) (x.approx n.succ.succ)
⊢ cast ⋯ i ≍ cast ⋯ i

Tactic:
trans i

Goal state after:
F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (x.approx n.succ) = head' (x.approx (succ 0))
n : ℕ
P' : Agree (x.approx n.succ) (x.approx n.succ.succ)
⊢ cast ⋯ i ≍ i

F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (x.approx n.succ) = head' (x.approx (succ 0))
n : ℕ
P' : Agree (x.approx n.succ) (x.approx n.succ.succ)
⊢ i ≍ cast ⋯ i
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit0
d n : PosNum
⊢ ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d →
    ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit0).2 +
          ↑d *
            ↑(match d.divMod n with
                | (q, r₁) => d.divModAux q r₁.bit0).1 =
        ↑n.bit0 ∧
      ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit0).2 <
        ↑d

Tactic:
obtain ⟨q, r⟩ := divMod d n

Goal state after:
case bit0
d n : PosNum
q r : Num
⊢ ↑(q, r).2 + ↑d * ↑(q, r).1 = ↑n ∧ ↑(q, r).2 < ↑d →
    ↑(match (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit0).2 +
          ↑d *
            ↑(match (q, r) with
                | (q, r₁) => d.divModAux q r₁.bit0).1 =
        ↑n.bit0 ∧
      ↑(match (q, r) with
            | (q, r₁) => d.divModAux q r₁.bit0).2 <
        ↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case cons
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_hd : F.Idx
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → iselect ps_tail x = default.head
x : F.M
h : ¬IsPath (ps_hd :: ps_tail) x
⊢ iselect (ps_hd :: ps_tail) x = default.head

Tactic:
obtain ⟨a, i⟩ := ps_hd

Goal state after:
case cons
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → iselect ps_tail x = default.head
x : F.M
a : F.A
i : F.B a
h : ¬IsPath (⟨a, i⟩ :: ps_tail) x
⊢ iselect (⟨a, i⟩ :: ps_tail) x = default.head
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
l' : ℕ
e : Raised l' l.size
H : BalancedSz l' r.size
⊢ ∃ l' r', BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')

Tactic:
exact ⟨_, _, H, Or.inl ⟨e.dist_le', rfl⟩⟩

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case refine_1.left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁✝ : ι
i : α a₁✝
a₂✝ : ι
a : α a₂✝
hji : a₁✝ < a₂✝
hij : a₂✝ < a₁✝
⊢ False

pp: case refine_1.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁✝ : ι
i a : α a₁✝
hji : a₁✝ < a₁✝
hab : a < i
⊢ False

pp: case refine_1.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hij : i < i
⊢ False

pp: case refine_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hab : b₂✝ < b₁✝
⊢ False

Tactic:
· exact hij.not_gt hji

Goal state after:
case refine_1.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁✝ : ι
i a : α a₁✝
hji : a₁✝ < a₁✝
hab : a < i
⊢ False

case refine_1.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hij : i < i
⊢ False

case refine_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hab : b₂✝ < b₁✝
⊢ False
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
⊢ 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size

Tactic:
intro _ _

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
a✝¹ : 1 ≤ t.size
a✝ : 1 ≤ rr.size
⊢ rr.size ≤ delta * t.size
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t ↑rx
e : t.size = ls + rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
rw [hl.2.1] at e
  rw [hl.2.1, hr.2.1, delta] at h
  rcases hr.3.1 with (H | ⟨hr₁, hr₂⟩); · lia
  suffices H₂ : _ by
    suffices H₁ : _ by
      refine ⟨Valid'.balanceL_aux v hr.right H₁ H₂ ?_, ?_⟩
      · rw [e]; exact Or.inl (Valid'.merge_lemma h hr₁)
      · rw [balanceL_eq_balance v.2 hr.2.2.2 H₁ H₂, balance_eq_balance' v.3 hr.3.2.2 v.2 hr.2.2.2,
          size_balance' v.2 hr.2.2.2, e, hl.2.1, hr.2.1]
        abel
    · rw [e, add_right_comm]; rintro ⟨⟩
  intro _ _; rw [e]; unfold delta at hr₂ ⊢; lia

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

Goal state before:
pp: case node.bal.right
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (map f l✝).Balanced ∧ (map f r✝).Balanced

Tactic:
· constructor
        · exact t_l_valid.bal
        · exact t_r_valid.bal

Goal state after:
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 (wrepr ((P F).wMk a f' f)) ((P F).wMk' ((TypeVec.id ::: wrepr) <$$> ⟨a, (P F).appendContents f' f⟩))

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' ((TypeVec.id ::: wrepr) <$$> ⟨a, (P F).appendContents f' f⟩)) ((P F).wMk a f' f)

Tactic:
· apply wEquiv.abs'
      rw [wrepr_wMk, q.P.wDest'_wMk', q.P.wDest'_wMk', abs_repr]

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)
⊢ WEquiv ((P F).wMk' ((TypeVec.id ::: wrepr) <$$> ⟨a, (P F).appendContents f' f⟩)) ((P F).wMk a f' f)
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
⊢ (TypeVec.id ::: Quot.mk r') <$$> x.dest = (TypeVec.id ::: Quot.mk r') <$$> y.dest

Tactic:
have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
      rw [← Quot.factor_mk_eq _ _ this]
      dsimp [r']
      rw [appendFun_comp_id]
      rw [@comp_map _ _ q _ _ _ (appendFun id (Quot.mk r)),
        @comp_map _ _ q _ _ _ (appendFun id (Quot.mk r))]
      rw [h _ _ r'xy]

Goal state after:
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 := ⋯
x y : Cofix F α
rxy : r x y
⊢ ∀ (x y : Cofix F α), r' x y → (TypeVec.id ::: Quot.mk r') <$$> x.dest = (TypeVec.id ::: Quot.mk r') <$$> y.dest

Tactic:
intro x y r'xy
    cases r'xy with
    | inl h =>
      rw [h]
    | inr r'xy =>
      have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
      rw [← Quot.factor_mk_eq _ _ this]
      dsimp [r']
      rw [appendFun_comp_id]
      rw [@comp_map _ _ q _ _ _ (appendFun id (Quot.mk r)),
        @comp_map _ _ q _ _ _ (appendFun id (Quot.mk r))]
      rw [h _ _ r'xy]

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

Goal state before:
pp: case inr.inl
⊢ sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1

pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Tactic:
· exact Or.inr <| Or.inl <| sign_zero

Goal state after:
case inr.inr
r : ℝ
hp : 0 < r
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
z : ℤ
hn : z < 0
⊢ -1 = -↑1

Tactic:
Int.cast_one

Goal state after:
case inl
z : ℤ
hn : z < 0
⊢ -1 = -1
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
z : ℤ
hp : 0 < z
⊢ 1 = ↑1

Tactic:
Int.cast_one

Goal state after:
case inr.inr
z : ℤ
hp : 0 < z
⊢ 1 = 1
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
p : ↑((P F₂).comp (P F₁)) α
⊢ F₂ (F₁ α)

Tactic:
exact abs ⟨p.1.1, fun x => abs ⟨p.1.2 x, fun y => p.2 ⟨x, y⟩⟩⟩

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

Goal state before:
pp: 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 (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inl i) =
    Sum.elim _root_.id (corec' g) (Sum.inl i)

Tactic:
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)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: 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 (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inr i) =
    Sum.elim _root_.id (corec' g) (Sum.inr i)

Tactic:
corec_roll

Goal state after:
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: case some
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
val : Seq1 (Option α)
⊢ match
    match
      match some val with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c ↦
              match c.destruct with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    some val with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c ↦
            match c.destruct with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Tactic:
obtain ⟨o, s'⟩ := val
    simp

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a : WSeq α
b : WSeq β
⊢ LiftRel R a b → Computation.LiftRel (LiftRelO R S) a.destruct b.destruct

Tactic:
ab

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a : WSeq α
b : WSeq β
ab : LiftRel R a b
⊢ Computation.LiftRel (LiftRelO R S) a.destruct b.destruct
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case refine_1.left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ j✝ : ι
b : α i✝
a : α j✝
hji : i✝ < j✝
hij : j✝ < i✝
⊢ False

pp: case refine_1.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hji : i✝ < i✝
hab : a < b
⊢ False

pp: case refine_1.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hij : i✝ < i✝
⊢ False

pp: case refine_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hab : a < b
⊢ False

Tactic:
· exact hij.not_gt hji

Goal state after:
case refine_1.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hji : i✝ < i✝
hab : a < b
⊢ False

case refine_1.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hij : i✝ < i✝
⊢ False

case refine_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hab : a < b
⊢ False
Module: Mathlib.Data.WSeq.Basic

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

Tactic:
rcases o with e | IH

Goal state after:
case intro.inl
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons x✝ (s✝.append S.join)
m : a = x✝ ∨ a ∈ s✝.append S.join
e : a = x✝
⊢ (a = x✝ ∨ a ∈ s✝) ∨ ∃ s ∈ S, a ∈ s

case intro.inr
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons x✝ (s✝.append S.join)
m : a = x✝ ∨ a ∈ s✝.append S.join
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    s.append S_1.join = s✝.append S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
⊢ (a = x✝ ∨ a ∈ s✝) ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
⊢ C a

Tactic:
by
  let T : WSeq (Computation (α × Computation α)) := S.map fun c => c.map fun a => (a, c)
  have : S = T.map (map fun c => c.1) := by
    rw [← WSeq.map_comp]
    refine (WSeq.map_id _).symm.trans (congr_arg (fun f => WSeq.map f S) ?_)
    funext c
    dsimp [id, Function.comp_def]
    rw [← map_comp]
    exact (map_id _).symm
  have pe := congr_arg parallel this
  rw [← map_parallel] at pe
  have h' := h
  rw [pe] at h'
  haveI : Terminates (parallel T) := (terminates_map_iff _ _).1 ⟨⟨_, h'⟩⟩
  rcases e : get (parallel T) with ⟨a', c⟩
  have : a ∈ c ∧ c ∈ S := by
    rcases exists_of_mem_map h' with ⟨d, dT, cd⟩
    rw [get_eq_of_mem _ dT] at e
    cases e
    dsimp at cd
    cases cd
    rcases exists_of_mem_parallel dT with ⟨d', dT', ad'⟩
    rcases WSeq.exists_of_mem_map dT' with ⟨c', cs', e'⟩
    rw [← e'] at ad'
    rcases exists_of_mem_map ad' with ⟨a', ac', e'⟩
    injection e' with i1 i2
    constructor
    · rwa [i1, i2] at ac'
    · rwa [i2] at cs'
  obtain ⟨ac, cs⟩ := this
  apply H _ cs _ ac

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_2
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (VectorAllP p (a :: w) ↔ ∀ (i : Fin2 (n + 1)), p ((a :: w) i))

Tactic:
· simp only [vectorAllP_cons]
    refine fun {n} a v IH =>
      (and_congr_right fun _ => IH).trans
        ⟨fun ⟨pa, h⟩ i => by
          refine i.cases' ?_ ?_
          exacts [pa, h], fun h => ⟨?_, fun i => ?_⟩⟩
    · simpa using h fz
    · simpa using h (fs i)

Goal state after:
Module: Mathlib.Order.SemiconjSup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
⊢ IsOrderRightAdjoint (f ∘ ⇑e) (⇑e.symm ∘ g)

Tactic:
intro y
  change IsLUB (e ⁻¹' { x | f x ≤ y }) (e.symm (g y))
  rw [e.isLUB_preimage, e.apply_symm_apply]
  exact h y

Goal state after: