mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ (0 + f₁ (insert a s)) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [zero_add, collapse_eq hat, mul_add]

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ ((f₁ (insert a s) * if t ∈ ℬ then f₂ t else 0) + f₁ (insert a s) * if insert a t ∈ ℬ then f₂ (insert a t) else 0) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
x✝ : G.Colorable 1
C : G.Coloring (Fin 1)
u v : V
h : G.Adj u v
⊢ False

Tactic:
exact C.map_rel h <| Subsingleton.elim ..

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case refine_2
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
⊢ ∀ ⦃s t : Finset (Fin n)⦄, s ⊆ range'k ∧ #s = r → toColex t < toColex s ∧ #t = r → t ⊆ range'k ∧ #t = r

Tactic:
rintro A B hA ⟨HB₁, HB₂⟩

Goal state after:
case refine_2
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ : toColex B < toColex A
HB₂ : #B = r
⊢ B ⊆ range'k ∧ #B = r
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ s(v, w) ∉ (Walk.map (Hom.ofLE ⋯) p).edges

Tactic:
Walk.edges_map,

Goal state after:
case h
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ s(v, w) ∉ List.map (Sym2.map ⇑(Hom.ofLE ⋯)) p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w v' w' : V
p : G.Walk v' w'
h : s(v, w) ∉ p.edges
e : Sym2 V
ep : e ∈ p.edges
⊢ e ∈ (G.deleteEdges {s(v, w)}).edgeSet

Tactic:
edgeSet_deleteEdges

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
v w v' w' : V
p : G.Walk v' w'
h : s(v, w) ∉ p.edges
e : Sym2 V
ep : e ∈ p.edges
⊢ e ∈ G.edgeSet \ {s(v, w)}
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : ↑(card α) ≤ G.chromaticNumber
C : G.Coloring α
⊢ Surjective ⇑C

Tactic:
rw [C.colorable.chromaticNumber_eq_sInf, Nat.cast_le] at h
    intro i
    by_contra! hi
    let D : G.Coloring {a // a ≠ i} := ⟨fun v ↦ ⟨C v, hi v⟩, (C.valid · <| congr_arg Subtype.val ·)⟩
    classical
    exact Nat.notMem_of_lt_sInf ((Nat.sub_one_lt_of_lt <| card_pos_iff.2 ⟨i⟩).trans_le h)
      ⟨G.recolorOfEquiv (equivOfCardEq <| by simp) D⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
⊢ ↑n ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring (Fin n)), Surjective ⇑C

Tactic:
simp [← card_le_chromaticNumber_iff_forall_surjective]

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

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
p : (G.deleteEdges {s(y, x)}).Walk u x
hx₂ : G.Adj x p.penultimate
hy₂ : ¬p.penultimate = y
⊢ False

Tactic:
exact hy₂ <| hx hx₂ hxy

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

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
p : (G.deleteEdges {s(y, x)}).Walk v x
hx₂ : G.Adj x p.penultimate
hy₂ : ¬p.penultimate = y
⊢ False

Tactic:
exact hy₂ <| hx hx₂ hxy

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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
⊢ G'.edist u v ≤ G.edist u v

Tactic:
obtain ⟨_, hw⟩ := hr.exists_walk_length_eq_edist

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : ↑w✝.length = G.edist u v
⊢ G'.edist u v ≤ G.edist u v
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ A.compl i j = 0 ∨ A.compl i j = 1

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
  without the `simp`. This is probably a problem at Mathlib's end rather than `grind`'s,
  as we are relying on seeing through the definition of `Matrix`, and `of`. -/
  simp [compl]
  grind

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

Goal state before:
pp: case refine_2.a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑(⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).2 ≤ ↑v.2

Tactic:
rw [Nat.div_le_iff_le_mul_add_pred v.1.pos, mul_comm r ↑v.2]

Goal state after:
case refine_2.a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑⟨↑v.2 * r + ↑v.1, ⋯⟩ ≤ ↑v.2 * r + (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
u : α
⊢ G.eccent u = ⊤

Tactic:
by
  rw [connected_iff_exists_forall_reachable] at h
  push Not at h
  obtain ⟨v, h⟩ := h u
  rw [eq_top_iff, ← edist_eq_top_of_not_reachable h]
  exact le_iSup (G.edist u) v

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
huv : ⊤.Adj u v
⊢ u ≠ v

Tactic:
exact huv.ne

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.ediam = ↑1 ↔ G = ⊤

Tactic:
Nat.cast_one,

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.ediam = 1 ↔ G = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
sec : s ∈ G.end
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : v ∉ Opposite.unop L
hs : s L = G.componentComplMk vnL
⊢ s K = G.componentComplMk ⋯

Tactic:
← sec h,

Goal state after:
V : Type u
G : SimpleGraph V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
sec : s ∈ G.end
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : v ∉ Opposite.unop L
hs : s L = G.componentComplMk vnL
⊢ (ConcreteCategory.hom (G.componentComplFunctor.map h)) (s L) = G.componentComplMk ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
cf : G.CliqueFree (0 + 1)
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % 0) ^ 2) * (0 - 1) / (2 * 0) + (n % 0).choose 2

Tactic:
rw [cliqueFree_one, ← Fintype.card_eq_zero_iff] at cf

Goal state after:
case inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
cf : Fintype.card V = 0
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % 0) ^ 2) * (0 - 1) / (2 * 0) + (n % 0).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
cf : Fintype.card V = 0
⊢ #G.edgeFinset ≤ (Fintype.card V ^ 2 - (Fintype.card V % 0) ^ 2) * (0 - 1) / (2 * 0) + (Fintype.card V % 0).choose 2

Tactic:
zero_tsub,

Goal state after:
case inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
cf : Fintype.card V = 0
⊢ #G.edgeFinset ≤ (Fintype.card V ^ 2 - (Fintype.card V % 0) ^ 2) * 0 / (2 * 0) + (Fintype.card V % 0).choose 2
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 : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
| #K.verts - t'

Tactic:
K.card_verts,

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 : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
| r * t' - t'
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'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
| ↑n * (↑(#K.verts) * ε - ↑(#K.verts) * (1 / ↑r) + (↑t' - ↑t)) - ↑(#K.verts) * (↑t' - ↑t)

Tactic:
K.card_verts,

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'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
| ↑n * (↑(r * t') * ε - ↑(r * t') * (1 / ↑r) + (↑t' - ↑t)) - ↑(r * t') * (↑t' - ↑t)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r : ℕ
h : Maximal (fun H ↦ H.CliqueFree (0 + 1)) G
⊢ G.Colorable 0 ↔ G.IsCompleteMultipartite

Tactic:
exact ⟨fun _ ↦ ⟨fun x ↦ cliqueFree_one.1 h.1 |>.elim' x⟩,
                fun _ ↦ G.colorable_zero_iff.2 <| cliqueFree_one.1 h.1⟩

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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ Injective g'

pp: case refine_3
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (a : ↑p₁), G.Adj ↑a ↑(f' a)

pp: case refine_4
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (b : ↑p₂), G.Adj ↑(g' b) ↑b

Tactic:
· exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective

Goal state after:
case refine_3
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (a : ↑p₁), G.Adj ↑a ↑(f' a)

case refine_4
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (b : ↑p₂), G.Adj ↑(g' b) ↑b
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
h : a ≠ b
⊢ List.count b (a :: p.tail.support) = 1

Tactic:
List.count_cons_of_ne h,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
h : a ≠ b
⊢ List.count b p.tail.support = 1
Module: Mathlib.Combinatorics.SimpleGraph.LineGraph

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
e₁ e₂ : ↑G.edgeSet
hadj : e₁ ≠ e₂ ∧ (↑↑e₁ ∩ ↑↑e₂).Nonempty
⊢ e₂ ≠ e₁ ∧ (↑↑e₂ ∩ ↑↑e₁).Nonempty

Tactic:
rwa [ne_comm, Set.inter_comm]

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

Goal state before:
pp: case convert_3
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #((G.neighborFinset w \ G.neighborFinset v) \ {v}) = k - ℓ - 1

Tactic:
card_sdiff_of_subset s,

Goal state after:
case convert_3
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w \ G.neighborFinset v) - #{v} = k - ℓ - 1
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
⊢ #(Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ) = r ∨ t = 0

Tactic:
card_map,

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
⊢ #univ = r ∨ t = 0
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 < (⊤.deleteVerts u).coe.oddComponents.ncard
⊢ u.ncard < (⊤.deleteVerts u).coe.oddComponents.ncard

Tactic:
have := ncard_oddComponents_mono _ (Subgraph.deleteVerts_mono' (G := G) (G' := G') u h)

Goal state after:
V : Type u_1
G G' : SimpleGraph V
inst✝ : Finite V
u : Set V
h : G ≤ G'
ht : u.ncard < (⊤.deleteVerts u).coe.oddComponents.ncard
this : (⊤.deleteVerts u).coe.oddComponents.ncard ≤ (⊤.deleteVerts u).coe.oddComponents.ncard
⊢ u.ncard < (⊤.deleteVerts u).coe.oddComponents.ncard
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ ν : YoungDiagram
h : (fun y ↦ ↑y.cells) μ = (fun y ↦ ↑y.cells) ν
⊢ μ = ν

Tactic:
by rwa [YoungDiagram.ext_iff, ← Finset.coe_inj]

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
l : List (List α)
⊢ List.foldr (fun b s ↦ (fun x1 x2 ↦ x1 ++ x2) (l, b, s).2.1 (l, b, s).2.2) [] (id l) = l.flatten

Tactic:
by
    dsimp; induction l <;> simp [*]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
e : decode n = Option.none
⊢ (do
      let n ← Nat.pair <$> Part.some n <*> (↑Option.none).bind fun a ↦ map encode (f a)
      (↑(decode n)).bind fun a ↦ map encode ((fun p ↦ g p.1 p.2) a)) =
    (↑Option.none).bind fun a ↦ map encode ((fun a ↦ (f a).bind (g a)) a)

Tactic:
simp [Seq.seq, e, encodek]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
val✝ : α
e : decode n = Option.some val✝
⊢ (do
      let n ← Nat.pair <$> Part.some n <*> (↑(Option.some val✝)).bind fun a ↦ map encode (f a)
      (↑(decode n)).bind fun a ↦ map encode ((fun p ↦ g p.1 p.2) a)) =
    (↑(Option.some val✝)).bind fun a ↦ map encode ((fun a ↦ (f a).bind (g a)) a)

Tactic:
simp [Seq.seq, e, encodek]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
⊢ (((↑(decode n)).bind fun a ↦ Part.map encode (↑f a)).bind fun n_1 ↦
      Nat.rec ((↑(decode n)).bind fun a ↦ Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode ((fun p ↦ h p.1 p.2) a))
        n_1) =
    (↑(decode n)).bind fun a ↦ Part.map encode ((fun a ↦ Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) (f a)) a)

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

Goal state after:
case none
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
e : decode n = Option.none
⊢ (((↑Option.none).bind fun a ↦ Part.map encode (↑f a)).bind fun n_1 ↦
      Nat.rec ((↑Option.none).bind fun a ↦ Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode ((fun p ↦ h p.1 p.2) a))
        n_1) =
    (↑Option.none).bind fun a ↦
      Part.map encode ((fun a ↦ Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) (f a)) a)

case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
⊢ (((↑(Option.some a)).bind fun a ↦ Part.map encode (↑f a)).bind fun n_1 ↦
      Nat.rec ((↑(Option.some a)).bind fun a ↦ Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode ((fun p ↦ h p.1 p.2) a))
        n_1) =
    (↑(Option.some a)).bind fun a ↦
      Part.map encode ((fun a ↦ Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) (f a)) a)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
⊢ (((↑(decode n)).bind fun a ↦ Part.some (encode (g a))).bind fun n ↦
      (↑(decode n)).bind fun a ↦ Part.map encode (f a)) =
    (↑(decode n)).bind fun a ↦ Part.map encode (f (g a))

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

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
e : decode n = Option.none
⊢ (((↑Option.none).bind fun a ↦ Part.some (encode (g a))).bind fun n ↦
      (↑(decode n)).bind fun a ↦ Part.map encode (f a)) =
    (↑Option.none).bind fun a ↦ Part.map encode (f (g a))

case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
a : α
e : decode n = Option.some a
⊢ (((↑(Option.some a)).bind fun a ↦ Part.some (encode (g a))).bind fun n ↦
      (↑(decode n)).bind fun a ↦ Part.map encode (f a)) =
    (↑(Option.some a)).bind fun a ↦ Part.map encode (f (g a))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
pf : Primrec' f
⊢ Primrec f

Tactic:
induction pf with
  | zero => exact .const 0
  | succ => exact _root_.Primrec.succ.comp .vector_head
  | get i => exact Primrec.vector_get.comp .id (.const i)
  | comp _ _ _ hf hg => exact hf.comp (.vector_ofFn fun i => hg i)
  | @prec n f g _ _ hf hg =>
    exact
      .nat_rec' .vector_head (hf.comp Primrec.vector_tail)
        (hg.comp <|
          Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
          Primrec.vector_cons.comp (Primrec.snd.comp .snd) <|
            (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case comp
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 : ℕ), (fun n ↦ f✝ (g✝ n)) n < ack m n

Tactic:
exact
      ⟨max a b + 2, fun n =>
        (ha _).trans <| (ack_strictMono_right a <| hb n).trans <| ack_ack_lt_ack_max_add_two a b n⟩

Goal state after: