mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
S : LightProfinite
x : X.obj.obj (Opposite.op S)
⊢ Continuous fun a ↦
    (ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1}))))
      ((ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) a).op)) x)

Tactic:
show (fun (a : S) ↦ f.hom.app ⟨of PUnit⟩ (X.obj.map ((of PUnit.{u + 1}).const a).op x)) = _
        from funext fun a ↦ NatTrans.naturality_apply f.hom ((of PUnit.{u + 1}).const a).op x

Goal state after:
X Y : LightCondSet
f : X ⟶ Y
S : LightProfinite
x : X.obj.obj (Opposite.op S)
⊢ Continuous fun a ↦
    (ConcreteCategory.hom (Y.obj.map (CompHausLike.const (of PUnit.{u + 1}) a).op))
      ((ConcreteCategory.hom (f.hom.app (Opposite.op S))) x)
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X Y✝ : LightCondSet
f : X ⟶ Y✝
Y : LightCondSet
⊢ lightCondSetToTopCat.map ({ app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 }.app Y) ≫
      { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }.app (lightCondSetToTopCat.obj Y) =
    𝟙 (lightCondSetToTopCat.obj Y)

Tactic:
by
    ext
    change Y.obj.map (𝟙 _) _ = _
    simp

Goal state after:
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ (lightProfiniteToLightCondSet.map π ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv (lightProfiniteToLightCondSet.obj S) Y) p).hom =
    ((coherentTopology LightProfinite).yonedaEquiv.symm
        ((ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
          ((coherentTopology LightProfinite).yonedaEquiv
            (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p)))).hom

Tactic:
GrothendieckTopology.map_yonedaEquiv',

Goal state after:
R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ (lightProfiniteToLightCondSet.map π ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv (lightProfiniteToLightCondSet.obj S) Y) p).hom =
    ((coherentTopology LightProfinite).yonedaEquiv.symm
        ((ConcreteCategory.hom
            ((((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p).hom.app (Opposite.op T)))
          (Quiver.Hom.unop (Opposite.op π)))).hom
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X Y : CondensedSet
⊢ condensedSetToTopCat.map ({ app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 }.app Y) ≫
      { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }.app (condensedSetToTopCat.obj Y) =
    𝟙 (condensedSetToTopCat.obj Y)

Tactic:
by
    ext
    change Y.obj.map (𝟙 _) _ = _
    simp

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
⊢ y = b

Tactic:
rcases le_total i j with H | H

Goal state after:
case pos.mpr.inr.inl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ y = b

case pos.mpr.inr.inr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ y = b
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : f.Realizer
x✝ : Set β
⊢ x✝ ∈ { f := fun s ↦ m '' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (map m f).sets

Tactic:
simp only [CFilter.toFilter, image_subset_iff, mem_ofPred_eq, Filter.mem_sets, mem_map]
      rw [F.mem_sets]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ (f.rangeIcc g).support
h : x ∉ f.support ∪ g.support
⊢ Icc 0 (g x) = 0

Tactic:
notMem_support_iff.1 (notMem_mono subset_union_right h)

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ (f.rangeIcc g).support
h : x ∉ f.support ∪ g.support
⊢ Icc 0 0 = 0
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
| recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) α =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
lhs; unfold recEmptyOption

Goal state after:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
| match cardeq : card α with
  | 0 => congr pempty inst✝ cardeq empty
  | n.succ =>
    let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n)) ↑↑(finChoice n)) inst✝ ⋯
      (option fN (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin n))))
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
h : ¬a ∈ s
⊢ ⟨a, b⟩ :: kerase a s.entries = ⟨a, b⟩ :: s.entries

Tactic:
kerase_of_notMem_keys h

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
h : ¬a ∈ s
⊢ ⟨a, b⟩ :: s.entries = ⟨a, b⟩ :: s.entries
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: α β : Type u_1
h : α → β
⊢ Functor.map h ∘ ofList = ofList ∘ Functor.map h

Tactic:
by
  funext; simp only [Function.comp_apply, fmap_def, map_coe, List.map_eq_map]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (dlookup a l).toList.Nodup

Tactic:
apply Option.toList_nodup

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a' : α
tl : List (Sigma β)
h : a' ≠ a'
ih : dlookup a' (kerase a' tl) = dlookup a' tl
bh : β a'
⊢ dlookup a' (kerase a' (⟨a', bh⟩ :: tl)) = dlookup a' (⟨a', bh⟩ :: tl)

Tactic:
cases Ne.irrefl h

Goal state after:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
suffices f.toAList.lookup a = some (f a) by simp [this]

Goal state after:
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ lookup a f.toAList = some (f a)
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
⊢ find? p (head :: tail) = (dropWhile (fun x ↦ !p x) (head :: tail)).head?

Tactic:
rw [find?_cons_of_neg phh', dropWhile_cons_of_pos]

Goal state after:
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
⊢ find? p tail = (dropWhile (fun x ↦ !p x) tail).head?

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
Module: Mathlib.Data.List.Map2

Goal state before:
pp: case cons.cons
α : Type u
β : Type v
head✝¹ : α
atl : List α
head✝ : β
btl : List β
⊢ (head✝¹, some head✝) :: zipWithLeft Prod.mk atl btl = (zipWithLeft' Prod.mk (head✝¹ :: atl) (head✝ :: btl)).fst

Tactic:
zipWithLeft',

Goal state after:
case cons.cons
α : Type u
β : Type v
head✝¹ : α
atl : List α
head✝ : β
btl : List β
⊢ (head✝¹, some head✝) :: zipWithLeft Prod.mk atl btl =
    ((head✝¹, some head✝) :: (zipWithLeft' Prod.mk atl btl).fst, (zipWithLeft' Prod.mk atl btl).snd).fst
Module: Mathlib.Data.List.Map2

Goal state before:
pp: case cons.cons
α : Type u
β : Type v
head✝¹ : α
atl : List α
head✝ : β
btl : List β
⊢ zipWithLeft Prod.mk (head✝¹ :: atl) (head✝ :: btl) = (zipWithLeft' Prod.mk (head✝¹ :: atl) (head✝ :: btl)).fst

Tactic:
rw [zipWithLeft, zipWithLeft', cons_inj_right]

Goal state after:
case cons.cons
α : Type u
β : Type v
head✝¹ : α
atl : List α
head✝ : β
btl : List β
⊢ zipWithLeft Prod.mk atl btl = (zipWithLeft' Prod.mk atl btl).fst
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
l : List α
⊢ l.length < (head :: tail).length → Acc (Shortlex r) l

Tactic:
ll

Goal state after:
case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
l : List α
ll : l.length < (head :: tail).length
⊢ Acc (Shortlex r) l
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_1
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = true
h : m ∈ splitBy.loop r l b (a :: g) []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
apply IH _ (isChain_cons.2 ⟨hga, hg⟩) h

Goal state after:
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = true
h : m ∈ splitBy.loop r l b (a :: g) []
⊢ ∀ (b_1 : α), b_1 ∈ (a :: g).head? → r b_1 b = true
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast hn) x = false
⊢ splitBy r (a :: l ++ m) = (a :: l) :: splitBy r m

Tactic:
rw [cons_append, splitBy, splitByLoop_append h ha]

Goal state after:
case cons
α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast hn) x = false
⊢ ([].reverse ++ a :: l) :: splitBy r m = (a :: l) :: splitBy r 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
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
⊢ w.HasPeriod (p.gcd q)

Tactic:
have IH : HasPeriod (drop q w) ((p - q).gcd q) :=
        per_diff.gcd per_q' (by simp; lia)

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
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
IH : (drop q w).HasPeriod ((p - q).gcd q)
⊢ w.HasPeriod (p.gcd q)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : {x | x ∈ l'}.Pairwise (Coprime on s)
co : {x | x ∈ l}.Pairwise (Coprime on s)
lco : List.Pairwise (Coprime on s) l
⊢ ∀ {m' : Multiset ι} {e : ↑l = m'} {nod'' : m'.Nodup} {hs'' : ∀ i ∈ m', s i ≠ 0}
    {co'' : {x | x ∈ m'}.Pairwise (Coprime on s)},
    ↑(Eq.ndrec (motive := fun m ↦
          m.Nodup → (∀ i ∈ m, s i ≠ 0) → {x | x ∈ m}.Pairwise (Coprime on s) → { k // ∀ i ∈ m, k ≡ a i [MOD s i] })
          (fun nod x co ↦ chineseRemainderOfList a s l ⋯) e nod'' hs'' co'') =
      ↑(chineseRemainderOfList a s l lco)

Tactic:
rintro _ rfl _ _ _; rfl

Goal state after:
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
m : Multiset ι
nod : m.Nodup
hs : ∀ i ∈ m, s i ≠ 0
pp : {x | x ∈ m}.Pairwise (Coprime on s)
⊢ ↑(chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s m).prod

Tactic:
induction m using Quot.ind with | _ l

Goal state after:
case mk
ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, s i ≠ 0
pp : {x | x ∈ Quot.mk (⇑(List.isSetoid ι)) l}.Pairwise (Coprime on s)
⊢ ↑(chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s (Quot.mk (⇑(List.isSetoid ι)) l)).prod
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: a : ℕ
l : List ℕ
hl : (a :: l).IsZeckendorfRep
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Tactic:
by
    have hl' := hl
    simp only [IsZeckendorfRep, cons_append, isChain_iff_pairwise, pairwise_cons, mem_append,
      mem_singleton, or_imp, forall_and, forall_eq, zero_add] at hl
    rw [← isChain_iff_pairwise] at hl
    have ha : 0 < a := hl.1.2.trans_lt' zero_lt_two
    suffices h : greatestFib (fib a + sum (map fib l)) = a by
      simp only [map, List.sum_cons, add_pos_iff, fib_pos.2 ha, true_or, zeckendorf_of_pos, h,
      add_tsub_cancel_left, zeckendorf_sum_fib hl.2]
    simp only [add_comm, add_assoc, greatestFib, findGreatest_eq_iff, ne_eq, ha.ne',
      not_false_eq_true, le_add_iff_nonneg_left, _root_.zero_le, forall_true_left, not_le, true_and]
    refine ⟨le_add_of_le_right <| le_fib_add_one _, fun n hn _ ↦ ?_⟩
    rw [add_comm, ← List.sum_cons, ← map_cons]
    exact hl'.sum_fib_lt (by simpa)

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
⊢ p (nth p a)

Tactic:
by
  by_cases h' : ∀ hf : (Set.ofPred p).Finite, a < #hf.toFinset
  · exact nth_mem a h'
  · simp only [not_forall, not_lt] at h'
    have h'b : ∃ hf : (Set.ofPred p).Finite, #hf.toFinset ≤ b := by
      rcases h' with ⟨hf, ha⟩
      exact ⟨hf, ha.trans hab⟩
    have ha0 : nth p a = 0 := by simp [nth_eq_zero, h']
    have hb0 : nth p b = 0 := by simp [nth_eq_zero, h'b]
    rw [ha0]
    rwa [hb0] at h

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.size l.dual.size

Tactic:
size_dual

Goal state after:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.size l.size
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)

Tactic:
refine ⟨a, fun i => (f i).val, ?_, fun i => (f i).property⟩

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ x = ⟨a, fun i ↦ ↑(f i)⟩
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mpr
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x

Tactic:
simp only [liftp_iff']

Goal state after:
case mpr
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
⊢ BalancedSz l r₂

Tactic:
by
  refine or_iff_not_imp_left.2 fun h => ?_
  refine ⟨?_, h₂.resolve_left h⟩
  cases H with
  | inl H =>
    cases r₂
    · cases h (le_trans (Nat.add_le_add_left (Nat.zero_le _) _) H)
    · exact le_trans (le_trans (Nat.le_add_right _ _) H) (Nat.le_add_left 1 _)
  | inr H =>
    exact le_trans H.1 (Nat.mul_le_mul_left _ h₁)

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

Goal state before:
pp: α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
⊢ BalancedSz r.size l.dual.size

Tactic:
size_dual

Goal state after:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
⊢ BalancedSz r.size l.size
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
x✝ : m ∣ n
k : ZNum
e : n = m * k
⊢ ↑n = ↑m * ↑k

Tactic:
by simp [e]

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

Goal state before:
pp: case neg.inr.refine_5
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
⊢ l.size + ml.size + 1 ≤ delta * (mr.size + r.size + 1)

Tactic:
exact Valid'.node4L_lemma₄ lr₁ mr₂ mm₁

Goal state after:
Module: Mathlib.Data.Num.ZNum

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

Tactic:
simp only [natSize_to_nat, cast_mul]

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

Goal state before:
pp: ⊢ ∀ (a b : Num), ↑(a.gcd b) = (↑a).gcd ↑b

Tactic:
have : ∀ a b : Num, (a * b).natSize ≤ a.natSize + b.natSize := by
    intros
    simp only [natSize_to_nat, cast_mul]
    rw [Nat.size_le, pow_add]
    exact mul_lt_mul'' (Nat.lt_size_self _) (Nat.lt_size_self _) (Nat.zero_le _) (Nat.zero_le _)

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.Num.ZNum

Goal state before:
pp: n d : PosNum
⊢ -[↑n.pred' / ↑d+1] = -[↑n.pred' / (↑d.pred' + 1)+1]

Tactic:
d.to_nat_eq_succ_pred

Goal state after:
n d : PosNum
⊢ -[↑n.pred' / (↑d.pred' + 1)+1] = -[↑n.pred' / (↑d.pred' + 1)+1]
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
⊢ ↑(↑n.pred' / ↑d).succ = ↑(↑n.pred' / (↑d.pred' + 1)).succ

Tactic:
d.to_nat_eq_succ_pred

Goal state after:
n d : PosNum
⊢ ↑(↑n.pred' / (↑d.pred' + 1)).succ = ↑(↑n.pred' / (↑d.pred' + 1)).succ
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ delta * r.size < l.dual.size

Tactic:
size_dual

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ delta * r.size < l.size