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

Goal state before:
pp: case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝

Tactic:
h'.2

Goal state after:
case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ some y✝ = some y✝
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), ((s, f).2 i).isSome = true ↔ i ∈ (s, f).1
⊢ (fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩)
      ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ }) ⟨(s, f), hf⟩) =
    ⟨(s, f), hf⟩

Tactic:
dsimp only at hf

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), (f i).isSome = true ↔ i ∈ s
⊢ (fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩)
      ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ }) ⟨(s, f), hf⟩) =
    ⟨(s, f), hf⟩
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ (if s = ∅ then ∅ else t) = (image (const α✝ id) s).sup fun f ↦ image f t

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Goal state after:
case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
t : Finset β✝
⊢ (if ∅ = ∅ then ∅ else t) = (image (const α✝ id) ∅).sup fun f ↦ image f t

case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
⊢ (if s = ∅ then ∅ else t) = (image (const α✝ id) s).sup fun f ↦ image f t
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
⊢ ∀ {a_1 b : Sigma β}, a_1.fst ≠ b.fst → decide (a = a_1.fst) = true → decide (a = b.fst) = true → False

Tactic:
intros

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
a✝³ b✝ : Sigma β
a✝² : a✝³.fst ≠ b✝.fst
a✝¹ : decide (a = a✝³.fst) = true
a✝ : decide (a = b✝.fst) = true
⊢ False
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b ↑n).testBit 0 = b

Tactic:
rw [bit_coe_nat]

Goal state after:
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit 0 = b
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (bit b ↑n).testBit m.succ = (↑n).testBit m

Tactic:
rw [bit_coe_nat]

Goal state after:
m : ℕ
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit m.succ = (↑n).testBit m
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case inr.inr.gt
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
⊢ w.HasPeriod (p.gcd q)

Tactic:
have q_lt_p : q < p := Nat.compare_eq_gt.mp hyp

Goal state after:
case inr.inr.gt
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
⊢ w.HasPeriod (p.gcd q)
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
p : (digits 10 n).Palindrome
h : Even (digits 10 n).length
dig : List ℤ := List.map (fun n ↦ ↑n) (digits 10 n)
⊢ 11 ∣ n

Tactic:
replace h : Even dig.length := by rwa [List.length_map]

Goal state after:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n ↦ ↑n) (digits 10 n)
h : Even dig.length
⊢ 11 ∣ n
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
⊢ n.properDivisors = Finset.image (fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) (Finset.Iio n.factorization)

Tactic:
apply Finset.coe_inj.mp
  grind [coe_properDivisors_eq_prod_pow_lt_factorization]

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

Goal state before:
pp: a b n : ℕ
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
obtain rfl | hn := eq_or_ne n 0

Goal state after:
case inl
a b : ℕ
⊢ a ^ 0 ∣ b ↔ a ∣ floorRoot 0 b

case inr
a b n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
⊢ nth p 0 = sInf (Set.ofPred p)

Tactic:
rw [nth_eq_sInf]

Goal state after:
p : ℕ → Prop
⊢ sInf {x | p x ∧ ∀ k < 0, nth p k < x} = sInf (Set.ofPred p)
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case pos.h
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ nth p n ≤ f n

Tactic:
rw [nth_eq_sInf]

Goal state after:
case pos.h
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ sInf {x | p x ∧ ∀ k < n, nth p k < x} ≤ f n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case succ
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ f (n + 1) ≤ nth p (n + 1)

Tactic:
rw [nth_eq_sInf]

Goal state after:
case succ
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ f (n + 1) ≤ sInf {x | p x ∧ ∀ k < n + 1, nth p k < x}
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case neg
a✝ : PosNum
⊢ -(neg a✝).succ = (-neg a✝).pred

Tactic:
succ,

Goal state after:
case neg
a✝ : PosNum
⊢ -a✝.pred'.toZNumNeg = (-neg a✝).pred
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
⊢ ∀ (i : Fin2 n) (x : P.B a i), ∃ y, f i y = f i x

Tactic:
intros

Goal state after:
case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
i✝ : Fin2 n
x✝ : P.B a i✝
⊢ ∃ y, f i✝ y = f i✝ x✝
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x : F.M
⊢ Agree' n x x

Tactic:
induction n generalizing x with

Goal state after:
case zero
F : PFunctor.{uA, uB}
x : F.M
⊢ Agree' 0 x x

case succ
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
x : F.M
⊢ Agree' (n✝ + 1) x x
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize

Tactic:
intros

Goal state after:
a✝ b✝ : Num
⊢ (a✝ * b✝).natSize ≤ a✝.natSize + b✝.natSize
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
⊢ ∀ (a b : Num), ↑(a.gcd b) = (↑a).gcd ↑b

Tactic:
intros

Goal state after:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
⊢ ↑(a✝.gcd b✝) = (↑a✝).gcd ↑b✝
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x : F.M
⊢ Agree' n x x

Tactic:
induction n generalizing x with | zero => ?_ | succ _ n_ih => ?_ <;>
  induction x using PFunctor.M.casesOn' <;> constructor <;> try rfl

Goal state after:
case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ ∀ (i : F.B a✝), Agree' n✝ (f✝ i) (f✝ i)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ ↑(0 / 0) = ↑0 / ↑0

Tactic:
by simp [Int.ediv_zero]

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
x : P.last.M
i : Fin2 n
inst✝ : Inhabited (P.drop.B x.head i)
a : P.last.A := x.head
f : P.last.B x.head → P.last.M := x.children
⊢ ∀ (a_1 : P.last.A) (f_1 : P.last.B a_1 → P.last.M), x.dest = ⟨a, f⟩

Tactic:
intros

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
x : P.last.M
i : Fin2 n
inst✝ : Inhabited (P.drop.B x.head i)
a : P.last.A := x.head
f : P.last.B x.head → P.last.M := x.children
a✝ : P.last.A
f✝ : P.last.B a✝ → P.last.M
⊢ x.dest = ⟨a, f⟩
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
this : BalancedSz l.size rl.size ∧ BalancedSz (l.size + rl.size + 1) rr.size
⊢ Valid' o₁ (l.node3L x rl rx rr) o₂

Tactic:
by
      exact hl.node3L hr.left hr.right this.1 this.2

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

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_2
f : X → ↑F X
x₀ : X
⊢ M.corec f x₀ = M.mk (F.map (M.corec f) (f x₀))

Tactic:
dsimp only [M.corec, M.mk]

Goal state after:
F : PFunctor.{uA, uB}
X : Type u_2
f : X → ↑F X
x₀ : X
⊢ { approx := sCorec f x₀, consistent := ⋯ } = { approx := Approx.sMk (F.map (M.corec f) (f x₀)), consistent := ⋯ }
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
x y z : F.M
hx : Agree' n z x
hy : Agree' n z y
hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y
⊢ x.approx (n + 1) = y.approx (n + 1)

Tactic:
induction n generalizing x y z with
  | zero =>
    specialize hrec [] rfl
    induction x using PFunctor.M.casesOn'
    induction y using PFunctor.M.casesOn'
    simp only [iselect_nil] at hrec
    subst hrec
    simp only [approx_mk, heq_iff_eq, CofixA.intro.injEq,
      eq_iff_true_of_subsingleton, and_self]
  | succ n n_ih =>
    cases hx
    cases hy
    induction x using PFunctor.M.casesOn'
    induction y using PFunctor.M.casesOn'
    subst z
    iterate 3 (have := mk_inj ‹_›; cases this)
    rename_i n_ih a f₃ f₂ hAgree₂ _ _ h₂ _ _ f₁ h₁ hAgree₁ clr
    simp only [approx_mk]
    have := mk_inj h₁
    cases this; clear h₁
    have := mk_inj h₂
    cases this; clear h₂
    congr
    ext i
    apply n_ih
    · solve_by_elim
    · solve_by_elim
    introv h
    specialize hrec (⟨_, i⟩ :: ps) (congr_arg _ h)
    simp only [iselect_cons] at hrec
    exact hrec

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

Goal state before:
pp: F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ x = y

Tactic:
by
  apply ext'; intro i
  induction i with
  | zero => subsingleton
  | succ i i_ih =>
    apply ext_aux x y x
    · rw [← agree_iff_agree']
      apply x.consistent
    · rw [← agree_iff_agree', i_ih]
      apply y.consistent
    introv H'
    dsimp only [iselect] at H
    cases H'
    apply H ps

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

Goal state before:
pp: case inl.inl
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
h : l' + r.size ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
exact le_trans (Nat.le_add_left _ _) (le_trans h (Nat.le_add_left _ _))

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α γ : TypeVec.{u} n
g : α ⟹ γ
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ (g ::: P.wMap g) <$$> P.objAppend1 a f' f = P.objAppend1 a (g ⊚ f') fun x ↦ P.wMap g (f x)

Tactic:
objAppend1,

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α γ : TypeVec.{u} n
g : α ⟹ γ
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ (g ::: P.wMap g) <$$> ⟨a, splitFun f' f⟩ = P.objAppend1 a (g ⊚ f') fun x ↦ P.wMap g (f x)
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α γ : TypeVec.{u} n
g : α ⟹ γ
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ (g ::: P.wMap g) <$$> ⟨a, splitFun f' f⟩ = P.objAppend1 a (g ⊚ f') fun x ↦ P.wMap g (f x)

Tactic:
objAppend1,

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α γ : TypeVec.{u} n
g : α ⟹ γ
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ (g ::: P.wMap g) <$$> ⟨a, splitFun f' f⟩ = ⟨a, splitFun (g ⊚ f') fun x ↦ P.wMap g (f x)⟩
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m.factorMultiset.prod.factorMultiset.prod * (n.factorMultiset - m.factorMultiset).prod = n

Tactic:
rw [← PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, add_tsub_cancel_of_le h,
      prod_factorMultiset]

Goal state after:
Module: Mathlib.Data.Pi.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
b✝ b x : (i : ι) → α i
⊢ (∀ (a : ι), x a ≤ b a) ↔ x ≤ b

Tactic:
le_def

Goal state after:
Module: Mathlib.Data.Pi.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a✝ a x : (i : ι) → α i
⊢ (∀ (a_1 : ι), a a_1 ≤ x a_1) ↔ a ≤ x

Tactic:
le_def

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

Goal state before:
pp: n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α β : TypeVec.{u} m
f : α ⟹ β
inst✝¹ : MvQPF F
inst✝ : (i : Fin2 n) → MvQPF (G i)
⊢ ∀ {α : TypeVec.{u} m} (x : Comp F G α),
    (Comp.mk ∘ (MvFunctor.map fun x ↦ abs) ∘ abs ∘ comp.get)
        ((comp.mk ∘ repr ∘ (MvFunctor.map fun i ↦ repr) ∘ Comp.get) x) =
      x

Tactic:
intros

Goal state after:
n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α β : TypeVec.{u} m
f : α ⟹ β
inst✝¹ : MvQPF F
inst✝ : (i : Fin2 n) → MvQPF (G i)
α✝ : TypeVec.{u} m
x✝ : Comp F G α✝
⊢ (Comp.mk ∘ (MvFunctor.map fun x ↦ abs) ∘ abs ∘ comp.get)
      ((comp.mk ∘ repr ∘ (MvFunctor.map fun i ↦ repr) ∘ Comp.get) x✝) =
    x✝
Module: Mathlib.Data.QPF.Multivariate.Constructions.Comp

Goal state before:
pp: n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α β : TypeVec.{u} m
f : α ⟹ β
inst✝¹ : MvQPF F
inst✝ : (i : Fin2 n) → MvQPF (G i)
⊢ ∀ {α β : TypeVec.{u} m} (f : α ⟹ β) (p : ↑((P F).comp fun i ↦ P (G i)) α),
    (Comp.mk ∘ (MvFunctor.map fun x ↦ abs) ∘ abs ∘ comp.get) (f <$$> p) =
      f <$$> (Comp.mk ∘ (MvFunctor.map fun x ↦ abs) ∘ abs ∘ comp.get) p

Tactic:
intros

Goal state after:
n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α β : TypeVec.{u} m
f : α ⟹ β
inst✝¹ : MvQPF F
inst✝ : (i : Fin2 n) → MvQPF (G i)
α✝ β✝ : TypeVec.{u} m
f✝ : α✝ ⟹ β✝
p✝ : ↑((P F).comp fun i ↦ P (G i)) α✝
⊢ (Comp.mk ∘ (MvFunctor.map fun x ↦ abs) ∘ abs ∘ comp.get) (f✝ <$$> p✝) =
    f✝ <$$> (Comp.mk ∘ (MvFunctor.map fun x ↦ abs) ∘ abs ∘ comp.get) p✝
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 ⊚ TypeVec.id ::: u ∘ Quot.mk r) <$$> M.dest (P F) a₁) =
    abs ((g ⊚ TypeVec.id ::: u ∘ Quot.mk r) <$$> M.dest (P F) a₂)

Tactic:
appendFun_comp

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.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (Ordnode.insert x t).Valid

Tactic:
insert_eq_insertWith

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith (fun x_1 ↦ x) x t).Valid
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case refine_1
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀✝ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀✝) ((P F).wMk a₁ f'₁ f₁)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ : (P F).last.B a → (P F).W α
⊢ ∀ (f₁ : (P F).last.B a → (P F).W α),
    (∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)) →
      (∀ (x : (P F).last.B a), recF u (f₀ x) = recF u (f₁ x)) → recF u ((P F).wMk a f' f₀) = recF u ((P F).wMk a f' f₁)

Tactic:
f₁

Goal state after:
case refine_1
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀✝ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁✝ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀✝) ((P F).wMk a₁ f'₁ f₁✝)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
⊢ (∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)) →
    (∀ (x : (P F).last.B a), recF u (f₀ x) = recF u (f₁ x)) → recF u ((P F).wMk a f' f₀) = recF u ((P F).wMk a f' f₁)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) → ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)

Tactic:
intros

Goal state after:
case mp.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
a✝ : ∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u
i✝ : Fin2 n
x✝ : (P F).B a i✝
⊢ p (f i✝ x✝)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ (∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)) → ∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u

Tactic:
intros

Goal state after:
case mp.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
a✝¹ : ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
i✝ : Fin2 n
u✝ : α i✝
x✝ : (P F).B a i✝
a✝ : f i✝ x✝ = u✝
⊢ p u✝
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case refine_1
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
⊢ ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → (P F).W α),
    (∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)) →
      (∀ (x : (P F).last.B a), recF u (f₀ x) = recF u (f₁ x)) → recF u ((P F).wMk a f' f₀) = recF u ((P F).wMk a f' f₁)

Tactic:
intro a f' f₀ f₁ _h ih; simp only [recF_eq]
        congr 4; funext; apply ih

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{?u.5} n
⊢ ∀ {α : TypeVec.{?u.5} n} (x : ↑P α), id (id x) = x

Tactic:
intros

Goal state after:
n : ℕ
P : MvPFunctor.{?u.5} n
α✝ : TypeVec.{?u.5} n
x✝ : ↑P α✝
⊢ id (id x✝) = x✝
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
P : MvPFunctor.{?u.5} n
⊢ ∀ {α β : TypeVec.{?u.5} n} (f : α ⟹ β) (p : ↑P α), id (f <$$> p) = f <$$> id p

Tactic:
intros

Goal state after:
n : ℕ
P : MvPFunctor.{?u.5} n
α✝ β✝ : TypeVec.{?u.5} n
f✝ : α✝ ⟹ β✝
p✝ : ↑P α✝
⊢ id (f✝ <$$> p✝) = f✝ <$$> id p✝
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case refine_2
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀✝ : (P F).A
f'₀✝ : (P F).drop.B a₀✝ ⟹ α
f₀✝ : (P F).last.B a₀✝ → (P F).W α
a₁✝ : (P F).A
f'₁✝ : (P F).drop.B a₁✝ ⟹ α
f₁ : (P F).last.B a₁✝ → (P F).W α
h : WEquiv ((P F).wMk a₀✝ f'₀✝ f₀✝) ((P F).wMk a₁✝ f'₁✝ f₁)
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
⊢ ∀ (f₁ : (P F).last.B a₁ → (P F).W α),
    abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩ →
      recF u ((P F).wMk a₀ f'₀ f₀) = recF u ((P F).wMk a₁ f'₁ f₁)

Tactic:
f₁

Goal state after:
case refine_2
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀✝ : (P F).A
f'₀✝ : (P F).drop.B a₀✝ ⟹ α
f₀✝ : (P F).last.B a₀✝ → (P F).W α
a₁✝ : (P F).A
f'₁✝ : (P F).drop.B a₁✝ ⟹ α
f₁✝ : (P F).last.B a₁✝ → (P F).W α
h : WEquiv ((P F).wMk a₀✝ f'₀✝ f₀✝) ((P F).wMk a₁✝ f'₁✝ f₁✝)
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
⊢ abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩ →
    recF u ((P F).wMk a₀ f'₀ f₀) = recF u ((P F).wMk a₁ f'₁ f₁)