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

Goal state before:
pp: case refine_3
α : 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
⊢ 2 * l.size ≤ 9 * r.dual.size + 5 ∨ l.size ≤ 3

Tactic:
size_dual

Goal state after:
case refine_3
α : 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
⊢ 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
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₂
H₁ : r.size = 0 → l.size ≤ 1
H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size
H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
this :
  (r.size = 0 → l.dual.size ≤ 1) →
    (1 ≤ r.size → 1 ≤ l.dual.size → l.dual.size ≤ delta * r.size) →
      2 * r.size ≤ 9 * l.dual.size + 5 ∨ r.size ≤ 3 → Valid' o₂ (r.dual.balanceL x l.dual) o₁
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁

Tactic:
size_dual

Goal state after:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : r.size = 0 → l.size ≤ 1
H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size
H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
this :
  (r.size = 0 → l.size ≤ 1) →
    (1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size) →
      2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3 → Valid' o₂ (r.dual.balanceL x l.dual) o₁
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a.hm
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ m.factorMultiset

pp: case a.hn
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ n.factorMultiset

Tactic:
· exact inf_le_left

Goal state after:
case a.hn
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ n.factorMultiset
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case refine_2.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁✝ : ι
j : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : a₁✝ < a₂✝
hba : ¬⟨a₂✝, b⟩ ≤ ⟨a₁✝, j⟩
⊢ ⟨a₁✝, j⟩ < ⟨a₂✝, b⟩

Tactic:
exact Lex.left _ _ hij

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

Goal state before:
pp: u : XgcdType
⊢ u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y

Tactic:
rw [mul_comm u.x, mul_comm u.zp, add_comm u.zp]

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : (P F).B a ⟹ α
haf : abs ⟨a, f⟩ = x
⊢ LiftP (fun i u ↦ u ∈ f i '' univ) x

Tactic:
liftP_iff

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : (P F).B a ⟹ α
haf : abs ⟨a, f⟩ = x
⊢ ∃ a_1 f_1, x = abs ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_1 i), f_1 i j ∈ f i '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
this : LiftP (fun i u ↦ u ∈ supp x i) x
⊢ ∃ a f,
    abs ⟨a, f⟩ = x ∧ ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ

Tactic:
liftP_iff

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
this : ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), f i j ∈ supp x i
⊢ ∃ a f,
    abs ⟨a, f⟩ = x ∧ ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs ⟨a, f⟩ = x
h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u

Tactic:
liftP_iff

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs ⟨a, f⟩ = x
h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
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
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l r : Ordnode α
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ (∃ l', Raised l' r.size ∧ BalancedSz l' l.dual.size) ∨ ∃ r', Raised l.dual.size r' ∧ BalancedSz r.size r'

Tactic:
size_dual

Goal state after:
α : Type u_1
l r : Ordnode α
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ (∃ l', Raised l' r.size ∧ BalancedSz l' l.size) ∨ ∃ r', Raised l.size r' ∧ BalancedSz r.size r'
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ l✝ a₂ → Valid' (Option.map f a₁) (map f l✝) (Option.map f a₂) ∧ (map f l✝).size = l✝.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ r✝ a₂ → Valid' (Option.map f a₁) (map f r✝) (Option.map f a₂) ∧ (map f r✝).size = r✝.size
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_ih_l' : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝) ∧ (map f l✝).size = l✝.size
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    (map f (Ordnode.node size✝ l✝ x✝ r✝)).size = (Ordnode.node size✝ l✝ x✝ r✝).size

Tactic:
have t_ih_r' := t_ih_r h.right

Goal state after:
case node
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ l✝ a₂ → Valid' (Option.map f a₁) (map f l✝) (Option.map f a₂) ∧ (map f l✝).size = l✝.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ r✝ a₂ → Valid' (Option.map f a₁) (map f r✝) (Option.map f a₂) ∧ (map f r✝).size = r✝.size
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_ih_l' : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝) ∧ (map f l✝).size = l✝.size
t_ih_r' : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂) ∧ (map f r✝).size = r✝.size
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    (map f (Ordnode.node size✝ l✝ x✝ r✝)).size = (Ordnode.node size✝ l✝ x✝ r✝).size
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_l a₂ → Valid' a₁ (erase x t_l) a₂ ∧ Raised (erase x t_l).size t_l.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (erase x t_l).size t_l.size
⊢ Valid' a₁
      (match cmpLE x t_x 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₂ ∧
    Raised
      (match cmpLE x t_x 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
      size✝

Tactic:
have t_ih_r' := t_ih_r h.right

Goal state after:
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_l a₂ → Valid' a₁ (erase x t_l) a₂ ∧ Raised (erase x t_l).size t_l.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (erase x t_l).size t_l.size
t_ih_r' : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match cmpLE x t_x 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₂ ∧
    Raised
      (match cmpLE x t_x 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
      size✝
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l : ∀ {a₁ : WithBot α} {a₂ : WithTop α}, Valid' a₁ t_l a₂ → x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r : ∀ {a₁ : WithBot α} {a₂ : WithTop α}, Valid' a₁ t_r a₂ → x ∈ t_r → (erase x t_r).size = t_r.size - 1
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : x ∈ node size✝ t_l t_x t_r
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
⊢ (erase x (node size✝ t_l t_x t_r)).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
have t_ih_r' := t_ih_r h.right

Goal state after:
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l : ∀ {a₁ : WithBot α} {a₂ : WithTop α}, Valid' a₁ t_l a₂ → x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r : ∀ {a₁ : WithBot α} {a₂ : WithTop α}, Valid' a₁ t_r a₂ → x ∈ t_r → (erase x t_r).size = t_r.size - 1
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : x ∈ node size✝ t_l t_x t_r
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
⊢ (erase x (node size✝ t_l t_x t_r)).size = (node size✝ t_l t_x t_r).size - 1
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ (TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$$> x.dest =
    (TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$$> y.dest

Tactic:
rw [appendFun_comp_id]

Goal state after:
case h.inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ ((TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) ⊚ (TypeVec.id ::: Quot.mk r)) <$$> x.dest =
    ((TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) ⊚ (TypeVec.id ::: Quot.mk r)) <$$> y.dest
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.gt.zero
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_pos_t_r_size : 0 < 0
⊢ t_l.size + (0 - 1) + 1 = (node (t_l.size + 0 + 1) t_l t_x t_r).size - 1

pp: case node.gt.succ
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size✝ : Raised (erase x t_r).size t_r.size
t_r_size : ℕ
h_pos_t_r_size : 0 < t_r_size + 1
⊢ t_l.size + (t_r_size + 1 - 1) + 1 = (node (t_l.size + (t_r_size + 1) + 1) t_l t_x t_r).size - 1

Tactic:
· cases h_pos_t_r_size

Goal state after:
case node.gt.succ
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size✝ : Raised (erase x t_r).size t_r.size
t_r_size : ℕ
h_pos_t_r_size : 0 < t_r_size + 1
⊢ t_l.size + (t_r_size + 1 - 1) + 1 = (node (t_l.size + (t_r_size + 1) + 1) t_l t_x t_r).size - 1
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'
⊢ f <$> Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest = f <$> Quot.mk r <$> abs ((P F).map (Quot.mk Mcongr) b.dest)

Tactic:
abs_map

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'
⊢ f <$> Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest = f <$> Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩

Tactic:
rwa [supp_eq_of_isUniform, PFunctor.supp_eq]

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

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
h : LiftpPreservation
⊢ SuppPreservation

Tactic:
rintro α ⟨a, f⟩
    simp only [LiftpPreservation] at h
    simp only [supp, h]

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

Goal state before:
pp: case some
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
t' : α × WSeq α
td : some a ∈ t'.2.destruct
ht' : some t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd (some t') = t
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
exact ⟨_, ht'⟩

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

Goal state before:
pp: α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
o : Option α
⊢ ∀ (s' : Seq (Option α)), some a = o ∨ C s' → C (Seq.cons o s')

Tactic:
s'

Goal state after:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
o : Option α
s' : Seq (Option α)
⊢ some a = o ∨ C s' → C (Seq.cons o s')
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case h2
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b → Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux a) (tail.aux b)

Tactic:
exact fun {a b} o =>
      match a, b, o with
      | none, none, _ => by simp
      | some (a, s), some (b, t), ⟨_, h2⟩ => by simpa [tail.aux] using liftRel_destruct h2

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

Goal state before:
pp: case h1
α : Type u
s : WSeq α
a : α
h : a ∈ s
a' : α
⊢ ∀ (s' : WSeq α), (a = a' ∨ ∃ n, some a ∈ s'.get? n) → ∃ n, some a ∈ (cons a' s').get? n

Tactic:
s'

Goal state after:
case h1
α : Type u
s : WSeq α
a : α
h : a ∈ s
a' : α
s' : WSeq α
⊢ (a = a' ∨ ∃ n, some a ∈ s'.get? n) → ∃ n, some a ∈ (cons a' s').get? n
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
t : ↑P
ht : t ∈ ⋯.toFinset
⊢ Nat.card ↑(s ∩ ↑t) = ?m.54 t

Tactic:
exact hst' ↑t

Goal state after:
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
g : G
h : g ∈ {g | g • s =ᵐ[μ] s}
⊢ g⁻¹ ∈ {g | g • s =ᵐ[μ] s}

Tactic:
by simpa using! (smul_set_ae_eq g⁻¹).2 h.out.symm

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
⊢ f (fract x) - fract x = f x - x

Tactic:
rw [Int.fract, f.map_sub_int, sub_sub_sub_cancel_right]

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
t : Set α
hsub : t ⊆ s
htm : MeasurableSet t
hts : t =ᵐ[μ] s
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
rcases hf.exists_mem_iterate_mem' htm (by rwa [measure_congr hts]) with ⟨x, hxt, m, hm₀, hmt⟩

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
t : Set α
hsub : t ⊆ s
htm : MeasurableSet t
hts : t =ᵐ[μ] s
x : α
hxt : x ∈ t
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ t
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: case intro
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
⊢ {p | p.support = U}.Finite

Tactic:
classical
  -- Patterns with support U biject with (U → A) via restriction/extension
  let e : { p : Pattern A G // p.support = U } ≃ (U → A) :=
  { toFun := fun p i => p.1.config i.1
    invFun := fun f => ⟨{ config := fun g => if h : g ∈ U then f ⟨g, h⟩ else default,
                           support := U,
                           condition := fun g hg => by simp [hg] }, rfl⟩
    left_inv := by
      rintro ⟨⟨cfg, dom, cond⟩, hU⟩
      simp only at hU; subst hU
      apply Subtype.ext
      simp only [Pattern.mk.injEq, and_true]
      funext g
      by_cases hg : g ∈ dom
      · simp [hg]
      · simp [hg, cond g hg]
    right_inv := fun f => by ext i; simp [i.2] }
  let : Fintype { p : Pattern A G | p.support = U } := Fintype.ofEquiv (U → A) e.symm
  apply toFinite

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h✝ : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h✝.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν')
⊢ ∀ᵐ (x : α) ∂ν.restrict t, μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x

Tactic:
ae_restrict_iff' ht

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h✝ : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h✝.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν')
⊢ ∀ᵐ (x : α) ∂ν, x ∈ t → μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n ↑s
⊢ ∃ t, IsDynCoverOf T F U n ↑t ∧ #t ≤ #s ∧ ∀ x ∈ t, (ball x (dynEntourage T U n) ∩ F).Nonempty

Tactic:
use {x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}

Goal state after:
case h
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n ↑s
⊢ IsDynCoverOf T F U n ↑({x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}) ∧
    #({x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}) ≤ #s ∧
      ∀ x ∈ {x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}, (ball x (dynEntourage T U n) ∩ F).Nonempty
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case h
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n ↑s
y : X
y_F : y ∈ F
⊢ ∃ y_1 ∈ {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty}, (y, y_1) ∈ dynEntourage T U n

Tactic:
obtain ⟨z, z_s, y_Bz⟩ := h y_F

Goal state after:
case h
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n ↑s
y : X
y_F : y ∈ F
z : X
z_s : z ∈ ↑s
y_Bz : (y, z) ∈ dynEntourage T U n
⊢ ∃ y_1 ∈ {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty}, (y, y_1) ∈ dynEntourage T U n
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : SetRel X X
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ (fun U ↦ netEntropyEntourage T F U) (s i) ≤ ⨆ i, ⨆ (_ : p i), netEntropyEntourage T F (s i)

Tactic:
exact le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ netEntropyEntourage T F (s i)) i h_i

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
⊢ IsEmpty Language.empty.Symbols

Tactic:
simp only [Language.Symbols, isEmpty_sum, isEmpty_sigma]
  exact ⟨fun _ => inferInstance, fun _ => inferInstance⟩

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: M : Type w
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
⊢ (LHom.constantsOnMap f).IsExpansionOn M

Tactic:
let := constantsOn.structure fα

Goal state after:
M : Type w
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
this : (constantsOn α).Structure M := constantsOn.structure fα
⊢ (LHom.constantsOnMap f).IsExpansionOn M
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
α : Type w'
ie : IsEmpty α
⊢ ((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)).comp LHom.sumInl = LHom.id L

Tactic:
LHom.sumElim_comp_inl

Goal state after:
L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
α : Type w'
ie : IsEmpty α
⊢ LHom.id L = LHom.id L
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝ : L.Structure M
e : M ≃ N
⊢ N → M

Tactic:
letI : L.Structure N := inducedStructure e
    exact DFunLike.coe (@inducedStructureEquiv L M N _ e).symm

Goal state after: