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

Goal state before:
pp: V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
⊢ Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) T ↔ T.IsTree

Tactic:
have := hG.nonempty

Goal state after:
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
this : Nonempty V
⊢ Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) T ↔ T.IsTree
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
this : (α : Type u_1) → [Finite α] → Fintype α
T : SimpleGraph V
hle : T ≤ G
hT : T.IsTree
⊢ T.edgeFinset.card ≤ G.edgeFinset.card

Tactic:
exact Finset.card_mono <| by simpa

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

Goal state before:
pp: case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ↑u = n + 2 - 1
hv : ¬↑v = n + 2 - 1
⊢ 2 ≠ ⟨↑v % 2, ⋯⟩

pp: case pos
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ↑v = n + 2 - 1
⊢ ⟨↑u % 2, ⋯⟩ ≠ 2

pp: case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
⊢ ⟨↑u % 2, ⋯⟩ ≠ ⟨↑v % 2, ⋯⟩

Tactic:
· refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val (?_))).symm
        exact v.val.mod_lt Nat.zero_lt_two

Goal state after:
case pos
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ↑v = n + 2 - 1
⊢ ⟨↑u % 2, ⋯⟩ ≠ 2

case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
⊢ ⟨↑u % 2, ⋯⟩ ≠ ⟨↑v % 2, ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case e'_1
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ univ ∧ ¬G.Adj s a✝ ↔ h.setoid s a✝

Tactic:
simp +instances [setoid]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
c : G.ConnectedComponent
⊢ (c ∈ univ ∧ Odd c.supp.ncard) ∧ c.supp ⊆ c'.supp ↔
    (c ∈ univ ∧ c.supp ⊆ c'.supp) ∧ Odd #(filter (Membership.mem c.supp) univ)

Tactic:
← Set.ncard_coe_finset,

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
c : G.ConnectedComponent
⊢ (c ∈ univ ∧ Odd c.supp.ncard) ∧ c.supp ⊆ c'.supp ↔
    (c ∈ univ ∧ c.supp ⊆ c'.supp) ∧ Odd (↑(filter (Membership.mem c.supp) univ)).ncard
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
⊢ r * t * ((r - 1) * t) = r * (r - 1) * t ^ 2

Tactic:
rw [← mul_assoc, mul_comm r _, mul_assoc t _ _, mul_comm t, mul_assoc _ t, ← pow_two]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
h : r = 0 ∨ t = 0
ht : t = 0
⊢ #∅ = r ∨ t = 0

Tactic:
by simp [ht]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
⊢ Even (K.supp \ s).ncard

Tactic:
by_cases h : Even K.supp.ncard
  · simpa [hrep.ncard_sdiff_of_notMem
      (by simpa [Set.ncard_image_of_injective, ← Nat.not_odd_iff_even] using h)] using h
  · have : K.supp.ncard ≠ 0 := Nat.ne_of_odd_add (Nat.not_even_iff_odd.mp h)
    rw [hrep.ncard_sdiff_of_mem (Nat.not_even_iff_odd.mp h), Nat.even_sub (by lia)]
    simpa [Nat.even_sub] using Nat.not_even_iff_odd.mp h

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

Goal state before:
pp: case neg
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
⊢ (completeEquipartiteGraph r t).Copy G

Tactic:
· have : Nonempty (Fin r ↪ K.parts) := by
      rw [Embedding.nonempty_iff_card_le,
        Fintype.card_fin, card_coe, K.card_parts.resolve_right ht]
    let fᵣ : Fin r ↪ K.parts := Classical.arbitrary (Fin r ↪ K.parts)
    have (p : K.parts) : Nonempty (Fin t ↪ p) := by
      rw [Embedding.nonempty_iff_card_le, Fintype.card_fin, card_coe, K.card_mem_parts p.prop]
    let fₜ (p : K.parts) : Fin t ↪ p :=
      Classical.arbitrary (Fin t ↪ p)
    let f : (Fin r) × (Fin t) ↪ V := by
      use fun (i, j) ↦ fₜ (fᵣ i) j
      intro (i₁, j₁) (i₂, j₂) heq
      rw [Prod.mk.injEq]
      contrapose! heq with hne
      rcases eq_or_ne i₁ i₂ with heq | hne
      · rw [heq, ← Subtype.ext_iff.ne]
        exact (fₜ _).injective.ne (hne heq)
      · refine (K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop).ne
        exact Subtype.ext_iff.ne.mp <| fᵣ.injective.ne hne
    refine ⟨⟨f, fun hne ↦ ?_⟩, f.injective⟩
    refine K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop
    exact Subtype.ext_iff.ne.mp <| fᵣ.injective.ne hne

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.ediam = 0
⊢ Subsingleton α

Tactic:
by
  contrapose! h
  exact ediam_ne_zero

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
r t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
⊢ (between (↑K.verts) (↑K.verts)ᶜ G).IsBipartiteWith (↑K.verts) (↑K.verts)ᶜ

Tactic:
exact between_isBipartiteWith (disjoint_compl_right)

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

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ zarankiewicz m n s t =
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
let e₁ := completeBipartiteGraphCongr
    (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
  let K := completeBipartiteGraph (Fin s) (Fin t)
  let e₂ := completeBipartiteGraphCongr
    (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
  rw [zarankiewicz, le_antisymm_iff]
  and_intros
  on_goal 1 =>
    let e₁ := e₁.symm
    let K := completeBipartiteGraph α β
    let e₂ := e₂.symm
  all_goals
    simp_rw [Finset.sup_le_iff, mem_filter, mem_univ, true_and]
    intro G ⟨h_le, h_free⟩
    simp_rw [Iso.card_edgeFinset_eq (.map e₁.toEquiv G)]
    have h' : G.map e₁.toEquiv.toEmbedding ∈ univ.filter fun G ↦
        G ≤ completeBipartiteGraph _ _ ∧ K.Free G := by
      rw [mem_filter_univ, map_le_iff_le_comap]
      refine ⟨fun _ _ hadj ↦ ?_, ?_⟩
      · replace h_le := h_le hadj
        rw [← Embedding.map_adj_iff e₁.toEmbedding, ← comap_adj] at h_le
        exact h_le
      · rw [Function.Embedding.coeFn_mk, ← free_congr e₂ (.map e₁.toEquiv G)]
        exact h_free
    have h_le_sup := @le_sup _ _ _ _ _ (#·.edgeFinset) (G.map e₁.toEquiv.toEmbedding) h'
    simp_rw [← card_coe, mem_edgeFinset] at h_le_sup ⊢
    exact h_le_sup

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard

Tactic:
obtain hs | hs := s.infinite_or_finite
  · rw [hs.ncard]
    by_cases h : 1 = 0
    · simp [h]
    · exact finsum_mem_eq_zero_of_infinite (by simpa [Function.support_const h])
  · simp [finsum_mem_eq_finite_toFinset_sum _ hs, Set.ncard_eq_toFinset_card s hs]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
hp : p.IsHamiltonian
⊢ p.length + 1 = Fintype.card α

Tactic:
by
    rw [← length_support, ← List.sum_toFinset_count_eq_length, Finset.sum_congr rfl fun _ _ ↦ hp _,
      ← card_eq_sum_ones, hp.toFinset_support, card_univ]

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : MulZeroOneClass R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
h : e ∈ G.incidenceSet a
⊢ incMatrix R G a e = 1

Tactic:
by
  rw [incMatrix_apply, Set.indicator_of_mem h, Pi.one_apply]

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
⊢ LinearIndependent ℝ G.lapMatrix_ker_basis_aux

Tactic:
rw [Fintype.linearIndependent_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 → ℝ), ∑ i, g i • G.lapMatrix_ker_basis_aux i = 0 → ∀ (i : G.ConnectedComponent), g i = 0
Module: Mathlib.Combinatorics.SimpleGraph.Star

Goal state before:
pp: case inr
V : Type u_1
r v w : V
hadj : v ≠ w ∧ (v = r ∨ w = r)
this : ∀ {V : Type u_1} (r v w : V), v ≠ w ∧ (v = r ∨ w = r) → v = r → (starGraph r).IsBridge s(v, w)
h : v ≠ r
⊢ (starGraph r).IsBridge s(v, w)

Tactic:
rw [Sym2.eq_swap]
    exact this r w v ⟨hadj.1.symm, hadj.2.symm⟩ (hadj.2.resolve_left h)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
i j : G.deleteUniversalVerts.coe.ConnectedComponent
hij : i ≠ j
⊢ Disjoint (complMatch i).verts (complMatch j).support

Tactic:
hcomplMatch_compl i,

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
i j : G.deleteUniversalVerts.coe.ConnectedComponent
hij : i ≠ j
⊢ Disjoint (Subtype.val '' i.supp \ M1.verts) (complMatch j).support
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case refine_4
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
p₁✝ p₂✝ : Finset (Fin n)
v₁ v₂ : Fin n
hv₂ : v₂ ∈ ↑p₂✝
p₁ : Finset (Fin n)
hp₁ : p₁ ∈ K.parts
hne : y p₁ ⋯ ≠ p₂✝
hv₁ : v₁ ∈ ↑(y p₁ ⋯)
hyp₁ : y p₁ ⋯ = p₁✝
hy₁' : y p₁ hp₁ ⊆ p₁ ∧ #(y p₁ hp₁) = t
p₂ : Finset (Fin n)
hp₂ : p₂ ∈ K.parts
hyp₂ : y p₂ ⋯ = p₂✝
⊢ G.Adj v₁ v₂

Tactic:
rw [← hyp₂] at hv₂ hne

Goal state after:
case refine_4
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
p₁✝ p₂✝ : Finset (Fin n)
v₁ v₂ : Fin n
p₁ : Finset (Fin n)
hp₁ : p₁ ∈ K.parts
hv₁ : v₁ ∈ ↑(y p₁ ⋯)
hyp₁ : y p₁ ⋯ = p₁✝
hy₁' : y p₁ hp₁ ⊆ p₁ ∧ #(y p₁ hp₁) = t
p₂ : Finset (Fin n)
hp₂ : p₂ ∈ K.parts
hne : y p₁ ⋯ ≠ y p₂ ⋯
hv₂ : v₂ ∈ ↑(y p₂ ⋯)
hyp₂ : y p₂ ⋯ = p₂✝
⊢ G.Adj v₁ v₂
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
this :
  ∀ (a : Option α) (b : Option β),
    Option.map (fun p ↦ f p.1 p.2) (a.bind fun a ↦ Option.map (Prod.mk a) b) = a.bind fun a ↦ Option.map (f a) b
⊢ Primrec₂ f ↔ Nat.Primrec (Nat.unpaired fun m n ↦ encode ((decode m).bind fun a ↦ Option.map (f a) (decode n)))

Tactic:
simp [Primrec₂, Primrec, this]

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: this : PrimrecRel fun a b ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : ¬k = 0
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun x1 x2 ↦ x1 / x2) (a, k).1 (a, k).2 = q

Tactic:
else

Goal state after:
this : PrimrecRel fun a b ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : ¬k = 0
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun x1 x2 ↦ x1 / x2) (a, k).1 (a, k).2 = q
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
⊢ (do
      let n ← (↑(decode n)).bind fun a ↦ map encode (↑f a)
      ↑n.ppred) =
    (↑(decode n)).bind fun a ↦ map encode ((fun a ↦ ↑(f a)) a)

Tactic:
rcases decode (α := α) n with - | a

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
⊢ (do
      let n ← (↑Option.none).bind fun a ↦ map encode (↑f a)
      ↑n.ppred) =
    (↑Option.none).bind fun a ↦ map encode ((fun a ↦ ↑(f a)) a)

case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ (do
      let n ← (↑(Option.some a)).bind fun a ↦ map encode (↑f a)
      ↑n.ppred) =
    (↑(Option.some a)).bind fun a ↦ map encode ((fun a ↦ ↑(f a)) a)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: m n : ℕ
f : List.Vector ℕ m → List.Vector ℕ n
h : Vec f
⊢ Primrec f

Tactic:
by simpa using Primrec.vector_ofFn fun i => to_prim (h i)

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
⊢ encode (cf.pair cg) < encode (cf.comp cg)

Tactic:
simp [encodeCode_eq, encodeCode]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
⊢ encode (cf.pair cg) < encode (cf.prec cg)

Tactic:
simp [encodeCode_eq, encodeCode]

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun x ↦ x ^ (p - 1) * (log x ^ 2)⁻¹) =o[atTop] fun z ↦ z ^ (p - 1) * 1⁻¹

Tactic:
refine IsBigO.mul_isLittleO (isBigO_refl _ _)
              (IsLittleO.inv_rev ?_ (by simp))

Goal state after:
p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ 1) =o[atTop] fun x ↦ log x ^ 2
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly✝ : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
hq_poly :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b' * x) x,
      (fun x ↦ ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x ↦ ‖deriv q x‖) x) (c₂ * (fun x ↦ ‖deriv q x‖) x)
h_tendsto : Tendsto (fun x ↦ b' * x) atTop atTop
n : ℕ
hn : ∀ u ∈ Set.Icc (b' * ↑n) ↑n, ‖deriv q u‖ ∈ Set.Icc (c₁ * ‖deriv q ↑n‖) (c₂ * ‖deriv q ↑n‖)
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
h_ge_n₀ : R.n₀ ≤ n
h_n_pos : 0 < n
h_bn : 1 < b' * ↑n
z : ℝ
hz : z ∈ Set.Icc (b' * ↑n) ↑n
⊢ DifferentiableAt ℝ q z

Tactic:
refine hq_diff.differentiableAt (Ioi_mem_nhds ?_)
    calc 1 < b' * n := h_bn
         _ ≤ z := hz.1

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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ GrowsPolynomially fun x ↦ ‖f x‖

Tactic:
simp only [norm_eq_abs]
  exact hf.abs

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

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
x : ℝ
hx₁ : 0 ≤ f x
hx₂ : 0 ≤ g x
⊢ f x * g x = |f x| * |g x|

Tactic:
rw [abs_of_nonneg hx₁, abs_of_nonneg hx₂]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
u : ℕ
hu : r i n ≤ u ∧ u < n
this : 0 < u
⊢ ↑u ≤ ↑n

Tactic:
by exact_mod_cast (le_of_lt hu.2)

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n x : ℕ
left✝ : n ≤ k
h : ∃ a, evaln (k + 1) cf n = some a ∧ ∃ a_1, evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x
⊢ ∃ a ∈ cf.eval n, ∃ a_1 ∈ cg.eval n, Nat.pair a a_1 = x

Tactic:
rcases h with ⟨y, ef, z, eg, rfl⟩

Goal state after:
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
y : ℕ
ef : evaln (k + 1) cf n = some y
z : ℕ
eg : evaln (k + 1) cg n = some z
⊢ ∃ a ∈ cf.eval n, ∃ a_1 ∈ cg.eval n, Nat.pair a a_1 = Nat.pair y z
Module: Mathlib.Computability.Language

Goal state before:
pp: case a
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ m∗ * n ≤ l

Tactic:
rw [kstar_eq_iSup_pow, iSup_mul, iSup_le_iff]

Goal state after:
case a
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ ∀ (i : ℕ), m ^ i * n ≤ l
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 0
⊢ (match 0 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match 0 + Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
Fin.zero_add,

Goal state after:
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 0
⊢ (match 0 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : Code → Code
hf : Computable f
g : ℕ → ℕ → Part ℕ :=
  fun x y ↦ do
    let b ← (ofNat Code x).eval x
    (ofNat Code b).eval y
this : Partrec₂ g
cg : Code
eg : cg.eval = fun n ↦ (↑(decode n)).bind fun a ↦ Part.map encode ((fun p ↦ g p.1 p.2) a)
⊢ ∀ (a n : ℕ), cg.eval (Nat.pair a n) = Part.map encode (g a n)

Tactic:
by simp [eg]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a✝¹ (some s)) ↔ x✝ ∈ M.step a✝¹ s

Tactic:
M.toεNFA_εClosure

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ M.toεNFA.step a✝¹ (some s) ↔ x✝ ∈ M.step a✝¹ s
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: this : ∀ (f : ℕ →. ℕ), Nat.Partrec f → Partrec' fun v ↦ f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec f
⊢ Partrec' f

Tactic:
let g := fun n₁ =>
        (Part.ofOption (decode (α := List.Vector ℕ n) n₁)).bind (fun a => Part.map encode (f a))
      exact
        (comp₁ g (this g hf) (prim Nat.Primrec'.encode)).of_eq fun i => by
          dsimp only [g]; simp [encodek, Part.map_id']

Goal state after: