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

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
ha : a ∉ s
⊢ (a ⊔ v) \ u ∈ s

Tactic:
obtain h | ⟨-, b, hb, hba⟩ := h

Goal state after:
case inl
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
h : a ∈ s ∧ compress u v a ∈ s
⊢ (a ⊔ v) \ u ∈ s

case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
hba : compress u v b = a
⊢ (a ⊔ v) \ u ∈ s
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : compress u v b ∉ s
this : Disjoint u (u \ v)
⊢ u = ⊥

Tactic:
by rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this

Goal state after:
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a✝ b✝ a b : α
hab : a ≤ b
hba : b ≤ a
⊢ lift a = lift b

Tactic:
hab.antisymm hba

Goal state after:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a✝ b✝ a b : α
hab : a ≤ b
hba : b ≤ a
⊢ lift b = lift b
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a✝ b✝ a b : α
hab : b ≤ a
hba : a ≤ b
⊢ comp a = comp b

Tactic:
hab.antisymm hba

Goal state after:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a✝ b✝ a b : α
hab : b ≤ a
hba : a ≤ b
⊢ comp a = comp a
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: case h₂
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
⊢ 2 ^ #s * (#(Finset.memberSubfamily a (𝒜 ∩ ℬ)) + #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ)) =
    2 ^ #s * #(𝒜 ∩ ℬ)

Tactic:
← nonMemberSubfamily_inter,

Goal state after:
case h₂
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
⊢ 2 ^ #s * (#(Finset.memberSubfamily a (𝒜 ∩ ℬ)) + #(Finset.nonMemberSubfamily a (𝒜 ∩ ℬ))) = 2 ^ #s * #(𝒜 ∩ ℬ)
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ s

Tactic:
rw [h (Insert.insert b s) _ (subset_insert _ _)]

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ insert b s

α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ (insert b s).Intersecting
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝¹ : v \ u = v
this✝ : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
⊢ False

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝¹ : v \ u = v
this✝ : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
⊢ False

Tactic:
· obtain ⟨z, hz, hxy⟩ := huv w hwu
    apply m z (disjoint_right.1 hsv hz)
    have : insert w ((s ∪ v) \ u) ∈ 𝒜 := mem_of_mem_compression hw𝒜' ‹_› (aux huv)
    have : (insert w ((s ∪ v) \ u) ∪ erase u w) \ erase v z ∈ 𝒜 := by
      refine sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ((erase_subset _ _).trans ‹_›) ?_
      rw [← sdiff_erase (mem_union_left _ <| hus hwu)]
      exact disjoint_sdiff
    convert! this using 1
    rw [insert_union_comm, insert_erase ‹w ∈ u›,
      sdiff_union_of_subset (hus.trans subset_union_left),
      sdiff_erase (mem_union_right _ ‹z ∈ v›), union_sdiff_cancel_right hsv]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝¹ : v \ u = v
this✝ : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
⊢ False
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case intro.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
h𝒜 : 𝒜.Nonempty
⊢ IsInitSeg (∂ 𝒜) (r - 1)

Tactic:
obtain ⟨s, rfl, rfl⟩ := h₁.exists_initSeg h𝒜

Goal state after:
case intro.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : #s > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) #s
⊢ IsInitSeg (∂ (initSeg s)) (#s - 1)
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
· obtain ⟨u, hu, hsu⟩ := hs.2 ht
      rw [mem_nonMemberSubfamily] at hu
      refine ⟨_, hu.1, ?_⟩
      rwa [insert_inter_of_notMem hu.2, hsu, erase_eq_self]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
⊢ G.Reachable u v ∨ Gᶜ.Reachable u w

Tactic:
by
  refine or_iff_not_imp_left.mpr fun huv ↦ ?_
  by_cases huw : G.Reachable u w
  · have huv' := G.reachable_or_compl_adj .. |>.resolve_left huv
    have hvw' := G.reachable_or_compl_adj .. |>.resolve_left fun hvw ↦ huv <| huw.trans hvw.symm
    exact huv'.reachable.trans hvw'.reachable
  exact G.reachable_or_compl_adj .. |>.resolve_left huw |>.reachable

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.CliqueFree n

Tactic:
refine this.cliqueFree ?_

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.chromaticNumber.toNat < n
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
hh : G.degree u < k
⊢ False

Tactic:
← card_incidenceSet_eq_degree,

Goal state after:
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
hh : Fintype.card ↑(G.incidenceSet u) < k
⊢ False
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:
specialize ih (collapse_nonneg h₁) (collapse_nonneg h₂) (collapse_nonneg h₃)
      (collapse_nonneg h₄) (collapse_modular hu h₁ h₂ h₃ h₄ h 𝒜 ℬ) Subset.rfl Subset.rfl

Goal state after:
case insert
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a : α
u : Finset α
hu : a ∉ u
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 α)
ih :
  (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) * ∑ s ∈ u.powerset, collapse ℬ a f₂ s ≤
    (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s) * ∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hℬ : ℬ ⊆ (insert a u).powerset
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ Maximal Subgraph.Connected C.toSubgraph

Tactic:
refine C.ind fun v ↦ ⟨connected_toSubgraph _, fun G' hconn hle ↦ ?_⟩

Goal state after:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
G' : G.Subgraph
hconn : G'.Connected
hle : (G.connectedComponentMk v).toSubgraph ≤ G'
⊢ G' ≤ (G.connectedComponentMk v).toSubgraph
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.toSubgraph.IsInduced ↔ w.IsChordless

Tactic:
Subgraph.IsInduced,

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ (∀ ⦃v_1 : V⦄,
      v_1 ∈ w.toSubgraph.verts → ∀ ⦃w_1 : V⦄, w_1 ∈ w.toSubgraph.verts → G.Adj v_1 w_1 → w.toSubgraph.Adj v_1 w_1) ↔
    w.IsChordless
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h✝ : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
this : s.encard + t.encard ≤ ENat.card V
⊢ 4 * (s.encard * t.encard) ≤ ENat.card V ^ 2

Tactic:
rw [ENat.card_eq_coe_natCard, ← s.toFinite.cast_ncard_eq, ← t.toFinite.cast_ncard_eq] at this ⊢

Goal state after:
V : Type u_1
G : SimpleGraph V
h✝ : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
this : ↑s.ncard + ↑t.ncard ≤ ↑(Nat.card V)
⊢ 4 * (↑s.ncard * ↑t.ncard) ≤ ↑(Nat.card V) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Metric

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

Tactic:
use hn, this

Goal state after:
case right
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
hn : u ≠ v
this : ¬G.Adj u v
⊢ G.commonNeighbors u v = ∅
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
⊢ w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    (Or.by_cases x (fun hG ↦ cons ⋯ w'.ofBoxProdLeft) fun hH ↦ ⋯ ▸ w'.ofBoxProdLeft).length +
      (⋯.by_cases (fun hH ↦ cons ⋯ w'.ofBoxProdRight) fun hG ↦ ⋯ ▸ w'.ofBoxProdRight).length

pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₂ : H.Adj b₁ c.2 ∧ a₁ = c.1
⊢ w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    (Or.by_cases x (fun hG ↦ cons ⋯ w'.ofBoxProdLeft) fun hH ↦ ⋯ ▸ w'.ofBoxProdLeft).length +
      (⋯.by_cases (fun hH ↦ cons ⋯ w'.ofBoxProdRight) fun hG ↦ ⋯ ▸ w'.ofBoxProdRight).length

Tactic:
· simp only [h₁, and_self, ↓reduceDIte, length_cons, Or.by_cases]
      rw [add_comm, add_comm w'.ofBoxProdLeft.length 1, add_assoc]
      congr <;> simp [h₁.2.symm]

Goal state after:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₂ : H.Adj b₁ c.2 ∧ a₁ = c.1
⊢ w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    (Or.by_cases x (fun hG ↦ cons ⋯ w'.ofBoxProdLeft) fun hH ↦ ⋯ ▸ w'.ofBoxProdLeft).length +
      (⋯.by_cases (fun hH ↦ cons ⋯ w'.ofBoxProdRight) fun hG ↦ ⋯ ▸ w'.ofBoxProdRight).length
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G.neighborFinset x.1).card * 1 + 1 * (H.neighborFinset x.2).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card

Tactic:
mul_one,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G.neighborFinset x.1).card + 1 * (H.neighborFinset x.2).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : (G □ H).edist x y = ⊤
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

pp: case neg
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
· rw [top_case] at h
    aesop

Goal state after:
case neg
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
v : V
hv : v ∈ s
sv : Set V
svs : sv ⊆ s
hu' : u ∈ sv
hv' : v ∈ sv
uv : (induce sv G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
⊢ (induce s G).Reachable ⟨u, hu⟩ ⟨v, hv⟩

Tactic:
exact uv.map (induceHomOfLE _ svs).toHom

Goal state after:
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 = 1 ↔ A i j = 0

Tactic:
obtain h | h := h.zero_or_one i j

Goal state after:
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

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
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
⊢ Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) T ↔ T.IsTree

Tactic:
have := hG.nonempty
  refine ⟨fun h ↦ ⟨⟨fun u v ↦ ?_⟩, h.1.2⟩, fun hT' ↦ ?_⟩
  · exact G.reachable_eq_of_maximal_isAcyclic T h ▸ hG.preconnected u v
  · rw [maximal_isAcyclic_iff_reachable_eq hT hT'.isAcyclic,
      T.preconnected_iff_reachable_eq_top.mp hT'.preconnected,
      G.preconnected_iff_reachable_eq_top.mp hG.preconnected]

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

Goal state before:
pp: case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
⊢ ¬↑u % 2 = ↑v % 2

Tactic:
cases hadj with
        | inl huv =>
          rw [← add_eq_of_eq_sub' huv.symm]
          simp only [Fin.val_add_eq_of_add_lt hv', Fin.val_add_eq_of_add_lt hu', Fin.val_one]
          rw [show ∀ x y : ℕ, x % 2 = y % 2 ↔ (Even x ↔ Even y) by simp [Nat.even_iff]; lia,
            Nat.even_add]
          simp only [Nat.not_even_one, iff_false, not_iff_self, iff_not_self]
          exact id

| inr huv =>
          rw [← add_eq_of_eq_sub' huv.symm]
          simp only [Fin.val_add_eq_of_add_lt hv', Fin.val_add_eq_of_add_lt hu', Fin.val_one]
          rw [show ∀ x y : ℕ, x % 2 = y % 2 ↔ (Even x ↔ Even y) by simp [Nat.even_iff]; lia,
            Nat.even_add]
          simp only [Nat.not_even_one, iff_false, not_iff_self, iff_not_self]
          exact id

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

Goal state before:
pp: α : 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
⊢ ↑↑(Nonempty.some ⋯).length = ↑↑(Nonempty.some ⋯).length

Tactic:
← Fin.ofNat_eq_cast,

Goal state after:
α : 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
⊢ ↑(Fin.ofNat 2 (Nonempty.some ⋯).length) = ↑(Fin.ofNat 2 (Nonempty.some ⋯).length)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1

Tactic:
by
    rw [← card_filter, ← this]; apply Nat.eq_sub_of_add_eq'
    rw [card_filter_add_card_filter_not, card_range]

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

Goal state before:
pp: case mpr
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
⊢ G.eccent u ≤ 1

Tactic:
rw [eccent_le_iff]

Goal state after:
case mpr
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
⊢ ∀ (v : α), G.edist u v ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.ediam ≠ 0

Tactic:
by
  obtain ⟨u, v, huv⟩ := exists_pair_ne ‹_›
  contrapose huv
  simp only [ediam, eccent, ENat.iSup_eq_zero, edist_eq_zero_iff] at huv
  exact huv u v

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

Goal state before:
pp: case inr
α : Type u_1
G : SimpleGraph α
h✝ : Nonempty α
⊢ G.ediam ≤ 2 * G.radius

Tactic:
by_cases hdiam : G.ediam = ⊤
    · simp [hdiam, ediam_eq_top_iff_radius_eq_top.mp hdiam]
    · obtain ⟨w, hw⟩ := G.exists_eccent_eq_radius
      obtain ⟨_, _, h⟩ := G.exists_edist_eq_ediam_of_ne_top hdiam
      apply le_trans (h ▸ G.edist_triangle (v := w))
      rw [two_mul]
      exact hw ▸ add_le_add (G.edist_comm ▸ G.edist_le_eccent) G.edist_le_eccent

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K✝ L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
⊢ Finite (G.ComponentCompl ↑K)

Tactic:
rcases K.eq_empty_or_nonempty with rfl | h

Goal state after:
case inl
V : Type u
G : SimpleGraph V
K L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
⊢ Finite (G.ComponentCompl ↑∅)

case inr
V : Type u
G : SimpleGraph V
K✝ L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
h : K.Nonempty
⊢ Finite (G.ComponentCompl ↑K)
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
⊢ ↑(#G.edgeFinset) ≤ ↑((n + 1).choose 2) * ↑(extremalNumber n H) / ↑(n.choose 2)

Tactic:
le_div_iff₀' (mod_cast Nat.choose_pos hn),

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.choose 2) * ↑(#G.edgeFinset) ≤ ↑((n + 1).choose 2) * ↑(extremalNumber n H)
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
⊢ ∀ b ∈ G.edgeFinset, n - 1 ≤ ↑(#(bipartiteBelow (fun v e ↦ v ∉ e) univ b))

Tactic:
intro e he
    simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]

Goal state after: