mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: case ok
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : α✝
⊢ Except.map (⇑e.symm) (Except.map (⇑e) (ok a✝)) = ok a✝

Tactic:
simp [Except.map]

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: case error
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : ε
⊢ Except.map (⇑e) (Except.map (⇑e.symm) (error a✝)) = error a✝

Tactic:
simp [Except.map]

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: case ok
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : β✝
⊢ Except.map (⇑e) (Except.map (⇑e.symm) (ok a✝)) = ok a✝

Tactic:
simp [Except.map]

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Equiv.traverse eqv (Comp.mk ∘ map x✝² ∘ x✝¹) x✝ = Comp.mk (traverse x✝² <$> traverse x✝¹ x✝)

Tactic:
Equiv.comp_traverse,

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Comp.mk (Equiv.traverse eqv x✝² <$> Equiv.traverse eqv x✝¹ x✝) = Comp.mk (traverse x✝² <$> traverse x✝¹ x✝)
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : f i ∈ t i
hi : i ∈ f.support
H : t i = 0
⊢ f i = 0

Tactic:
H,

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : f i ∈ 0
hi : i ∈ f.support
H : t i = 0
⊢ f i = 0
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ (x✝ <* y✝).out = (Function.const β✝ <$> x✝ <*> y✝).out

Tactic:
simp [Seq.seq, SeqLeft.seqLeft]

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
x : α
⊢ List.idxOf x xs < xs.length

Tactic:
List.idxOf_lt_length_iff

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
x : α
⊢ x ∈ xs
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ'✝ : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝¹ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
this : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
⊢ (lightProfiniteToLightCondSet ⋙ free R).map (π' ≫ y' ▷ ℕ∪{∞}) ≫ f =
    (((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯)).ι.app
          Limits.WalkingParallelPair.one ≫
        hc.desc (cocone R π' ((lightProfiniteToLightCondSet ⋙ free R).map g' ≫ g) r_inf split.section_ hr)) ≫
      p

Tactic:
rw [hc.fac]

Goal state after:
case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ'✝ : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝¹ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
this : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
⊢ (lightProfiniteToLightCondSet ⋙ free R).map (π' ≫ y' ▷ ℕ∪{∞}) ≫ f =
    (cocone R π' ((lightProfiniteToLightCondSet ⋙ free R).map g' ≫ g) r_inf split.section_ hr).ι.app
        Limits.WalkingParallelPair.one ≫
      p
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : Option.map (Sigma.mk a) (dlookup a tail✝) = find? (fun s ↦ decide (a = s.fst)) tail✝
⊢ Option.map (Sigma.mk a) (dlookup a (s :: tail✝)) = find? (fun s ↦ decide (a = s.fst)) (s :: tail✝)

Tactic:
by_cases s.fst = a <;> grind

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

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
⊢ IsEmpty ↑S'.toTop

Tactic:
by simpa using hS'

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
⊢ (⟨a₂, b₂⟩ ∈ if a = a₁ then some ⟨a, b⟩ else none) → a₁ = a₂

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
h : a = a₁
⊢ ⟨a₂, b₂⟩ ∈ some ⟨a, b⟩ → a₁ = a₂

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
h : ¬a = a₁
⊢ ⟨a₂, b₂⟩ ∈ none → a₁ = a₂
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (if h : a' = a then (some (⋯ ▸ b), l) else ((kextract a l).fst, ⟨a', b⟩ :: (kextract a l).snd)) =
    (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a' = a
⊢ (some (⋯ ▸ b), l) = (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a' = a
⊢ ((kextract a l).fst, ⟨a', b⟩ :: (kextract a l).snd) = (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))
Module: Mathlib.Data.Finsupp.AList

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

Tactic:
by simp [h, this]

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

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k✝ : κ
f : ι k✝ →₀ M
k : κ
i : ι k
⊢ f.embSigma ⟨k, i⟩ = if h : ⟨k, i⟩.fst = k✝ then f (h ▸ ⟨k, i⟩.snd) else 0

Tactic:
split_ifs with h

Goal state after:
case pos
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k✝ : κ
f : ι k✝ →₀ M
k : κ
i : ι k
h : ⟨k, i⟩.fst = k✝
⊢ f.embSigma ⟨k, i⟩ = f (h ▸ ⟨k, i⟩.snd)

case neg
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k✝ : κ
f : ι k✝ →₀ M
k : κ
i : ι k
h : ¬⟨k, i⟩.fst = k✝
⊢ f.embSigma ⟨k, i⟩ = 0
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a ^ 2 < b ^ 2

Tactic:
rw [sq, sq]
  exact natAbs_lt_iff_mul_self_lt

Goal state after:
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:
by gcongr; positivity

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n → α
r : α → α → Prop
⊢ IsChain r (ofFn f) ↔ ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)

Tactic:
by
  simp_rw [isChain_iff_getElem, List.getElem_ofFn, length_ofFn]

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑(if v % r < b % r then 1 else 0)

Tactic:
split_ifs with h

Goal state after:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑1

case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑0
Module: Mathlib.Data.List.TakeWhile

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

Tactic:
by
  induction l with
  | nil =>
    simp only [takeWhile_nil, Bool.not_eq_true, true_iff]
    intro h
    simp at h
  | cons x xs IH => by_cases hp : p x <;> simp [hp]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
⊢ (match p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse).reverse =
    if p x = true then (dropWhile p l.reverse).reverse else l ++ [x]

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ (match p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse).reverse =
    (dropWhile p l.reverse).reverse

case neg
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ (match p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse).reverse =
    l ++ [x]
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
⊢ (match p x with
      | true => x :: takeWhile p l.reverse
      | false => []).reverse =
    if p x = true then (takeWhile p l.reverse).reverse ++ [x] else []

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ (match p x with
      | true => x :: takeWhile p l.reverse
      | false => []).reverse =
    (takeWhile p l.reverse).reverse ++ [x]

case neg
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ (match p x with
      | true => x :: takeWhile p l.reverse
      | false => []).reverse =
    []
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
⊢ IsChain (fun a b ↦ b = a.succ) (Ico n m)

Tactic:
by
  by_cases! h : n < m
  · rw [eq_cons h]
    unfold List.Ico
    exact isChain_range' _ (_ + 1) 1
  · rw [eq_nil_of_le h]
    exact .nil

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

Goal state before:
pp: case inl
n m l : ℕ
hml : m ≤ l
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n (min m l)

Tactic:
rw [min_eq_left hml, filter_lt_of_top_le hml]

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

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
i : ℕ
⊢ i < w.length - p → w[i]? = w[i + p]?

Tactic:
less

Goal state after:
case mpr
α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
i : ℕ
less : i < w.length - p
⊢ w[i]? = w[i + p]?
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case inr.inr.gt
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
⊢ w.HasPeriod (p.gcd q)

Tactic:
have q_lt_p : q < p := Nat.compare_eq_gt.mp hyp
      have gcd_lt_p : p.gcd q < p := by
        have : p.gcd q ≠ p := by
          simp [gcd_eq_left_iff_dvd, not_dvd_of_pos_of_lt q_pos q_lt_p]
        exact this.lt_of_le (gcd_le_left q p_pos)
      have per_diff : HasPeriod (drop q w) (p - q) := by
        have : p = (p - q) + q := by lia
        exact per_q.drop_of_hasPeriod_add (this ▸ per_p)
      have per_q' : HasPeriod (drop q w) q := by
        apply @HasPeriod.factor _ (take q w) (drop q w) [] q
        all_goals simp_all
      have gcd_stable : (p - q).gcd q = p.gcd q := gcd_sub_self_left (le_of_lt q_lt_p)
      have drop_len : q ≤ (drop q w).length := by
        rw [length_drop]
        have : p.gcd q ≤ p - q := by
          rw [← gcd_stable]; apply gcd_le_left q; lia
        lia
      have take_eq : take q (drop q w) = take q w := by
          let ⟨z, hz⟩ := per_q.drop_prefix
          convert_to take q (drop q w) = take q (drop q w ++ z)
          · rw [hz]
          exact (take_append_of_le_length drop_len).symm
      -- the induction step
      have IH : HasPeriod (drop q w) ((p - q).gcd q) :=
        per_diff.gcd per_q' (by simp; lia)
      convert_to HasPeriod (take q (drop q w) ++ drop q w) (p.gcd q)
      · rw [take_eq, take_append_drop q w]
      · exact (gcd_stable ▸ IH).take_append (p.gcd q) q (drop q w)
          (gcd_dvd_right p q) drop_len

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
⊢ Function.Injective2 fromRows

Tactic:
intro x1 x2 y1 y2

Goal state after:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
x1 x2 : Matrix m₁ n R
y1 y2 : Matrix m₂ n R
⊢ x1.fromRows y1 = x2.fromRows y2 → x1 = x2 ∧ y1 = y2
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
⊢ Function.Injective2 fromCols

Tactic:
intro x1 x2 y1 y2

Goal state after:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
x1 x2 : Matrix m n₁ R
y1 y2 : Matrix m n₂ R
⊢ x1.fromCols y1 = x2.fromCols y2 → x1 = x2 ∧ y1 = y2
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ M = M - {b} + {b}

Tactic:
rw [tsub_add_cancel_of_le]

Goal state after:
case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ {b} ≤ M
Module: Mathlib.Data.Multiset.DershowitzManna

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

Tactic:
induction Z using Multiset.induction_on generalizing X Y M N with
  | empty => simp at hZ
  | cons z Z ih => ?_

Goal state after:
case cons
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
⊢ TransGen OneStep M N
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
⊢ WellFounded (TransGen OneStep)

Tactic:
exact isDershowitzMannaLT_singleton_wf.transGen

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

Goal state before:
pp: p n k : ℕ
hp : Prime p
hn : n < p
hk : k ≤ n
⊢ p.Coprime (n.descFactorial k)

Tactic:
rw [Nat.descFactorial_eq_div hk]
  refine (hp.coprime_factorial_of_lt hn).coprime_div_right ?_
  simp [Nat.factorial_dvd_factorial]

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

Goal state before:
pp: n k m : ℕ
⊢ n * k - m * k + (m * k - n * k) = (n - m) * k + (m - n) * k

Tactic:
tsub_mul n,

Goal state after:
n k m : ℕ
⊢ n * k - m * k + (m * k - n * k) = n * k - m * k + (m - n) * k
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a n : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k ↦ p ^ (k / n)) =
    if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
split_ifs with h

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

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
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n a : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2).factorization = a.factorization ⌊/⌋ n

Tactic:
split_ifs with h

Goal state after:
case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌊/⌋ n

case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ ((a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2).factorization = a.factorization ⌊/⌋ n
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a n : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k ↦ p ^ ((k + n - 1) / n)) =
    if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
split_ifs with h

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

case neg
a n : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ (a.factorization.prod fun p k ↦ p ^ ((k + n - 1) / n)) = (a.factorization ⌈/⌉ n).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n a : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 ↦ x1 ^ x2).factorization = a.factorization ⌈/⌉ n

Tactic:
split_ifs with h

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

case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ ((a.factorization ⌈/⌉ n).prod fun x1 x2 ↦ x1 ^ x2).factorization = a.factorization ⌈/⌉ n
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
⊢ (if (k % p, k / p) ∈ range (n % p + 1) ×ˢ range (n / p + 1) then
      1 * ↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2)
    else 0) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
split_ifs with h

Goal state after:
case pos
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 : (k % p, k / p) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ 1 * ↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

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 : (k % p, k / p) ∉ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: k a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑((p ^ k * a).choose (p ^ k * b)) ≡ ↑(a.choose b) [ZMOD ↑p]

Tactic:
induction k with
  | zero => simp [Int.ModEq.refl]
  | succ k ih =>
    grw [Nat.pow_succ', mul_assoc, mul_assoc, choose_mul_mul_modEq_choose, ih]

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

Goal state before:
pp: case succ.refine_2
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
m : ℕ
hm : m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ n < m

Tactic:
apply hmono.reflect_lt <;> grind

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

Goal state before:
pp: p : PosNum
⊢ ↑p.bit0 = ZNum.pos p.bit0

Tactic:
have := congr_arg ZNum.bit0 (cast_to_znum p)

Goal state after:
p : PosNum
this : (↑p).bit0 = (ZNum.pos p).bit0
⊢ ↑p.bit0 = ZNum.pos p.bit0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑a.pred'.toZNum = ↑a - ↑1

Tactic:
Num.cast_toZNum,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑a.pred' = ↑a - ↑1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ ↑(r.sub' (Num.pos d)) = ↑r₂.toZNum ↔ ↑r = ↑r₂ + ↑d

Tactic:
Num.cast_toZNum,

Goal state after:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ ↑(r.sub' (Num.pos d)) = ↑r₂ ↔ ↑r = ↑r₂ + ↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.intro
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : CofixA F n) (y : CofixA F n.succ), Agree x y → truncate y = x
a✝ : F.A
f : F.B a✝ → CofixA F n
y : F.B a✝ → CofixA F (n + 1)
h₁ : ∀ (i : F.B a✝), Agree (f i) (y i)
⊢ truncate (CofixA.intro a✝ y) = CofixA.intro a✝ f

Tactic:
| intro f y h₁ =>

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

Goal state before:
pp: this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
⊢ ↑(if a✝ ≤ b✝ then gcdAux (a✝.natSize + b✝.natSize) a✝ b✝ else gcdAux (b✝.natSize + a✝.natSize) b✝ a✝) = (↑a✝).gcd ↑b✝

Tactic:
split_ifs with h

Goal state after:
case pos
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
h : a✝ ≤ b✝
⊢ ↑(gcdAux (a✝.natSize + b✝.natSize) a✝ b✝) = (↑a✝).gcd ↑b✝

case neg
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
h : ¬a✝ ≤ b✝
⊢ ↑(gcdAux (b✝.natSize + a✝.natSize) b✝ a✝) = (↑a✝).gcd ↑b✝