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

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ (casesOn (id (node rs rl rx rr))
        (casesOn (id l) (Ordnode.singleton x) fun ls ll lx lr ↦
          casesOn (id ll)
            (casesOn lr (node 2 l x nil) fun size l lrx r ↦ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x))
            fun lls l x_1 r ↦
            casesOn (id lr) (node 3 ll lx (Ordnode.singleton x)) fun lrs lrl lrx lrr ↦
              if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
              else node (ls + 1) (node (lls + lrl.size + 1) ll lx lrl) lrx (node (lrr.size + 1) lrr x nil))
        fun rs_1 l_1 x_1 r ↦
        casesOn (id l) (node (rs_1 + 1) nil x (node rs rl rx rr)) fun ls ll lx lr ↦
          if ls > delta * rs_1 then
            casesOn (id ll) nil fun lls l x_2 r ↦
              casesOn (id lr) nil fun lrs lrl lrx lrr ↦
                if lrs < ratio * lls then node (ls + rs_1 + 1) ll lx (node (rs_1 + lrs + 1) lr x (node rs rl rx rr))
                else
                  node (ls + rs_1 + 1) (node (lls + lrl.size + 1) ll lx lrl) lrx
                    (node (lrr.size + rs_1 + 1) lrr x (node rs rl rx rr))
          else node (ls + rs_1 + 1) l x (node rs rl rx rr)).dual =
    casesOn (id (node rs rl rx rr).dual)
      (casesOn (id l.dual) (Ordnode.singleton x) fun rs rl rx rr ↦
        casesOn (id rr)
          (casesOn rl (node 2 nil x l.dual) fun size l rlx r ↦ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx))
          fun rrs l x_1 r ↦
          casesOn (id rl) (node 3 (Ordnode.singleton x) rx rr) fun rls rll rlx rlr ↦
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else node (rs + 1) (node (rll.size + 1) nil x rll) rlx (node (rlr.size + rrs + 1) rlr rx rr))
      fun ls l_1 x_1 r ↦
      casesOn (id l.dual) (node (ls + 1) (node rs rl rx rr).dual x nil) fun rs_1 rl_1 rx_1 rr_1 ↦
        if rs_1 > delta * ls then
          casesOn (id rr_1) nil fun rrs l x_2 r ↦
            casesOn (id rl_1) nil fun rls rll rlx rlr ↦
              if rls < ratio * rrs then
                node (ls + rs_1 + 1) (node (ls + rls + 1) (node rs rl rx rr).dual x rl_1) rx_1 rr_1
              else
                node (ls + rs_1 + 1) (node (ls + rll.size + 1) (node rs rl rx rr).dual x rll) rlx
                  (node (rlr.size + rrs + 1) rlr rx_1 rr_1)
        else node (ls + rs_1 + 1) (node rs rl rx rr).dual x l.dual

Tactic:
· obtain - | ⟨ls, ll, lx, lr⟩ := l; · rfl
    dsimp only [dual, id]
    split_ifs; swap; · simp [add_comm]
    obtain - | ⟨lls, lll, llx, llr⟩ := ll <;> obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr <;> try rfl
    dsimp only [dual, id]
    split_ifs with h <;> simp [add_comm]

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (((match l with
            | nil => 0
            | node sz l x r => sz) +
            match m with
            | nil => 0
            | node sz l x r => sz) +
          1 +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2

Tactic:
add_right_comm _ 1

Goal state after:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (((match l with
            | nil => 0
            | node sz l x r => sz) +
            match m with
            | nil => 0
            | node sz l x r => sz) +
          match r with
          | nil => 0
          | node sz l x r => sz) +
        1 +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
P : α → Prop
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ Any P (node size✝ l x r) ↔ ∃ x_1, Any (Eq x_1) (node size✝ l x r) ∧ P x_1

Tactic:
simp [Any, any_iff_exists, or_and_right, exists_or]

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

Goal state before:
pp: a b : ℕ+
⊢ (start a b).IsSpecial

Tactic:
dsimp [start, IsSpecial]

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

Goal state before:
pp: u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q + u.x)

Tactic:
rw [mul_add, mul_comm u.y u.x, ← hs]

Goal state after:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q) + (u.wp + u.zp + u.wp * u.zp)
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case left
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
c : α j
hb : c < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨j, b⟩

Tactic:
exact ⟨⟨j, c⟩, left _ _ h, right _ hb⟩

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

Goal state before:
pp: a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
⊢ w * z = (x * y).succPNat ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
have hb' : (b' : ℕ) = y + z := gcdB'_coe a b

Goal state after:
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
⊢ w * z = (x * y).succPNat ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs (((g ::: u) ⊚ (TypeVec.id ::: Quot.mk r)) <$$> M.dest (P F) a₁) =
    abs (((g ::: u) ⊚ (TypeVec.id ::: Quot.mk r)) <$$> M.dest (P F) a₂)

Tactic:
q.P.comp_map,

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs ((g ::: u) <$$> (TypeVec.id ::: Quot.mk r) <$$> M.dest (P F) a₁) =
    abs (((g ::: u) ⊚ (TypeVec.id ::: Quot.mk r)) <$$> M.dest (P F) a₂)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs ((g ::: u) <$$> (TypeVec.id ::: Quot.mk r) <$$> M.dest (P F) a₁) =
    abs (((g ::: u) ⊚ (TypeVec.id ::: Quot.mk r)) <$$> M.dest (P F) a₂)

Tactic:
q.P.comp_map,

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs ((g ::: u) <$$> (TypeVec.id ::: Quot.mk r) <$$> M.dest (P F) a₁) =
    abs ((g ::: u) <$$> (TypeVec.id ::: Quot.mk r) <$$> M.dest (P F) a₂)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ MvQPF.abs (((TypeVec.id ::: f) ⊚ (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr)) <$$> M.dest (P F) a) =
    MvQPF.abs (((TypeVec.id ::: f) ⊚ (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr)) <$$> M.dest (P F) b)

Tactic:
q.P.comp_map,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ MvQPF.abs ((TypeVec.id ::: f) <$$> (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> M.dest (P F) a) =
    MvQPF.abs (((TypeVec.id ::: f) ⊚ (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr)) <$$> M.dest (P F) b)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ MvQPF.abs ((TypeVec.id ::: f) <$$> (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> M.dest (P F) a) =
    MvQPF.abs (((TypeVec.id ::: f) ⊚ (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr)) <$$> M.dest (P F) b)

Tactic:
q.P.comp_map,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ MvQPF.abs ((TypeVec.id ::: f) <$$> (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: f) <$$> (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> M.dest (P F) b)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)

Tactic:
have : recF g ∘ fixToW = Fix.rec g := by
    apply funext
    apply Quotient.ind
    intro x
    apply recF_eq_of_wEquiv
    apply wrepr_equiv
  conv =>
    lhs
    rw [Fix.rec, Fix.mk]
    dsimp
  rcases h : repr x with ⟨a, f⟩
  rw [MvPFunctor.map_eq, recF_eq', ← MvPFunctor.map_eq, MvPFunctor.wDest'_wMk']
  rw [← MvPFunctor.comp_map, abs_map, ← h, abs_repr, ← appendFun_comp, id_comp, this]

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ rec (Functor.map mk) (mk x) = x

Tactic:
rw [Fix.rec_eq, ← Fix.dest, ← comp_map]

Goal state after:
F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ rec (MvFunctor.map (TypeVec.id ::: mk)) (mk x) = x

Tactic:
rw [Fix.rec_eq, ← Fix.dest, ← comp_map]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
this : Liftp (fun x_1 ↦ x_1 ∈ supp x) x
⊢ ∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ

Tactic:
rw [liftp_iff] at this

Goal state after:
case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
this : ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), f i ∈ supp x
⊢ ∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R✝ : α → β → Prop
s : WSeq α
t : WSeq β
R : WSeq α → WSeq β → Prop
h1 : R s t
h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R✝ R) s.destruct t.destruct
⊢ Computation.LiftRel (LiftRelO R✝ (LiftRel R✝)) s.destruct t.destruct

Tactic:
by
    refine Computation.LiftRel.imp ?_ _ _ (h2 h1)
    apply LiftRelO.imp_right
    exact fun s' t' h' => ⟨R, h', @h2⟩

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

Goal state before:
pp: case mp
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ some none :: f
⊢ some (some a) ∈ f

Tactic:
apply (Stream'.eq_or_mem_of_mem_cons h).resolve_left

Goal state after:
case mp
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ some none :: f
⊢ ¬some (some a) = some none
Module: Mathlib.Data.Set.FiniteExhaustion

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

Tactic:
by_cases h : Nonempty s

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

case neg
α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty ↑s
⊢ Nonempty s.FiniteExhaustion
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: case hj
α : 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
x : α
hx : x ∈ s
⊢ ∃ a ∈ s, a ∈ ⋯.choose

Tactic:
use x, hx, (hP.2 x).exists.choose_spec.2

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
x✝¹ : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) none none
x✝ : S.destruct.Results none m
rs2 : (destruct_join.aux none).Results a k
mT : none ∈ T.destruct
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
simp only [destruct_join]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
x✝¹ : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) none none
x✝ : S.destruct.Results none m
rs2 : (destruct_join.aux none).Results a k
mT : none ∈ T.destruct
⊢ ∃ b ∈ T.destruct.bind destruct_join.aux, LiftRelO R U a b
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case refl.refl
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
this✝ : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : (a, c) ∈ map (fun a ↦ (a, c')) c'
cs' : c' ∈ S
e'✝ : map (fun a ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
e' : (a', c') = (a, c)
⊢ a ∈ c ∧ c ∈ S

Tactic:
injection e' with i1 i2

Goal state after:
case refl.refl
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
this✝ : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : (a, c) ∈ map (fun a ↦ (a, c')) c'
cs' : c' ∈ S
e' : map (fun a ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
⊢ a ∈ c ∧ c ∈ S
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
m n : ℕ
C : Vector3 α (n + 1) → Sort u
H : (a : α) → (t : Vector3 α n) → C (a :: t)
v : Vector3 α (n + 1)
⊢ C v

Tactic:
rw [← cons_head_tail v]

Goal state after:
α : Type u_1
m n : ℕ
C : Vector3 α (n + 1) → Sort u
H : (a : α) → (t : Vector3 α n) → C (a :: t)
v : Vector3 α (n + 1)
⊢ C (v.head :: v.tail)
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 t : Set α
h : s =ᵐ[μ] t
g : G
⊢ g • s =ᵐ[μ] s ↔ g • t =ᵐ[μ] t

Tactic:
h.congr_right,

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s t : Set α
h : s =ᵐ[μ] t
g : G
⊢ g • s =ᵐ[μ] t ↔ g • t =ᵐ[μ] t
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: X : Type u_2
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : R1Space X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
M : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : MulAction M X
inst✝³ : ContinuousSMul M X
g : M
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
n : ℕ
⊢ g ^ n ∈ {g | (fun x ↦ g • x) ⁻¹' s = s}

Tactic:
rw [mem_ofPred, ← smul_iterate, preimage_iterate_eq, iterate_fixed hs]

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

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
⊢ μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν

Tactic:
refine .of_forall_eventually_lt_iff fun c ↦ ?_

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
⊢ ∀ᵐ (a : X) ∂ν, (μ.rnDeriv ν ∘ f) a < c ↔ μ.rnDeriv ν a < c
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case hfi
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := ⋯
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ ∫⁻ (x : X) in s \ f ⁻¹' s, μ.rnDeriv ν x ∂ν ≠ ⊤

pp: case h
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := ⋯
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ ∀ᵐ (x : X) ∂ν, x ∈ s \ f ⁻¹' s → μ.rnDeriv ν x < c

Tactic:
· rw [setLIntegral_rnDeriv hμν]
        finiteness

Goal state after:
case h
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := ⋯
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ ∀ᵐ (x : X) ∂ν, x ∈ s \ f ⁻¹' s → μ.rnDeriv ν x < c