mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s).PairwiseDisjoint Finsupp.support
this : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ (s.sum id).support = s.sup Finsupp.support

Tactic:
convert! Multiset.support_sum_eq s.1 this

Goal state after:
case e'_2
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s).PairwiseDisjoint Finsupp.support
this : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ s.sum id = s.val.sum
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ f.neLocus (f - g) = g.support

Tactic:
rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false
n : ℤ
⊢ bit false n = 2 * n + bif false then 1 else 0

pp: case true
n : ℤ
⊢ bit true n = 2 * n + bif true then 1 else 0

Tactic:
· apply (add_zero _).symm

Goal state after:
case true
n : ℤ
⊢ bit true n = 2 * n + bif true then 1 else 0
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
hn : 0 ≤ b
⊢ |a| ≤ sqrt ↑b.toNat ↔ |a| * |a| ≤ ↑b.toNat

Tactic:
eq_natCast_toNat.mpr (abs_nonneg a),

Goal state after:
a b : ℤ
hn : 0 ≤ b
⊢ ↑|a|.toNat ≤ sqrt ↑b.toNat ↔ ↑|a|.toNat * ↑|a|.toNat ≤ ↑b.toNat
Module: Mathlib.Data.List.Indexes

Goal state before:
pp: case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
this : (arr.push PUnit.unit).size = arr.size + 1
⊢ (do
      head
      mapIdxMAux' f (arr.size + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)

Tactic:
← this,

Goal state after:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
this : (arr.push PUnit.unit).size = arr.size + 1
⊢ (do
      head
      mapIdxMAux' f (arr.push PUnit.unit).size tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ (takeWhile p l.reverse ++ dropWhile p l.reverse).reverse = l

Tactic:
takeWhile_append_dropWhile,

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ l.reverse.reverse = l
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
| (map length ((take (i + 1) sz).splitLengths l))[i]

Tactic:
rw [getElem_map]

Goal state after:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
| ((take (i + 1) sz).splitLengths l)[i].length
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: case h2
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ snd (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) i✝ j✝ =
    (fst (of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) •
          snd (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j)) +
        MulOpposite.op (fst (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))) •
          snd (of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)))
      i✝ j✝

Tactic:
smul_eq_mul,

Goal state after:
case h2
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ snd (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) i✝ j✝ =
    (fst (of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) *
          snd (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j)) +
        MulOpposite.op (fst (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))) •
          snd (of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)))
      i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: case h2
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ ∑ x, (fst (A i✝ x) * snd (B x j✝) + snd (A i✝ x) * fst (B x j✝)) =
    ∑ x, fst (A i✝ x) * snd (B x j✝) + ∑ x, snd (A i✝ x) * fst (B x j✝)

Tactic:
rw [← Finset.sum_add_distrib]

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
v₁ : n₁ → R
v₂ : n₂ → R
x✝ : m
⊢ (A₁.fromCols A₂ *ᵥ Sum.elim v₁ v₂) x✝ = (A₁ *ᵥ v₁ + A₂ *ᵥ v₂) x✝

Tactic:
simp [Matrix.mulVec, fromCols]

Goal state after:
Module: Mathlib.Data.Multiset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.Icc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)

Tactic:
by
  simp_rw [Icc_eq, Finset.card_map, DFinsupp.card_Icc, Nat.card_Icc, Multiset.toDFinsupp_apply,
    toDFinsupp_support]

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case empty
α : Type u_1
inst✝ : Preorder α
M : Multiset α
hM : ∀ (x : α), x ∈ 0 → Acc LT.lt x
⊢ Acc OneStep 0

Tactic:
constructor
    simp [OneStep, eq_comm (b := _ + _)]

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
hs : ∀ i ∈ l, s i ≠ 0
⊢ ↑(chineseRemainderOfList a s l co) < (List.map s l).prod

Tactic:
cases l with
  | nil => simp
  | cons i l =>
    simp only [chineseRemainderOfList, List.map_cons, List.prod_cons]
    have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
    refine chineseRemainder_lt_mul this (a i) (chineseRemainderOfList a s l co.of_cons)
      (hs i List.mem_cons_self) ?_
    simp only [ne_eq, List.prod_eq_zero_iff, List.mem_map, not_exists, not_and]
    intro j hj
    exact hs j (List.mem_cons_of_mem _ hj)

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

Goal state before:
pp: A : Type u_1
inst✝² : Ring A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP A p
n : ℕ
⊢ IsUnit ↑n ! ↔ n < p

Tactic:
have hp : p.Prime := Fact.out

Goal state after:
A : Type u_1
inst✝² : Ring A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP A p
n : ℕ
hp : Nat.Prime p
⊢ IsUnit ↑n ! ↔ n < p
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:
by
  rw [← Int.natCast_modEq_iff]
  exact_mod_cast choose_pow_mul_pow_mul_modEq_choose

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

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ ((Icc 1 (n - 1)).gcd n.choose).primeFactors = {n.minFac}

Tactic:
have ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0 :=
    gcd_ne_zero_iff.mpr ⟨1, by simp; grind [IsPrimePow.two_le h]⟩

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
⊢ ((Icc 1 (n - 1)).gcd n.choose).primeFactors = {n.minFac}
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ (Icc 1 (n - 1)).gcd n.choose = n.minFac

Tactic:
have ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0 :=
    gcd_ne_zero_iff.mpr ⟨1, by simp; grind [IsPrimePow.two_le h]⟩

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
⊢ (Icc 1 (n - 1)).gcd n.choose = n.minFac
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : n ≡ 0 [MOD q]
this✝ : Fact (Nat.Prime q)
this : n = q ^ multiplicity q n
⊢ q ∣ n

Tactic:
modEq_zero_iff_dvd

Goal state after:
n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : q ∣ n
this✝ : Fact (Nat.Prime q)
this : n = q ^ multiplicity q n
⊢ q ∣ n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case succ.refine_1
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ {x | p x ∧ ∀ k < n + 1, nth p k < x}.Nonempty

Tactic:
use nth p (n + 1), nth_mem _ hn
      exact fun k hk => nth_lt_nth' hk hn

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑n.bitm1 = ↑n + ↑n - 1

Tactic:
by
  conv =>
    lhs
    rw [← zneg_zneg n]
  rw [← zneg_bit1, cast_zneg, cast_bit1]
  have : ((-1 + n + n : ℤ) : α) = (n + n + -1 : ℤ) := by simp [add_comm]
  simpa [sub_eq_add_neg] using this

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

Goal state before:
pp: p : PosNum
⊢ ↑p.bit1 = ZNum.pos p.bit1

Tactic:
by
      have := congr_arg ZNum.bit1 (cast_to_znum p)
      rwa [← ZNum.bit1_of_bit1] at this

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ¬↑n < ↑m ↔ m ≤ n

Tactic:
exact not_congr cast_lt

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

Goal state before:
pp: case inr.inr
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
rw [Nat.mul_succ]

Goal state after:
case inr.inr
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * l.size + 3
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
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₀ : (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)
⊢ a = a'

Tactic:
clear 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₀ : (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)
⊢ a = a'
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
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:
clear 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₀ : (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)
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: u v : PrimeMultiset
h : u ≤ v ↔ u.prod ∣ v.prod
⊢ u.prod ∣ v.prod ↔ u ≤ v

Tactic:
exact h.symm

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

Goal state before:
pp: u v : PrimeMultiset
⊢ (u ⊓ v).prod = u.prod.gcd v.prod

Tactic:
let n := u.prod

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
⊢ (u ⊓ v).prod = u.prod.gcd v.prod
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: u v : PrimeMultiset
⊢ (u ⊔ v).prod = u.prod.lcm v.prod

Tactic:
let n := u.prod

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
⊢ (u ⊔ v).prod = u.prod.lcm v.prod
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case mp
u : XgcdType
h : u.bp = u.ap
⊢ u.ap = u.bp

Tactic:
exact h.symm

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

Goal state before:
pp: case mpr
u : XgcdType
h : u.ap = u.bp
⊢ u.bp = u.ap

Tactic:
exact h.symm

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

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ x✝.reduce.IsReduced

Tactic:
reduce_b h,

Goal state after:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.flip.IsReduced
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ x✝.reduce.v = x✝.v

Tactic:
reduce_b h,

Goal state after:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.flip.v = x✝.v
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.left
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₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
⊢ abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b₁) = abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b₂)

Tactic:
let u : Quot r → Quot r' :=
          Quot.lift (fun x : q.P.M α => Quot.mk r' (g <$$> x))
            (by
              intro a₁ a₂ ra₁a₂
              apply Quot.sound
              exact ⟨a₁, a₂, ra₁a₂, rfl, rfl⟩)

Goal state after:
case h.left
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₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
⊢ abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b₁) = abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b₂)
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
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
⊢ ∀ u_1 ∈ f' u '' univ, p u u_1

Tactic:
rintro b ⟨i, _, hi⟩

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
b : α u
i : (P F).B a' u
left✝ : i ∈ univ
hi : f' u i = b
⊢ p u b
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case left
α : 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
h_balanceable : ?m.149
⊢ Valid' a₁
    (match Ordering.lt with
    | Ordering.lt => (erase x t_l).balanceR t_x t_r
    | Ordering.eq => t_l.glue t_r
    | Ordering.gt => t_l.balanceL t_x (erase x t_r))
    a₂

pp: case right
α : 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
h_balanceable : ?m.149
⊢ Raised
    (match Ordering.lt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
    (t_l.size + t_r.size + 1)

Tactic:
· exact Valid'.balanceR t_l_valid h.right h_balanceable

Goal state after:
case right
α : 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
h_balanceable :
  (∃ 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'
⊢ Raised
    (match Ordering.lt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
    (t_l.size + t_r.size + 1)
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 : 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 y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)

Tactic:
← this,

Goal state after:
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 y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ MvQPF.abs ((TypeVec.id ::: f ∘ Quot.mk r ∘ Quot.mk Mcongr) <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: f ∘ Quot.mk r ∘ Quot.mk Mcongr) <$$> M.dest (P F) b)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs a.dest = Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest
h₁ : ∀ (u v : (P F).M), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ abs ((P F).map (Quot.mk r') a.dest) = abs ((P F).map (Quot.mk r') b.dest)

Tactic:
← this,

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs a.dest = Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest
h₁ : ∀ (u v : (P F).M), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ abs ((P F).map (f ∘ Quot.mk r ∘ Quot.mk Mcongr) a.dest) = abs ((P F).map (f ∘ Quot.mk r ∘ Quot.mk Mcongr) b.dest)
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
⊢ ∀ {α : TypeVec.{u} n} (x : Fix F α), Quot.mk WEquiv (fixToW x) = x

Tactic:
by
    intro α
    apply Quot.ind
    intro a
    apply Quot.sound
    apply wrepr_equiv

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

Goal state before:
pp: r : ℝ
⊢ (-r).sign = -r.sign

Tactic:
by
  obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
  · rw [sign_of_neg hn, sign_of_pos (neg_pos.mpr hn), neg_neg]
  · rw [sign_zero, neg_zero, sign_zero]
  · rw [sign_of_pos hp, sign_of_neg (neg_lt_zero.mpr hp)]

Goal state after:
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
x : F₂ (F₁ α)
⊢ abs ⟨(repr x).fst, fun x_1 ↦ abs ⟨(repr ((repr x).snd x_1)).fst, fun y ↦ (repr ((repr x).snd x_1)).snd y⟩⟩ = x

Tactic:
conv =>
      rhs
      rw [← abs_repr x]

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
x : F₂ (F₁ α)
⊢ abs ⟨(repr x).fst, fun x_1 ↦ abs ⟨(repr ((repr x).snd x_1)).fst, fun y ↦ (repr ((repr x).snd x_1)).snd y⟩⟩ =
    abs (repr x)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
a : α × WSeq α
h : some a ∈ instAlternativeComputation.toFunctor.1 (fun o ↦ Option.rec nil Prod.snd o) s.destruct >>= destruct
t : WSeq α
tm : t ∈ instAlternativeComputation.toFunctor.1 (fun o ↦ Option.rec nil Prod.snd o) s.destruct
td : some a ∈ t.destruct
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
clear h

Goal state after:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
tm : t ∈ instAlternativeComputation.toFunctor.1 (fun o ↦ Option.rec nil Prod.snd o) s.destruct
td : some a ∈ t.destruct
⊢ ∃ a', some a' ∈ s.destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
a : α
h : some a ∈ Computation.map (fun x ↦ Prod.fst <$> x) s.tail.destruct
o : Option (α × WSeq α)
md : o ∈ s.tail.destruct
e : Prod.fst <$> o = some a
⊢ ∃ a', some a' ∈ s.head

Tactic:
clear h

Goal state after:
α : Type u
s : WSeq α
a : α
o : Option (α × WSeq α)
md : o ∈ s.tail.destruct
e : Prod.fst <$> o = some a
⊢ ∃ a', some a' ∈ s.head
Module: Mathlib.Data.Set.FiniteExhaustion

Goal state before:
pp: α : Type u_1
s : Set α
⊢ Nonempty s.FiniteExhaustion ↔ s.Countable

Tactic:
refine ⟨fun ⟨K⟩ ↦ ?_, fun h ↦ ⟨h.finiteExhaustion⟩⟩

Goal state after:
α : Type u_1
s : Set α
x✝ : Nonempty s.FiniteExhaustion
K : s.FiniteExhaustion
⊢ s.Countable
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
dsm : none ∈ s.destruct
dse : Prod.fst <$> none = o
dtm : none ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none none
⊢ Prod.fst <$> none ∈ t.head

Tactic:
apply Computation.mem_map _ dtm

Goal state after: