mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise f
hg : g = hs.piecewise f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
hg_inj : InjOn g (⋃ i, s i)
⊢ BijOn g (⋃ i, s i) (⋃ i, t i)

Tactic:
exact bijOn_iUnion hg_bij hg_inj

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ C.toSimpleGraph.Preconnected

Tactic:
intro ⟨u, hu⟩ ⟨v, hv⟩
    exact C.reachable_toSimpleGraph hu hv

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
inst✝¹ : Fintype α
inst✝ : Fintype ↑C.colorClasses
⊢ card ↑C.colorClasses ≤ card α

Tactic:
simp only [colorClasses]

Goal state after:
V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
inst✝¹ : Fintype α
inst✝ : Fintype ↑C.colorClasses
⊢ card ↑(Setoid.ker ⇑C).classes ≤ card α
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
⊢ ¬(G.deleteEdges {s(v, w)}).Reachable v w ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges

Tactic:
reachable_deleteEdges_iff_exists_walk,

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
⊢ (¬∃ p, s(v, w) ∉ p.edges) ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst✝ : Fintype ↑(G.neighborSet u)
h : G.IsEdgeReachable k u v
huv : u ≠ v
⊢ k ≤ G.degree u

Tactic:
classical
  by_contra! hh
  rw [← card_incidenceSet_eq_degree, ← ENat.natCast_lt_natCast, Set.coe_fintypeCard] at hh
  obtain ⟨w, _⟩ := h hh |>.exists_isPath
  simpa using w.adj_snd <| mt Walk.Nil.eq huv

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
⊢ (between s t G).Adj v w ↔ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)

Tactic:
by rfl

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hμ : Monotone μ
hf : 0 < f
hg : 0 ≤ 0
hfg : ∑ a, f a = ∑ a, 0 a
h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)
⊢ ∑ a, μ a * f a ≤ ∑ a, μ a * 0 a

Tactic:
simp only [Pi.zero_apply, sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg
    simp [hfg]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ 2 < G.edist u v ↔ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ lt_of_le_of_ne ?_ (Ne.symm ?_)⟩

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
⊢ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅

case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ 2 ≤ G.edist u v

case refine_3
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ G.edist u v ≠ 2
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:

Tactic:
p.length
      _ = G.dist u v := hp
      _ ≤ p.bypass.length := dist_le p.bypass

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

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅

Tactic:
obtain h | h := Finset.eq_empty_or_nonempty {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}

Goal state after:
case h.inl
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅

case h.inr
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v v✝ : V
h✝¹ : G.Adj u v✝
h✝ : G.Adj v✝ v
hp : (Walk.cons h✝¹ (Walk.cons h✝ Walk.nil)).length = 2
⊢ (fun w ↦ ⟨(Adj.toWalk ⋯).concat ⋯, ⋯⟩) ((fun p ↦ ⟨(↑p).snd, ⋯⟩) ⟨Walk.cons h✝¹ (Walk.cons h✝ Walk.nil), hp⟩) =
    ⟨Walk.cons h✝¹ (Walk.cons h✝ Walk.nil), hp⟩

Tactic:
by rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
s : Set G
⊢ circulantGraph s = circulantGraph (s ∪ -s)

Tactic:
ext
  simp only [circulantGraph_adj, Set.mem_union, Set.mem_neg, neg_sub]
  grind

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 y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
⊢ ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)

Tactic:
refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩

Goal state after:
case refine_1
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 y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
⊢ ¬y = default

case refine_2
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 y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
⊢ ((f y).firstDart ⋯).toProd = (y, x)
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
x✝ : G.Reachable u v
p : G.Walk u v
this✝¹ : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
this✝ : v ∉ s
u' v' : V
huv : G.Adj (u', v').1 (u', v').2
left✝ : { fst := u', snd := v', adj := huv } ∈ p.darts
hu : { fst := u', snd := v', adj := huv }.toProd.1 ∈ s
hv : { fst := u', snd := v', adj := huv }.toProd.2 ∉ s
this : ¬F.Reachable v' u'
⊢ False

Tactic:
suffices F ⊔ edge v' u' ≤ F by grind [Adj.reachable, sup_le_iff, le_iff_adj]

Goal state after:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
x✝ : G.Reachable u v
p : G.Walk u v
this✝¹ : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
this✝ : v ∉ s
u' v' : V
huv : G.Adj (u', v').1 (u', v').2
left✝ : { fst := u', snd := v', adj := huv } ∈ p.darts
hu : { fst := u', snd := v', adj := huv }.toProd.1 ∈ s
hv : { fst := u', snd := v', adj := huv }.toProd.2 ∉ s
this : ¬F.Reachable v' u'
⊢ F ⊔ edge v' u' ≤ F
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case map_rel'
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w✝ : α
hv : w✝ ∈ c.supp
a b : ↥c
hab : c.toSimpleGraph.Adj a b
he : Fin.ofNat 2 (Nonempty.some ⋯).length = Fin.ofNat 2 (Nonempty.some ⋯).length
⊢ Odd (((Nonempty.some ⋯).concat hab).append (Nonempty.some ⋯).reverse).length

Tactic:
length_append,

Goal state after:
case map_rel'
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w✝ : α
hv : w✝ ∈ c.supp
a b : ↥c
hab : c.toSimpleGraph.Adj a b
he : Fin.ofNat 2 (Nonempty.some ⋯).length = Fin.ofNat 2 (Nonempty.some ⋯).length
⊢ Odd (((Nonempty.some ⋯).concat hab).length + (Nonempty.some ⋯).reverse.length)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
v w : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).Adj v w ↔ v.1 ≠ w.1

Tactic:
by rfl

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v w : Fin r × Fin t
⊢ (SimpleGraph.turanGraph (r * t) r).Adj
      ({ toFun := fun v ↦ ⟨↑v.2 * r + ↑v.1, ⋯⟩, invFun := fun v ↦ (⟨↑v % r, ⋯⟩, ⟨↑v / r, ⋯⟩), left_inv := ⋯,
          right_inv := ⋯ }
        v)
      ({ toFun := fun v ↦ ⟨↑v.2 * r + ↑v.1, ⋯⟩, invFun := fun v ↦ (⟨↑v % r, ⋯⟩, ⟨↑v / r, ⋯⟩), left_inv := ⋯,
          right_inv := ⋯ }
        w) ↔
    (completeEquipartiteGraph r t).Adj v w

Tactic:
rw [turanGraph_adj, Equiv.coe_fn_mk, Nat.mul_add_mod_self_right, Nat.mod_eq_of_lt v.1.prop,
      Nat.mul_add_mod_self_right, Nat.mod_eq_of_lt w.1.prop, ← Fin.ext_iff.ne,
      ← completeEquipartiteGraph_adj]

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

Goal state before:
pp: case refine_1
r t : ℕ
x✝ : (completeEquipartiteGraph r t).edgeSet.Nonempty
e : Sym2 (Fin r × Fin t)
he : e ∈ (completeEquipartiteGraph r t).edgeSet
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)

pp: case refine_2
r t : ℕ
x✝ : Nontrivial (Fin r) ∧ Nonempty (Fin t)
i₁ i₂ : Fin r
hv : i₁ ≠ i₂
x : Fin t
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty

Tactic:
· induction e with | _ v₁ v₂
    rw [mem_edgeSet, completeEquipartiteGraph_adj] at he
    exact ⟨⟨v₁.1, v₂.1, he⟩, ⟨v₁.2⟩⟩

Goal state after:
case refine_2
r t : ℕ
x✝ : Nontrivial (Fin r) ∧ Nonempty (Fin t)
i₁ i₂ : Fin r
hv : i₁ ≠ i₂
x : Fin t
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty
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
z : Finset V
zc : #z = r
⊢ ∃ x ∈ ↑z, ∃ y ∈ ↑z, x ≠ y ∧ ¬G.Adj x y

Tactic:
simp_rw [h.not_adj_iff_part_eq]

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
z : Finset V
zc : #z = r
⊢ ∃ x ∈ ↑z, ∃ y ∈ ↑z, x ≠ y ∧ h.finpartition.part x = h.finpartition.part y
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
⊢ ∑ v, (r - 1) * t = 2 * (r.choose 2 * t ^ 2)

Tactic:
rw [sum_const, smul_eq_mul, card_univ, card_prod, Fintype.card_fin, Fintype.card_fin]

Goal state after:
r t : ℕ
⊢ r * t * ((r - 1) * t) = 2 * (r.choose 2 * t ^ 2)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑n * (↑n - 1) / 2 * ↑(#G.edgeFinset) ≤ ↑(n + 1) * (↑(n + 1) - 1) / 2 * ↑(extremalNumber n H)

Tactic:
Nat.cast_add_one,

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑n * (↑n - 1) / 2 * ↑(#G.edgeFinset) ≤ (↑n + 1) * (↑n + 1 - 1) / 2 * ↑(extremalNumber n H)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_1
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
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
⊢ ({G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
      #x.edgeFinset) ≤
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
simp_rw [Finset.sup_le_iff, mem_filter, mem_univ, true_and]

Goal state after:
case refine_1
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
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
⊢ ∀ (b : SimpleGraph (Fin m ⊕ Fin n)),
    b ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free b →
      #b.edgeFinset ≤
        {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_2
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
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
⊢ ({G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset) ≤
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
      #x.edgeFinset

Tactic:
simp_rw [Finset.sup_le_iff, mem_filter, mem_univ, true_and]

Goal state after:
case refine_2
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
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
⊢ ∀ (b : SimpleGraph (V ⊕ W)),
    b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b →
      #b.edgeFinset ≤
        {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
          #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : G.IsMatchingFree
⊢ ∃ Gmax, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ∃ M, M.IsPerfectMatching

Tactic:
← @not_forall_not _ Subgraph.IsPerfectMatching

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : G.IsMatchingFree
⊢ ∃ Gmax, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : G.IsMatchingFree
Gmax : SimpleGraph V
hGmax : G ≤ Gmax ∧ Maximal IsMatchingFree Gmax
⊢ ∃ Gmax, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching

Tactic:
exact ⟨Gmax, ⟨hGmax.1, ⟨hGmax.2.prop, fun _ h' ↦ hGmax.2.not_prop_of_gt h'⟩⟩⟩

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
x : V → ℝ
⊢ (((toLinearMap₂' ℝ) (lapMatrix ℝ G)) x) x = 0 ↔ ∀ (i j : V), G.Reachable i j → x i = x j

Tactic:
by
  rw [lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj]
  refine ⟨?_, fun h i j hA ↦ h i j hA.reachable⟩
  intro h i j ⟨w⟩
  induction w with
  | nil => rfl
  | cons hA _ h' => exact (h _ _ hA).trans h'

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : u ≠ v
hs : s(v, u) ∉ p.edges
c : (completeGraph V).Walk v v := cons ⋯ (Walk.mapLe ⋯ p)
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).IsCycles

Tactic:
have : p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe := by
    ext w x
    simp only [sup_adj, Subgraph.spanningCoe_adj, completeGraph_eq_top, edge_adj, c,
      Walk.toSubgraph, Subgraph.sup_adj, subgraphOfAdj_adj, adj_toSubgraph_mapLe]
    grind

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : u ≠ v
hs : s(v, u) ∉ p.edges
c : (completeGraph V).Walk v v := cons ⋯ (Walk.mapLe ⋯ p)
this : p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).IsCycles
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
⊢ G ≤ G

Tactic:
by rfl

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
⊢ h.toFinset.card ≤ Fintype.card (Fin n)

Tactic:
have : Fintype C.colorClasses := C.colorClasses_finite.fintype

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
this : Fintype ↑C.colorClasses
⊢ h.toFinset.card ≤ Fintype.card (Fin n)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
this : p.toSubgraph.verts = c.supp
⊢ ∃ p, p.IsCycle ∧ p.toSubgraph.verts = c.supp

Tactic:
use p.rotate v hvp

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
this : p.toSubgraph.verts = c.supp
⊢ (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = c.supp
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
⊢ (M.spanningCoe ∆ M'.spanningCoe).IsAlternating M'.spanningCoe

Tactic:
simpa [symmDiff_comm] using isAlternating_symmDiff_left hM' hM

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

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
h : (i, j) ∈ μ
x✝ : ℕ
hmj : x✝ ≤ j
⊢ i ≤ i

Tactic:
by rfl

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

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
h : ∀ m ≤ j, (i, m) ∈ μ
⊢ j ≤ j

Tactic:
by rfl

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

Goal state before:
pp: μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, μ.rowLen i1) ∈ μ
⊢ μ.rowLen i1 ≤ μ.rowLen i1

Tactic:
by rfl

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

Goal state before:
pp: μ : YoungDiagram
i✝ j1✝ j2✝ : ℕ
hj : j1✝ < j2✝
hcell : (i✝, j2✝) ∈ μ
⊢ i✝ ≤ i✝

Tactic:
by rfl

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

Goal state before:
pp: μ : YoungDiagram
i1✝ i2✝ j✝ : ℕ
hi : i1✝ < i2✝
hcell : (i2✝, j✝) ∈ μ
⊢ j✝ ≤ j✝

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
f : α → Fin n
this : Primcodable { a // a < n } := Primcodable.subtype ⋯
⊢ (Primrec fun a ↦ ↑(f a)) ↔ Primrec fun a ↦ ↑(Fin.equivSubtype (f a))

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Primrec (f i)
⊢ Primrec fun a ↦ List.ofFn fun i ↦ f i a

Tactic:
by
    simpa using list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case inr.inr
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)
h₁ : m ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (ack (max a b + 9) (m + n)) ≤ ack (max a b + 9) (m + (n + 1))

Tactic:
rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one,
            ack_succ_succ (_ + 8), add_assoc]

Goal state after:
case inr.inr
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)
h₁ : m ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n
⊢ ack (b + (4 + 4)) (ack (max a b + 8 + 1) (m + n)) ≤ ack (max a b + 8) (ack (max a b + 8 + 1) (m + n))