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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P.toCondensed ⊗ S.toCondensed) ⟶ B
h :
  ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g',
        (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫
            (free R).map (μIso lightProfiniteToLightCondSet P S).inv ≫ g =
          g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫ g = g' ≫ e

Tactic:
obtain ⟨S', π, hπ, g', hh⟩ := h

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P.toCondensed ⊗ S.toCondensed) ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P ⊗ S').toCondensed ⟶ A
hh :
  (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫
      (free R).map (μIso lightProfiniteToLightCondSet P S).inv ≫ g =
    g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫ g = g' ≫ e
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S ⊗ P).toCondensed ⟶ B
h :
  ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g',
        (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫
            (free R).map (μIso lightProfiniteToLightCondSet S P).hom ≫ g =
          g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g = g' ≫ e

Tactic:
obtain ⟨S', π, hπ, g', hh⟩ := h

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S ⊗ P).toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S'.toCondensed ⊗ P.toCondensed) ⟶ A
hh :
  (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫
      (free R).map (μIso lightProfiniteToLightCondSet S P).hom ≫ g =
    g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g = g' ≫ e
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S.toCondensed ⊗ P.toCondensed) ⟶ B
h :
  ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g',
        (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫
            (free R).map (μIso lightProfiniteToLightCondSet S P).inv ≫ g =
          g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫ g = g' ≫ e

Tactic:
obtain ⟨S', π, hπ, g', hh⟩ := h

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S.toCondensed ⊗ P.toCondensed) ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S' ⊗ P).toCondensed ⟶ A
hh :
  (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫
      (free R).map (μIso lightProfiniteToLightCondSet S P).inv ≫ g =
    g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫ g = g' ≫ e
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // α.PredLast pp p_1 }) i.fs
⊢ True = ofRepeat (α.PredLast' pp i.fs ↑x)

Tactic:
erw [const_iff_true]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ Part.fix g = g (Part.fix g)

Tactic:
rw [fix_eq_ωSup_of_ωScottContinuous hc, hc.map_ωSup]
  apply le_antisymm
  · apply ωSup_le_ωSup_of_le _
    intro i
    exists i
    apply le_f_of_mem_approx _ ⟨i, rfl⟩
  · apply ωSup_le_ωSup_of_le _
    intro i
    exists i.succ

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_2
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ card α = 1

pp: case e_3
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ equiv ≍ Equiv.ofUnique α (Fin 1)

pp: case e_4
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b

Tactic:
· exact card_eq_one α

Goal state after:
case e_3
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ equiv ≍ Equiv.ofUnique α (Fin 1)

case e_4
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
⊢ insertRec H0 IH { entries := [], nodupKeys := ⋯ } = H0

Tactic:
insertRec

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
⊢ H0 = H0
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
hl : l.NodupKeys
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ insertRec H0 IH { entries := c :: l, nodupKeys := ⋯ } ≍
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })

Tactic:
insertRec

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
hl : l.NodupKeys
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ ⋯.mpr (IH c.fst c.snd { entries := l, nodupKeys := ⋯ } ⋯ (insertRec H0 IH { entries := l, nodupKeys := ⋯ })) ≍
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a ∉ erase a s

Tactic:
rw [mem_erase, not_and_or, not_not]
  left
  rfl

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

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

Tactic:
by_cases h₂ : a' = ah

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

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)
Module: Mathlib.Data.List.Sigma

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

Tactic:
by_cases h₂ : a' = ah

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

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: x a : ℤ
⊢ fib (x + a) ^ 2 - fib x * fib (x + 2 * a) =
    (fib x * fib (a + 1) + fib (x - 1) * fib a) ^ 2 -
      fib x * (fib x * (fib (a + 1) ^ 2 + fib a ^ 2) + fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a))

Tactic:
add_comm x

Goal state after:
x a : ℤ
⊢ fib (a + x) ^ 2 - fib x * fib (x + 2 * a) =
    (fib x * fib (a + 1) + fib (x - 1) * fib a) ^ 2 -
      fib x * (fib x * (fib (a + 1) ^ 2 + fib a ^ 2) + fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise or m n = m.lor n

Tactic:
rcases m with m | m <;> rcases n with n | n <;> try {rfl}
    <;> simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff,
      negSucc.injEq, Bool.true_or]

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(x || !y)) m n = Nat.bitwise (fun a b ↦ a && !b) n m

case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || y)) m n = Nat.bitwise (fun a b ↦ a && !b) m n

case negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || !y)) m n = m &&& n
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
v : β → α → β
a : α
b : β
hv : RightCommutative v
⊢ foldl v (v b a) l = v (foldl v b l) a

Tactic:
induction l generalizing a b

Goal state after:
case nil
α : Type u_1
β : Type u_2
v : β → α → β
hv : RightCommutative v
a : α
b : β
⊢ foldl v (v b a) [] = v (foldl v b []) a

case cons
α : Type u_1
β : Type u_2
v : β → α → β
hv : RightCommutative v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {a : α} {b : β}, foldl v (v b a) tail✝ = v (foldl v b tail✝) a
a : α
b : β
⊢ foldl v (v b a) (head✝ :: tail✝) = v (foldl v b (head✝ :: tail✝)) a
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β → β
a : α
b : β
hf : LeftCommutative f
⊢ f a (foldr f b l) = foldr f (f a b) l

Tactic:
induction l generalizing a b

Goal state after:
case nil
α : Type u_1
β : Type u_2
f : α → β → β
hf : LeftCommutative f
a : α
b : β
⊢ f a (foldr f b []) = foldr f (f a b) []

case cons
α : Type u_1
β : Type u_2
f : α → β → β
hf : LeftCommutative f
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {a : α} {b : β}, f a (foldr f b tail✝) = foldr f (f a b) tail✝
a : α
b : β
⊢ f a (foldr f b (head✝ :: tail✝)) = foldr f (f a b) (head✝ :: tail✝)
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile (fun a ↦ decide (p a = true ∧ p a = true)) l = takeWhile p l

Tactic:
and_self_iff,

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile (fun a ↦ decide (p a = true)) l = takeWhile p l
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: m : ℕ
h : 0 < m
⊢ Ico (m - 1) m = [m - 1]

Tactic:
simp [Ico, Nat.sub_sub_self (succ_le_of_lt h)]

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

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
n : ℕ
⊢ (n :: sz).splitLengths l = take n l :: sz.splitLengths (drop n l)

Tactic:
by
  simp [splitLengths]

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

Goal state before:
pp: case zero
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a.length = 0
⊢ Acc (Shortlex r) a

Tactic:
List.length_eq_zero_iff

Goal state after:
case zero
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a = []
⊢ Acc (Shortlex r) a
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
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 = false
IH :
  ∀ {a_1 : α} {g_1 : List α},
    (∀ (b : α), b ∈ g_1.head? → r b a_1 = true) →
      IsChain (fun y x ↦ r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun b a ↦ r a b = true) (g.reverse ++ [a]).reverse

Tactic:
rw [reverse_append, reverse_cons, reverse_nil, nil_append, reverse_reverse]

Goal state after:
case h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
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 = false
IH :
  ∀ {a_1 : α} {g_1 : List α},
    (∀ (b : α), b ∈ g_1.head? → r b a_1 = true) →
      IsChain (fun y x ↦ r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun b a ↦ r a b = true) ([a] ++ g)
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p : ℕ
per : w.HasPeriod p
⊢ take p w ++ drop p w <+: take p w ++ w

Tactic:
simp_all [HasPeriod, take_append_drop]

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

Goal state before:
pp: α : 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
⊢ p.gcd q ≤ p - q

Tactic:
← gcd_stable

Goal state after:
α : 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
⊢ (p - q).gcd q ≤ p - q
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : 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 q (drop q w) = take q w

Tactic:
let ⟨z, hz⟩ := per_q.drop_prefix

Goal state after:
α : 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
z : List α
hz : drop q w ++ z = w
⊢ take q (drop q w) = take q w
Module: Mathlib.Data.Multiset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ ∏ x ∈ (toDFinsupp s).support ∪ (toDFinsupp t).support, (count x t + 1 - count x s) =
    ∏ x ∈ s.toFinset ∪ t.toFinset, (count x t + 1 - count x s)

Tactic:
toDFinsupp_support

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ ∏ x ∈ (toDFinsupp s).support ∪ (toDFinsupp t).support, ((↑(count x t) - ↑(count x s)).natAbs + 1) =
    ∏ x ∈ s.toFinset ∪ t.toFinset, ((↑(count x t) - ↑(count x s)).natAbs + 1)

Tactic:
toDFinsupp_support

Goal state after:
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:
by
  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: case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌊/⌋ n

Tactic:
obtain rfl | rfl := h <;> simp

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

Goal state before:
pp: case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌈/⌉ n

Tactic:
obtain rfl | rfl := h <;> simp

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: case case1
⊢ (map fib (zeckendorf 0)).sum = 0

Tactic:
simp_all [fib_greatestFib_le]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: case case2
n✝ : ℕ
ih1✝ : (map fib (n✝ + 1 - fib (n✝ + 1).greatestFib).zeckendorf).sum = n✝ + 1 - fib (n✝ + 1).greatestFib
⊢ (map fib n✝.succ.zeckendorf).sum = n✝.succ

Tactic:
simp_all [fib_greatestFib_le]

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

Goal state before:
pp: case node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
exact node (rs + 1) nil x r

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

Goal state before:
pp: case node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

Tactic:
· refine if rs > delta * ls then ?_ else node (ls + rs + 1) l x r
      rcases id rr with _ | rrs
      · exact nil
      --should not happen
      rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
      · exact nil
      --should not happen
      exact
        if rls < ratio * rrs then node (ls + rs + 1) (node (ls + rls + 1) l x rl) rx rr
        else
          node (ls + rs + 1) (node (ls + size rll + 1) l x rll) rlx
            (node (size rlr + rrs + 1) rlr rx rr)

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

Goal state before:
pp: case h.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ x = ⟨a, fun i ↦ (↑(f i)).1⟩

Tactic:
← xeq,

Goal state after:
case h.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun t ↦ (↑t).1) <$> u = ⟨a, fun i ↦ (↑(f i)).1⟩
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ x = ⟨a, fun i j ↦ (↑(f i j)).1⟩

Tactic:
← xeq,

Goal state after:
case h.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).1) <$$> u = ⟨a, fun i j ↦ (↑(f i j)).1⟩
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
h :
  ↑d ≤
    ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2
r₂ : ℕ
e' :
  ↑d + r₂ =
    ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2
⊢ False

Tactic:
← Num.to_of_nat r₂,

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
r₂ : ℕ
e' :
  ↑d + ↑↑r₂ =
    ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2
⊢ False
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : 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✝ : delta * (ratio * l.size) ≤ ratio * (ml.size + mr.size + 1) + ratio * r.size
this : delta * (ratio * l.size) ≤ ratio * (ml.size + mr.size + 1) + (ml.size + mr.size + 1)
⊢ 2 * l.size ≤ ml.size + mr.size + 1

Tactic:
← Nat.succ_mul

Goal state after:
α : 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✝ : delta * (ratio * l.size) ≤ ratio * (ml.size + mr.size + 1) + ratio * r.size
this : delta * (ratio * l.size) ≤ ratio.succ * (ml.size + mr.size + 1)
⊢ 2 * l.size ≤ ml.size + mr.size + 1
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 cons
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → iselect ps_tail x = default.head
x : F.M
a : F.A
i : F.B a
h : ¬IsPath (⟨a, i⟩ :: ps_tail) x
⊢ iselect (⟨a, i⟩ :: ps_tail) x = default.head

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

Goal state after:
case cons.f
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → iselect ps_tail x = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
⊢ iselect (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩) = default.head
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ : dropFun ((TypeVec.id ::: Quot.mk R) ⊚ fx) = dropFun ((TypeVec.id ::: Quot.mk R) ⊚ fy)
⊢ dropFun fx = dropFun fy

Tactic:
simpa using! h₁

Goal state after: