mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ G.Adj u v

Tactic:
obtain ⟨w, hw⟩ := exists_walk_of_edist_ne_top <| by rw [h]; simp

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
w : G.Walk u v
hw : ↑w.length = G.edist u v
⊢ G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G

Tactic:
have : Fintype α := .ofFinite α

Goal state after:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this : Fintype α
⊢ completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (hasse α).Reachable a b

Tactic:
reachable_iff_reflTransGen

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ ReflTransGen (hasse α).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case refine_2.hu
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ u ∈ ↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset)

Tactic:
simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion,
                 Set.mem_ofPred_eq, Walk.start_mem_support, exists_prop, and_true]

Goal state after:
case refine_2.hu
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ ∃ i, i ∈ t
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
⊢ {p | p.length = n + 1} = ⋃ w, ⋃ (h : G.Adj u w), cons h '' {p' | p'.length = n}

Tactic:
ext p

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ {p | p.length = n + 1} ↔ p ∈ ⋃ w, ⋃ (h : G.Adj u w), cons h '' {p' | p'.length = n}
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
u v : V
⊢ ↑(G.finsetWalkLengthLT n u v) = {p | p.length < n}

Tactic:
ext p

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
u v : V
p : G.Walk u v
⊢ p ∈ ↑(G.finsetWalkLengthLT n u v) ↔ p ∈ {p | p.length < n}
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
inst✝¹ : Semigroup M
inst✝ : IsLeftCancelMul M
s : Set M
u v d : M
⊢ (mulCayley s).Adj (d * u) (d * v) ↔ (mulCayley s).Adj u v

Tactic:
by
  simp [mulCayley_adj', mul_assoc]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case cons.inr
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
h' : tail.length > 0
⊢ u' ∉ tail.support

Tactic:
by_contra hh

Goal state after:
case cons.inr
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
h' : tail.length > 0
hh : u' ∈ tail.support
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : extremalNumber (Fintype.card V) H < #G.edgeFinset
⊢ H ⊑ G

Tactic:
contrapose h; push Not
  exact card_edgeFinset_le_extremalNumber h

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = (f b).firstDart ⋯
⊢ a = b

Tactic:
exact (congrArg (·.fst) h)

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
x : V
h : G.Adj x default
h' : (f x).length ≤ 0
⊢ x ∉ nil.support

Tactic:
simpa using h.ne

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ (turanGraph n r).Adj = ⊤.Adj ↔ r = 0 ∨ n ≤ r

Tactic:
funext_iff,

Goal state after:
n r : ℕ
⊢ (∀ (x x_1 : Fin n), (turanGraph n r).Adj x x_1 = ⊤.Adj x x_1) ↔ r = 0 ∨ n ≤ r
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case refine_2.inr
n r : ℕ
h : n ≤ r
a b : Fin n
⊢ ↑a % r = ↑b % r ↔ a = b

Tactic:
Nat.mod_eq_of_lt (a.2.trans_le h),

Goal state after:
case refine_2.inr
n r : ℕ
h : n ≤ r
a b : Fin n
⊢ ↑a = ↑b % r ↔ a = b
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ ∀ {a b : Fin 2},
    (pathGraph n).Adj ({ toFun := fun v ↦ ⟨↑v, ⋯⟩, inj' := ⋯ } a) ({ toFun := fun v ↦ ⟨↑v, ⋯⟩, inj' := ⋯ } b) ↔
      (pathGraph 2).Adj a b

Tactic:
by simp [pathGraph]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), Even w.length

Tactic:
← Nat.not_odd_iff_even

Goal state after:
α : Type u_1
G : SimpleGraph α
⊢ G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ∀ ⦃x : Finset V⦄, ¬(#x = r ∧ G.IsClique ↑x)

Tactic:
not_and,

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ∀ ⦃x : Finset V⦄, #x = r → ¬G.IsClique ↑x
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : IsEmpty α
⊢ G.ediam = ⊤

Tactic:
exfalso

Goal state after:
case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : IsEmpty α
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inr
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h✝ : Nonempty α
⊢ G.diam = 0

Tactic:
· rw [diam, ediam_eq_top_of_not_connected h, ENat.toNat_top]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
⊢ C.supp.Infinite ↔ ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C

Tactic:
by
  classical
    constructor
    · rintro Cinf L h
      obtain ⟨v, ⟨vK, rfl⟩, vL⟩ := Set.Infinite.nonempty (Set.Infinite.sdiff Cinf L.finite_toSet)
      exact ⟨componentComplMk _ vL, rfl⟩
    · rintro h Cfin
      obtain ⟨D, e⟩ := h (K ∪ Cfin.toFinset) Finset.subset_union_left
      obtain ⟨v, vD⟩ := D.nonempty
      let Ddis := D.disjoint_right
      simp_rw [Finset.coe_union, Set.Finite.coe_toFinset, Set.disjoint_union_left,
        Set.disjoint_iff] at Ddis
      exact Ddis.right ⟨(ComponentCompl.hom_eq_iff_le _ _ _).mp e vD, vD⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs✝¹ : t ≤ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
s : Finset (Fin n)
hs✝ : s ∈ powersetCard t ({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
hs : s ⊆ {v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v} ∧ #s = t
hs' : s ∈ powersetCard t p
w : Fin n
hw✝ : w ∈ s
hw : w ∈ id p ∧ (between (↑K.verts) (↑K.verts)ᶜ G).Adj w v
⊢ ?m.327 hs' w hw✝

Tactic:
between_adj

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs✝¹ : t ≤ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
s : Finset (Fin n)
hs✝ : s ∈ powersetCard t ({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
hs : s ⊆ {v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v} ∧ #s = t
hs' : s ∈ powersetCard t p
w : Fin n
hw✝ : w ∈ s
hw : w ∈ id p ∧ G.Adj w v ∧ (w ∈ ↑K.verts ∧ v ∈ (↑K.verts)ᶜ ∨ w ∈ (↑K.verts)ᶜ ∧ v ∈ ↑K.verts)
⊢ ?m.327 hs' w hw✝
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ (G.subgraphOfAdj h).IsMatching

Tactic:
by
  intro _ hv
  rw [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at hv
  cases hv with
  | inl => use w; aesop
  | inr => use v; aesop

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∈ G.edgeSet
⊢ ↑(#{x | e ∈ G.incidenceSet x}) = 2

pp: case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∉ G.edgeSet
⊢ ↑(#{x | e ∈ G.incidenceSet x}) = 0

Tactic:
· revert h
    refine e.ind ?_
    intro v w h
    rw [← Nat.cast_two, ← card_pair (G.ne_of_adj h)]
    simp only [mk'_mem_incidenceSet_iff, G.mem_edgeSet.mp h, true_and]
    congr 2
    ext u
    simp

Goal state after:
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∉ G.edgeSet
⊢ ↑(#{x | e ∈ G.incidenceSet x}) = 0
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ ∑ i, ↑(G.degree i) * x i * x i - x ⬝ᵥ adjMatrix R G *ᵥ x = (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
dotProduct_mulVec_adjMatrix,

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ (∑ i, ↑(G.degree i) * x i * x i - ∑ i, ∑ j, if G.Adj i j then x i * x j else 0) =
    (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ p.toSubgraph.spanningCoe.IsCycles

Tactic:
intro v hv
  apply hpc.ncard_neighborSet_toSubgraph_eq_two
  obtain ⟨_, hw⟩ := hv
  exact p.mem_verts_toSubgraph.mp <| p.toSubgraph.edge_vert hw

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ∑ i, g i • G.lapMatrix_ker_basis_aux i = 0
⊢ ∀ (i : G.ConnectedComponent), g i = 0

Tactic:
Subtype.ext_iff

Goal state after:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ∀ (i : G.ConnectedComponent), g i = 0
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.IsEulerian ↔ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

Tactic:
by
  constructor
  · intro h
    exact ⟨h.isTrail, fun _ => h.mem_edges_iff.mpr⟩
  · rintro ⟨h, hl⟩
    exact h.isEulerian_of_forall_mem hl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r✝ : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun H ↦ H.CliqueFree (r + 3)) H
⊢ G.Colorable (r + 2)

Tactic:
apply Colorable.mono_left hle

Goal state after:
α : Type u_1
G : SimpleGraph α
r✝ : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun H ↦ H.CliqueFree (r + 3)) H
⊢ H.Colorable (r + 2)
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.vertexCoverNum ≤ ENat.card V - 1

Tactic:
nontriviality V

Goal state after:
V : Type u_1
G : SimpleGraph V
a✝ : Nontrivial V
⊢ G.vertexCoverNum ≤ ENat.card V - 1
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
inst✝ : Finite V
u : Set V
h : G ≤ G'
ht : u.ncard < {c | Odd c.supp.ncard}.ncard
this : {c | Odd c.supp.ncard}.ncard ≤ {c | Odd c.supp.ncard}.ncard
⊢ u.ncard < {c | Odd c.supp.ncard}.ncard

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `lia` closed this goal.
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. The original proof was: `lia` -/

Goal state after:
V : Type u_1
G G' : SimpleGraph V
inst✝ : Finite V
u : Set V
h : G ≤ G'
ht : u.ncard < {c | Odd c.supp.ncard}.ncard
this : {c | Odd c.supp.ncard}.ncard ≤ {c | Odd c.supp.ncard}.ncard
⊢ u.ncard < {c | Odd c.supp.ncard}.ncard
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
j : ℕ
⊢ μ.colLen j = (μ.col j).card

Tactic:
simp [col_eq_prod]

Goal state after:
Module: Mathlib.Combinatorics.Young.SemistandardTableau

Goal state before:
pp: μ : YoungDiagram
T T' : SemistandardYoungTableau μ
h : ∀ (i j : ℕ), T i j = T' i j
x✝ : ℕ
⊢ T x✝ = T' x✝

Tactic:
funext
    apply h

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ (ofRowLens μ.rowLens ⋯).cells ↔ (i, j) ∈ μ.cells

Tactic:
simp only [mem_cells, mem_ofRowLens, length_rowLens, get_rowLens]

Goal state after:
μ : YoungDiagram
i j : ℕ
⊢ (∃ (_ : i < μ.colLen 0), j < μ.rowLen i) ↔ (i, j) ∈ μ
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Nat.unpaired
      (fun z n ↦
        Nat.casesOn n 0 fun y ↦
          Nat.unpaired
            (fun z n ↦
              Nat.rec (encode (Option.map f (decode z)))
                (fun y IH ↦
                  encode
                    (Option.map (fun p ↦ g p.1 p.2)
                      (decode
                        (Nat.pair (Nat.unpair (Nat.pair z (Nat.pair y IH))).1
                          (Nat.pair (Nat.unpair (Nat.unpair (Nat.pair z (Nat.pair y IH))).2).1
                            (Nat.unpair (Nat.unpair (Nat.pair z (Nat.pair y IH))).2).2.pred)))))
                n)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2 (Nat.unpair (Nat.unpair (Nat.pair z y)).1).2))
      (Nat.pair (id n) (encode (decode (Nat.unpair n).1))) =
    Nat.unpaired
      (fun m n ↦
        encode ((decode m).bind fun a ↦ Option.map (fun n ↦ Nat.rec (f a) (fun n IH ↦ g a (n, IH)) n) (decode n)))
      n

Tactic:
simp only [Nat.unpaired, id_eq, Nat.unpair_pair, decode_prod_val, decode_nat,
        Option.bind_some, Option.map_map, Option.map_some]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Nat.rec 0
      (fun n_1 n_ih ↦
        Nat.rec (encode (Option.map f (decode n_1)))
          (fun y IH ↦
            encode
              (Option.map (fun p ↦ g p.1 p.2)
                ((decode n_1).bind fun a ↦ Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode (decode (Nat.unpair n).1)) =
    encode ((decode (Nat.unpair n).1).bind fun a ↦ some (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) (Nat.unpair n).2))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case hi.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n✝ n : ℕ
IH :
  ∀ m ≤ n,
    encode
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) m)) =
      encode (decode m)
a : α
⊢ encode
      ((some a).bind fun a ↦
        Option.map (List.cons (encode a))
          (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode (Option.map (fun x1 x2 ↦ x1 :: x2) (some a) <*> decode (Nat.unpair n).2)

Tactic:
simp only [Option.bind_some, Option.map_some]

Goal state after:
case hi.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n✝ n : ℕ
IH :
  ∀ m ≤ n,
    encode
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) m)) =
      encode (decode m)
a : α
⊢ encode
      (Option.map (List.cons (encode a))
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode ((some fun x2 ↦ a :: x2) <*> decode (Nat.unpair n).2)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode
      (bif n.bodd then Option.map (fun b ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun b ↦ 2 * encode b) (decode n.div2)) =
    encode
      (match n.bodd, n.div2 with
      | false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m))

Tactic:
cases Nat.bodd n <;> simp

Goal state after:
case false
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b ↦ 2 * encode b) (decode n.div2)) = encode (Option.map Sum.inl (decode n.div2))

case true
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b ↦ 2 * encode b + 1) (decode n.div2)) = encode (Option.map Sum.inr (decode n.div2))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
⊢ a ∈ rfindOpt f

Tactic:
have := (H (le_max_left _ _) h).symm.trans (H (le_max_right _ _) hk)

Goal state after:
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
this : Option.some a = Option.some ((rfindOpt f).get h')
⊢ a ∈ rfindOpt f
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' fun v ↦ (unpair (f v)).1

Tactic:
have s := sqrt.comp₁ _ hf
  have fss := sub.comp₂ _ hf (mul.comp₂ _ s s)
  refine (if_lt fss s fss s).of_eq fun v => ?_
  simp [Nat.unpair]; split_ifs <;> rfl

Goal state after:
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:

Tactic:
(fun x => deriv (fun z => z ^ p * (1 - ε z)) x) =Θ[atTop] fun z => p * z ^ (p - 1) :=
        (isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn hp).isTheta
    _ =Θ[atTop] fun z => z ^ (p - 1) := IsTheta.const_mul_left hp <| isTheta_refl _ _

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: h₁ : ε =o[atTop] fun x ↦ 1
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε ↑n

Tactic:
isLittleO_iff

Goal state after:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε ↑n