mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
⊢ ∀ (ch : F.B (head' (x.approx 1)) → CofixA F n),
    x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch →
      (CofixA.intro (head' (x.approx 1)) fun i ↦ (x.children i).approx n) = CofixA.intro (head' (x.approx 1)) ch

Tactic:
intro ch h

Goal state after:
case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
⊢ (CofixA.intro (head' (x.approx 1)) fun i ↦ (x.children i).approx n) = CofixA.intro (head' (x.approx 1)) ch
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mpr.succ.step
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
x y : F.M
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : x = M.mk ⟨a, x'⟩
a✝ : y = M.mk ⟨a, y'⟩
⊢ Agree (x.approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))

Tactic:
induction x using PFunctor.M.casesOn' with | _ x_a x_f
       =>  _ 

Goal state after:
case mpr.succ.step.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
y : F.M
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : y = M.mk ⟨a, y'⟩
x_a : F.A
x_f : F.B x_a → F.M
a✝ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
⊢ Agree ((M.mk ⟨x_a, x_f⟩).approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))
Module: Mathlib.Data.PFunctor.Univariate.M

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

Tactic:
induction n generalizing x y with
    | zero => constructor
    | succ _ n_ih =>
      obtain - | @⟨_, a, x', y'⟩ := h
      induction x using PFunctor.M.casesOn' with | _ x_a x_f
      induction y using PFunctor.M.casesOn' with | _ y_a y_f
      simp only [approx_mk]
      have h_a_1 := mk_inj ‹M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩›
      cases h_a_1
      replace h_a_2 := mk_inj ‹M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩›
      cases h_a_2
      constructor
      intro i
      apply n_ih
      simp [*]

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

Goal state before:
pp: case succ.step.step.f.f
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁸ : F.A
x✝¹ y✝¹ : F.B a✝⁸ → F.M
a✝⁷ : ∀ (i : F.B a✝⁸), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁶ : F.A
x✝ y✝ : F.B a✝⁶ → F.M
a✝⁵ : ∀ (i : F.B a✝⁶), Agree' n (x✝ i) (y✝ i)
a✝⁴ : F.A
f✝¹ : F.B a✝⁴ → F.M
a✝³ : M.mk ⟨a✝⁴, f✝¹⟩ = M.mk ⟨a✝⁸, y✝¹⟩
a✝² : F.A
f✝ : F.B a✝² → F.M
a✝¹ : M.mk ⟨a✝², f✝⟩ = M.mk ⟨a✝⁶, y✝⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁴, f✝¹⟩) = iselect ps (M.mk ⟨a✝², f✝⟩)
a✝ : M.mk ⟨a✝⁸, x✝¹⟩ = M.mk ⟨a✝⁶, x✝⟩
⊢ (M.mk ⟨a✝⁴, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝², f✝⟩).approx (n + 1 + 1)

Tactic:
have := mk_inj ‹_›

Goal state after:
case succ.step.step.f.f
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁸ : F.A
x✝¹ y✝¹ : F.B a✝⁸ → F.M
a✝⁷ : ∀ (i : F.B a✝⁸), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁶ : F.A
x✝ y✝ : F.B a✝⁶ → F.M
a✝⁵ : ∀ (i : F.B a✝⁶), Agree' n (x✝ i) (y✝ i)
a✝⁴ : F.A
f✝¹ : F.B a✝⁴ → F.M
a✝³ : M.mk ⟨a✝⁴, f✝¹⟩ = M.mk ⟨a✝⁸, y✝¹⟩
a✝² : F.A
f✝ : F.B a✝² → F.M
a✝¹ : M.mk ⟨a✝², f✝⟩ = M.mk ⟨a✝⁶, y✝⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁴, f✝¹⟩) = iselect ps (M.mk ⟨a✝², f✝⟩)
a✝ : M.mk ⟨a✝⁸, x✝¹⟩ = M.mk ⟨a✝⁶, x✝⟩
this : ⟨a✝⁸, x✝¹⟩ = ⟨a✝⁶, x✝⟩
⊢ (M.mk ⟨a✝⁴, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝², f✝⟩).approx (n + 1 + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)

Tactic:
have := mk_inj ‹_›

Goal state after:
case succ.step.step.f.f.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
this : ⟨a✝⁷, x✝⟩ = ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)

Tactic:
have := mk_inj ‹_›

Goal state after:
case succ.step.step.f.f.refl.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
this : ⟨a✝⁷, x✝⟩ = ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: case refine_3
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 α
r : R x y
this : ∀ (x y : P.M α), Relation.EqvGen R x y → x = y
⊢ x = y

pp: case refine_1
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 α
r : R x y
⊢ Equivalence (Relation.EqvGen R)

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 α
r : R x y
⊢ ∀ (x y : P.M α),
    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:
· solve_by_elim [Relation.EqvGen.rel]

Goal state after:
case refine_1
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 α
r : R x y
⊢ Equivalence (Relation.EqvGen R)

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 α
r : R x y
⊢ ∀ (x y : P.M α),
    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: case f.f.cons.f.f
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
f₁ : F.B a₀ → F.M
h₁ : R (M.mk ⟨a₀, f₀⟩) (M.mk ⟨a₀, f₁⟩)
h' : f' i = M.mk ⟨a₀, f₁⟩
⊢ (isubtree ps (M.mk ⟨a₀, f₀⟩)).head = (isubtree ps (M.mk ⟨a₀, f₁⟩)).head ∧
    ∃ a f f',
      isubtree ps (M.mk ⟨a₀, f₀⟩) = M.mk ⟨a, f⟩ ∧
        isubtree ps (M.mk ⟨a₀, f₁⟩) = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)

Tactic:
apply ps_ih _ _ _ h₁

Goal state after:
case f.f.cons.f.f
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
f₁ : F.B a₀ → F.M
h₁ : R (M.mk ⟨a₀, f₀⟩) (M.mk ⟨a₀, f₁⟩)
h' : f' i = M.mk ⟨a₀, f₁⟩
⊢ IsPath ps (M.mk ⟨a₀, f₀⟩) ∨ IsPath ps (M.mk ⟨a₀, f₁⟩)
Module: Mathlib.Data.PNat.Interval

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.uIcc a b) = (↑↑b - ↑↑a).natAbs + 1

Tactic:
← card_uIcc,

Goal state after:
a b : ℕ+
⊢ Fintype.card ↑(Set.uIcc a b) = #(uIcc a b)
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
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ ↑z * ↑a' = x * ↑b' + 1

Tactic:
ha',

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
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ ↑z * (↑w + x) = x * ↑b' + 1
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
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
⊢ ↑w * ↑b' = y * ↑a' + 1

Tactic:
ha',

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
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
⊢ ↑w * ↑b' = y * (↑w + x) + 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ Ordnode.insert x (node size✝ l y r) = insertWith (fun x_1 ↦ x) x (node size✝ l y r)

Tactic:
unfold Ordnode.insert insertWith; cases cmpLE x y <;> simp [insert_eq_insertWith]

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

Goal state before:
pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ IsUniform → SuppPreservation

Tactic:
rintro h α ⟨a, f⟩

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
x : (P F).W
⊢ Wequiv (Wrepr x) x

Tactic:
induction x with | _ a f ih

Goal state after:
case mk
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)) (WType.mk a f)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a → Fix F
h : repr x = ⟨a, f⟩
⊢ recF g (PFunctor.W.mk ((P F).map fixToW ⟨a, f⟩)) = g (rec g <$> x)

Tactic:
rw [PFunctor.map_eq, recF_eq, ← PFunctor.map_eq, PFunctor.W.dest_mk, PFunctor.map_map, abs_map,
    ← h, abs_repr, this]

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

Goal state before:
pp: case mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
x : (P F).W
⊢ g₁ (Quot.mk (⇑Wsetoid) x) = g₂ (Quot.mk (⇑Wsetoid) x)

Tactic:
induction x with | _ a f ih

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ g₁ (Quot.mk (⇑Wsetoid) (WType.mk a f)) = g₂ (Quot.mk (⇑Wsetoid) (WType.mk a f))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x✝ : Fix F
x : (P F).W
⊢ p (Quot.mk (⇑Wsetoid) x)

Tactic:
induction x with | _ a f ih

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid) (f a))
⊢ p (Quot.mk (⇑Wsetoid) (WType.mk a f))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ supp x = {u | ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ}

Tactic:
by
  ext
  apply mem_supp

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

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

Tactic:
rintro h α ⟨a, f⟩

Goal state after:
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⟩
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
x : Option (β × WSeq β)
y : Option (α × WSeq α)
⊢ Function.swap (LiftRelO R C) x y = LiftRelO (Function.swap R) (Function.swap C) x y

Tactic:
rcases x with ⟨⟩ | ⟨hx, jx⟩ <;> rcases y with ⟨⟩ | ⟨hy, jy⟩ <;> rfl

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

Goal state before:
pp: case inr
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m✝ : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
m : Any (fun b ↦ some (some a) = b) ↑s'
⊢ Any (fun b ↦ some (some a) = b) (some (some a') :: ↑s')

Tactic:
exact Stream'.mem_cons_of_mem _ m

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

Goal state before:
pp: case zero.think
α : Type u
a : α
s✝ : WSeq α
m : a ∈ s✝.think.tail
e : some (some a) = (↑s✝.think.tail).get 0
⊢ a ∈ s✝.think

pp: case succ.think
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
s✝ : WSeq α
m : a ∈ s✝.think.tail
e : some (some a) = (↑s✝.think.tail).get (n✝ + 1)
⊢ a ∈ s✝.think

Tactic:
case zero.think => injections

Goal state after:
case succ.think
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
s✝ : WSeq α
m : a ∈ s✝.think.tail
e : some (some a) = (↑s✝.think.tail).get (n✝ + 1)
⊢ a ∈ s✝.think
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n → a ∈ s
s : WSeq α
m : a ∈ s.think.tail
e : some (some a) = (↑s.think.tail).get (n + 1)
⊢ a ∈ s.think

Tactic:
simp only [tail_think, mem_think] at m e ⊢
    apply IH m
    rw [e]
    cases tail s
    rfl

Goal state after:
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: case left_inv
α : 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
x y : α
hy : y ∈ s
hyt : y ∈ ↑t
a✝ : Finite ↑(s ∩ ↑t)
hxs : x ∈ s
⊢ x ∈ ↑t → ⟨⋯.choose, ⋯⟩ = t

Tactic:
hxt

Goal state after:
case left_inv
α : 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
x y : α
hy : y ∈ s
hyt : y ∈ ↑t
a✝ : Finite ↑(s ∩ ↑t)
hxs : x ∈ s
hxt : x ∈ ↑t
⊢ ⟨⋯.choose, ⋯⟩ = t
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case right
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
⊢ ∀ {b : Option (β × WSeq β)},
    b ∈ T.join.destruct →
      ∃ a ∈ S.join.destruct,
        LiftRelO R
          (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
          a b

Tactic:
intro b mb
          rw [← LiftRelO.swap]
          apply liftRel_join.lem (swap R)
          · rw [← LiftRel.swap R, ← LiftRel.swap]
            apply ST
          · rw [← LiftRel.swap R, ← LiftRel.swap (LiftRel R)]
            exact fun s1 s2 ⟨s, t, S, T, h1, h2, st, ST⟩ => ⟨t, s, T, S, h2, h1, st, ST⟩
          · exact mb

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ (ret s).join ~ʷ s

Tactic:
by simpa [ret] using think_equiv _

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (n + 1)
⊢ α

Tactic:
by
  refine i.cases' ?_ ?_
  · exact a
  · exact v

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
f : Vector3 α 0 → Prop
x✝ : Exists f
v : Vector3 α 0
fv : f v
⊢ f v

Tactic:
exact fv

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n : ℕ
f : Vector3 α n.succ → Prop
x✝ : Exists f
v : Vector3 α n.succ
fv : f v
⊢ f v

Tactic:
exact fv

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∃ a ∈ s, ∀ᵐ (b : G) ∂μ, b * a ∈ s ↔ a ∈ s

Tactic:
refine (hμs.and_eventually ?_).exists
    rw [ae_ae_comm]
    · exact ae_of_all _ fun b ↦ (hs b).mem_iff
    · exact ((hsm.preimage <| measurable_snd.mul measurable_fst).mem.iff
        (hsm.preimage measurable_fst).mem).setOf

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

Goal state before:
pp: f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist ((f ^ n) 0 + (g ^ n) 0) ((f ^ n * g ^ n) 0) ≤ 1

Tactic:
exact le_of_lt ((f ^ n).dist_map_map_zero_lt (g ^ n))

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n ↦ ((f ^ n) x - x) / ↑n) atTop (𝓝 (τ f))

Tactic:
rw [← translationNumber_conj_eq' (translate <| Multiplicative.ofAdd x)]
  refine (tendsto_translation_number₀ _).congr fun n ↦ ?_
  simp [sub_eq_neg_add, Units.conj_pow']

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
g : M
⊢ (fun m ↦ m • 1) g ∈ {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}

Tactic:
simpa using hs g

Goal state after:
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
hlt : x < y
x✝ : Ioo x y = ∅ ∨ (Ioo x y).Nonempty
⊢ False

Tactic:
cases (Ioo x y).eq_empty_or_nonempty with

Goal state after: