mathlib-initiative/mathlib-tactics huggingface dataset:
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]

Goal state after:
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
this : Nonempty (Fin r ↪ ↥K.parts)
⊢ (completeEquipartiteGraph r t).Copy G
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case a
n r c : ℕ
hr : r > 0
⊢ 1 ≤ #({i ∈ range r | c % r = (n + i) % r})

Tactic:
one_le_card

Goal state after:
case a
n r c : ℕ
hr : r > 0
⊢ {i ∈ range r | c % r = (n + i) % r}.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case inj'.inl
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne : i₁ = i₂ → j₁ ≠ j₂
heq : i₁ = i₂
⊢ ↑((fₜ (fᵣ i₁)) j₁) ≠ ↑((fₜ (fᵣ i₂)) j₂)

pp: case inj'.inr
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne✝ : i₁ = i₂ → j₁ ≠ j₂
hne : i₁ ≠ i₂
⊢ ↑((fₜ (fᵣ i₁)) j₁) ≠ ↑((fₜ (fᵣ i₂)) j₂)

Tactic:
· rw [heq, ← Subtype.ext_iff.ne]
        exact (fₜ _).injective.ne (hne heq)

Goal state after:
case inj'.inr
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne✝ : i₁ = i₂ → j₁ ≠ j₂
hne : i₁ ≠ i₂
⊢ ↑((fₜ (fᵣ i₁)) j₁) ≠ ↑((fₜ (fᵣ i₂)) j₂)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_2
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
i₁ i₂ : Fin r
h :
  ∀ (a : V),
    a ∈ map { toFun := fun j ↦ f (i₁, j), inj' := ⋯ } univ ↔ a ∈ map { toFun := fun j ↦ f (i₂, j), inj' := ⋯ } univ
this : NeZero t
w✝ : Fin t
heq : (i₁, w✝) = (i₂, 0)
⊢ i₁ = i₂

Tactic:
rw [Prod.mk.injEq] at heq

Goal state after:
case neg.refine_2
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
i₁ i₂ : Fin r
h :
  ∀ (a : V),
    a ∈ map { toFun := fun j ↦ f (i₁, j), inj' := ⋯ } univ ↔ a ∈ map { toFun := fun j ↦ f (i₂, j), inj' := ⋯ } univ
this : NeZero t
w✝ : Fin t
heq : i₁ = i₂ ∧ w✝ = 0
⊢ i₁ = i₂
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties

Goal state before:
pp: V : Type
G : SimpleGraph V
inst✝ : Finite V
⊢ ∀ (a : ↑G.end), False

Tactic:
by
    rintro ⟨s, _⟩
    cases nonempty_fintype V
    obtain ⟨v, h⟩ := (s <| Opposite.op Finset.univ).nonempty
    exact Set.disjoint_iff.mp (s _).disjoint_right
        ⟨by simp only [Finset.coe_univ, Set.mem_univ], h⟩

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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
⊢ ⊥ ⊑ G ↔ ∃ K, ∀ p ∈ K.parts, ∀ ⦃v₁ : V⦄, v₁ ∈ ↑p → ∀ ⦃v₂ : V⦄, v₂ ∈ ↑∅ → G.Adj v₁ v₂

Tactic:
mem_coe,

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
⊢ ⊥ ⊑ G ↔ ∃ K, ∀ p ∈ K.parts, ∀ ⦃v₁ : V⦄, v₁ ∈ p → ∀ ⦃v₂ : V⦄, v₂ ∈ ∅ → G.Adj v₁ v₂
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ Subtype.val '' ⇑f ⁻¹' range Sum.inl ∪ Subtype.val '' ⇑f ⁻¹' range Sum.inr = s

Tactic:
simp [← image_union, ← preimage_union]

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'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ Fintype.card ↥(K.parts.pi fun x ↦ powersetCard t x) * t ≤ Fintype.card ↥(filter K t)

Tactic:
card_coe

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ #(K.parts.pi fun x ↦ powersetCard t x) * t ≤ #(filter K t)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
w : V
hvw : M.Adj v w
⊢ v ∈ M.support

Tactic:
exact ⟨_, hvw⟩

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
x : ↥(toLin' (lapMatrix ℝ G)).ker
a✝ : x ∈ ⊤
⊢ ∀ (a b : V), G.Reachable a b → ↑x a = ↑x b

Tactic:
rw [← lapMatrix_mulVec_eq_zero_iff_forall_reachable,
    ← toLin'_apply, LinearMap.map_coe_ker]

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

Goal state before:
pp: case refine_2
ε : ℝ
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
⊢ Fintype.card ↥K.parts = r ∨ t = 0

Tactic:
card_coe

Goal state after:
case refine_2
ε : ℝ
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
⊢ #K.parts = r ∨ t = 0
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : Set V
⊢ G.IsVertexCover c → G.IsIndepSet cᶜ

Tactic:
grind [IsVertexCover, Set.Pairwise]

Goal state after:
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)
hne : p₁ ≠ p₂
v₁ : Fin n
hv₁ : v₁ ∈ ↑p₁
v₂ : Fin n
hv₂ : v₂ ∈ ↑p₂
hp₁ : ∃ x ∈ ↑K.parts.attach, y ↑x ⋯ = p₁
hp₂ : ∃ x ∈ ↑K.parts.attach, y ↑x ⋯ = p₂
⊢ G.Adj v₁ v₂

Tactic:
mem_coe,

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)
hne : p₁ ≠ p₂
v₁ : Fin n
hv₁ : v₁ ∈ ↑p₁
v₂ : Fin n
hv₂ : v₂ ∈ ↑p₂
hp₁ : ∃ x ∈ K.parts.attach, y ↑x ⋯ = p₁
hp₂ : ∃ x ∈ K.parts.attach, y ↑x ⋯ = p₂
⊢ G.Adj v₁ v₂
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ ν : YoungDiagram
h : μ.transpose.transpose ≤ ν
⊢ μ.transpose ≤ ν.transpose

Tactic:
exact YoungDiagram.le_of_transpose_le h

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

Goal state before:
pp: case inr
ε : ℝ
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
K' : G.CompleteEquipartiteSubgraph r t :=
  { parts := Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ, card_parts := ⋯, card_mem_parts := ⋯,
    isCompleteBetween := ⋯ }
p' : Finset (Fin n)
v w : Fin n
hw : w ∈ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ ErdosStone.filter K t) s)
w' : ↥(ErdosStone.filter K t)
hw'_eq : ↑w' = w
p : Finset (Fin n)
hp : p ∈ K.parts
hv : v ∈ ↑(y p hp)
hp'_eq : y p hp = p'
hw'_mem : (fun p hp ↦ ⋯.choose) = y
⊢ G.Adj v w

Tactic:
mem_coe,

Goal state after:
case inr
ε : ℝ
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
K' : G.CompleteEquipartiteSubgraph r t :=
  { parts := Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ, card_parts := ⋯, card_mem_parts := ⋯,
    isCompleteBetween := ⋯ }
p' : Finset (Fin n)
v w : Fin n
hw : w ∈ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ ErdosStone.filter K t) s)
w' : ↥(ErdosStone.filter K t)
hw'_eq : ↑w' = w
p : Finset (Fin n)
hp : p ∈ K.parts
hv : v ∈ y p hp
hp'_eq : y p hp = p'
hw'_mem : (fun p hp ↦ ⋯.choose) = y
⊢ G.Adj v w
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case none
m n : ℕ
s : m.psub n = none
⊢ m < n

Tactic:
refine lt_of_not_ge fun h => ?_

Goal state after:
case none
m n : ℕ
s : m.psub n = none
h : n ≤ m
⊢ False
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
o : Option α
⊢ (Option.casesOn (id o) [] fun b ↦ [id b]) = o.toList

Tactic:
by rcases o <;> simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
val✝ : α
⊢ ((↑(encode (decode (Nat.unpair n).2)).ppred).bind fun y ↦
      Part.some (encode ((decode (Nat.unpair n).2).bind fun a ↦ f val✝ a))) =
    (↑(Option.map (Prod.mk val✝) (decode (Nat.unpair n).2))).bind fun a ↦ Part.some (encode (f a.1 a.2))

Tactic:
cases decode (α := β) n.unpair.2

Goal state after:
case some.none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
val✝ : α
⊢ ((↑(encode Option.none).ppred).bind fun y ↦ Part.some (encode (Option.none.bind fun a ↦ f val✝ a))) =
    (↑(Option.map (Prod.mk val✝) Option.none)).bind fun a ↦ Part.some (encode (f a.1 a.2))

case some.some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
val✝¹ : α
val✝ : β
⊢ ((↑(encode (Option.some val✝)).ppred).bind fun y ↦ Part.some (encode ((Option.some val✝).bind fun a ↦ f val✝¹ a))) =
    (↑(Option.map (Prod.mk val✝¹) (Option.some val✝))).bind fun a ↦ Part.some (encode (f a.1 a.2))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_1.succ
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
n✝ : ℕ
_x : ∃ b', Sum.inl b' ∈ F a (n✝ + 1)
h₁ : ∀ {m : ℕ}, m < n✝ + 1 → ∃ b, Sum.inr b ∈ F a m
h₂ :
  Sum.inl b ∈
      Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.rec (fun val ↦ Part.some s) (fun val ↦ f val) s)
        n✝ ∨
    ∃ b_1,
      Sum.inr b_1 ∈
          Nat.rec (Part.some (Sum.inr a))
            (fun x IH ↦ IH.bind fun s ↦ Sum.rec (fun val ↦ Part.some s) (fun val ↦ f val) s) n✝ ∧
        Sum.inl b ∈ f b_1
⊢ b ∈ f.fix a

Tactic:
obtain ⟨c, hc⟩ := h₁ (Nat.lt_succ_self _)

Goal state after:
case refine_1.succ
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
n✝ : ℕ
_x : ∃ b', Sum.inl b' ∈ F a (n✝ + 1)
h₁ : ∀ {m : ℕ}, m < n✝ + 1 → ∃ b, Sum.inr b ∈ F a m
h₂ :
  Sum.inl b ∈
      Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.rec (fun val ↦ Part.some s) (fun val ↦ f val) s)
        n✝ ∨
    ∃ b_1,
      Sum.inr b_1 ∈
          Nat.rec (Part.some (Sum.inr a))
            (fun x IH ↦ IH.bind fun s ↦ Sum.rec (fun val ↦ Part.some s) (fun val ↦ f val) s) n✝ ∧
        Sum.inl b ∈ f b_1
c : α
hc : Sum.inr c ∈ F a n✝
⊢ b ∈ f.fix a
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
⊢ rec (f m) (fun y IH ↦ g (pair m (pair y IH))) (n + 1) < ack (max a b + 9) (m + (n + 1))

Tactic:
simp only
        apply (hb _).trans ((ack_pair_lt _ _ _).trans_le _)
        -- If m is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ m with h₁ | h₁
        · rw [max_eq_left h₁.le]
          gcongr <;> omega
        rw [max_eq_right h₁]
        -- We get rid of the second `pair`.
        apply (ack_pair_lt _ _ _).le.trans
        -- If n is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ n with h₂ | h₂
        · rw [max_eq_left h₂.le, add_assoc]
          exact
            ack_le_ack (Nat.add_le_add (le_max_right a b) <| by simp)
              ((le_succ n).trans <| self_le_add_left _ _)
        rw [max_eq_right h₂]
        -- We now use the inductive hypothesis, and some simple algebraic manipulation.
        apply (ack_strictMono_right _ IH).le.trans
        rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one,
            ack_succ_succ (_ + 8), add_assoc]
        exact ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖) =Θ[atTop] fun z ↦ z ^ (p - 1)

Tactic:
refine IsTheta.norm_left ?_

Goal state after:
p : ℝ
hp : p ≠ 0
⊢ (deriv fun z ↦ z ^ p * (1 - ε z)) =Θ[atTop] fun z ↦ z ^ (p - 1)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖) =Θ[atTop] fun z ↦ z ^ (p - 1)

Tactic:
refine IsTheta.norm_left ?_

Goal state after:
p : ℝ
hp : p ≠ 0
⊢ (deriv fun z ↦ z ^ p * (1 + ε z)) =Θ[atTop] fun z ↦ z ^ (p - 1)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ (fun z ↦ -deriv ε z) =o[atTop] fun x ↦ x⁻¹

Tactic:
rw [isLittleO_neg_left]

Goal state after:
⊢ deriv ε =o[atTop] fun x ↦ x⁻¹
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case rfind'
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
⊢ ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)

Tactic:
induction y generalizing m with simp [evaln, Option.bind_eq_some_iff]
    | zero =>
      simp at hy₁
      rcases hf hy₁ with ⟨k, hk⟩
      exact ⟨_, Nat.le_of_lt_succ <| evaln_bound hk, _, hk, by simp⟩
    | succ y IH =>
      rcases hy₂ (Nat.succ_pos _) with ⟨a, ha, a0⟩
      rcases hf ha with ⟨k₁, hk₁⟩
      rcases IH m.succ (by simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hy₁)
          fun {i} hi => by
          simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using
            hy₂ (Nat.succ_lt_succ hi) with
        ⟨k₂, hk₂⟩
      use (max k₁ k₂).succ
      rw [zero_add] at hk₁
      use Nat.le_succ_of_le <| le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁
      use a
      use evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_left _ _) hk₁
      simpa [a0, add_comm, add_left_comm] using
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case head
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v s : List (Symbol T N)
⊢ ∃ p q, Symbol.nonterminal r.input :: s = p ++ [Symbol.nonterminal r.input] ++ q ∧ r.output ++ s = p ++ r.output ++ q

Tactic:
use [], s
    simp

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
⊢ ((reindex g) M).accepts = M.accepts

Tactic:
by
  ext x
  simp [mem_accepts]

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

Goal state before:
pp: n : ℕ
⊢ n < 2 ^ n.size

Tactic:
induction n using binaryRec' with
  | zero => simp
  | bit b n h IH =>
    rw [← Nat.bit_ne_zero_iff] at h
    rwa [size_bit h, bit_lt_two_pow_succ_iff]

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

Goal state before:
pp: C : SNum → Sort u_1
z : (b : Bool) → C (zero b)
s : (b : Bool) → (p : SNum) → C p → C (b::p)
b : Bool
⊢ C (b::zero (decide ¬b = true))

Tactic:
exact s b (SNum.zero (Not b)) (z (Not b))

Goal state after: