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

Goal state before:
pp: α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ (monotoneCurry α β γ) (fun a ↦ ωSup (c.map (evalOrderHom a))) x y =
    ωSup (((c.map (monotoneCurry α β γ)).map (evalOrderHom x)).map (evalOrderHom y))

Tactic:
map_comp,

Goal state after:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ (monotoneCurry α β γ) (fun a ↦ ωSup (c.map (evalOrderHom a))) x y =
    ωSup ((c.map (monotoneCurry α β γ)).map ((evalOrderHom y).comp (evalOrderHom x)))
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup ((c.map (evalOrderHom x)).map (evalOrderHom y)) =
    ωSup ((c.map (monotoneUncurry α β γ)).map (evalOrderHom ⟨x, y⟩))

Tactic:
map_comp,

Goal state after:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup (c.map ((evalOrderHom y).comp (evalOrderHom x))) =
    ωSup ((c.map (monotoneUncurry α β γ)).map (evalOrderHom ⟨x, y⟩))
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
⊢ subtypeVal p ⊚ toSubtype p = fun x ↦ Subtype.val

Tactic:
ext i x
  induction i <;> simp only [toSubtype, comp, subtypeVal] at *
  simp [*]

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s

Tactic:
have := @mem_nhds_toTopsp _ _ F.F s a; rwa [F.eq] at this

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
refine heq_of_cast_eq ?_ (Subsingleton.allEq _ _)
      exact congrArg (α ≃ Fin ·) <| card_eq_one α

Goal state after:
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Nat.card (Perm α) = (Nat.card α)!

Tactic:
by
  classical
  have := Fintype.ofFinite α
  rw [card_eq_fintype_card, card_eq_fintype_card, Fintype.card_perm]

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
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 π') ⋯))
⊢ (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π') ≫ snd S' ℕ∪{∞} =
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞} ≫ lift (𝟙 S') (CompHausLike.const S' ∞)) ≫
      snd S' ℕ∪{∞}

Tactic:
by ext a; exact a.prop

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case refine_2
α : Type u
β : α → Type v
γ : Type ?u.32
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
this : s.entries.NodupKeys
⊢ (Quotient.liftOn s.entries (fun l ↦ { Dom := l.NodupKeys, get := fun nd ↦ f { entries := l, nodupKeys := nd } })
      ⋯).Dom

Tactic:
revert this

Goal state after:
case refine_2
α : Type u
β : α → Type v
γ : Type ?u.32
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ s.entries.NodupKeys →
    (Quotient.liftOn s.entries (fun l ↦ { Dom := l.NodupKeys, get := fun nd ↦ f { entries := l, nodupKeys := nd } })
        ⋯).Dom
Module: Mathlib.Data.List.AList

Goal state before:
pp: case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ s₁.entries.keys
⊢ False

Tactic:
apply h _ h''

Goal state after:
case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ s₁.entries.keys
⊢ x✝ ∈ s₂.keys
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'
⊢ (lookupAll a l).head? = dlookup a (⟨a', b⟩ :: l)

pp: case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst

Tactic:
dlookup_cons_ne,

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ (lookupAll a l).head? = dlookup a l

case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst

case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
ht : ¬t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
exact let ⟨p, hp⟩ := exists_gt (s.max' hs); ⟨p, by simp_all⟩

Goal state after:
Module: Mathlib.Data.Finmap

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

Tactic:
by
  simp [(· ∪ ·), union]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup x s = some b
⊢ lookup x (singleton x b) = lookup x s

Tactic:
lookup_singleton_eq,

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup x s = some b
⊢ some b = lookup x s
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : tl.sum.support ⊆ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
⊢ (hd + tl.sum).support ⊆ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ (hd :: tl)

Tactic:
exact Finsupp.support_add.trans (Finset.union_subset_union Finset.Subset.rfl IH)

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

Goal state before:
pp: case ofNat
a✝ : ℕ
⊢ (-ofNat a✝).bodd = (ofNat a✝).bodd

Tactic:
simp only [← negOfNat_eq, bodd_negOfNat, neg_negSucc]

Goal state after:
case ofNat
a✝ : ℕ
⊢ a✝.bodd = (ofNat a✝).bodd
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc
a✝ : ℕ
⊢ (- -[a✝+1]).bodd = -[a✝+1].bodd

Tactic:
simp only [← negOfNat_eq, bodd_negOfNat, neg_negSucc]

Goal state after:
case negSucc
a✝ : ℕ
⊢ (↑(a✝ + 1)).bodd = -[a✝+1].bodd
Module: Mathlib.Data.LawfulXor.Basic

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

Tactic:
by
   rw [xor_eq_iff_right_eq, xor_self a]

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

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).xor (bit b n) = bit (a ^^ b) (m.xor n)

Tactic:
by
  rw [← bitwise_xor, bitwise_bit]

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

Goal state before:
pp: case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝¹ + 1 = n✝ + 1

Tactic:
Nat.succ_inj

Goal state after:
case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝¹ = n✝
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inr.nil
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
⊢ Shortlex r s₁ (s₂ ++ [])

Tactic:
rw [List.append_nil]
    exact h

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

Goal state before:
pp: α : 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
⊢ head ≤ l.length ∧ map length (tail.splitLengths (drop head l)) = tail

Tactic:
rw [ih]

Goal state after:
α : 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
⊢ head ≤ l.length ∧ tail = tail

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

Goal state before:
pp: case pos
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : p = 0
⊢ w[i % p]? = w[i]?

pp: case neg
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
⊢ w[i % p]? = w[i]?

Tactic:
· rw [p_zero, mod_zero]

Goal state after:
case neg
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
⊢ w[i % p]? = w[i]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r [] a g gs)

Tactic:
rw [splitBy.loop, reverse_cons]
    apply List.isChain_reverse.1
    simpa using isChain_cons.2 ⟨hga, hgs⟩

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

Goal state before:
pp: case neg
α : 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
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : ¬j < n
j_minus : j - n < w.length
n_le_j : n ≤ j
⊢ (take n w ++ w)[j]? = w[j % p]?

Tactic:
clear j_lt_n

Goal state after:
case neg
α : 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
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
⊢ (take n w ++ w)[j]? = w[j % p]?
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
⊢ A₁.fromRows A₂ * B = (A₁ * B).fromRows (A₂ * B)

Tactic:
ext (_ | _) _

Goal state after:
case inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
val✝ : m₁
j✝ : m
⊢ (A₁.fromRows A₂ * B) (Sum.inl val✝) j✝ = (A₁ * B).fromRows (A₂ * B) (Sum.inl val✝) j✝

case inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
val✝ : m₂
j✝ : m
⊢ (A₁.fromRows A₂ * B) (Sum.inr val✝) j✝ = (A₁ * B).fromRows (A₂ * B) (Sum.inr val✝) j✝
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
inst✝ : Semiring R
⊢ fromRows 0 0 = 0

Tactic:
ext (_ | _) _

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Semiring R
val✝ : m₁
j✝ : n
⊢ fromRows 0 0 (Sum.inl val✝) j✝ = 0 (Sum.inl val✝) j✝

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Semiring R
val✝ : m₂
j✝ : n
⊢ fromRows 0 0 (Sum.inr val✝) j✝ = 0 (Sum.inr val✝) j✝
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
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)

Tactic:
ext (_ | _) _

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝ : m₁
j✝ : n
⊢ (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inl val✝) j✝ =
    (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inl val✝) j✝

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝ : m₂
j✝ : n
⊢ (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inr val✝) j✝ =
    (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inr val✝) j✝
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
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
⊢ (A₁.fromCols A₂)ᴴ = A₁ᴴ.fromRows A₂ᴴ

Tactic:
ext (_ | _) _

Goal state after:
case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
val✝ : n₁
j✝ : m
⊢ (A₁.fromCols A₂)ᴴ (Sum.inl val✝) j✝ = A₁ᴴ.fromRows A₂ᴴ (Sum.inl val✝) j✝

case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
val✝ : n₂
j✝ : m
⊢ (A₁.fromCols A₂)ᴴ (Sum.inr val✝) j✝ = A₁ᴴ.fromRows A₂ᴴ (Sum.inr val✝) j✝
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
h0 : a ::ₘ M = X + {a}
h2 : ∀ (y : α), y ∈ Y → y < a
⊢ ∃ M', X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a

pp: case inr
α : 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', X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a

Tactic:
· refine ⟨Y, .inr ⟨?_, h2⟩⟩
    simpa [add_comm _ {a}, singleton_add, eq_comm] using h0

Goal state after:
case inr
α : 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', X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case intro.intro.inr.cons
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
b : α
N : Multiset α
ihN : (∀ (x : α), x ∈ N → x < a) → Acc OneStep (M + N)
hba : b < a
hN : ∀ (a_1 : α), a_1 ∈ N → a_1 < a
⊢ Acc OneStep (b ::ₘ (M + N))

Tactic:
exact ha _ hba <| ihN hN

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

Goal state before:
pp: q₁ q₂ : ℚ≥0
⊢ ↑q₁.num * ↑q₂.num = ↑(q₁ * q₂).num * ↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den))

Tactic:
convert! Rat.num_mul_num_eq_num_mul_gcd q₁ q₂

Goal state after:
case e'_2.e'_5
q₁ q₂ : ℚ≥0
⊢ ↑q₁.num = (↑q₁).num

case e'_2.e'_6
q₁ q₂ : ℚ≥0
⊢ ↑q₂.num = (↑q₂).num

case e'_3.e'_5
q₁ q₂ : ℚ≥0
⊢ ↑(q₁ * q₂).num = (↑q₁ * ↑q₂).num

case e'_3.e'_6.e'_3.e'_1
q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = ((↑q₁).num * (↑q₂).num).natAbs
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case succ
A : Type u_1
inst✝² : Ring A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP A p
hp : Nat.Prime p
n : ℕ
ih : IsUnit ↑n ! ↔ n < p
⊢ ¬p ∣ n + 1 ∧ n + 1 ≤ p ↔ n + 1 < p

Tactic:
exact ⟨fun ⟨h1, h2⟩ ↦ lt_of_le_of_ne h2 (mt (· ▸ dvd_rfl) h1),
      fun h ↦ ⟨not_dvd_of_pos_of_lt (Nat.succ_pos _) h, h.le⟩⟩

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.divisors = Finset.image (fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) (Finset.Iic n.factorization)

Tactic:
exact divisors_eq_image_Iic_factorization_prod_pow hn

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

Goal state before:
pp: n a : ℕ
l : List ℕ
hl : (a :: l).IsZeckendorfRep
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
⊢ (map fib (a :: l)).sum < fib n

Tactic:
simp only [IsZeckendorfRep, cons_append, isChain_iff_pairwise, pairwise_cons] at hl

Goal state after:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
hl : (∀ a' ∈ l ++ [0], a' + 2 ≤ a) ∧ Pairwise (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum < fib n
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (n - fib n.greatestFib).greatestFib ≤ n.greatestFib - 2

Tactic:
rw [← Nat.lt_succ_iff, greatestFib_lt, tsub_lt_iff_right n.fib_greatestFib_le, Nat.sub_succ,
    succ_pred, ← fib_add_one]
  · exact n.lt_fib_greatestFib_add_one
  · simpa
  · simpa [← succ_le_iff, tsub_eq_zero_iff_le] using hn.bot_lt

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

Goal state before:
pp: case refine_2
p : ℕ → Prop
n : ℕ
⊢ (p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ n) → nth p n = 0

Tactic:
rintro (⟨h₀, rfl⟩ | ⟨hf, hle⟩)

Goal state after:
case refine_2.inl
p : ℕ → Prop
h₀ : p 0
⊢ nth p 0 = 0

case refine_2.inr
p : ℕ → Prop
n : ℕ
hf : (Set.ofPred p).Finite
hle : #hf.toFinset ≤ n
⊢ nth p n = 0
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
⊢ p (nth p a)

Tactic:
by_cases h' : ∀ hf : (Set.ofPred p).Finite, a < #hf.toFinset

Goal state after:
case pos
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∀ (hf : (Set.ofPred p).Finite), a < #hf.toFinset
⊢ p (nth p a)

case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ¬∀ (hf : (Set.ofPred p).Finite), a < #hf.toFinset
⊢ p (nth p a)
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case neg
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ ↑(n.minFacAux fuel k.succ) = (↑n).minFacAux (↑k.bit1 + 2)

Tactic:
rw [ih]

Goal state after:
case neg
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ (↑n).minFacAux ↑k.succ.bit1 = (↑n).minFacAux (↑k.bit1 + 2)

case neg
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ (↑n).sqrt < fuel + ↑k.succ.bit1
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit1
n : PosNum
⊢ (↑n.bit1).sqrt < ↑n + ↑(bit1 1)

Tactic:
simp only [cast_one, cast_bit1]

Goal state after:
case bit1
n : PosNum
⊢ (↑n + ↑n + 1).sqrt < ↑n + (1 + 1 + 1)
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case refine_2
n : PosNum
⊢ n.bit0 = n.bit0.minFac ↔ n = 1

Tactic:
exact ⟨bit0.inj, congr_arg _⟩

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

Goal state after:
case succ.refine_2.ha
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 ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

case succ.refine_2.hb
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
⊢ m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

case succ.refine_2.h
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
⊢ f n < f m
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
hp : (Set.ofPred p).Infinite
n : ℕ
⊢ count p (nth p n + 1) = n + 1

Tactic:
by
  rw [count_succ, count_nth_of_infinite hp, if_pos (nth_mem_of_infinite hp _)]

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

Goal state before:
pp: a b : PosNum
this : Ordering.casesOn (b.cmp a) (↑b < ↑a) (b = a) (↑a < ↑b)
⊢ Ordering.casesOn ((neg a).cmp (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))

Tactic:
revert this

Goal state after:
a b : PosNum
⊢ Ordering.casesOn (b.cmp a) (↑b < ↑a) (b = a) (↑a < ↑b) →
    Ordering.casesOn ((neg a).cmp (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case h₂
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑b % ↑(pos a) ≤ ↑(pos a) * (↑b / ↑(pos a))

Tactic:
grw [Nat.mod_lt, ← le_to_nat.2 ab]

Goal state after:
case h₂
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) ≤ ↑(pos a) * (↑(pos a) / ↑(pos a))

case hy
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ 0 < ↑(pos a)