mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
X : LightProfinite
inst✝ : Finite ↑X.toTop
x✝¹ : Cofan fun x ↦ LightProfinite.of PUnit.{?u.15 + 1}
x✝ : (fintypeCatAsCofan X).pt ⟶ x✝¹.pt
h : ∀ (j : ↑X.toTop), (fintypeCatAsCofan X).inj j ≫ x✝ = x✝¹.inj j
⊢ x✝ = ConcreteCategory.ofHom { toFun := fun x ↦ (ConcreteCategory.hom (x✝¹.inj x)) PUnit.unit, continuous_toFun := ⋯ }

Tactic:
by ext x; exact CategoryTheory.congr_fun (h x) _

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (toLightProfinite.op ⋙ F).map x✝ ≫ (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop Y✝))).hom =
    (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop X✝))).hom ≫ (finYoneda F).map x✝

Tactic:
simp only [comp_obj, op_obj, finYoneda_obj, Functor.comp_map, op_map]

Goal state after:
S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ F.map (toLightProfinite.map x✝.unop).op ≫ (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop Y✝))).hom =
    (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop X✝))).hom ≫ (finYoneda F).map x✝
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case e_a
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj
      (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom
            ((↾fun f ↦ ⇑f) ≫ (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv)).toFun
        f) =
    (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom ((counitApp X).app (Opposite.op (toLightProfinite.obj (Opposite.unop Y))))).toFun f)

Tactic:
dsimp [toLightProfinite_obj]

Goal state after:
case e_a
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj
      (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (LightProfinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (counitAppApp (LightProfinite.of (Opposite.unop Y).obj) X)) f)
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ : CondensedSet
X : CompactlyGenerated
⊢ IsIso (compactlyGeneratedAdjunction.counit.app X)

Tactic:
exact inferInstanceAs (IsIso (compactlyGeneratedAdjunctionCounitIso X).hom)

Goal state after:
Module: Mathlib.Control.Fix

Goal state before:
pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
⊢ hwf✝.fix (fixAux f) z x' = f (Fix.approx f 0) x'

Tactic:
WellFounded.fix_eq,

Goal state after:
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
⊢ fixAux f z (fun y x ↦ hwf✝.fix (fixAux f) y) x' = f (Fix.approx f 0) x'
Module: Mathlib.Control.Fix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
⊢ hwf✝.fix (fixAux f) z x' = f (Fix.approx f (n + 1)) x'

Tactic:
WellFounded.fix_eq,

Goal state after:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
⊢ fixAux f z (fun y x ↦ hwf✝.fix (fixAux f) y) x' = f (Fix.approx f (n + 1)) x'
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x✝ : Chain (Unit → Part α)
⊢ (toUnitMono { toFun := f, monotone' := ⋯ }) (ωSup x✝) = ωSup (x✝.map (toUnitMono { toFun := f, monotone' := ⋯ }))

Tactic:
by
  ext ⟨⟩ : 1
  dsimp [OmegaCompletePartialOrder.ωSup]
  erw [hc.map_ωSup]
  rw [Chain.map_comp]
  rfl

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) → (x : α) → (y : β x) → γ x y
hc : ωScottContinuous _f
| curry (fix (uncurry ∘ _f ∘ curry))

Tactic:
erw [LawfulFix.fix_eq (uncurry_curry_ωScottContinuous hc)]

Goal state after:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) → (x : α) → (y : β x) → γ x y
hc : ωScottContinuous _f
| curry
    (((monotoneUncurry α β γ).comp ({ toFun := _f, monotone' := ⋯ }.comp (monotoneCurry α β γ)))
      (fix ⇑((monotoneUncurry α β γ).comp ({ toFun := _f, monotone' := ⋯ }.comp (monotoneCurry α β γ)))))
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r Fin2.fz
⊢ (toSubtype' r ⊚ ofSubtype' r) Fin2.fz x = id Fin2.fz x

Tactic:
dsimp only [id, toSubtype', comp, ofSubtype'] at *

Goal state after:
case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r Fin2.fz
⊢ ⟨↑x, ⋯⟩ = x
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop) (x : Subtype_ r a✝),
    (toSubtype' r ⊚ ofSubtype' r) a✝ x = id a✝ x
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r a✝.fs
⊢ (toSubtype' r ⊚ ofSubtype' r) a✝.fs x = id a✝.fs x

Tactic:
dsimp only [id, toSubtype', comp, ofSubtype'] at *

Goal state after:
case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop) (x : Subtype_ r a✝), toSubtype' r a✝ (ofSubtype' r a✝ x) = x
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r a✝.fs
⊢ toSubtype' (dropFun r) a✝ (ofSubtype' (dropFun r) a✝ x) = x
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
⊢ F.toTopsp = T

Tactic:
by
  refine TopologicalSpace.ext_nhds fun x ↦ ?_
  ext s
  rw [mem_nhds_toTopsp, H]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
fst_i : α
snd_i : β fst_i
⊢ a ∈ (⟨fst_i, snd_i⟩ :: xs).toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ ⟨fst_i, snd_i⟩ :: xs

Tactic:
simp only [toFinmap_cons, *, exists_or, mem_cons, mem_insert, exists_and_left, Sigma.mk.inj_iff]

Goal state after:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
fst_i : α
snd_i : β fst_i
⊢ (a = fst_i ∨ ∃ b, ⟨a, b⟩ ∈ xs) ↔ (a = fst_i ∧ ∃ x, x ≍ snd_i) ∨ ∃ x, ⟨a, x⟩ ∈ xs
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
⊢ ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid

Tactic:
by
  let := Classical.decEq β
  refine Finset.induction_on s ?_ ?_
  · simp [slice_zero]
  · intro _ _ h_not_in ih
    rw [Finset.sum_insert h_not_in, ih, slice_add, Finset.sum_insert h_not_in]

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

Goal state before:
pp: case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ (!p head) = true

Tactic:
· simpa using phh

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

Goal state before:
pp: case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : true = p head
⊢ ¬(!p head) = true

Tactic:
· simpa using phh

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

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

pp: case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
modifyLast.go

Goal state after:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (#[].push hd))

case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (head✝ :: (tl ++ [a])) #[] = head✝ :: (tl ++ [f a])

Tactic:
modifyLast.go

Goal state after:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (#[].push head✝) = head✝ :: (tl ++ [f a])

case cons.x_3
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ tl ++ [a] = [] → False
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
gs : List (List α)
⊢ splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []

Tactic:
induction l generalizing a g gs with
  | nil => simp [splitBy.loop]
  | cons b l IH =>
    simp_rw [splitBy.loop]
    split <;> rw [IH]
    conv_rhs => rw [IH]
    simp

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' : IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (a :: l)
y : α
hy : y ∈ l.flatten.head?
⊢ r (a.getLast ⋯) y = false

Tactic:
← head_of_mem_head? hy

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' : IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (a :: l)
y : α
hy : y ∈ l.flatten.head?
⊢ r (a.getLast ⋯) (l.flatten.head ⋯) = false
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ ↑(chineseRemainderOfList a s (i :: l) co) < (List.map s (i :: l)).prod

Tactic:
simp only [chineseRemainderOfList, List.map_cons, List.prod_cons]

Goal state after:
case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ ↑(chineseRemainder ⋯ (a i) ↑(chineseRemainderOfList a s l ⋯)) < s i * (List.map s l).prod
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.divisors =
    Finset.image (⇑{ toFun := fun x ↦ (↑x).prod fun x1 x2 ↦ x1 ^ x2, inj' := ⋯ }) (Finset.Iic n.factorization).attach

Tactic:
change _ = (Finset.Iic n.factorization).attach.image ((·.prod (· ^ ·)) ∘ Subtype.val)

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n.divisors = Finset.image ((fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) ∘ Subtype.val) (Finset.Iic n.factorization).attach
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case none
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
⊢ ↑(match none with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d * (↑q + ↑q) =
      ↑n ∧
    ↑(match none with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

Tactic:
refine ⟨h₁, lt_of_not_ge fun h => ?_⟩

Goal state after:
case none
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
h :
  ↑d ≤
    ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2
⊢ False
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ ⟨a,
      splitFun (dropFun f)
        ((corec' P (fun b ↦ (g b).fst) (fun b ↦ dropFun (g b).snd) fun b ↦ lastFun (g b).snd) ∘ lastFun f)⟩ =
    (TypeVec.id ::: corec P g) <$$> ⟨a, f⟩

Tactic:
MvPFunctor.map_eq

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ ⟨a,
      splitFun (dropFun f)
        ((corec' P (fun b ↦ (g b).fst) (fun b ↦ dropFun (g b).snd) fun b ↦ lastFun (g b).snd) ∘ lastFun f)⟩ =
    ⟨a, (TypeVec.id ::: corec P g) ⊚ f⟩
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case head
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)
this : Inhabited P.A
⊢ ∀ {a a' : P.A} {f : P.B a → P.M} {f' : P.B a' → P.M}, R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩) → a = a'

Tactic:
introv ih

Goal state after:
case head
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)
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
⊢ a = a'
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case tail
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)
this : Inhabited P.A
⊢ ∀ {a : P.A} {f f' : P.B a → P.M}, R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) → ∀ (i : P.B a), R (f i) (f' i)

Tactic:
introv ih

Goal state after:
case tail
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)
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
⊢ R (f i) (f' i)
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: m : ℕ+
v : PrimeMultiset
h : m.factorMultiset ≤ v.prod.factorMultiset ↔ m ∣ v.prod := factorMultiset_le_iff
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod

Tactic:
rw [v.factorMultiset_prod] at h

Goal state after:
m : ℕ+
v : PrimeMultiset
h : m.factorMultiset ≤ v ↔ m ∣ v.prod
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
h✝ : rls < ratio * rrs
⊢ (node ls ll lx lr).node3L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (ls + rs + 1) (node (ls + rls + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)

pp: case neg
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
h✝ : ¬rls < ratio * rrs
⊢ (node ls ll lx lr).node4L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (ls + rs + 1) (node (ls + rll.size + 1) (node ls ll lx lr) x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))

Tactic:
· simp [node3L, node', sr.1]; abel

Goal state after:
case neg
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
h✝ : ¬rls < ratio * rrs
⊢ (node ls ll lx lr).node4L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (ls + rs + 1) (node (ls + rll.size + 1) (node ls ll lx lr) x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case left
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
⊢ w * z = (x * y).succPNat

Tactic:
exact hdet

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

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ All P (l.balanceR x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
rw [balanceR_eq_balance' hl hr sl sr H, all_balance']

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
⊢ (∃ l', Raised l.size l' ∧ BalancedSz l' (insertWith f x r).size) ∨
    ∃ r', Raised r' (insertWith f x r).size ∧ BalancedSz l.size r'

Tactic:
exact Or.inr ⟨_, e, h.3.1⟩

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr x y
| (TypeVec.id ::: Quot.factor r Mcongr this ∘ Quot.mk r) <$$> abs (M.dest (P F) x) =
    (TypeVec.id ::: Quot.factor r Mcongr this ∘ Quot.mk r) <$$> abs (M.dest (P F) y)

Tactic:
lhs
        rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map,
          ← appendFun_comp_id]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr x y
| (TypeVec.id ::: Quot.factor r Mcongr this ∘ Quot.mk r) <$$> abs (M.dest (P F) y)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (abs (g <$$> ⟨a, f⟩)) i = g i '' supp (abs ⟨a, f⟩) i

Tactic:
MvPFunctor.map_eq

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (abs ⟨a, g ⊚ f⟩) i = g i '' supp (abs ⟨a, f⟩) i
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 (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ g (abs ⟨a, splitFun f' (recF g ∘ f)⟩) = g (abs ⟨a, (TypeVec.id ::: recF g) ⊚ splitFun f' f⟩)

Tactic:
appendFun_comp_splitFun,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ g (abs ⟨a, splitFun f' (recF g ∘ f)⟩) = g (abs ⟨a, splitFun (TypeVec.id ⊚ f') (recF g ∘ f)⟩)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv
    ((P F).wMk a (dropFun ((TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f))
      (lastFun ((TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f)))
    ((P F).wMk a f' f)

Tactic:
appendFun_comp_splitFun,

Goal state after:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv
    ((P F).wMk a (dropFun (splitFun (TypeVec.id ⊚ f') (wrepr ∘ f))) (lastFun (splitFun (TypeVec.id ⊚ f') (wrepr ∘ f))))
    ((P F).wMk a f' f)
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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ abs ((TypeVec.id ::: fixToW) <$$> ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩) =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))

Tactic:
MvPFunctor.map_eq

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ abs ⟨a, (TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))