mathlib-initiative/mathlib-tactics huggingface dataset:
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:
← hh

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 ≫
      (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫
        (free R).map (μIso lightProfiniteToLightCondSet S P).hom ≫ g
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:
← hh

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 ≫
      (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫
        (free R).map (μIso lightProfiniteToLightCondSet S P).inv ≫ g
Module: Mathlib.Control.Fix

Goal state before:
pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x✝).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ (assert (¬p ↑z) fun h ↦ hwf✝.fix (fixAux f) (z.succ h) x) = Fix.approx f 0 x

Tactic:
assert_neg

Goal state after:
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x✝).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ none = Fix.approx f 0 x

case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x✝).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ ¬¬p ↑z
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : α → β → β
x✝¹ x✝ : FreeMonoid α
⊢ ↾flip (List.foldr f) (FreeMonoid.toList (x✝¹ * x✝)) =
    ↾flip (List.foldr f) (FreeMonoid.toList x✝¹) * ↾flip (List.foldr f) (FreeMonoid.toList x✝)

Tactic:
apply ConcreteCategory.ext
    ext
    apply List.foldr_append

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
x✝ y✝ : FreeMonoid α
⊢ unop (op (flip (List.foldlM f) (FreeMonoid.toList (x✝ * y✝)))) =
    unop (op (flip (List.foldlM f) (FreeMonoid.toList x✝)) * op (flip (List.foldlM f) (FreeMonoid.toList y✝)))

Tactic:
funext

Goal state after:
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
x✝¹ y✝ : FreeMonoid α
x✝ : KleisliCat.mk m β
⊢ unop (op (flip (List.foldlM f) (FreeMonoid.toList (x✝¹ * y✝)))) x✝ =
    unop (op (flip (List.foldlM f) (FreeMonoid.toList x✝¹)) * op (flip (List.foldlM f) (FreeMonoid.toList y✝))) x✝
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
x✝ y✝ : FreeMonoid α
⊢ flip (List.foldrM f) (FreeMonoid.toList (x✝ * y✝)) =
    flip (List.foldrM f) (FreeMonoid.toList x✝) * flip (List.foldrM f) (FreeMonoid.toList y✝)

Tactic:
funext

Goal state after:
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
x✝¹ y✝ : FreeMonoid α
x✝ : KleisliCat.mk m β
⊢ flip (List.foldrM f) (FreeMonoid.toList (x✝¹ * y✝)) x✝ =
    (flip (List.foldrM f) (FreeMonoid.toList x✝¹) * flip (List.foldrM f) (FreeMonoid.toList y✝)) x✝
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_2
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)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = ↑n
i : X
s : S
h : σ (Option.some i) s = x
⊢ σ (Option.some n) s = x

Tactic:
← h,

Goal state after:
case refine_2
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)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : (π (σ (Option.some i) s)).2 = ↑n
h : σ (Option.some i) s = x
⊢ σ (Option.some n) s = x
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_2
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)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : Option.some i = ↑n
h : σ (Option.some i) s = x
⊢ σ (Option.some n) s = x

Tactic:
← h,

Goal state after:
case refine_2
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)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : Option.some i = ↑n
h : σ (Option.some i) s = x
⊢ σ (Option.some n) s = σ (Option.some i) s
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
x✝ : Set α
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => { σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.f s ∪ { σ := σ✝, F := F✝, eq := ⋯ }.F.f t,
            pt := ({ σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.pt, { σ := σ✝, F := F✝, eq := ⋯ }.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => ({ σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.inf a b, { σ := σ✝, F := F✝, eq := ⋯ }.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (F✝¹.toFilter ⊔ F✝.toFilter).sets

Tactic:
simp [CFilter.toFilter]

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (∃ a ∈ s.pi t, { toFun := fun f ↦ DFinsupp.mk s fun i ↦ f ↑i ⋯, inj' := ⋯ } a = f) →
    f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i

Tactic:
rintro ⟨f, hf, rfl⟩

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
⊢ ({ toFun := fun f ↦ DFinsupp.mk s fun i ↦ f ↑i ⋯, inj' := ⋯ } f).support ⊆ s ∧
    ∀ i ∈ s, ({ toFun := fun f ↦ DFinsupp.mk s fun i ↦ f ↑i ⋯, inj' := ⋯ } f) i ∈ t i
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬a ∈ range ⇑x
⊢ (snoc x ha) (last n) = a

Tactic:
rw [coe_snoc, Fin.snoc_last]

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

Tactic:
simp only [ne_eq, h, not_false_iff, lookupAll_cons_ne]

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ map (Sigma.mk a) (lookupAll a l) <+ ⟨a', b'⟩ :: l
Module: Mathlib.Data.Multiset.Functor

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

Tactic:
funext

Goal state after:
α β : Type u_1
h : α → β
x✝ : List α
⊢ (Functor.map h ∘ ofList) x✝ = (ofList ∘ Functor.map h) x✝
Module: Mathlib.Data.List.Sigma

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

Tactic:
rw [lookupAll_eq_dlookup a h]; apply Option.toList_nodup

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : l.Nodup
hs : (↑l.toFinset).PairwiseDisjoint Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) l.toFinset.val

Tactic:
List.toFinset_val,

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : l.Nodup
hs : (↑l.toFinset).PairwiseDisjoint Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) ↑l.dedup
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ f.neLocus (f - g) = g.support

Tactic:
neLocus_self_sub_right

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ g.support = g.support
Module: Mathlib.Data.Int.AbsoluteValue

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : CommRing S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
x : ℤˣ
⊢ abv ↑↑x = 1

Tactic:
by rcases Int.units_eq_one_or x with (rfl | rfl) <;> simp

Goal state after:
Module: Mathlib.Data.Int.AbsoluteValue

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
x : ℤˣ
y : R
⊢ abv (x • y) = abv y

Tactic:
by rcases Int.units_eq_one_or x with (rfl | rfl) <;> simp

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: ds₁ ds₂ is : List ℕ
eq : ds₁ = ds₂
h : Forall₂ (fun x1 x2 ↦ x1 < x2) is ds₁
⊢ ↑(cast ⋯ ⟨is, h⟩) = is

Tactic:
by subst eq; rfl

Goal state after:
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 ⋯ = x

Tactic:
by
  apply slice_eq _ _ _
  ext i hid
  rw [← slice_sum]
  simp only [slice_unitVec_mul hid]
  rw [Finset.sum_eq_single (Subtype.mk i <| Finset.mem_range.2 hid)]
  · simp
  · intro (b : { x // x ∈ Finset.range d }) (_ : b ∈ (Finset.range d).attach) (hbi : b ≠ ⟨i, _⟩)
    have hbi' : i ≠ b := by simpa only [Ne, Subtype.ext_iff, Subtype.coe_mk] using hbi.symm
    simp [hbi']
  · intro (hid' : Subtype.mk i _ ∉ Finset.attach (Finset.range d))
    exfalso
    exact absurd (Finset.mem_attach _ _) hid'

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (m + 1 + n) (x₁ + x₂ + y)

Tactic:
suffices CPRankMax (m + n + 1) (x₁ + (x₂ + y)) by
      simpa only [add_comm, add_assoc, add_left_comm] using this
    apply CPRankMax.succ
    · assumption
    · exact cprankMax_add hx₂ hy

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ count (fun x ↦ x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0

Tactic:
rw [← ofNat_inj, count_modEq_card_eq_ceil _ hr, cast_add]

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r⌉ = ↑(b / r) + ↑(if v % r < b % r then 1 else 0)
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m k : ℕ
h₁ : k ≤ n
⊢ map (fun x ↦ x - k) (range' n (m - n)) = range' (n - k) (m - n)

Tactic:
map_sub_range' h₁

Goal state after:
n m k : ℕ
h₁ : k ≤ n
⊢ range' (n - k) (m - n) = range' (n - k) (m - n)
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ decide (k < l) = true

Tactic:
by
    simp only [(lt_of_lt_of_le (mem.1 hk).2 hml), decide_true]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
z : α
M N X Y : Multiset α
hM : M = X + Y
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    0 ≠ ∅ → M = X + Y → N = X + 0 → (∀ (y : α), y ∈ Y → ∃ z, z ∈ 0 ∧ y < z) → TransGen OneStep M N
hZ : z ::ₘ 0 ≠ ∅
hN : N = X + z ::ₘ 0
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ 0 ∧ y < z_1
⊢ ∀ (y : α), y ∈ Y → y < z

Tactic:
by simpa using hYZ

Goal state after:
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 _ _ _

Goal state after:
ι : 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
nod''✝ : (↑l).Nodup
hs''✝ : ∀ i ∈ ↑l, s i ≠ 0
co''✝ : {x | x ∈ ↑l}.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 ⋯) ⋯ nod''✝ hs''✝ co''✝) =
    ↑(chineseRemainderOfList a s l lco)
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case refine_2
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∣ n

Tactic:
← h,

Goal state after:
case refine_2
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∣ n

Tactic:
← h,

Goal state after:
n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n a : ℕ
⊢ (n.floorRoot a).factorization = a.factorization ⌊/⌋ n

Tactic:
by
  rw [floorRoot_def]
  split_ifs with h
  · obtain rfl | rfl := h <;> simp
  apply a.factorization_prod_pow_eq_self_of_le_factorization
  exact le_self_nsmul (by simp) (by lia) |>.trans <| smul_floorDiv_le (by lia)

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

Goal state before:
pp: case inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inr.inr.inl
b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ 0 ^ n ∣ b ↔ 0 ∣ n.floorRoot b

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

Goal state before:
pp: a b n : ℕ
hn : n ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
b n : ℕ
hn : n ≠ 0
⊢ 0 ∣ b ^ n ↔ n.ceilRoot 0 ∣ b

case inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case neg
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 ∨ ¬(k % p, k / p).2 < n / p + 1
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
not_lt

Goal state after:
case neg
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 ∨ n / p + 1 ≤ (k % p, k / p).2
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

Tactic:
rcases id l with _ | ⟨ls, ll, lx, lr⟩
    · exact ι x
    · rcases id ll with _ | lls
      · rcases lr with _ | ⟨_, _, lrx⟩
        · exact node 2 l x nil
        · exact node 3 (ι lx) lrx ι x
      · rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)

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

Goal state before:
pp: case mp
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ Liftr r x y → ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)

pp: case mpr
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ (∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)) → Liftr r x y

Tactic:
· rintro ⟨u, xeq, yeq⟩
    rcases h : u with ⟨a, f⟩
    use a, fun i => (f i).val.fst, fun i => (f i).val.snd
    constructor
    · rw [← xeq, h]
      rfl
    constructor
    · rw [← yeq, h]
      rfl
    intro i
    exact (f i).property

Goal state after:
case mpr
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ (∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)) → Liftr r x y
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑↑m = ↑↑n ↔ m = n

Tactic:
Int.cast_inj (α := α),

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑m = ↑n ↔ m = n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : ZNum), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
by
    intro a b
    transfer_rw
    apply lt_iff_le_not_ge

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

Goal state before:
pp: case succ.step.step.f.f.refl.refl.refl.refl.refl.hrec
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
i : F.B a
ps : Path F
hrec : iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f₂⟩) = iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f₁⟩)
h : n = length ps
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)

Tactic:
simp only [iselect_cons] at hrec

Goal state after:
case succ.step.step.f.f.refl.refl.refl.refl.refl.hrec
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
i : F.B a
ps : Path F
h : n = length ps
hrec : iselect ps (f₂ i) = iselect ps (f₁ i)
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)
Module: Mathlib.Data.Ordmap.Ordset

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

Tactic:
rcases Nat.eq_zero_or_pos (size rl) with rl0 | rl0
    · rw [rl0, not_lt, Nat.le_zero, Nat.mul_eq_zero] at h
      replace h := h.resolve_left (by decide)
      rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2
      rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1
      cases H1 (by decide)
    refine hl.node4L hr.left hr.right rl0 ?_
    rcases Nat.eq_zero_or_pos (size l) with l0 | l0
    · replace H3 := H3_0 l0
      rcases Nat.eq_zero_or_pos (size rr) with rr0 | rr0
      · have := hr.3.1
        rw [rr0] at this
        exact Or.inl ⟨l0, le_antisymm (balancedSz_zero.1 this) rl0, rr0.symm ▸ zero_le_one⟩
      exact Or.inl ⟨l0, le_antisymm (ablem rr0 <| by rwa [add_comm]) rl0, ablem rl0 H3⟩
    exact
      Or.inr ⟨l0, not_lt.1 h, H2, Valid'.rotateL_lemma₄ (H3p l0), (hr.3.1.resolve_left (hlp l0)).1⟩

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

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (l.node4R x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Tactic:
by
  cases m <;> simp [node4R, all_node', All, all_node3R, and_assoc]

Goal state after: