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 : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj S.toCondensed ⊗ (free R).obj P ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S'.toCondensed ⊗ P) ⟶ A
hh : (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ (μIso (free R) S.toCondensed P).inv ≫ g = g' ≫ e
⊢ (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ g = ((μIso (free R) S'.toCondensed P).hom ≫ g') ≫ e

Tactic:
assoc,

Goal state after:
case refine_2
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 ⊗ (free R).obj P ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S'.toCondensed ⊗ P) ⟶ A
hh : (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ (μIso (free R) S.toCondensed P).inv ≫ g = g' ≫ e
⊢ (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ g = (μIso (free R) S'.toCondensed P).hom ≫ 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 (P ⊗ S).toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P.toCondensed ⊗ S'.toCondensed) ⟶ A
hh :
  (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫
      (free R).map (μIso lightProfiniteToLightCondSet P S).hom ≫ g =
    g' ≫ e
⊢ (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫ g =
    ((free R).map (μIso lightProfiniteToLightCondSet P S').inv ≫ g') ≫ e

Tactic:
assoc,

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 (P ⊗ S).toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P.toCondensed ⊗ S'.toCondensed) ⟶ A
hh :
  (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫
      (free R).map (μIso lightProfiniteToLightCondSet P S).hom ≫ g =
    g' ≫ e
⊢ (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫ g =
    (free R).map (μIso lightProfiniteToLightCondSet P S').inv ≫ 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 (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
⊢ (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫ g =
    ((free R).map (μIso lightProfiniteToLightCondSet P S').hom ≫ g') ≫ e

Tactic:
assoc,

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
⊢ (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫ g =
    (free R).map (μIso lightProfiniteToLightCondSet P S').hom ≫ 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
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
⊢ (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g =
    ((free R).map (μIso lightProfiniteToLightCondSet S' P).inv ≫ g') ≫ e

Tactic:
assoc,

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
⊢ (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g =
    (free R).map (μIso lightProfiniteToLightCondSet S' P).inv ≫ 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
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
⊢ (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫ g =
    ((free R).map (μIso lightProfiniteToLightCondSet S' P).hom ≫ g') ≫ e

Tactic:
assoc,

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
⊢ (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫ g =
    (free R).map (μIso lightProfiniteToLightCondSet S' P).hom ≫ g' ≫ e
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = List.foldl f x (FreeMonoid.toList (FreeMonoid.ofList (toList xs)))

Tactic:
← foldl.unop_ofFreeMonoid

Goal state after:
α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = (ConcreteCategory.hom (unop ((Foldl.ofFreeMonoid f) (FreeMonoid.ofList (toList xs))))) x
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:
conv =>

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.FinEnum

Goal state before:
pp: α : Type u
β✝ : α → Type v
β : Type ?u.19
f : β → α
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Surjective f
x✝ : α
⊢ x✝ ∈ List.map f (toList β)

Tactic:
simpa using h _

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
i : Fin (List.take m l).length
⊢ (List.take m l).get i = (take m h l.get ∘ Fin.cast ⋯) i

Tactic:
simp only [List.get_eq_getElem, List.getElem_take, comp_apply, take_apply, val_castLE, val_cast]

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u_1
inst✝³ : FinEnum α✝
β : α✝ → Type u_2
inst✝² : (a : α✝) → FinEnum (β a)
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
⊢ ∀ (x : (hp : p) → α hp), x ∈ map (fun x x_1 ↦ x) (FinEnum.toList (α hp))

Tactic:
by intro x; simpa using ⟨x hp, rfl⟩

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ extract a s = (lookup a s, erase a s)

Tactic:
by
  simp [extract]; constructor <;> rfl

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case snd
α : 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
x✝ : α
a✝ : β x✝
⊢ (↑((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⟩))).2
        x✝ =
      some a✝ ↔
    (↑⟨(s, f), hf⟩).2 x✝ = some a✝

Tactic:
simp +contextual [lookup_eq_some_iff, ← hf]

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

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
⊢ ofList <$> Traversable.traverse f a = ofList <$> Traversable.traverse f b

Tactic:
induction p with
  | nil => rfl
  | @cons x l₁ l₂ _ h =>
    have :
      Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₁ =
        Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₂ := by
      rw [h]
    simpa [functor_norm] using! this
  | swap x y l =>
    have :
      (fun a b (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x =
        (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y := by
      rw [CommApplicative.commutative_map]
      congr 2
      funext a b l
      simpa [flip] using! Perm.swap a b l
    simp [Function.comp_def, this, functor_norm]
  | trans => simp [*]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ s₃✝ : Finmap β
s₁ s₂ s₃ : AList β
⊢ ⟦s₁⟧ ∪ ⟦s₂⟧ ∪ ⟦s₃⟧ = ⟦s₁⟧ ∪ (⟦s₂⟧ ∪ ⟦s₃⟧)

Tactic:
simp only [AList.toFinmap_eq, union_toFinmap, AList.union_assoc]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ∅ ∪ ⟦s₁⟧ = ⟦s₁⟧

Tactic:
← empty_toFinmap

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦∅⟧ ∪ ⟦s₁⟧ = ⟦s₁⟧
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦s₁⟧ ∪ ∅ = ⟦s₁⟧

Tactic:
← empty_toFinmap

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦s₁⟧ ∪ ⟦∅⟧ = ⟦s₁⟧
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
⊢ ((t i).sup (f i) ⊓ s.inf fun i ↦ (t i).sup (f i)) =
    ((insert i s).pi t).sup fun g ↦ (insert i s).attach.inf fun i_1 ↦ f (↑i_1) (g ↑i_1 ⋯)

Tactic:
ih,

Goal state after:
case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
⊢ ((t i).sup (f i) ⊓ (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)) =
    ((insert i s).pi t).sup fun g ↦ (insert i s).attach.inf fun i_1 ↦ f (↑i_1) (g ↑i_1 ⋯)
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
⊢ (f a✝).slice i hid + ∑ x ∈ s✝, (f x).slice i hid = (∑ x ∈ insert a✝ s✝, f x).slice i hid

Tactic:
ih,

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.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℤ
⊢ bit b n = 2 * n + bif b then 1 else 0

Tactic:
cases b

Goal state after:
case false
n : ℤ
⊢ bit false n = 2 * n + bif false then 1 else 0

case true
n : ℤ
⊢ bit true n = 2 * n + bif true then 1 else 0
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (2 * ↑n + bif b then 1 else 0) = ↑(2 * n + b.toNat)

Tactic:
cases b

Goal state after:
case false
n : ℕ
⊢ (2 * ↑n + bif false then 1 else 0) = ↑(2 * n + false.toNat)

case true
n : ℕ
⊢ (2 * ↑n + bif true then 1 else 0) = ↑(2 * n + true.toNat)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + (!b).toNat+1]

Tactic:
cases b

Goal state after:
case false
n : ℕ
⊢ (2 * -[n+1] + bif false then 1 else 0) = -[2 * n + (!false).toNat+1]

case true
n : ℕ
⊢ (2 * -[n+1] + bif true then 1 else 0) = -[2 * n + (!true).toNat+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℤ
⊢ (2 * n + bif b then 1 else 0).bodd = b

Tactic:
cases b

Goal state after:
case false
n : ℤ
⊢ (2 * n + bif false then 1 else 0).bodd = false

case true
n : ℤ
⊢ (2 * n + bif true then 1 else 0).bodd = true
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
cases b

Goal state after:
case false
m n : ℕ
⊢ (!(Nat.bit (!false) n).testBit m.succ) = !n.testBit m

case true
m n : ℕ
⊢ (!(Nat.bit (!true) n).testBit m.succ) = !n.testBit m
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 = 0

pp: case H
b : Bool
n : ℤ
⊢ 2 ≠ 0

Tactic:
cases b

Goal state after:
case false
n : ℤ
⊢ (bif false then 1 else 0) / 2 = 0

case true
n : ℤ
⊢ (bif true then 1 else 0) / 2 = 0

case H
b : Bool
n : ℤ
⊢ 2 ≠ 0
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a ^^^ b = 0 ↔ a = b

Tactic:
xor_eq_iff_left_eq,

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a = 0 ^^^ b ↔ a = b
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ b ^^^ a = a ↔ b = 0

Tactic:
xor_eq_iff_left_eq,

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ b = a ^^^ a ↔ b = 0
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mpr
a b r v : ℕ
x : ℤ
h : (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x

Tactic:
lift x to ℕ using (by omega)

Goal state after:
case mpr
a b r v x : ℕ
h : (↑a ≤ ↑x ∧ ↑x < ↑b) ∧ ↑x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = ↑x
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons.nil
α : Type u_1
f : α → α
l₁ : List α
hd : α
x✝ : [hd] ≠ []
⊢ modifyLast f (l₁ ++ [hd]) = l₁ ++ modifyLast f [hd]

Tactic:
simp only [modifyLast, modifyLast.go, Array.toListAppend_eq, nil_append]
      exact modifyLast_concat _ hd _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
⊢ Set.range (foldr f a) ⊆ Set.range (foldr g a)

Tactic:
rintro _ ⟨l, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
l : List β
⊢ foldr f a l ∈ Set.range (foldr g a)
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c ↦ f c a) ⊆ Set.range fun b c ↦ g c b
a : α
⊢ (Set.range fun l ↦ foldl f a l) ⊆ Set.range fun l ↦ foldl g a l

Tactic:
← (foldr_reverse),

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c ↦ f c a) ⊆ Set.range fun b c ↦ g c b
a : α
⊢ (Set.range fun l ↦ foldr (fun y x ↦ f x y) a l.reverse) ⊆ Set.range fun l ↦ foldr (fun y x ↦ g x y) a l.reverse
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Trichotomous r
⊢ Function.Injective fun a ↦ (a.length, a)

Tactic:
by simp [Function.Injective]

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

Goal state before:
pp: α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ take head l ++ (tail.splitLengths (drop head l)).flatten = l

Tactic:
ih,

Goal state after:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ take head l ++ drop head l = l

case h
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ (drop head l).length ≤ tail.sum
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: case h
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ tail.sum ≤ (drop head l).length

Tactic:
· simp [Nat.le_sub_of_add_le' h]

Goal state after:
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) ([].reverse ++ [a] ++ g.reverse.reverse)

Tactic:
reverse_nil,

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.reverse.reverse)
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case inr
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
⊢ (take n w ++ w).HasPeriod p

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | pos

Goal state after:
case inr.inl
α : Type u_1
p : ℕ
w : List α
per : w.HasPeriod p
p_pos : p > 0
dvd : p ∣ 0
len : 0 ≤ w.length
⊢ (take 0 w ++ w).HasPeriod p

case inr.inr
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
⊢ (take n w ++ w).HasPeriod p
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:
by
  induction m using Quot.ind with | _ l
  unfold chineseRemainderOfMultiset
  simpa using! chineseRemainderOfList_lt_prod a s l
    (List.Nodup.pairwise_of_forall_ne nod pp) (by simpa using! hs)

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)
k k' : ℕ
| X ^ (k + p * k') * (↑((n % p).choose k) * ↑((n / p).choose k'))

Tactic:
← cast_mul

Goal state after:
n k✝ p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
k k' : ℕ
| X ^ (k + p * k') * ↑((n % p).choose k * (n / p).choose k')
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case pos
a n : ℕ
h : n = 0 ∨ a = 0
⊢ 0 = 0

Tactic:
simp [Finsupp.floorDiv_def, prod_mapRange_index pow_zero]

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

Goal state before:
pp: case neg
a n : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ (a.factorization.prod fun p k ↦ p ^ (k / n)) = (a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
simp [Finsupp.floorDiv_def, prod_mapRange_index pow_zero]

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)) * ↑(∏ i ∈ range a.succ, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD
    ↑p]

Tactic:
prod_range_succ,

Goal state after:
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)) *
      ↑((∏ x ∈ range a, (n / p ^ x % p).choose (k / p ^ x % p)) * (n / p ^ a % p).choose (k / p ^ a % p)) [ZMOD
    ↑p]
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
⊢ a ≤ nth p k

Tactic:
by
  rcases (Set.ofPred p).finite_or_infinite with hf | hf
  · rcases exists_lt_card_finite_nth_eq hf ha with ⟨n, hn, rfl⟩
    rcases lt_or_ge (k + 1) #hf.toFinset with hk | hk
    · rwa [(nth_strictMonoOn hf).lt_iff_lt hn hk, Nat.lt_succ_iff,
        ← (nth_strictMonoOn hf).le_iff_le hn (k.lt_succ_self.trans hk)] at h
    · rw [nth_of_card_le _ hk] at h
      exact absurd h (zero_le _).not_gt
  · rcases subset_range_nth ha with ⟨n, rfl⟩
    rwa [nth_lt_nth hf, Nat.lt_succ_iff, ← nth_le_nth hf] at h

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

Goal state before:
pp: n : PosNum
⊢ ↑n + ↑n + ↑n = ↑n * (1 + 1 + 1)

Tactic:
by simp only [mul_add, mul_one]

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

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
h : p (nth p 0)
⊢ f (sInf {i | p (f i)}) = sInf (Set.ofPred p)

Tactic:
← hs h0,

Goal state after:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
h : p (nth p 0)
⊢ f (sInf {i | p (f i)}) = sInf (f '' {i | p (f i)})
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = Num.zero.succ'
| p = Num.zero.succ'

Tactic:
conv =>

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = Num.zero.succ'
| p = 1