mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step (Cfg.ret k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)

Tactic:
reaches_eval

Goal state after:
case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step ?m.167 = do
    let a ← k.eval v'
    pure (Cfg.halt a)

case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Reaches step (Cfg.ret k v') ?m.167

f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case e'_2
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (update S k₁ L₂) k₂ (L₁ ++ S k₂) =
    update (update (update S rev []) k₁ L₂) k₂
      ((update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ rev).reverseAux
        (update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ k₂))

Tactic:
rw [show update S rev [] = S by rw [← h₂, Function.update_eq_self]]

Goal state after:
case e'_2
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (update S k₁ L₂) k₂ (L₁ ++ S k₂) =
    update (update S k₁ L₂) k₂
      ((update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ rev).reverseAux
        (update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ k₂))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case e'_2
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) =
    update (update (update S rev []) k₁ (val✝ :: L₂)) k₂
      ((update (update S rev L₁.reverse) k₁ (val✝ :: L₂) rev).reverse ++
        update (update S rev L₁.reverse) k₁ (val✝ :: L₂) k₂)

Tactic:
rw [show update S rev [] = S by rw [← h₂, Function.update_eq_self]]

Goal state after:
case e'_2
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) =
    update (update S k₁ (val✝ :: L₂)) k₂
      ((update (update S rev L₁.reverse) k₁ (val✝ :: L₂) rev).reverse ++
        update (update S rev L₁.reverse) k₁ (val✝ :: L₂) k₂)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
⊢ PreirreducibleSpace X

Tactic:
apply (preirreducibleSpace_iff_open_dense X).mpr (fun s hs sn ↦ ?_)

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
⊢ Dense s
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
⊢ PreirreducibleSpace X

Tactic:
by
  apply (preirreducibleSpace_iff_open_dense X).mpr (fun s hs sn ↦ ?_)
  apply dense_iff_closure_eq.mpr
  cases preconnectedSpace_iff_clopen.mp h' (closure s) ⟨isClosed_closure, h.open_closure s hs⟩
  · simp_all
  · assumption

Goal state after:
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: case h
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑(toCompHaus.obj X).toTop
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
f' : ↑(toCompHaus.obj X).toTop → ↑B.toTop
h : Continuous f' ∧ ⇑(TopCat.Hom.hom f.hom) ∘ f' = ⇑(TopCat.Hom.hom φ.hom)
a✝ : ↑(toCompHaus.obj X).toTop
⊢ (ConcreteCategory.hom (ofHom (fun x ↦ True) { toFun := f', continuous_toFun := ⋯ } ≫ f)) a✝ =
    (ConcreteCategory.hom φ) a✝

Tactic:
exact congr_fun h.right _

Goal state after:
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: case h
X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑(toProfinite.obj X).toTop
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
f' : ↑(toProfinite.obj X).toTop → ↑B.toTop
h : Continuous f' ∧ ⇑(TopCat.Hom.hom f.hom) ∘ f' = ⇑(TopCat.Hom.hom φ.hom)
a✝ : ↑(toProfinite.obj X).toTop
⊢ (ConcreteCategory.hom (ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := f', continuous_toFun := ⋯ } ≫ f)) a✝ =
    (ConcreteCategory.hom φ) a✝

Tactic:
exact congr_fun h.right _

Goal state after:
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: case h
X B C : Stonean
φ : X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑X.toTop
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
f' : ↑X.toTop → ↑B.toTop
h : Continuous f' ∧ ⇑(TopCat.Hom.hom f.hom) ∘ f' = ⇑(TopCat.Hom.hom φ.hom)
a✝ : ↑X.toTop
⊢ (ConcreteCategory.hom (ofHom (fun X ↦ ExtremallyDisconnected ↑X) { toFun := f', continuous_toFun := ⋯ } ≫ f)) a✝ =
    (ConcreteCategory.hom φ) a✝

Tactic:
exact congr_fun h.right _

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
this : CompactSpace (Quotient S.toSetoid)
⊢ Finite (Quotient S.toSetoid)

Tactic:
rwa [← isCompact_univ_iff, isCompact_iff_finite, finite_univ_iff] at this

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move
q' : Λ'
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q)

Tactic:
| move _ _ _ q q_ih =>

Goal state after:
case move
q' : Λ'
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p✝ k₁✝ k₂✝ q)
HS₁ : trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q) ⊆ S
⊢ Supports (trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q)) S

Tactic:
| move _ _ _ q q_ih =>

Goal state after:
case move
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p✝ k₁✝ k₂✝ q)
HS₁ : trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q) ⊆ S
⊢ Supports (trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q)) S
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: J : Type v
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
inhabited_h : Inhabited α
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
obtain ⟨j, gg, h⟩ := exists_locallyConstant_finite_aux _ hC f

Goal state after:
J : Type v
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : codeSupp' f.fix k ∪ contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.fix f k)) S

Tactic:
exact supports_union.2 ⟨codeSupp'_supports H, IH (Finset.union_subset_right H)⟩

Goal state after:
Module: Mathlib.Topology.Category.Sequential

Goal state before:
pp: X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : SequentialSpace X✝
X Y : Sequential
f : ↑X.toTop ≃ₜ ↑Y.toTop
⊢ InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ }) ≫
      InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f, continuous_toFun := ⋯ }) =
    𝟙 Y

Tactic:
ext x
    exact f.apply_symm_apply x

Goal state after:
Module: Mathlib.Topology.Category.CompactlyGenerated

Goal state before:
pp: X✝ : Type w
inst✝¹ : TopologicalSpace X✝
inst✝ : UCompactlyGeneratedSpace X✝
X Y : CompactlyGenerated
f : ↑X.toTop ≃ₜ ↑Y.toTop
⊢ ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ } ≫ ofHom { toFun := ⇑f, continuous_toFun := ⋯ } = 𝟙 Y

Tactic:
ext x
    exact f.apply_symm_apply x

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondSet
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite)
    (g : (free R).obj P ⊗ (free R).obj S.toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P ⊗ S.toCondensed) ⟶ B
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ g = g' ≫ e

Tactic:
specialize h e S ((μIso (free R) _ _).hom ≫ g)

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P ⊗ S.toCondensed) ⟶ B
h :
  ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g',
        (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (μIso (free R) P S.toCondensed).hom ≫ g =
          g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ g = g' ≫ e
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondSet
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite)
    (g : (free R).obj S.toCondensed ⊗ (free R).obj P ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S.toCondensed ⊗ P) ⟶ B
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ g = g' ≫ e

Tactic:
specialize h e S ((μIso (free R) _ _).hom ≫ g)

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S.toCondensed ⊗ P) ⟶ B
h :
  ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g',
        (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ (μIso (free R) S.toCondensed P).hom ≫ g =
          g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ g = g' ≫ e
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α : Type u
x : t α
⊢ traverse pure x = pure x

Tactic:
by
  have : traverse pure x = pure (traverse (m := Id) pure x) :=
      (naturality (PureTransformation F) pure x).symm
  rwa [id_traverse] at this

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ ωSup (approxChain f) x

Tactic:
trans approx f i.succ x

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ approx (⇑f) i.succ x

α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ approx (⇑f) i.succ x ≤ ωSup (approxChain f) x
Module: Mathlib.Data.TypeVec

Goal state before:
pp: ⊢ ∀ {n : ℕ} {α β : TypeVec.{u} n}, (id ⊗' id) = id

Tactic:
by
  intros
  ext i a
  induction i with
  | fz => cases a; rfl
  | fs _ i_ih => apply i_ih

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: z : ℤ
w : ℕ
⊢ (↑↑↑z).bmod (2 ^ (w + 1)) = (↑z).toInt

Tactic:
Fin.val_intCast,

Goal state after:
z : ℤ
w : ℕ
⊢ (↑(z % ↑(2 ^ (w + 1))).toNat).bmod (2 ^ (w + 1)) = (↑z).toInt
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
n : ↑ℕ∪{∞}.toTop
⊢ Continuous fun x ↦ ↑x n

Tactic:
by refine (continuous_apply _).comp ?_; fun_prop

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ 2 * count b l = if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1

Tactic:
by
  by_cases h2 : Even (length l)
  · rw [if_pos h2, hl.two_mul_count_bool_of_even h2]
  · rcases l with - | ⟨x, l⟩
    · exact (h2 .zero).elim
    grind [hl.tail.two_mul_count_bool_of_even]

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
a b : α
ab : b = a
c : α
ac : c = a
⊢ b = c

Tactic:
rwa [← ac] at ab

Goal state after:
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 => lhs; unfold recEmptyOption
  split
  · exact absurd (‹_› ▸ h) (card α).lt_irrefl
  · rcases Nat.succ.inj <| (card α).succ_pred_eq_of_pos h |>.trans ‹_› with rfl; rfl

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

Goal state before:
pp: α : Type u_1
f : α → Option α
a : α
l : List α
⊢ lookmap f (a :: l) =
    match f a with
    | none => a :: lookmap f l
    | some b => b :: l

Tactic:
cases h : f a <;> simp_all

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ ⟨a, b⟩ :: kerase a s₁.entries ~ ⟨a, b⟩ :: kerase a s₂.entries

Tactic:
exact p.kinsert s₁.nodupKeys

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

Goal state before:
pp: case swap
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
rcases h₁ : f a with - | c <;> rcases h₂ : f b with - | d
    · simpa [h₁, h₂] using Perm.swap _ _ _
    · simpa [h₁, lookmap_cons_some _ _ h₂] using Perm.swap _ _ _
    · simpa [lookmap_cons_some _ _ h₁, h₂] using Perm.swap _ _ _
    · rcases (pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) _ h₂ _ h₁ with ⟨rfl, rfl⟩
      exact Perm.refl _

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x s₁ = lookup x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∈ s₂
⊢ lookup x s₁ = lookup x s₂

Tactic:
lookup_union_left hs₂

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x s₁ = lookup x s₂
hs₁ : x ∉ s₁
hs₂ : x ∈ s₂
⊢ lookup x s₁ = lookup x s₂
Module: Mathlib.Data.Finset.Functor

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

Tactic:
rw [if_pos rfl, image_empty, sup_empty, bot_eq_empty]

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

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
⊢ (if s = ∅ then ∅ else t) = (image (const α✝ id) s).sup fun f ↦ image f t

Tactic:
ext a
        rw [if_neg hs.ne_empty, mem_sup]
        refine ⟨fun ha => ⟨id, mem_image_const_self.2 hs, by rwa [image_id]⟩, ?_⟩
        rintro ⟨f, hf, ha⟩
        rw [mem_image] at hf ha
        obtain ⟨b, hb, rfl⟩ := ha
        obtain ⟨_, _, rfl⟩ := hf
        exact hb

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

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f : α →₀ N
a✝ : α
⊢ f a✝ ≠ 0 a✝ ↔ f a✝ ≠ 0

Tactic:
coe_zero,

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f : α →₀ N
a✝ : α
⊢ f a✝ ≠ 0 a✝ ↔ f a✝ ≠ 0
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ (x ⊗ y ⊗ z) t = (x ⊗ (y ⊗ z)).assocLeft t

Tactic:
rw [assocLeft]
    unfold mul
    rw [mul_assoc, ← HolorIndex.take_take, ← HolorIndex.drop_take, ← HolorIndex.drop_drop,
      cast_type]
    · rfl
    rw [append_assoc]

Goal state after:
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: n : ℤ
⊢ fib (n + 1) * fib (n - 1) - fib n ^ 2 = (-1) ^ n.natAbs

Tactic:
obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
  · exact fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq n
  · if hn : n = 0 then simp [hn] else
    obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
    simp_rw [show -((i + 1 : ℕ) : ℤ) + 1 = -i by simp, sub_eq_add_neg, ← neg_add, fib_neg,
      natAbs_neg, natAbs_natCast, ← fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq]
    grind

Goal state after:
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: x a : ℤ
⊢ fib (a + x) ^ 2 - fib x * fib (x + 2 * a) =
    (fib x * fib (a + 1) + fib (x - 1) * fib a) ^ 2 -
      fib x * (fib x * (fib (a + 1) ^ 2 + fib a ^ 2) + fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a))

Tactic:
simp only [two_mul, fib_add, fib_one, mul_one, reduceAdd, fib_two, ← add_sub, sub_add_cancel]

Goal state after:
x a : ℤ
⊢ (fib (a - 1) * fib x + fib a * (fib (x - 1) + fib x)) ^ 2 -
      fib x *
        (fib (x - 1) * (fib (a - 1) * fib a + fib a * (fib (a - 1) + fib a)) +
          fib x * (fib (a - 1) * fib (a - 1) + fib a * fib a + (fib (a - 1) * fib a + fib a * (fib (a - 1) + fib a)))) =
    (fib x * (fib (a - 1) + fib a) + fib (x - 1) * fib a) ^ 2 -
      fib x *
        (fib x * ((fib (a - 1) + fib a) ^ 2 + fib a ^ 2) +
          fib (x - 1) * (fib a * (fib (a - 1) + fib a) + fib (a - 1) * fib a))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ Function.swap (Nat.bitwise fun y x ↦ !(x || !y)) m n = Nat.bitwise (fun a b ↦ a && !b) n m

Tactic:
Function.swap

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun y x ↦ !(x || !y)) n m = Nat.bitwise (fun a b ↦ a && !b) n m
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ ↑(Function.swap (Nat.bitwise fun y x ↦ !x && y) m n) = -[m+1].land (ofNat n)

Tactic:
Function.swap

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise (fun y x ↦ !x && y) n m) = -[m+1].land (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ ↑(Function.swap (Nat.bitwise fun y x ↦ !x && !!y) m n) = ↑(Nat.bitwise (fun a b ↦ a && !b) n m)

Tactic:
Function.swap

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun y x ↦ !x && !!y) n m) = ↑(Nat.bitwise (fun a b ↦ a && !b) n m)
Module: Mathlib.Data.List.Intervals

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

Tactic:
· rw [eq_nil_of_le h]
    exact .nil

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

Goal state before:
pp: case intro.intro.inl
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
p : List α
lt : Shortlex r p (xa :: xb)
h1 : p.length < (xa :: xb).length
⊢ Acc (Shortlex r) p

Tactic:
exact ih _ h1

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

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

Tactic:
simpa using Matrix.ext_iff.2 h default j

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

Goal state before:
pp: x✝ : ℚ≥0
num : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : num.natAbs.Coprime den✝
hq : 0 ≤ { num := num, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ (fun x ↦
        match x with
        | ⟨num, ⟨den, prop⟩⟩ => ⟨{ num := ↑num, den := den, den_nz := ⋯, reduced := ⋯ }, ⋯⟩)
      ((fun q ↦ ⟨q.num, ⟨q.den, ⋯⟩⟩) ⟨{ num := num, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }, hq⟩) =
    ⟨{ num := num, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }, hq⟩

Tactic:
lift num to ℕ using Rat.num_nonneg.mpr hq

Goal state after:
x✝ : ℚ≥0
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
num : ℕ
reduced✝ : (↑num).natAbs.Coprime den✝
hq : 0 ≤ { num := ↑num, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ (fun x ↦
        match x with
        | ⟨num, ⟨den, prop⟩⟩ => ⟨{ num := ↑num, den := den, den_nz := ⋯, reduced := ⋯ }, ⋯⟩)
      ((fun q ↦ ⟨q.num, ⟨q.den, ⋯⟩⟩) ⟨{ num := ↑num, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }, hq⟩) =
    ⟨{ num := ↑num, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }, hq⟩
Module: Mathlib.Data.Nat.Choose.Dvd

Goal state before:
pp: p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
⊢ p ∣ (a + b).choose a

Tactic:
have h₁ : p ∣ (a + b)! := hp.dvd_factorial.2 h

Goal state after:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : p ∣ (a + b)!
⊢ p ∣ (a + b).choose a
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inr.inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization ≤ n • b.factorization ↔ a.factorization ⌈/⌉ n ≤ b.factorization

Tactic:
ceilDiv_le_iff_le_smul (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)

Goal state after:
case inr.inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization ≤ n • b.factorization ↔ a.factorization ≤ n • b.factorization
Module: Mathlib.Data.Nat.Factorization.Root

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

Tactic:
rw [← factorization_le_iff_dvd ha (pow_ne_zero _ hb),
    ← factorization_le_iff_dvd (ceilRoot_ne_zero.2 ⟨hn, ha⟩) hb, factorization_pow,
    factorization_ceilRoot, ceilDiv_le_iff_le_smul (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]

Goal state after: