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

Goal state before:
pp: case h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α},
    (∀ (b : α), b ∈ g_1.head? → r b a_1 = true) →
      IsChain (fun y x ↦ r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])

pp: case h_2.inr
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
hm : m ∈ splitBy.loop r l b [] []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
· apply List.isChain_reverse.1
        rw [reverse_append, reverse_cons, reverse_nil, nil_append, reverse_reverse]
        exact isChain_cons.2 ⟨hga, hg⟩

Goal state after:
case h_2.inr
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
hm : m ∈ splitBy.loop r l b [] []
⊢ IsChain (fun x y ↦ r x y = true) m
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
⊢ p - q + q - (p - q).gcd q ≤ (drop q w).length

Tactic:
simp; lia

Goal state after:
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
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
R' : Type u_8
f : R → R'
⊢ (A₁.fromRows A₂).map f = (A₁.map f).fromRows (A₂.map f)

Tactic:
ext (_ | _)

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
R' : Type u_8
f : R → R'
val✝ : m₁
j✝ : n
⊢ (A₁.fromRows A₂).map f (Sum.inl val✝) j✝ = (A₁.map f).fromRows (A₂.map f) (Sum.inl val✝) j✝

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
R' : Type u_8
f : R → R'
val✝ : m₂
j✝ : n
⊢ (A₁.fromRows A₂).map f (Sum.inr val✝) j✝ = (A₁.map f).fromRows (A₂.map f) (Sum.inr val✝) j✝
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
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
v : n → R
⊢ A₁.fromRows A₂ *ᵥ v = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v)

Tactic:
ext (_ | _)

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
v : n → R
val✝ : m₁
⊢ (A₁.fromRows A₂ *ᵥ v) (Sum.inl val✝) = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) (Sum.inl val✝)

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
v : n → R
val✝ : m₂
⊢ (A₁.fromRows A₂ *ᵥ v) (Sum.inr val✝) = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) (Sum.inr val✝)
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 m
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
v : m → R
⊢ v ᵥ* B₁.fromCols B₂ = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂)

Tactic:
ext (_ | _)

Goal state after:
case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype m
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
v : m → R
val✝ : n₁
⊢ (v ᵥ* B₁.fromCols B₂) (Sum.inl val✝) = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) (Sum.inl val✝)

case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype m
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
v : m → R
val✝ : n₂
⊢ (v ᵥ* B₁.fromCols B₂) (Sum.inr val✝) = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) (Sum.inr val✝)
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
| b ∣ n

Tactic:
← ofDigits_digits b' n

Goal state after:
b b' : ℕ
h : b' % b = 1
n : ℕ
| b ∣ ofDigits b' (b'.digits n)
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case succ
A : Type u_1
inst✝ : Semiring A
k : ℕ
ih : ∀ {m : ℕ}, IsUnit ↑(m + k)! → IsUnit ↑m !
m : ℕ
hn_fac : IsUnit ↑(m + 1 + k)!
this : IsUnit ↑(m + 1)!
⊢ IsUnit ↑m !

Tactic:
rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff] at this

Goal state after:
case succ
A : Type u_1
inst✝ : Semiring A
k : ℕ
ih : ∀ {m : ℕ}, IsUnit ↑(m + k)! → IsUnit ↑m !
m : ℕ
hn_fac : IsUnit ↑(m + 1 + k)!
this : IsUnit ↑(m + 1) ∧ IsUnit ↑m !
⊢ IsUnit ↑m !
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case succ
A : Type u_1
inst✝ : Semiring A
k : ℕ
ih : ∀ {m : ℕ}, IsUnit ↑(m + k)! → IsUnit ↑m !
m : ℕ
hn_fac : IsUnit ↑(m + (k + 1))!
⊢ IsUnit ↑m !

Tactic:
rw [← add_assoc, add_right_comm] at hn_fac
    have := ih hn_fac
    rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff] at this
    exact this.2

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌈/⌉ n).support
this : Prime p ∧ p ∣ a ∧ ¬a = 0
⊢ Prime p

Tactic:
exact this.1

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

Goal state before:
pp: case nil.node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
exact node 3 ll lx ι x

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

Goal state before:
pp: case node.nil.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
exact node 3 ll lx ι x

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 α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ x = ⟨a, fun i ↦ (↑(f i)).1⟩

Tactic:
rw [← xeq, h]

Goal state after:
case h.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun t ↦ (↑t).1) <$> ⟨a, f⟩ = ⟨a, fun i ↦ (↑(f i)).1⟩
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ x = ⟨a, fun i j ↦ (↑(f i j)).1⟩

Tactic:
rw [← xeq, h]

Goal state after:
case h.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).1) <$$> ⟨a, f⟩ = ⟨a, fun i j ↦ (↑(f i j)).1⟩
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mp.succ
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
x y : F.M
h : Agree (x.approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))
⊢ Agree' (n✝ + 1) x y

Tactic:
induction x using PFunctor.M.casesOn'
      induction y using PFunctor.M.casesOn'
      simp only [approx_mk] at h
      obtain - | ⟨_, _, hagree⟩ := h
      constructor <;> try rfl
      intro i
      apply n_ih
      apply hagree

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

Goal state before:
pp: case f.f.nil
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
hh : IsPath [] (M.mk ⟨a, f⟩) ∨ IsPath [] (M.mk ⟨a, f'⟩)
⊢ ∀ (i : F.B a), R (f i) (f' i)

Tactic:
apply bisim.tail h₀

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

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hm : nil.Sized
⊢ (l.node4L x nil y r).size = l.size + nil.size + r.size + 2

pp: case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.node4L x (node size✝ l✝ x✝ r✝) y r).size = l.size + (node size✝ l✝ x✝ r✝).size + r.size + 2

Tactic:
· simp [node4L, node3L, node']
    abel

Goal state after:
case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.node4L x (node size✝ l✝ x✝ r✝) y r).size = l.size + (node size✝ l✝ x✝ r✝).size + r.size + 2
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ Valid' o₁ (l.rotateR x r) o₂

Tactic:
by
  refine Valid'.dual_iff.2 ?_
  rw [dual_rotateR]
  refine hr.dual.rotateL hl.dual ?_ ?_ ?_
  · rwa [size_dual, size_dual, add_comm]
  · rwa [size_dual, size_dual]
  · rwa [size_dual, size_dual]

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

Goal state before:
pp: case refine_2
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 α
Hr : Relation.EqvGen R x y
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y

Tactic:
have : ∀ x y, R x y → Relation.EqvGen R x y := @Relation.EqvGen.rel _ R

Goal state after:
case refine_2
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 α
Hr : Relation.EqvGen R x y
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: 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)
⊢ ∀ (x y : P.M), R x y → x = y

Tactic:
by
  introv h'
  have := Inhabited.mk x.head
  apply eq_of_bisim R _ _ _ h'; clear h' x y
  constructor <;> introv ih <;> rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩ <;> clear h
  · replace h₀ := congr_arg Sigma.fst h₀
    replace h₁ := congr_arg Sigma.fst h₁
    simp only [dest_mk] at h₀ h₁
    rw [h₀, h₁]
  · simp only [dest_mk] at h₀ h₁
    cases h₀
    cases h₁
    apply h₂

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

Goal state before:
pp: v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Subtype.val l
p : ℕ
hp : p ∈ l'
⊢ Nat.Prime p

Tactic:
simp only [List.map_subtype, List.map_id_fun', id_eq, List.mem_unattach, l'] at hp

Goal state after:
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Subtype.val l
p : ℕ
hp : ∃ h, ⟨p, h⟩ ∈ l
⊢ Nat.Prime p
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: p : Nat.Primes
⊢ (↑p).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod

Tactic:
(p : ℕ+).prod_factorMultiset,

Goal state after:
p : Nat.Primes
⊢ ↑p = (PrimeMultiset.ofPrime p).prod
Module: Mathlib.Data.PNat.Interval

Goal state before:
pp: a b : ℕ+
⊢ #(Ioo a b) = ↑b - ↑a - 1

Tactic:
rw [← Nat.card_Ioo, ← map_subtype_embedding_Ioo, card_map]

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

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
b : α ⊤
⊢ ⟨⊤, b⟩ ≤ ⟨⊤, ⊤⟩

pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
ha : a < ⊤
⊢ ⟨a, b⟩ ≤ ⟨⊤, ⊤⟩

Tactic:
· exact Lex.right _ le_top

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
ha : a < ⊤
⊢ ⟨a, b⟩ ≤ ⟨⊤, ⊤⟩
Module: Mathlib.Data.PNat.Xgcd

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

Tactic:
hq,

Goal state after:
case pos
u : XgcdType
hr : u.r = 0
hq : u.q = 0
h : 0 + (u.bp + 1) * 0 = u.ap + 1
⊢ u.q = u.qp + 1
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case snd
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := ⋯
hr : u.r - 1 + 1 = u.r := ⋯
⊢ u.step.v.2 = u.v.swap.2

Tactic:
change ((u.w * u.q + u.x) * u.b + u.w * (u.r - 1 + 1) : ℕ) = u.w * u.a + u.x * u.b

Goal state after:
case snd
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑u.w * u.q + u.x) * ↑u.b + ↑u.w * (u.r - 1 + 1) = ↑u.w * ↑u.a + u.x * ↑u.b
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
h : u.r = 0
⊢ u.reduce = u.finish

Tactic:
rw [reduce]

Goal state after:
u : XgcdType
h : u.r = 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.finish
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
h : u.r ≠ 0
⊢ u.reduce = u.step.reduce.flip

Tactic:
rw [reduce]

Goal state after:
u : XgcdType
h : u.r ≠ 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.step.reduce.flip
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: n m : ℕ
H : Raised n m
⊢ n.dist m ≤ 1

Tactic:
obtain ⟨H1, H2⟩ := raised_iff.1 H

Goal state after:
n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ n.dist m ≤ 1
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.right
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 := ⋯
⊢ r' (g <$$> aa₁) (g <$$> aa₂)

Tactic:
exact ⟨aa₁, aa₂, ra₁a₂, rfl, rfl⟩

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
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)
u v : (P F).M α
⊢ Mcongr u v → Quot.mk r' u = Quot.mk r' v

Tactic:
cuv

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)
u v : (P F).M α
cuv : Mcongr u v
⊢ Quot.mk r' u = Quot.mk r' v
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
⊢ Liftp p x ↔ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

Tactic:
by
  constructor
  · rintro ⟨y, hy⟩
    rcases h : repr y with ⟨a, f⟩
    use a, fun i => (f i).val
    constructor
    · rw [← hy, ← abs_repr y, h, ← abs_map]
      rfl
    intro i
    apply (f i).property
  rintro ⟨a, f, h₀, h₁⟩
  use abs ⟨a, fun i => ⟨f i, h₁ i⟩⟩
  rw [← abs_map, h₀]; rfl

Goal state after:
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
u v : (P F).M
⊢ Mcongr u v → Quot.mk r' u = Quot.mk r' v

Tactic:
cuv

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
u v : (P F).M
cuv : Mcongr u v
⊢ Quot.mk r' u = Quot.mk r' v
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case cons.inr.inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : s.think ∈ l
ls : List (Computation α)
e' :
  (match Sum.inr ls with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inr ls
⊢ s ∈ l'

Tactic:
have := IH' m _ e

Goal state after:
case cons.inr.inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : s.think ∈ l
ls : List (Computation α)
e' :
  (match Sum.inr ls with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inr ls
this : s ∈ ls
⊢ s ∈ l'
Module: Mathlib.Data.Set.FiniteExhaustion

Goal state before:
pp: case pos
α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty ↑s
⊢ Nonempty s.FiniteExhaustion

pp: case neg
α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty ↑s
⊢ Nonempty s.FiniteExhaustion

Tactic:
· obtain ⟨f, hf⟩ := @exists_surjective_nat s h hs
    refine ⟨fun n ↦ (Subtype.val ∘ f) '' {i | i ≤ n}, ?_, ?_, ?_⟩
    · exact fun n ↦ Finite.image _ (finite_le_nat n)
    · grind
    · simp [← image_image, ← image_iUnion, iUnion_le_nat, range_eq_univ.mpr hf]

Goal state after:
case neg
α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty ↑s
⊢ Nonempty s.FiniteExhaustion
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case nil
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
⊢ F [] (parallel.aux2 [])

Tactic:
simp only [parallel.aux2, List.foldr]

Goal state after:
case nil
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
⊢ F [] (Sum.inr [])
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case cons
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
head✝ : Computation α
tail✝ : List (Computation α)
tail_ih✝ : F tail✝ (parallel.aux2 tail✝)
⊢ F (head✝ :: tail✝) (parallel.aux2 (head✝ :: tail✝))

Tactic:
simp only [parallel.aux2, List.foldr]

Goal state after:
case cons
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
head✝ : Computation α
tail✝ : List (Computation α)
tail_ih✝ : F tail✝ (parallel.aux2 tail✝)
⊢ F (head✝ :: tail✝)
    (match
      List.foldr
        (fun c o ↦
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
        (Sum.inr []) tail✝ with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' ↦ c' :: ls) head✝.destruct)
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iio a)) ↔
    ⟨j, b⟩ < ⟨i, a⟩

Tactic:
obtain rfl | hij := eq_or_ne i j
    · simp
    · simp [hij, lt_def, hij.symm]

Goal state after: