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

Goal state before:
pp: case pos
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : u = v
⊢ ⊤.dist u v = if u = v then 0 else 1

Tactic:
simp [h]

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

Goal state before:
pp: case neg
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : ¬u = v
⊢ ⊤.dist u v = if u = v then 0 else 1

Tactic:
simp [h]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
hh : G.dist u' v' < p₂.length
ru : G.Walk u u'
rv : G.Walk v' v
h : p₁ = (ru.append p₂).append rv
s : G.Walk u' v'
h✝ : s.IsPath ∧ s.length = G.dist u' v'
r : G.Walk u v := (ru.append s).append rv
⊢ p₁.length = ru.length + p₂.length + rv.length

Tactic:
simp [h]

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
p : H.coe.Walk ⟨u, hu⟩ ⟨v, hv⟩
⊢ (Walk.map H.hom p).toSubgraph ≤ H

Tactic:
simp [coeSubgraph_le]

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

Goal state before:
pp: V : Type u_3
G : SimpleGraph V
u v : V
w : G.Walk u v
hw : w.IsPath
⊢ pathGraph (w.length + 1) ⊑ G

Tactic:
classical
  exact ⟨hw.pathGraphCopy⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
v : V
⊢ Finset (G.Walk v v)

Tactic:
(Tactic.exact
 "exact"
 (choice
  («term{_}» "{" [`Walk.nil] "}")
  (Term.structInst
   "{"
   []
   (Term.structInstFields [(Term.structInstField (Term.structInstLVal `Walk.nil []) [])])
   (Term.optEllipsis [])
   []
   "}")))

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

Goal state before:
pp: V✝ : Type u_1
G✝ : SimpleGraph V✝
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
hle : x > y
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
rcases cycleGraph_adj'.mp hab with hab | hab

Goal state after:
case inl
V✝ : Type u_1
G✝ : SimpleGraph V✝
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab✝ : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
hle : x > y
hab : ↑(⟨x, hx⟩ - ⟨y, hy⟩) = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

case inr
V✝ : Type u_1
G✝ : SimpleGraph V✝
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab✝ : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
hle : x > y
hab : ↑(⟨y, hy⟩ - ⟨x, hx⟩) = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case refine_2.refine_3
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
hlen : p.tail.support.length = n
this✝ : ∀ (m : Fin n), p.support[m.succ] = p.tail.support[m]
this : p.tail.IsPath
⊢ Function.Injective ⇑{ toFun := fun n_1 ↦ p.tail.support[n_1], map_rel' := ⋯ }

Tactic:
exact hlen ▸ (isPath_iff_injective_get_support _ |>.mp this)

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

Goal state before:
pp: case inl
α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
i j : V
h : A i j = 0
⊢ ¬A i j = 1 ↔ A i j = 0

Tactic:
simp [h]

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

Goal state before:
pp: case inr
α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
i j : V
h : A i j = 1
⊢ ¬A i j = 1 ↔ A i j = 0

Tactic:
simp [h]

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

Goal state before:
pp: case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
h' : SimpleGraph.map (⇑e) G ∈ {x | H.Free x}
⊢ #G.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
Iso.card_edgeFinset_eq (.map e G)

Goal state after:
case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
h' : SimpleGraph.map (⇑e) G ∈ {x | H.Free x}
⊢ #(SimpleGraph.map (⇑e) G).edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
h' : SimpleGraph.map (⇑e) G ∈ {x | H.Free x}
⊢ #G.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
Iso.card_edgeFinset_eq (.map e G)

Goal state after:
case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
h' : SimpleGraph.map (⇑e) G ∈ {x | H.Free x}
⊢ #(SimpleGraph.map (⇑e) G).edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
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 α
h : A.IsSymm
⊢ A.compl.IsSymm

Tactic:
simp [h]

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

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

Tactic:
by simpa using ha

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
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
h3 : (f a).tail.length + 1 = (f b).length + 1
⊢ a ≠ default

Tactic:
by simpa using ha

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x y : V
⊢ (⨆ k, C.labelGraph k).Adj x y ↔ G.Adj x y

Tactic:
simp only [iSup_adj, EdgeLabeling.labelGraph_adj]

Goal state after:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x y : V
⊢ (∃ i, ∃ (H : G.Adj x y), C ⟨s(x, y), H⟩ = i) ↔ G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
n : ℕ
hn : n ≥ 3
hle : cycleGraph n ⊑ G
v : V
p : G.Walk v v
hcyc : p.IsCycle
hlen : p.length = n
⊢ False

Tactic:
exact h p hcyc

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

Goal state before:
pp: r t : ℕ
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty ↔ Nontrivial (Fin r) ∧ t ≠ 0

Tactic:
← Nat.pos_iff_ne_zero,

Goal state after:
r t : ℕ
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty ↔ Nontrivial (Fin r) ∧ 0 < t
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:
simp [ht]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ (s ∩ c.supp).ncard = 1

Tactic:
rw [Set.ncard_eq_one]

Goal state after:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ ∃ a, s ∩ c.supp = {a}
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : G.diam = 0
⊢ ∃ u v, G.dist u v = G.diam

Tactic:
simp [h]

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

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
u : α
hu : u ∈ Set.univ
⊢ e = G.radius

Tactic:
exact le_antisymm (le_iInf fun u ↦ (h u).ge) ((h Classical.ofNonempty) ▸ radius_le_eccent)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
⊢ #K.parts + 1 = #K'.parts

Tactic:
rw [K.card_parts.resolve_right ht, K'.card_parts.resolve_right ht]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
hs_mem : s ∈ K.parts
⊢ s.Nonempty

Tactic:
by
          rw [← Finset.card_pos, hs]
          exact Nat.pos_of_ne_zero ht

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

Goal state before:
pp: n r : ℕ
⊢ n ^ 2 * (r - 1) + 2 * r * (n % r).choose 2 - (n % r) ^ 2 * (r - 1) ≤ (r - 1) * n ^ 2

pp: n r : ℕ
⊢ (n % r) ^ 2 * (r - 1) ≤ n ^ 2 * (r - 1)

Tactic:
swap

Goal state after:
n r : ℕ
⊢ (n % r) ^ 2 * (r - 1) ≤ n ^ 2 * (r - 1)

n r : ℕ
⊢ n ^ 2 * (r - 1) + 2 * r * (n % r).choose 2 - (n % r) ^ 2 * (r - 1) ≤ (r - 1) * n ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v : V
⊢ v ∈ (↑(Opposite.unop (Opposite.op (singletonFinsubgraph v)))).verts

Tactic:
by
          unfold singletonFinsubgraph
          simp

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.IsAcyclic
⊢ G.girth = 0

Tactic:
simp [girth, h]

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

Goal state before:
pp: case pos
α : Type u_1
s : Set α
hs : s.Infinite
h : 1 = 0
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = 0

Tactic:
simp [h]

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

Goal state before:
pp: m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ ∀ (b : SimpleGraph (Fin m ⊕ Fin n)),
    b ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free b →
      #b.edgeFinset ≤ extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)

Tactic:
intro B

Goal state after:
m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
B : SimpleGraph (Fin m ⊕ Fin n)
⊢ B ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free B →
    #B.edgeFinset ≤ extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
have := h.to_subtype
  obtain ⟨f⟩ : Nonempty (s ≃ s ⊕ s) := by
    rw [← Cardinal.eq, ← add_def, add_mk_eq_self]
  refine ⟨Subtype.val '' f ⁻¹' (range .inl), Subtype.val '' f ⁻¹' (range .inr), ?_, ?_, ?_⟩
  · simp [← image_union, ← preimage_union]
  · exact disjoint_image_of_injective Subtype.val_injective
      (isCompl_range_inl_range_inr.disjoint.preimage f)
  · simp [mk_image_eq Subtype.val_injective]

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
⊢ (Subgraph.map (Hom.ofLE hGG') M).IsMatching

Tactic:
intro _ hv

Goal state after:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
hv : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
⊢ ∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

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

Tactic:
intro _ hv

Goal state after:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
hv : v✝ ∈ (G.subgraphOfAdj h).verts
⊢ ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
⊢ (Subgraph.coeSubgraph M).IsMatching

Tactic:
intro _ hv

Goal state after:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
⊢ ∃! w, (Subgraph.coeSubgraph M).Adj v✝ w
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a v : α
p : G.Walk a a
hv : v ∈ p.support
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle

Tactic:
cases (finite_or_infinite α).symm
  · simp
  cases nonempty_fintype α
  simp [isHamiltonianCycle_iff_isCycle_and_length_eq]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
c : G.ConnectedComponent
⊢ (M.induce (M.verts ∩ c.supp)).IsMatching

Tactic:
intro _ hv

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
c : G.ConnectedComponent
v✝ : V
hv : v✝ ∈ (M.induce (M.verts ∩ c.supp)).verts
⊢ ∃! w, (M.induce (M.verts ∩ c.supp)).Adj v✝ w
Module: Mathlib.Combinatorics.SimpleGraph.Star

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
r v : V
h : v ≠ r
⊢ (fun w ↦ (starGraph r).Adj v w) r

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
x✝ : α
hx : x✝ ∈ X
h : #({z ∈ W | ¬G.Adj x✝ z}) < 3
⊢ ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x✝ y

Tactic:
by simpa [X] using hx

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsVertexCover Set.univ

Tactic:
by
  simp [IsVertexCover]

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

Goal state before:
pp: V : Type u_1
c : Set V
⊢ ⊥.IsVertexCover c

Tactic:
by
  simp [IsVertexCover]

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
hM2 : M2.IsMatching
⊢ Disjoint M1.support M2.support

Tactic:
hM1.2.support_eq_verts,

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
hM2 : M2.IsMatching
⊢ Disjoint M1.verts M2.support
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
x✝¹ x✝ : ℕ × ℕ
h : x✝ ≤ x✝¹
hcell : (Equiv.prodComm ℕ ℕ).symm x✝¹ ∈ μ.cells
⊢ (Equiv.prodComm ℕ ℕ).symm x✝ ≤ (Equiv.prodComm ℕ ℕ).symm x✝¹

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_2
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
x✝ : pt₁.index = pt₂.index ∧ ∃ g, ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts
h : pt₁.index = pt₂.index
g : G
hg₁ : ⟦g⟧ = pt₁.groupElts
hg₂ : ⟦g⟧ = pt₂.groupElts
⊢ pt₁ = pt₂

Tactic:
rcases pt₁ with ⟨i₁, g₁⟩

Goal state after:
case refine_2
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₂ : PlacedTile ps
g : G
hg₂ : ⟦g⟧ = pt₂.groupElts
i₁ : ιₚ
g₁ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
x✝ :
  { index := i₁, groupElts := g₁ }.index = pt₂.index ∧
    ∃ g, ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = pt₂.groupElts
h : { index := i₁, groupElts := g₁ }.index = pt₂.index
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
⊢ { index := i₁, groupElts := g₁ } = pt₂
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_2
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
x✝ :
  pt₁.index = pt₂.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
        {pt₂.groupElts}
hi : pt₁.index = pt₂.index
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
      {pt₁.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
      {pt₂.groupElts}
⊢ pt₁ = pt₂

Tactic:
rcases pt₁ with ⟨i₁, g₁⟩

Goal state after:
case refine_2
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₂ : PlacedTile ps
i₁ : ιₚ
g₁ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
x✝ :
  { index := i₁, groupElts := g₁ }.index = pt₂.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
              (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₁ }.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
        {pt₂.groupElts}
hi : { index := i₁, groupElts := g₁ }.index = pt₂.index
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
            (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₁ }.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
      {pt₂.groupElts}
⊢ { index := i₁, groupElts := g₁ } = pt₂
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
h1 : (i2, j2).1 < w.length
h2 : (i2, j2).2 < w[(i2, j2).1]
⊢ ∃ (h : (i1, j1).1 < w.length), (i1, j1).2 < w[(i1, j1).1]

Tactic:
refine ⟨hi.trans_lt h1, ?_⟩

Goal state after:
w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
h1 : (i2, j2).1 < w.length
h2 : (i2, j2).2 < w[(i2, j2).1]
⊢ (i1, j1).2 < w[(i1, j1).1]
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: n : ℕ
⊢ (id n % 2 == 1) = n.bodd

Tactic:
cases H : n.bodd <;> simp [Nat.mod_two_of_bodd, H]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n ↦ (decode n).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a
n : ℕ
a : α
h : p a
⊢ encode (if decide (p a) = true then some a else none) = encode (if h : p a then some ⟨a, h⟩ else none)

Tactic:
simp [h]

Goal state after:
case pos
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n ↦ (decode n).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a
n : ℕ
a : α
h : p a
⊢ encode a = encode ⟨a, ⋯⟩
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n ↦ (decode n).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a
n : ℕ
a : α
h : ¬p a
⊢ encode (if decide (p a) = true then some a else none) = encode (if h : p a then some ⟨a, h⟩ else none)

Tactic:
simp [h]

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

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

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

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case comp
f f✝ g✝ : ℕ → ℕ
hf : Nat.Primrec f✝
hg : Nat.Primrec g✝
IHf : ∃ m, ∀ (n : ℕ), f✝ n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g✝ n < ack m n
⊢ ∃ m, ∀ (n : ℕ), (fun n ↦ f✝ (g✝ n)) n < ack m n

Tactic:
| comp hf hg IHf IHg =>

Goal state after: