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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup a s.toFinmap = dlookup a s

Tactic:
rw [List.toFinmap, lookup_toFinmap, lookup_to_alist]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case fst
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), (f i).isSome = true ↔ i ∈ s
a✝ : α
⊢ a✝ ∈
      (↑((fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩)
            ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ }) ⟨(s, f), hf⟩))).1 ↔
    a✝ ∈ (↑⟨(s, f), hf⟩).1

Tactic:
simp [keys, Multiset.keys, ← hf, Option.isSome_iff_exists]

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : a = a'
h✝ : decide (a = a') = true
⊢ some ⟨a, b⟩ = some ⟨a', b'⟩

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : a = a'
h✝ : ¬decide (a = a') = true
⊢ False

pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : decide (a = a') = true
⊢ False

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : ¬decide (a = a') = true
⊢ none = none

Tactic:
· subst a'
      simp [nd.eq_of_mk_mem h h']

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : a = a'
h✝ : ¬decide (a = a') = true
⊢ False

case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : decide (a = a') = true
⊢ False

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : ¬decide (a = a') = true
⊢ none = none
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ (kerase a l).keys = l.keys.erase a

Tactic:
by
  rw [keys, kerase, erase_eq_eraseP, eraseP_map, Function.comp_def]
  congr

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
h' : ¬a = a'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Tactic:
simp [h', ih h]

Goal state after:
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
l : List (ι →₀ M)
hl : Pairwise (_root_.Disjoint on Finsupp.support) l
⊢ l.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ l

Tactic:
induction l with
  | nil => simp
  | cons hd tl IH =>
    simp only [List.pairwise_cons] at hl
    simp only [List.sum_cons, List.foldr_cons]
    rw [Finsupp.support_add_eq, IH hl.right, Finset.sup_eq_union]
    suffices _root_.Disjoint hd.support (tl.foldr (fun x y ↦ (Finsupp.support x ⊔ y)) ∅) by
      exact Finset.disjoint_of_subset_right (List.support_sum_subset _) this
    rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset,
      Finset.disjoint_sup_right]
    intro f hf
    simp only [List.mem_toFinset, List.mem_map] at hf
    obtain ⟨f, hf, rfl⟩ := hf
    exact hl.left _ hf

Goal state after:
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
x✝ : α
⊢ x✝ ∈ ↑(f.neLocus g) ↔ x✝ ∈ {x | f x ≠ g x}

Tactic:
exact mem_neLocus

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

Goal state before:
pp: n : ℤ
⊢ (-n).bodd = n.bodd

Tactic:
by
  cases n <;> simp only [← negOfNat_eq, bodd_negOfNat, neg_negSucc] <;> simp [bodd]

Goal state after:
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: x a : ℤ
⊢ fib (x + a) ^ 2 - fib x * fib (x + 2 * a) =
    (fib x * fib (a + 1) + fib (x - 1) * fib a) ^ 2 -
      fib x * (fib x * (fib (a + 1) ^ 2 + fib a ^ 2) + fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a))

Tactic:
by
      rw [add_comm x]
      simp only [two_mul, fib_add, fib_one, mul_one, reduceAdd, fib_two, ← add_sub, sub_add_cancel]
      ring

Goal state after:
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: x a : ℤ
⊢ (fib x * fib (a + 1) + fib (x - 1) * fib a) ^ 2 -
      fib x * (fib x * (fib (a + 1) ^ 2 + fib a ^ 2) + fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a)) =
    (-1) ^ x.natAbs * fib a ^ 2

Tactic:
by grind [fib_succ_mul_fib_pred_sub_fib_sq, fib_add_two]

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

Goal state before:
pp: a b : ℤ
ha : a ≤ 0
hb : 0 ≤ b
⊢ a.natAbs = b.natAbs ↔ -a = b

Tactic:
by
  simpa only [Int.natAbs_neg] using natAbs_inj_of_nonneg_of_nonneg (neg_nonneg_of_nonpos ha) hb

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ rdropWhile p (l ++ [x]) = l ++ [x]

Tactic:
rw [rdropWhile_concat, if_neg h]

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

Goal state before:
pp: α : Type u_1
f : α → α
l₁ l₂ : List α
x✝ : l₂ ≠ []
⊢ modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂

Tactic:
by
  cases l₂ with
  | nil => contradiction
  | cons hd tl =>
    cases tl with
    | nil =>
      simp only [modifyLast, modifyLast.go, Array.toListAppend_eq, nil_append]
      exact modifyLast_concat _ hd _
    | cons hd' tl' =>
      rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
        modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
        modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
        append_assoc]
      all_goals { exact cons_ne_nil _ _ }

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

Goal state before:
pp: R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
⊢ A * B₁.fromCols B₂ = (A * B₁).fromCols (A * B₂)

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

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

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

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

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
m : ℕ
⊢ IsNat ⌈↑m⌉₊ m

Tactic:
exact ⟨by simp⟩

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
m : ℕ
⊢ IsNat ⌈↑(Int.negOfNat m)⌉₊ 0

Tactic:
exact ⟨by simp⟩

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

Goal state before:
pp: n : ℕ
h : IsPrimePow n
k : ℕ
left✝¹ : k ≤ log 2 n
left✝ : 0 < k
hn₁ : n = n.minFac ^ k
i : ℕ
hi : i ∈ Icc 1 (n - 1)
⊢ n.minFac ∣ n.choose i

Tactic:
hn₁

Goal state after:
n : ℕ
h : IsPrimePow n
k : ℕ
left✝¹ : k ≤ log 2 n
left✝ : 0 < k
hn₁ : n = n.minFac ^ k
i : ℕ
hi : i ∈ Icc 1 (n - 1)
⊢ n.minFac ∣ (n.minFac ^ k).choose i
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case refine_1
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ n.minFac ^ (k - 1) < n

Tactic:
hn₁

Goal state after:
case refine_1
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ n.minFac ^ (k - 1) < n.minFac ^ k
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case refine_2
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ emultiplicity n.minFac (n.choose (n.minFac ^ (k - 1))) < ↑2

Tactic:
hn₁

Goal state after:
case refine_2
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ emultiplicity n.minFac ((n.minFac ^ k).choose (n.minFac ^ (k - 1))) < ↑2
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case refine_2
p : ℕ → Prop
x : ℕ
h : p x
hf : (Set.ofPred p).Infinite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
rw [← @Set.mem_ofPred_eq _ _ p, ← range_nth_of_infinite hf] at h
    rcases h with ⟨n, hx⟩
    exact ⟨n, fun hf' => absurd hf' hf, hx⟩

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

Goal state before:
pp: case bit1
n : PosNum
⊢ ↑(n.bit1.minFacAux (↑n) 1) = if 2 ∣ ↑n.bit1 then 2 else (↑n.bit1).minFacAux 3

Tactic:
if_neg

Goal state after:
case bit1
n : PosNum
⊢ ↑(n.bit1.minFacAux (↑n) 1) = (↑n.bit1).minFacAux 3

case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑n.bit1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit0.sub' b.bit1) = ↑a.bit0 - ↑b.bit1

Tactic:
by
    rw [sub', ZNum.cast_bitm1, cast_sub' a b]
    have : ((-b + (a + (-b + -1)) : ℤ) : α) = (a + -1 + (-b + -b) : ℤ) := by
      simp [add_comm, add_left_comm]
    simpa [sub_eq_add_neg] using this

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

Goal state before:
pp: α : Type u_1
a : ZNum
⊢ ∀ (b c : ZNum), a ≤ b → b ≤ c → a ≤ c

Tactic:
b

Goal state after:
α : Type u_1
a b : ZNum
⊢ ∀ (c : ZNum), a ≤ b → b ≤ c → a ≤ c
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
a : ZNum
⊢ ∀ (b : ZNum), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
b

Goal state after:
α : Type u_1
a b : ZNum
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
a : ZNum
⊢ ∀ (b : ZNum), a ≤ b → b ≤ a → a = b

Tactic:
b

Goal state after:
α : Type u_1
a b : ZNum
⊢ a ≤ b → b ≤ a → a = b
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
a : ZNum
⊢ ∀ (b : ZNum), a ≤ b ∨ b ≤ a

Tactic:
b

Goal state after:
α : Type u_1
a b : ZNum
⊢ a ≤ b ∨ b ≤ a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case some.left
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ + ↑d * (2 * ↑q + 1) = ↑n

Tactic:
rwa [two_mul, add_comm _ 1, mul_add, mul_one, ← add_assoc, ← this]

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

Goal state before:
pp: case refine_2.rel
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : R x✝ y✝
⊢ (TypeVec.id ::: Quot.factor R (Relation.EqvGen R) this ∘ Quot.mk R) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.factor R (Relation.EqvGen R) this ∘ Quot.mk R) <$$> dest P y✝

Tactic:
appendFun_comp_id,

Goal state after:
case refine_2.rel
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : R x✝ y✝
⊢ ((TypeVec.id ::: Quot.factor R (Relation.EqvGen R) this) ⊚ (TypeVec.id ::: Quot.mk R)) <$$> dest P x✝ =
    ((TypeVec.id ::: Quot.factor R (Relation.EqvGen R) this) ⊚ (TypeVec.id ::: Quot.mk R)) <$$> dest P y✝
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.node.nil.refl.refl
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rlx : α
this : nil.size = 0 ∧ nil.size = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if (node 1 nil rlx nil).size < ratio * nil.size then nil.node3L x (node 1 nil rlx nil) rx nil
    else nil.node4L x (node 1 nil rlx nil) rx nil

pp: case nil.node.node.nil.refl.refl.hnc
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rlx : α
this : nil.size = 0 ∧ nil.size = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ ¬0 + (1 + 1) ≤ 1

Tactic:
if_neg

Goal state after:
case nil.node.node.nil.refl.refl
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rlx : α
this : nil.size = 0 ∧ nil.size = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) = nil.node4L x (node 1 nil rlx nil) rx nil

case nil.node.node.nil.refl.refl.hnc
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rlx : α
this : nil.size = 0 ∧ nil.size = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ ¬(node 1 nil rlx nil).size < ratio * nil.size

case nil.node.node.nil.refl.refl.hnc
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rlx : α
this : nil.size = 0 ∧ nil.size = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ ¬0 + (1 + 1) ≤ 1
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a
m n : ℕ+
⊢ m.lcm n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

Tactic:
apply lcm_dvd

Goal state after:
case a.hm
m n : ℕ+
⊢ m ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

case a.hn
m n : ℕ+
⊢ n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrx : α
this : nil.size = 0 ∧ nil.size = 0
hl : (nil.node' lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if (node 1 nil lrx nil).size < ratio * nil.size then nil.node3R lx (node 1 nil lrx nil) x nil
    else nil.node4R lx (node 1 nil lrx nil) x nil

pp: case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrx : α
this : nil.size = 0 ∧ nil.size = 0
hl : (nil.node' lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ ¬0 + 1 + 1 ≤ 1

Tactic:
if_neg

Goal state after:
case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrx : α
this : nil.size = 0 ∧ nil.size = 0
hl : (nil.node' lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) = nil.node4R lx (node 1 nil lrx nil) x nil

case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrx : α
this : nil.size = 0 ∧ nil.size = 0
hl : (nil.node' lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ ¬(node 1 nil lrx nil).size < ratio * nil.size

case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrx : α
this : nil.size = 0 ∧ nil.size = 0
hl : (nil.node' lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ ¬0 + 1 + 1 ≤ 1
Module: Mathlib.Data.PSigma.Order

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

Tactic:
obtain ⟨b, h⟩ := exists_gt a

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ 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✝ : ∀ (i : ι), NoMaxOrder (α i)
⊢ ∀ (a : Σₗ' (i : ι), α i), ∃ b, a < b

Tactic:
rintro ⟨i, a⟩
    obtain ⟨b, h⟩ := exists_gt a
    exact ⟨⟨i, b⟩, right _ h⟩

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

Goal state before:
pp: 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 f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)) ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u

Tactic:
← abs_repr x

Goal state after:
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 f, abs (repr x) = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)) ↔
    ∀ (i : Fin2 n), ∀ u ∈ supp (abs (repr x)) i, p i u
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

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

Tactic:
appendFun_comp_id,

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
⊢ supp (g <$$> x) i = g i '' supp x i

Tactic:
← abs_repr x

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
⊢ supp (g <$$> abs (repr x)) i = g i '' supp (abs (repr x)) i
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 : (P F).M α
⊢ ∀ ⦃y : (P F).M α⦄,
    r' a y →
      MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
        MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) y)

Tactic:
b

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' a b →
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
      MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F✝ : TypeVec.{u} n → Type u_1
q✝ : MvQPF F✝
F : TypeVec.{u} n → Type u_2
F' : TypeVec.{u} n → Type u_3
q : MvQPF F'
inst✝ : MvFunctor F
eqv : (α : TypeVec.{u} n) → F α ≃ F' α
map_eq : ∀ (α β : TypeVec.{u} n) (f : α ⟹ β) (a : F α), f <$$> a = (eqv β).symm (f <$$> (eqv α) a)
⊢ ∀ {α : TypeVec.{u} n} (x : F α), (eqv α).symm (abs (repr ((eqv α) x))) = x

Tactic:
by simp [q.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 : 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
⊢ (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)

Tactic:
appendFun_comp_id,

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
⊢ ((TypeVec.id ::: Quot.mk r) ⊚ (TypeVec.id ::: Quot.mk Mcongr)) <$$> MvQPF.abs (M.dest (P F) a) =
    ((TypeVec.id ::: Quot.mk r) ⊚ (TypeVec.id ::: Quot.mk Mcongr)) <$$> MvQPF.abs (M.dest (P F) b)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma

Goal state before:
pp: n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α : TypeVec.{u} n} (x : Pi F α), Pi.abs F (Pi.repr F x) = x

Tactic:
by
    rintro α f
    simp +instances only [Pi.abs, Pi.repr, Sigma.eta, abs_repr]

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
x : F α
⊢ id <$> x = x

Tactic:
← abs_repr x

Goal state after:
F : Type u → Type v
q : QPF F
α : Type u
x : F α
⊢ id <$> abs (repr x) = abs (repr x)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ (g ∘ f) <$> x = g <$> f <$> x

Tactic:
← abs_repr x

Goal state after:
F : Type u → Type v
q : QPF F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ (g ∘ f) <$> abs (repr x) = g <$> f <$> abs (repr x)