mathlib-initiative/mathlib-tactics huggingface dataset:
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 : SimpleGraph (Fin m ⊕ Fin n)
h_le : G ≤ completeBipartiteGraph (Fin m) (Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
h' : SimpleGraph.map (⇑e₁.toEmbedding) G ∈ {G | G ≤ completeBipartiteGraph V W ∧ K.Free G}
⊢ #(SimpleGraph.map (⇑e₁.toEquiv) G).edgeFinset ≤
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
have h_le_sup := @le_sup _ _ _ _ _ (#·.edgeFinset) (G.map e₁.toEquiv.toEmbedding) h'

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
G : SimpleGraph (Fin m ⊕ Fin n)
h_le : G ≤ completeBipartiteGraph (Fin m) (Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
h' : SimpleGraph.map (⇑e₁.toEmbedding) G ∈ {G | G ≤ completeBipartiteGraph V W ∧ K.Free G}
h_le_sup :
  #(SimpleGraph.map (⇑e₁.toEmbedding) G).edgeFinset ≤
    {G | G ≤ completeBipartiteGraph V W ∧ K.Free G}.sup fun x ↦ #x.edgeFinset
⊢ #(SimpleGraph.map (⇑e₁.toEquiv) G).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 : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
h' : SimpleGraph.map (⇑e₁.toEmbedding) G ∈ {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ K.Free G}
⊢ #(SimpleGraph.map (⇑e₁.toEquiv) G).edgeFinset ≤
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
      #x.edgeFinset

Tactic:
have h_le_sup := @le_sup _ _ _ _ _ (#·.edgeFinset) (G.map e₁.toEquiv.toEmbedding) h'

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)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
h' : SimpleGraph.map (⇑e₁.toEmbedding) G ∈ {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ K.Free G}
h_le_sup :
  #(SimpleGraph.map (⇑e₁.toEmbedding) G).edgeFinset ≤
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ K.Free G}.sup fun x ↦ #x.edgeFinset
⊢ #(SimpleGraph.map (⇑e₁.toEquiv) G).edgeFinset ≤
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
      #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

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

Tactic:
simp_rw [zarankiewicz_of_fintypeCard_eq hm hn hs ht,
    Finset.lt_sup_iff, mem_filter, mem_univ, true_and]

Goal state after:
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
x : ℕ
⊢ (∃ b, (b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b) ∧ x < #b.edgeFinset) ↔
    ∃ G x_1, G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ x < #G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
h : G ⊑ G'
⊢ G'.egirth ≤ G.egirth

Tactic:
by_cases hacyc : G.IsAcyclic

Goal state after:
case pos
α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
h : G ⊑ G'
hacyc : G.IsAcyclic
⊢ G'.egirth ≤ G.egirth

case neg
α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
h : G ⊑ G'
hacyc : ¬G.IsAcyclic
⊢ G'.egirth ≤ G.egirth
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).ncard = ∑ᶠ (i : ι), (s i).ncard

Tactic:
rw [← finsum_mem_univ, ← finite_univ.ncard_biUnion (by simpa) (fun _ _ _ _ hab ↦ h hab)]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).ncard = (⋃ i ∈ univ, s i).ncard
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
x 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
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hf : c = a → d ≠ b
⊢ False

Tactic:
apply h2.not_gt <| two_lt_card_iff.2 _

Goal state after:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x 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
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := ⋯
hf : c = a → d ≠ b
⊢ ∃ a b c,
    a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
      b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
        c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : MulZeroOneClass R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬G.Adj a b
⊢ (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 e = 0

Tactic:
Set.indicator_of_notMem

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : MulZeroOneClass R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬G.Adj a b
⊢ 0 = 0

case h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : MulZeroOneClass R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬G.Adj a b
⊢ e ∉ G.incidenceSet a ∩ G.incidenceSet b
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
⊢ M.support = M.verts

Tactic:
refine M.support_subset_verts.antisymm fun v hv => ?_
  obtain ⟨w, hvw, -⟩ := h hv
  exact ⟨_, hvw⟩

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : NonAssocSemiring R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ ∑ a_1, incMatrix R G a_1 s(a, b) = 2

Tactic:
rw [← Nat.cast_two, ← card_pair h.ne]

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : NonAssocSemiring R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ ∑ a_1, incMatrix R G a_1 s(a, b) = ↑(#{a, b})
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
⊢ Even (Fintype.card ↑c.supp)

Tactic:
#adaptation_note /-- https://github.com/leanprover/lean4/pull/5020
  some instances that use the chain of coercions
  `[SetLike X], X → Set α → Sort _` are
  blocked by the discrimination tree. This can be fixed by redeclaring the instance for `X`
  using the double coercion but the proper fix seems to avoid the double coercion. -/
  let : DecidablePred fun x ↦ x ∈ (M.induce c.supp).verts := fun a ↦ G.instDecidableMemSupp c a
  have := (hM.induce_connectedComponent_isMatching c).even_card
  simp only [Subgraph.induce_verts, Set.toFinset_card] at this
  exact this

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w w' : V
⊢ w ≠ w' → H.spanningCoe.Adj v w → H.spanningCoe.Adj v w' → (G'.Adj v w ↔ ¬G'.Adj v w')

Tactic:
hww'

Goal state after:
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w w' : V
hww' : w ≠ w'
⊢ H.spanningCoe.Adj v w → H.spanningCoe.Adj v w' → (G'.Adj v w ↔ ¬G'.Adj v w')
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case neg
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
⊢ w ≠ w' → (G ⊔ edge u x).Adj v w → (G ⊔ edge u x).Adj v w' → (G'.Adj v w ↔ ¬G'.Adj v w')

Tactic:
hww'

Goal state after:
case neg
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
⊢ (G ⊔ edge u x).Adj v w → (G ⊔ edge u x).Adj v w' → (G'.Adj v w ↔ ¬G'.Adj v w')
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
v w w' : V
⊢ w ≠ w' →
    (M.spanningCoe ∆ M'.spanningCoe).Adj v w →
      (M.spanningCoe ∆ M'.spanningCoe).Adj v w' → (M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w')

Tactic:
hww'

Goal state after:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w w' : V
hww' : w ≠ w'
⊢ (M.spanningCoe ∆ M'.spanningCoe).Adj v w →
    (M.spanningCoe ∆ M'.spanningCoe).Adj v w' → (M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w')
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)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
⊢ G.minDegree * ∑ x ∈ W, 1 + G.minDegree * 2 * ∑ x ∈ s ∩ t, 1 ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w

Tactic:
mul_sum,

Goal state after:
α : 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)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
⊢ ∑ i ∈ W, G.minDegree * 1 + ∑ i ∈ s ∩ t, G.minDegree * 2 * 1 ≤ ∑ w ∈ W, G.degree w + ∑ i ∈ s ∩ t, 2 * G.degree i
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
⊢ (Subtype.val '' ?m.40).ncard ≤ (universalVerts ?m.39).ncard

Tactic:
by
        simp only [IsTutteViolator, not_lt] at h
        rwa [Set.ncard_image_of_injective _ Subtype.val_injective, hrep.ncard_eq]

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
⊢ ∃ M, M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts

Tactic:
have exists_complMatch (K : G.deleteUniversalVerts.coe.ConnectedComponent) :
      ∃ M : Subgraph G, M.verts = Subtype.val '' K.supp \ M1.verts ∧ M.IsMatching := by
    have : G.IsClique (Subtype.val '' K.supp \ M1.verts) :=
      ((h' K).of_induce).subset Set.sdiff_subset
    rw [← this.even_iff_exists_isMatching (Set.toFinite _), hM1.1]
    exact even_ncard_image_val_supp_sdiff_image_val_rep_union _ ht hrep

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
exists_complMatch :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), ∃ M, M.verts = Subtype.val '' K.supp \ M1.verts ∧ M.IsMatching
⊢ ∃ M, M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode (decode n) = encode (decode n)

Tactic:
by
      rw [decode_ofEquiv]
      cases (@decode α _ n) <;>
        simp [encode_ofEquiv]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ encode
      (List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
        (ofNat (List ℕ) n).reverse) =
    encode (decode n)

Tactic:
List.foldl_reverse

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ encode
      (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) n)) =
    encode (decode n)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case cons
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b✝ : β
i : ℕ
hi : i ≤ m b✝ + 1
bindList_eq_nil : bindList b✝ (m b✝ + 1) = []
bs : List β
b : β
bs' : List β
ih : bs' ⊆ bs → mapGraph (List.map (fun x ↦ (x, f x)) bs) bs' = List.map f bs'
has : b :: bs' ⊆ bs
⊢ (List.lookup b (List.map (fun x ↦ (x, f x)) bs)).toList ++
      List.flatMap (fun x ↦ (List.lookup x (List.map (fun x ↦ (x, f x)) bs)).toList) bs' =
    f b :: List.map f bs'

Tactic:
have : b ∈ bs ∧ bs' ⊆ bs := by simpa using has

Goal state after:
case cons
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝¹ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this✝ : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b✝ : β
i : ℕ
hi : i ≤ m b✝ + 1
bindList_eq_nil : bindList b✝ (m b✝ + 1) = []
bs : List β
b : β
bs' : List β
ih : bs' ⊆ bs → mapGraph (List.map (fun x ↦ (x, f x)) bs) bs' = List.map f bs'
has : b :: bs' ⊆ bs
this : b ∈ bs ∧ bs' ⊆ bs
⊢ (List.lookup b (List.map (fun x ↦ (x, f x)) bs)).toList ++
      List.flatMap (fun x ↦ (List.lookup x (List.map (fun x ↦ (x, f x)) bs)).toList) bs' =
    f b :: List.map f bs'
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
⊢ False

Tactic:
Fintype.card_eq_nat_card

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Nat.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
⊢ False
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 + ε ↑n

Tactic:
by
  filter_upwards [eventually_one_add_smoothingFn_pos] with n hn; exact le_of_lt hn

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

Goal state before:
pp: case hbc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := ⋯
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ (b i)⁻¹ ≤ ↑⌈(b i)⁻¹⌉₊

Tactic:
exact Nat.le_ceil _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ (fun n ↦ -log (b i) * (1 / log ↑n ^ 2)) =Θ[atTop] fun n ↦ 1 / log ↑n ^ 2

Tactic:
have : -log (b i) ≠ 0 := by
        rw [neg_ne_zero]
        exact Real.log_ne_zero_of_pos_of_ne_one (R.b_pos i) (ne_of_lt <| R.b_lt_one i)

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
this : -log (b i) ≠ 0
⊢ (fun n ↦ -log (b i) * (1 / log ↑n ^ 2)) =Θ[atTop] fun n ↦ 1 / log ↑n ^ 2