mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
⊢ Countable (Clopens X)

Tactic:
let f : Clopens X → Finset (countableBasis X) := fun s ↦ (this s).choose

Goal state after:
case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s ↦ ⋯.choose
⊢ Countable (Clopens X)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case refine_2
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ c.eval v
⊢ halt v' ∈ eval (TM2.step tr) i

Tactic:
have := StateTransition.tr_eval (b₁ := Cfg.halt v') tr_respects h₁

Goal state after:
case refine_2
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ c.eval v
this : Cfg.halt v' ∈ eval step (stepNormal c Cont.halt v) → ∃ b₂, TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step tr) i
⊢ halt v' ∈ eval (TM2.step tr) i
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Type (u + 1)
⊢ Presheaf.IsSheaf (coherentTopology Profinite) (locallyConstantPresheaf X)

Tactic:
exact ((CompHausLike.LocallyConstant.functor.{u, u + 1}
      (hs := fun _ _ _ ↦ ((Profinite.effectiveEpi_tfae _).out 0 2).mp)).obj X).property

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

Goal state before:
pp: case hc
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ IsLimit ((forget R).mapCone c)

Tactic:
have := (freeForgetAdjunction R).isRightAdjoint

Goal state after:
case hc
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
this : (forget R).IsRightAdjoint
⊢ IsLimit ((forget R).mapCone c)
Module: Mathlib.Condensed.Light.InternallyProjective

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

Tactic:
simp only [μIso_inv, comp_obj, Functor.comp_map, μIso_hom, μ_natural_left_assoc, δ_μ_assoc]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
α✝ : Type ?u.17
x✝ : α✝
⊢ f (pure x✝) = pure x✝

Tactic:
simp only [map_one, pure]

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

Goal state before:
pp: case neg
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : ¬(π t).2 = none
⊢ ∃ a, coverToFun (fibreIncl π σ) (π_r π σ) a = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩

Tactic:
obtain ⟨n, hn⟩ := Option.ne_none_iff_exists'.mp h

Goal state after:
case neg
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : ¬(π t).2 = none
n : X
hn : (π t).2 = Option.some n
⊢ ∃ a, coverToFun (fibreIncl π σ) (π_r π σ) a = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
h2 : Even l.length
b : Bool
⊢ 2 * count b l = count (!b) l + count b l

Tactic:
hl.count_not_eq_count h2,

Goal state after:
l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
h2 : Even l.length
b : Bool
⊢ 2 * count b l = count b l + count b l
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: case cons
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
i j k : ι
hk : ∀ a_1 ∈ Finset.cons a s ha, f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a

Tactic:
Finset.forall_mem_cons

Goal state after:
case cons
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
i j k : ι
hk : (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ x ∈ s, f k x ≤ f i x ∧ f k x ≤ f j x
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: case cons
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ f a i + ∑ a ∈ s, f a j ≤ f a k + ∑ a ∈ s, f a k

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ f a i ≤ f a k

case h
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a✝¹ : α
s : Finset α
ha : a✝¹ ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
a✝ : a ∈ s
⊢ f a j ≤ f a k
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_5
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this✝ : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop :=
  fun n ↦
    ⇑(ConcreteCategory.hom
        (pullback.lift π (y' ▷ ℕ∪{∞}) (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
          (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
            (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n))
          ⋯))
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
hσ' :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).2 = x
this : CompactSpace ↑(fibres (⇑(ConcreteCategory.hom π')) σ')
⊢ Epi (cover ({ hom := TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ } } ≫ π'))

Tactic:
· rw [LightProfinite.epi_iff_surjective]
    exact coverToFun_surjective _ _ hσ hσ'

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β✝ : α → Type v
β : Type ?u.12
inst✝¹ : FinEnum α
inst✝ : FinEnum β
x : α ⊕ β
⊢ x ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)

Tactic:
cases x <;> simp

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ (insert a b' (insert a b s)).entries = (insert a b' s).entries

Tactic:
simp only [AList.entries_insert, List.kerase_cons_eq]

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

Goal state before:
pp: case h
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
a✝ : List α
⊢ (fun {α} ↦ eta.app α) (traverse f ⟦a✝⟧) = traverse ((fun {α} ↦ eta.app α) ∘ f) ⟦a✝⟧

Tactic:
simp only [quot_mk_to_coe, traverse, lift_coe, Function.comp_apply,
    ApplicativeTransformation.preserves_map, LawfulTraversable.naturality]

Goal state after:
Module: Mathlib.Data.Finset.Functor

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

Tactic:
exact (sup_bot _).symm

Goal state after:
Module: Mathlib.Data.Finset.PImage

Goal state before:
pp: α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
x : α
⊢ x ∈ o.toFinset ↔ x ∈ o

Tactic:
by
  simp [toFinset]

Goal state after:
Module: Mathlib.Data.Finset.PImage

Goal state before:
pp: α : Type u_1
inst✝ : Decidable none.Dom
⊢ none.toFinset = ∅

Tactic:
by
  simp [toFinset]

Goal state after:
Module: Mathlib.Data.Finset.PImage

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Decidable (some a).Dom
⊢ (some a).toFinset = {a}

Tactic:
by
  simp [toFinset]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : a✝ ∉ s✝
ih : ∑ x ∈ s✝, (f x).slice i hid = (∑ x ∈ s✝, f x).slice i hid
⊢ ∑ x ∈ insert a✝ s✝, (f x).slice i hid = (∑ x ∈ insert a✝ s✝, f x).slice i hid

Tactic:
Finset.sum_insert h_not_in,

Goal state after:
case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : a✝ ∉ s✝
ih : ∑ x ∈ s✝, (f x).slice i hid = (∑ x ∈ s✝, f x).slice i hid
⊢ (f a✝).slice i hid + ∑ x ∈ s✝, (f x).slice i hid = (∑ x ∈ insert a✝ s✝, f x).slice i hid
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
⊢ (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯).slice = x.slice

Tactic:
ext i hid

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯).slice i hid = x.slice i hid
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: i : ℕ
hn : ¬i + 1 = 0
⊢ ((if Even ↑i then -fib ↑i else fib ↑i) * if Even (↑(i + 1) + 1) then -fib (↑(i + 1) + 1) else fib (↑(i + 1) + 1)) +
      -(if Even ↑(i + 1) then -fib ↑(i + 1) else fib ↑(i + 1)) ^ 2 =
    (-1) ^ (-↑(i + 1)).natAbs

Tactic:
natAbs_neg,

Goal state after:
i : ℕ
hn : ¬i + 1 = 0
⊢ ((if Even ↑i then -fib ↑i else fib ↑i) * if Even (↑(i + 1) + 1) then -fib (↑(i + 1) + 1) else fib (↑(i + 1) + 1)) +
      -(if Even ↑(i + 1) then -fib ↑(i + 1) else fib ↑(i + 1)) ^ 2 =
    (-1) ^ (↑(i + 1)).natAbs
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℤ
⊢ (bit b n).bodd = b

Tactic:
rw [bit_val]

Goal state after:
b : Bool
n : ℤ
⊢ (2 * n + bif b then 1 else 0).bodd = b
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑0 - ↑v) / ↑r⌉ ≤ ⌈(↑b - ↑v) / ↑r⌉

Tactic:
gcongr

Goal state after:
case a
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ 0 ≤ b
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l = l ↔ ∀ (hl : 0 < l.length), ¬p l[0] = true

Tactic:
rcases l with - | ⟨hd, tl⟩
  · simp
  · rw [dropWhile]
    by_cases h_p_hd : p hd
    · simp only [h_p_hd, length_cons, Nat.zero_lt_succ, getElem_cons_zero, not_true_eq_false,
        imp_false, iff_false]
      intro h
      replace h := congrArg length h
      have := length_dropWhile_le p tl
      simp at h
      lia
    · simp [h_p_hd]

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

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

Tactic:
set ph := p head with phh

Goal state after:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
ph : Bool := p head
phh : ph = p head
⊢ find? p (head :: tail) = (dropWhile (fun x ↦ !p x) (head :: tail)).head?
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p l.reverse
⊢ p x = true

Tactic:
exact mem_takeWhile_imp hx

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

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

Tactic:
cons_inj_right

Goal state after:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) #[] = tl ++ [f a]
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 =
    ((head✝¹, some head✝) :: (zipWithLeft' Prod.mk atl btl).fst, (zipWithLeft' Prod.mk atl btl).snd).fst

Tactic:
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.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
bs : List β
⊢ zipWithLeft Prod.mk as bs = (zipWithLeft' Prod.mk as bs).fst

Tactic:
cases as with

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

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
⊢ splitBy r l = [] ↔ l = []

Tactic:
by
  have := flatten_splitBy r l
  refine ⟨fun _ ↦ ?_, ?_⟩ <;> simp_all

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

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

Tactic:
rw [nil_append]
    cases m with
    | nil => simp [splitBy.loop]
    | cons c m => simp_all [splitBy.loop, splitByLoop_eq_append [_], splitBy]

Goal state after:
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]; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : mulRightLinearMap l R a = 0
inhabited_h : Inhabited l
i : m
j : n
⊢ a i j = 0 i j

Tactic:
replace h := DFunLike.congr_fun h (Matrix.single (default : l) i 1)
    simpa using Matrix.ext_iff.2 h default j

Goal state after:
Module: Mathlib.Data.Nat.Prime.Factorial

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ p ∣ (n + 1)! ↔ p ≤ n + 1

Tactic:
rw [factorial_succ, hp.dvd_mul, Prime.dvd_factorial hp]
    exact
      ⟨fun h => h.elim (le_of_dvd (succ_pos _)) le_succ_of_le, fun h =>
        (_root_.lt_or_eq_of_le h).elim (Or.inr ∘ le_of_lt_succ) fun h => Or.inl <| by rw [h]⟩

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

Goal state before:
pp: n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ fib a + (map fib l).sum < fib a + fib (a - 1)

Tactic:
gcongr

Goal state after:
case bc
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib l).sum < fib (a - 1)
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h✝ : n % p < (k % p, k / p).1
⊢ ?m.472 < ?m.473

Tactic:
by tauto

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h✝ : n / p + 1 ≤ (k % p, k / p).2
⊢ ?m.472 < ?m.473

Tactic:
by tauto

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

Goal state before:
pp: _a _b : ℕ
hab : _a ≤ _b
⊢ _a + 1 ≤ _b + 1

Tactic:
gcongr

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

Goal state before:
pp: m n : ℕ
h : fib m ≤ n
⊢ fib m + 1 ≤ n + 1

Tactic:
gcongr

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) *
      ↑(∏ x ∈ range a, (n / p ^ x % p).choose (k / p ^ x % p)) [ZMOD
    ↑p]

Tactic:
gcongr

Goal state after:
case h₁
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a).choose (k / p ^ a)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Infinite
n : ℕ
h : n ≤ k
ha : p (nth p n)
⊢ nth p n ≤ nth p k

Tactic:
← nth_le_nth hf

Goal state after:
case inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Infinite
n : ℕ
h : nth p n ≤ nth p k
ha : p (nth p n)
⊢ nth p n ≤ nth p k
Module: Mathlib.Data.Ordmap.Ordnode

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

pp: case node.node.refine_2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

Tactic:
· rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
        · exact nil
        --should not happen
        rcases id rr with _ | rrs
        · 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:
case node.node.refine_2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(pos p).bit0 = ↑(pos p) + ↑(pos p)

Tactic:
rw [ZNum.bit0, cast_pos, cast_pos]

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit0 = ↑p + ↑p
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
a b c : ZNum
h : ↑a ≤ ↑b
⊢ ↑a + ↑c ≤ ↑b + ↑c

Tactic:
gcongr

Goal state after:
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
⊢ 2 * l.size ≤ ml.size + mr.size + 1

Tactic:
have := le_trans this (add_le_add_right mr₁ _)

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 * (ml.size + mr.size + 1) + (ml.size + mr.size + 1)
⊢ 2 * l.size ≤ ml.size + mr.size + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit1.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + 2 * (↑d * ↑q) + 1 = 2 * ↑n + 1

Tactic:
← mul_add,

Goal state after:
case bit1.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * (↑r + ↑d * ↑q) + 1 = 2 * ↑n + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit0.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + 2 * (↑d * ↑q) = 2 * ↑n

Tactic:
← mul_add,

Goal state after:
case bit0.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * (↑r + ↑d * ↑q) = 2 * ↑n
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case neg.inl
α : 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
rl0 : rl.size = 0
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂

Tactic:
rl0,

Goal state after:
case neg.inl
α : 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 : ¬0 < ratio * rr.size
rl0 : rl.size = 0
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂