mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
⊢ (take m ⋯ fun i ↦ addCases u v i) = take m h u

Tactic:
by
  ext i
  have : i < n := Nat.lt_of_lt_of_le i.isLt h
  simp only [take, addCases, this, val_castLE, ↓reduceDIte]
  congr

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ { card := card α, equiv := equiv, decEq := fun a b ↦ decEq a b } =
    { card := 0, equiv := Equiv.equivOfIsEmpty α (Fin 0), decEq := fun a b ↦ decidableEq_of_subsingleton a b }

Tactic:
congr 1

Goal state after:
case e_2
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ card α = 0

case e_3
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ equiv ≍ Equiv.equivOfIsEmpty α (Fin 0)

case e_4
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ { card := card α, equiv := equiv, decEq := fun a b ↦ decEq a b } =
    { card := 1, equiv := Equiv.ofUnique α (Fin 1), decEq := fun a b ↦ decidableEq_of_subsingleton a b }

Tactic:
congr 1

Goal state after:
case e_2
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ card α = 1

case e_3
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ equiv ≍ Equiv.ofUnique α (Fin 1)

case e_4
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (Perm α) = (Nat.card α)!

Tactic:
rw [card_eq_fintype_card, card_eq_fintype_card, Fintype.card_perm]

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

Goal state before:
pp: case cons.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝ → lookmap f l₁✝ ~ lookmap f l₂✝
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁✝)
val✝ : α
h : f a = some val✝
⊢ lookmap f (a :: l₁✝) ~ lookmap f (a :: l₂✝)

Tactic:
· simp [lookmap_cons_some _ _ h, p]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
⊢ b ∈ lookupAll a (⟨a', b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Tactic:
by
    by_cases h : a = a'
    · subst h
      simp [*, mem_lookupAll]
    · simp [*, mem_lookupAll]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝), (x✝³ && f x✝² x✝¹ && f x✝ b₂) = (x✝³ && f x✝ b₂ && f x✝² x✝¹)

Tactic:
by simp_rw [Bool.and_assoc, Bool.and_comm, imp_true_iff]

Goal state after:
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
⊢ (if t = ∅ then ∅ else s) = (image (const β✝) s).sup fun f ↦ image f t

Tactic:
· ext a
        rw [if_neg ht.ne_empty, mem_sup]
        refine ⟨fun ha => ⟨const _ a, mem_image_of_mem _ ha, mem_image_const_self.2 ht⟩, ?_⟩
        rintro ⟨f, hf, ha⟩
        rw [mem_image] at hf ha
        obtain ⟨b, hb, rfl⟩ := hf
        obtain ⟨_, _, rfl⟩ := ha
        exact hb

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✝ : AddGroup N
f g : α →₀ N
⊢ f.neLocus (f + g) = (f + 0).neLocus (f + g)

Tactic:
add_zero

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ f.neLocus (f + g) = f.neLocus (f + g)
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
h' : CPRankMax 1 (x + 0)
⊢ CPRankMax 1 x

Tactic:
add_zero

Goal state after:
α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
h' : CPRankMax 1 x
⊢ CPRankMax 1 x
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ b ^^^ a ^^^ a = b

Tactic:
xor_cancel_right

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ b = b
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℤ
hr : 0 < r
⊢ {x ∈ Ico a b | r ∣ x} = map { toFun := fun x ↦ x * r, inj' := ⋯ } (Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉)

Tactic:
ext x
  simp only [mem_map, mem_filter, mem_Ico, ceil_le, lt_ceil, div_le_iff₀, lt_div_iff₀,
    dvd_iff_exists_eq_mul_left, cast_pos.2 hr, ← cast_mul, cast_lt, cast_le]
  aesop

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

Goal state before:
pp: m n✝ k i n : ℕ
⊢ ↑m <<< ↑i = ↑(Nat.shiftLeft' false m (n + i) >>> n)

Tactic:
by simp [← Nat.shiftLeft_sub _]

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

Goal state before:
pp: case neg
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : ¬p hd = true
⊢ (match p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length), ¬p (hd :: tl)[0] = true

Tactic:
· simp [h_p_hd]

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ take (l.length - n) l = (drop n l.reverse).reverse

Tactic:
induction l using List.reverseRecOn generalizing n with
  | nil => simp
  | append_singleton xs x IH =>
    cases n
    · simp [take_length_add_append]
    · simp [take_append, IH]

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

Goal state before:
pp: α : Type u_1
f : α → α
a : α
tl : List α
r : Array α
⊢ go f (tl ++ [a]) r = r.toListAppend (go f (tl ++ [a]) #[])

Tactic:
cases tl with
  | nil =>
    simp only [nil_append, modifyLast.go]; simp
  | cons hd tl =>
    simp only [cons_append]
    rw [modifyLast.go, modifyLast.go]
    case x_3 | x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])
    rw [modifyLast.go_concat _ _ tl _, modifyLast.go_concat _ _ tl (Array.push #[] hd)]
    simp only [Array.toListAppend_eq, Array.toList_push, nil_append,
      append_assoc]

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

Goal state before:
pp: case pos
n m : ℕ
h : n < m
⊢ IsChain (fun a b ↦ b = a.succ) (n :: Ico (n + 1) m)

Tactic:
unfold List.Ico

Goal state after:
case pos
n m : ℕ
h : n < m
⊢ IsChain (fun a b ↦ b = a.succ) (n :: range' (n + 1) (m - (n + 1)))
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ splitBy.loop r l a g []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
induction l generalizing a g with
  | nil =>
    rw [splitBy.loop, reverse_cons, mem_append, mem_reverse, mem_singleton] at h
    obtain hm | rfl := h
    · cases not_mem_nil hm
    · apply List.isChain_reverse.1
      rw [reverse_reverse]
      exact isChain_cons.2 ⟨hga, hg⟩
  | cons b l IH =>
    simp only [splitBy.loop, reverse_cons] at h
    split at h
    · apply IH _ (isChain_cons.2 ⟨hga, hg⟩) h
      grind
    · rw [splitByLoop_eq_append, mem_append, reverse_singleton, mem_singleton] at h
      obtain rfl | hm := h
      · apply List.isChain_reverse.1
        rw [reverse_append, reverse_cons, reverse_nil, nil_append, reverse_reverse]
        exact isChain_cons.2 ⟨hga, hg⟩
      · grind

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (of fun i j ↦ fst ((algebraMap R (Matrix n n (DualNumber R))) r i j),
      of fun i j ↦ snd ((algebraMap R (Matrix n n (DualNumber R))) r i j)) =
    inl ((algebraMap R (Matrix n n R)) r)

Tactic:
algebraMap_eq_diagonal,

Goal state after:
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (of fun i j ↦ fst (diagonal ((algebraMap R (n → DualNumber R)) r) i j),
      of fun i j ↦ snd (diagonal ((algebraMap R (n → DualNumber R)) r) i j)) =
    inl (diagonal ((algebraMap R (n → R)) r))
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: case inl
q : ℚ
hq : q ≤ 0
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

pp: case inr
q : ℚ
hq : 0 ≤ q
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
· rw [toNNRat_eq_zero.mpr hq, inv_zero, toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)]

Goal state after:
case inr
q : ℚ
hq : 0 ≤ q
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: case inl
i j : ℕ
h✝ : i ≤ j
⊢ i.dist j = max i j - min i j

Tactic:
simp [Nat.dist, *]

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

Goal state before:
pp: case inr
i j : ℕ
h✝ : j ≤ i
⊢ i.dist j = max i j - min i j

Tactic:
simp [Nat.dist, *]

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

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

Tactic:
rw [sub', ZNum.cast_bit1, 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.PFunctor.Univariate.Basic

Goal state before:
pp: case h.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = ⟨a, f₀⟩
yeq : y = ⟨a, f₁⟩
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ (fun t ↦ (↑t).1) <$> ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩ = x

Tactic:
rw [xeq]
    rfl

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

Goal state before:
pp: n : ℕ
⊢ ofInt' ↑(n + 1) = -ofInt' -[n+1]

Tactic:
simp only [ofInt', Num.zneg_toZNumNeg]

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

Goal state before:
pp: case zero
F : PFunctor.{uA, uB}
x : CofixA F 0
y : CofixA F (succ 0)
h : Agree x y
⊢ truncate y = x

Tactic:
cases x
    cases y
    rfl

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

Goal state before:
pp: case one
d : PosNum
⊢ ↑(d.divMod one).2 + ↑d * ↑(d.divMod one).1 = ↑one ∧ ↑(d.divMod one).2 < ↑d

Tactic:
| one =>

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:
rwa [appendFun_comp_id, ← MvFunctor.map_map, ← MvFunctor.map_map, h]

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

Goal state before:
pp: n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset

Tactic:
have : n = u.prod := (prod_factorMultiset n).symm

Goal state after:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this : n = u.prod
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
⊢ (n ^ m).factorMultiset = m • n.factorMultiset

Tactic:
have : n = u.prod := (prod_factorMultiset n).symm

Goal state after:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (n ^ m).factorMultiset = m • n.factorMultiset
Module: Mathlib.Data.PNat.Find

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

Tactic:
| one =>

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

Goal state before:
pp: case a.left
m n : ℕ+
⊢ m ∣ m.lcm n

pp: case a.right
m n : ℕ+
⊢ n ∣ m.lcm n

Tactic:
· exact dvd_lcm_left m n

Goal state after:
case a.right
m n : ℕ+
⊢ n ∣ m.lcm n
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case pos
u : XgcdType
hr : u.r = 0
hq : u.q = 0
h : 0 + 0 = u.ap + 1
⊢ u.q = u.qp + 1

Tactic:
add_zero

Goal state after:
case pos
u : XgcdType
hr : u.r = 0
hq : u.q = 0
h : 0 = u.ap + 1
⊢ u.q = u.qp + 1
Module: Mathlib.Data.Pi.Interval

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

Tactic:
mem_piFinset,

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
b✝ b x : (i : ι) → α i
⊢ (x ∈ piFinset fun i ↦ Iic (b i)) ↔ x ≤ b

Tactic:
mem_piFinset,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
b✝ b x : (i : ι) → α i
⊢ (∀ (a : ι), x a ∈ Iic (b a)) ↔ x ≤ b
Module: Mathlib.Data.Pi.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a✝ a x : (i : ι) → α i
⊢ (x ∈ piFinset fun i ↦ Ici (a i)) ↔ a ≤ x

Tactic:
mem_piFinset,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a✝ a x : (i : ι) → α i
⊢ (∀ (a_1 : ι), x a_1 ∈ Ici (a a_1)) ↔ a ≤ x
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil.bot
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₂ : WithTop α
h : Valid' ⊥ nil a₂
⊢ nil.Bounded (Option.map f ⊥) (Option.map f a₂)

pp: case nil.coe
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₂ : WithTop α
a✝ : α
h : Valid' (↑a✝) nil a₂
⊢ nil.Bounded (Option.map f ↑a✝) (Option.map f a₂)

Tactic:
· trivial

Goal state after:
case nil.coe
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₂ : WithTop α
a✝ : α
h : Valid' (↑a✝) nil a₂
⊢ nil.Bounded (Option.map f ↑a✝) (Option.map f a₂)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil.coe.top
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a✝ : α
h : Valid' (↑a✝) nil ⊤
⊢ nil.Bounded (Option.map f ↑a✝) (Option.map f ⊤)

pp: case nil.coe.coe
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a✝¹ a✝ : α
h : Valid' (↑a✝¹) nil ↑a✝
⊢ nil.Bounded (Option.map f ↑a✝¹) (Option.map f ↑a✝)

Tactic:
· trivial

Goal state after:
case nil.coe.coe
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a✝¹ a✝ : α
h : Valid' (↑a✝¹) nil ↑a✝
⊢ nil.Bounded (Option.map f ↑a✝¹) (Option.map f ↑a✝)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case trans
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ y✝ x y z : (P F).W α
_e₁ : WEquiv x y
_e₂ : WEquiv y z
ih₁ : WEquiv y x
ih₂ : WEquiv z y
⊢ WEquiv z x

Tactic:
exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁

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

Goal state before:
pp: case mk.a
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (WType.mk a f)) (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩))

Tactic:
apply Wequiv.abs'
    have : Wrepr ⟨a, f⟩ = PFunctor.W.mk (repr (abs (q.P.map Wrepr ⟨a, f⟩))) := rfl
    rw [this, PFunctor.W.dest_mk, abs_repr]
    rfl

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

Goal state before:
pp: case fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
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), p (Quot.mk (⇑(wSetoid α)) (f i))
a✝ : Fin2 n
j : (P F).B a a✝.fs
⊢ α.PredLast p ((P F).appendContents f' (fun x ↦ ⟦f x⟧) a✝.fs j)

Tactic:
· trivial

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✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: ((Quot.mk fun x y ↦ x = mk y.dest) ∘ mk) ∘ fun i ↦ i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest

Tactic:
congr 1

Goal state after:
case e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: ((Quot.mk fun x y ↦ x = mk y.dest) ∘ mk) ∘ fun i ↦ i.dest) =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest)
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r

Tactic:
exact hp.le

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

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p x → p u) → ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ

pp: case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
⊢ (∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ) → ∀ ⦃p : α → Prop⦄, Liftp p x → p u

Tactic:
· intro h a f haf
    have : Liftp (fun u => u ∈ f '' univ) x := by
      rw [liftp_iff]
      exact ⟨a, f, haf.symm, fun i => mem_image_of_mem _ (mem_univ _)⟩
    exact h this

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
⊢ (∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ) → ∀ ⦃p : α → Prop⦄, Liftp p x → p u
Module: Mathlib.Data.WSeq.Basic

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

Tactic:
skip

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

Goal state before:
pp: case none.none
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none none
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd none

pp: case none.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
b : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none (some b)
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd (some b)

pp: case some.none
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) none
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd none

pp: case some.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd (some b)

Tactic:
· trivial

Goal state after:
case none.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
b : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none (some b)
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd (some b)

case some.none
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) none
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd none

case some.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd (some b)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case refine_2.none.none
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
ma : none ∈ s.destruct
mb : none ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none none

pp: case refine_2.none.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
ma : none ∈ s.destruct
b : α × WSeq α
mb : some b ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none (some b)

pp: case refine_2.some.none
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α × WSeq α
ma : some a ∈ s.destruct
mb : none ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) none

pp: case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α × WSeq α
ma : some a ∈ s.destruct
b : α × WSeq α
mb : some b ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) (some b)

Tactic:
· trivial

Goal state after:
case refine_2.none.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
ma : none ∈ s.destruct
b : α × WSeq α
mb : some b ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none (some b)

case refine_2.some.none
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α × WSeq α
ma : some a ∈ s.destruct
mb : none ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) none

case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α × WSeq α
ma : some a ∈ s.destruct
b : α × WSeq α
mb : some b ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) (some b)
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 := ⋯
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) = pure a → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
skip

Goal state after:
case h1
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop := ⋯
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) = pure a → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
⊢ ∀ (a₁ a₂ : Σₗ (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | ⟨_, b, h⟩)
    · obtain ⟨c, hb⟩ := exists_lt b
      exact ⟨⟨j, c⟩, left _ _ h, right _ _ hb⟩
    · obtain ⟨c, ha, hb⟩ := exists_between h
      exact ⟨⟨i, c⟩, right _ _ ha, right _ _ hb⟩

Goal state after: