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

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℝ
⊢ schnirelmannDensity A < x ↔ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < x

Tactic:
by
  rw [← not_le, le_schnirelmannDensity_iff]; simp

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
c : α
hc : c ∈ u
habc : Disjoint a c ∧ Disjoint b c
⊢ ∃ a_1 ∈ s, ∃ b_1, (∃ a ∈ t, ∃ b ∈ u, Disjoint a b ∧ a ⊔ b = b_1) ∧ Disjoint a_1 b_1 ∧ a_1 ⊔ b_1 = a ⊔ b ⊔ c

Tactic:
exact ⟨a, ha, _, ⟨b, hb, c, hc, habc.2, rfl⟩, hab.sup_right habc.1, (sup_assoc ..).symm⟩

Goal state after:
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ ¬SupPrime a ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

Tactic:
SupPrime,

Goal state after:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ ¬(¬IsMin a ∧ ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
Module: Mathlib.Order.Irreducible

Goal state before:
pp: case empty
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : ∅.sup f = a
⊢ ∃ i ∈ ∅, f i = a

Tactic:
simpa [ha.ne_bot] using h.symm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
h : A ∈ ↑(∂⁺ 𝒜)
⊢ #A = r + 1

Tactic:
obtain ⟨A, hA, i, hi, rfl⟩ := mem_upShadow_iff.1 h

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∉ A
h : insert i A ∈ ↑(∂⁺ 𝒜)
⊢ #(insert i A) = r + 1
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ Fintype.finsetEquivSet.symm (birkhoffSet (a ⊓ b)) =
    Fintype.finsetEquivSet.symm (birkhoffSet a) ∩ Fintype.finsetEquivSet.symm (birkhoffSet b)

Tactic:
simp [birkhoffSet_inf]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ #𝒜.shatterer ≤ ∑ k ≤ 𝒜.vcDim, (Fintype.card α).choose k

Tactic:
by
  simp_rw [← card_univ, ← card_powersetCard]
  refine (card_le_card fun s hs ↦ mem_biUnion.2 ⟨#s, ?_⟩).trans card_biUnion_le
  exact ⟨mem_Iic.2 (mem_shatterer.1 hs).card_le_vcDim, mem_powersetCard_univ.2 rfl⟩

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

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
⊢ (G.connectedComponentMk v).supp ⊆ c'.supp

Tactic:
by
  intro v' hv'
  simp only [mem_supp_iff, ConnectedComponent.eq] at hv' ⊢
  rw [ConnectedComponent.sound (hv'.mono h)]
  exact hc'

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.IsBridge s(u, v)
⊢ G.Reachable u v ↔ G.Adj u v

Tactic:
refine ⟨fun hreach ↦ G.mem_edgeSet.mp ?_, Adj.reachable⟩
  have : G.deleteEdges {s(u, v)} < G := deleteEdges_le _ |>.lt_of_ne <| by grind [isBridge_iff]
  grind [edgeSet_strict_mono this, edgeSet_deleteEdges]

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n → ∃ C, ∀ (v : V), C v < n

Tactic:
rintro hc
    have C : G.Coloring (Fin n) := hc.toColoring (by simp)
    let f := Embedding.completeGraph (@Fin.valEmbedding n)
    use f.toHom.comp C
    intro v
    exact Fin.is_lt (C.1 v)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
hG : G.Colorable (card α)
⊢ G.chromaticNumber = ↑(card α) ↔ ∀ (C : G.Coloring α), Surjective ⇑C

Tactic:
by
  rw [← hG.chromaticNumber_le.ge_iff_eq, card_le_chromaticNumber_iff_forall_surjective]

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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk : k ≠ 0
h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
s : Set (Sym2 V)
hs : s.encard < ↑(k + 1)
⊢ (G.deleteEdges s).Reachable u v

Tactic:
obtain rfl | ⟨e, he⟩ := s.eq_empty_or_nonempty

Goal state after:
case refine_2.inl
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk : k ≠ 0
h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
hs : ∅.encard < ↑(k + 1)
⊢ (G.deleteEdges ∅).Reachable u v

case refine_2.inr
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk : k ≠ 0
h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
s : Set (Sym2 V)
hs : s.encard < ↑(k + 1)
e : Sym2 V
he : e ∈ s
⊢ (G.deleteEdges s).Reachable u v
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a : α
u : Finset α
hu : a ∉ u
ih :
  ∀ {f₁ f₂ f₃ f₄ : Finset α → β},
    0 ≤ f₁ →
      0 ≤ f₂ →
        0 ≤ f₃ →
          0 ≤ f₄ →
            (∀ ⦃s : Finset α⦄, s ⊆ u → ∀ ⦃t : Finset α⦄, t ⊆ u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) →
              ∀ {𝒜 ℬ : Finset (Finset α)},
                𝒜 ⊆ u.powerset →
                  ℬ ⊆ u.powerset → (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
f₁ f₂ f₃ f₄ : Finset α → β
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 α)
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hℬ : ℬ ⊆ (insert a u).powerset
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s

Tactic:
| insert a u hu ih =>

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
rw [← huv, hpc.neighborSet_toSubgraph_endpoint]

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ {p.snd, p.penultimate}.ncard = 2
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.penultimate
⊢ p.reverse.IsCycle ∧ p.reverse.snd = w ∧ p.reverse.toSubgraph.verts = p.toSubgraph.verts

Tactic:
penultimate,

Goal state after:
case h
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.getVert (p.length - 1)
⊢ p.reverse.IsCycle ∧ p.reverse.snd = w ∧ p.reverse.toSubgraph.verts = p.toSubgraph.verts
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
⊢ (⊤.induce s).coe.Preconnected ↔ (⊤.induce s).Preconnected

Tactic:
← Subgraph.preconnected_iff

Goal state after:
V : Type u
G : SimpleGraph V
s : Set V
⊢ (⊤.induce s).Preconnected ↔ (⊤.induce s).Preconnected
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: case mp
M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
h : ∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w
g : M
hg : g ∈ s
a : M
ha : ¬a * g = a
⊢ G.Adj (a * g) a

Tactic:
exact h (a * g) a ha g hg (Or.inr rfl)

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

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s ∨ v - u ∈ s
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
cases h1 with

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

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
⊢ u - v ∈ s ∨ v - u ∈ s

Tactic:
cases h1 with

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj v w
hsupp : w ∈ p.support
⊢ w = p.penultimate

Tactic:
← snd_reverse

Goal state after:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj v w
hsupp : w ∈ p.support
⊢ w = p.reverse.snd
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

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

Tactic:
← apply_ne_one_iff h,

Goal state after:
α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i j : V
⊢ ¬¬A i j = 1 ↔ A i j = 1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case refine_2
n r : ℕ
⊢ r = 0 ∨ n ≤ r → ∀ (x x_1 : Fin n), ↑x % r = ↑x_1 % r ↔ x = x_1

Tactic:
· rintro (rfl | h) a b
    · simp [Fin.val_inj]
    · rw [Nat.mod_eq_of_lt (a.2.trans_le h), Nat.mod_eq_of_lt (b.2.trans_le h), Fin.val_inj]

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

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
⊢ Nat.card V ≤ Nat.card ↑G.edgeSet + 1

Tactic:
have := Fintype.ofFinite

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
this : (α : Type ?u.21) → [Finite α] → Fintype α
⊢ Nat.card V ≤ Nat.card ↑G.edgeSet + 1
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case refine_1.h
r t : ℕ
x✝ : (completeEquipartiteGraph r t).edgeSet.Nonempty
v₁ v₂ : Fin r × Fin t
he : s(v₁, v₂) ∈ (completeEquipartiteGraph r t).edgeSet
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)

Tactic:
rw [mem_edgeSet, completeEquipartiteGraph_adj] at he

Goal state after:
case refine_1.h
r t : ℕ
x✝ : (completeEquipartiteGraph r t).edgeSet.Nonempty
v₁ v₂ : Fin r × Fin t
he : v₁.1 ≠ v₂.1
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
c : G.ConnectedComponent
⊢ Odd c.supp.ncard ∧ c.supp ⊆ c'.supp ↔ c.supp ⊆ c'.supp ∧ Odd {x | G.connectedComponentMk x = c}.ncard

Tactic:
supp,

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
c : G.ConnectedComponent
⊢ Odd {v | G.connectedComponentMk v = c}.ncard ∧
      {v | G.connectedComponentMk v = c} ⊆ {v | G'.connectedComponentMk v = c'} ↔
    {v | G.connectedComponentMk v = c} ⊆ {v | G'.connectedComponentMk v = c'} ∧
      Odd {v | G.connectedComponentMk v = c}.ncard
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
⊢ r * (r - 1) * (t * t) = r * (r - 1) * t ^ 2

Tactic:
← pow_two

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

Goal state before:
pp: case map_rel_iff'
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
⊢ ↑(zm ⟨a, ⋯⟩) % r ≠ ↑(zm ⟨b, ⋯⟩) % r ↔ G.Adj a b

Tactic:
rw [← not_iff_not, not_ne_iff, this, card_parts]

Goal state after:
case map_rel_iff'
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % min (Fintype.card V) r = ↑(zm ⟨b, ⋯⟩) % min (Fintype.card V) r
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case map_rel_iff'.inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : r ≤ Fintype.card V
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % min (Fintype.card V) r = ↑(zm ⟨b, ⋯⟩) % min (Fintype.card V) r

Tactic:
rw [min_eq_right c]; rfl

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

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
h✝ : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
w✝¹ w✝ : α
h : G.edist w✝¹ w✝ = G.ediam
⊢ G.edist w✝¹ w + G.edist w w✝ ≤ G.radius + G.radius

Tactic:
exact hw ▸ add_le_add (G.edist_comm ▸ G.edist_le_eccent) G.edist_le_eccent

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

Goal state before:
pp: case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ x✝ : V
w✝³ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝³, j), inj' := ⋯ } univ = x✝³
w✝² : Fin r
h₂ : map { toFun := fun j ↦ f (w✝², j), inj' := ⋯ } univ = x✝²
w✝¹ : Fin t
h₁' : f (w✝³, w✝¹) = x✝¹
w✝ : Fin t
h₂' : f (w✝², w✝) = x✝
⊢ (completeEquipartiteGraph r t).Adj (w✝³, w✝¹) (w✝², w✝)

Tactic:
simp_rw [completeEquipartiteGraph_adj]

Goal state after:
case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ x✝ : V
w✝³ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝³, j), inj' := ⋯ } univ = x✝³
w✝² : Fin r
h₂ : map { toFun := fun j ↦ f (w✝², j), inj' := ⋯ } univ = x✝²
w✝¹ : Fin t
h₁' : f (w✝³, w✝¹) = x✝¹
w✝ : Fin t
h₂' : f (w✝², w✝) = x✝
⊢ w✝³ ≠ w✝²
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_2.refine_1
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
⊢ s ∉ K.parts

Tactic:
intro hs_mem

Goal state after:
case neg.refine_2.refine_1
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
⊢ False
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:
rw [← Finset.card_pos, hs]

Goal state after:
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
⊢ 0 < t
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ hom h C = D ↔ ¬Disjoint ↑C ↑D

Tactic:
rw [Set.not_disjoint_iff]

Goal state after:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ hom h C = D ↔ ∃ x ∈ ↑C, x ∈ ↑D
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: case hn
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
⊢ n - 1 ≤ n + 1 - 2

Tactic:
Nat.reduceSubDiff,

Goal state after:
case hn
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
⊢ n - 1 ≤ n - 1
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ᶜ ∧ (v ∉ K.vertsᶜ ∨ ¬∀ p ∈ K.parts, ∃ s ∈ powersetCard t p, ∀ w ∈ s, G.Adj v w)
⊢ (between (↑K.verts) (↑K.verts)ᶜ G).degree v < #K.verts - t' + t

Tactic:
and_or_left,

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ᶜ ∧ v ∉ K.vertsᶜ ∨ v ∈ K.vertsᶜ ∧ ¬∀ p ∈ K.parts, ∃ s ∈ powersetCard t p, ∀ w ∈ s, G.Adj v w
⊢ (between (↑K.verts) (↑K.verts)ᶜ G).degree v < #K.verts - t' + t
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype V
h : M.IsPerfectMatching
⊢ Even (Fintype.card V)

Tactic:
by
  classical
  simpa only [h.2.card_verts] using IsMatching.even_card h.1

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
hM : M.IsPerfectMatching
c : ↑(⊤.deleteVerts u).coe.oddComponents
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ (↑c).supp
hMmatch : (M.induce (Subtype.val '' (↑c).supp)).IsMatching
this✝ : Fintype ↑(M.induce (Subtype.val '' (↑c).supp)).verts
this : Fintype ↑(↑c).supp
⊢ Even (↑c).supp.ncard

Tactic:
simpa [Finset.card_image_of_injective] using hMmatch.even_card

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

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(toLin' (lapMatrix ℝ G)).ker
a✝ : x ∈ ⊤
⊢ lapMatrix ℝ G *ᵥ ↑x = 0

Tactic:
← toLin'_apply,

Goal state after:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(toLin' (lapMatrix ℝ G)).ker
a✝ : x ∈ ⊤
⊢ (toLin' (lapMatrix ℝ G)) ↑x = 0
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:
simp only [IsTutteViolator, not_lt] at h

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
h : (⊤.deleteVerts G.universalVerts).coe.oddComponents.ncard ≤ G.universalVerts.ncard
⊢ (Subtype.val '' ?m.40).ncard ≤ (universalVerts ?m.39).ncard
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: 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
a b : G
r :
  (QuotientGroup.leftRel (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt.index)).subtype (↑ps pt.index).symmetries)) a b
⊢ a • ↑(↑ps pt.index) = b • ↑(↑ps pt.index)

Tactic:
by
      rw [QuotientGroup.leftRel_eq] at r
      rw [eq_comm, ← inv_smul_eq_iff, smul_smul, ← MulAction.mem_stabilizer_iff]
      exact SetLike.le_def.1 (Subgroup.map_subtype_le _) r

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

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
⊢ (∃ (_ : i < μ.colLen 0), j < μ.rowLen i) ↔ (i, j) ∈ μ

Tactic:
simpa [← mem_iff_lt_colLen, mem_iff_lt_rowLen] using j.zero_le.trans_lt

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

Goal state before:
pp: p : ℕ
⊢ unpaired (fun z n ↦ Nat.rec (id z) (fun y IH ↦ (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2.pred) n) p =
    unpaired (fun x1 x2 ↦ x1 - x2) p

Tactic:
by
    simp; induction p.unpair.2 <;> simp [*, Nat.sub_add_eq]

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

Goal state before:
pp: case ha
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih : ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑k - 1) * x₀) (2 ^ (-↑k) * x₀) → f z = 0
z : ℝ
hx :
  z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) →
    f z ∈ Set.Icc (c₁ * f (2 ^ (-↑k - 1) * x₀)) (c₂ * f (2 ^ (-↑k - 1) * x₀))
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
⊢ 1 ≤ 2

pp: case hmn
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih : ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑k - 1) * x₀) (2 ^ (-↑k) * x₀) → f z = 0
z : ℝ
hx :
  z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) →
    f z ∈ Set.Icc (c₁ * f (2 ^ (-↑k - 1) * x₀)) (c₂ * f (2 ^ (-↑k - 1) * x₀))
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
⊢ -↑k - 1 ≤ -↑k

Tactic:
· norm_num

Goal state after:
case hmn
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih : ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑k - 1) * x₀) (2 ^ (-↑k) * x₀) → f z = 0
z : ℝ
hx :
  z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) →
    f z ∈ Set.Icc (c₁ * f (2 ^ (-↑k - 1) * x₀)) (c₂ * f (2 ^ (-↑k - 1) * x₀))
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
⊢ -↑k - 1 ≤ -↑k
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 : α
b : ℕ
⊢ ∀ᶠ (a : ℕ) in atTop, b ≤ r i a

Tactic:
have := R.eventually_r_ge b

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b✝ : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b✝ r
i : α
b : ℕ
this : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑b ≤ ↑(r i n)
⊢ ∀ᶠ (a : ℕ) in atTop, b ≤ r i a