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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ #∅ ≤ #∅.shatterer

pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ #{∅} ≤ #{∅}.shatterer

pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
    #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer →
      #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer → #𝒜 ≤ #𝒜.shatterer

Tactic:
· simp

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ #{∅} ≤ #{∅}.shatterer

case refine_3
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
    #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer →
      #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer → #𝒜 ≤ #𝒜.shatterer
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3
α : 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)
⊢ Disjoint ((memberSubfamily a 𝒜).shatterer ∪ (nonMemberSubfamily a 𝒜).shatterer) ℬ

Tactic:
simp only [ℬ, disjoint_left, mem_union, mem_shatterer, mem_image, not_exists, not_and]
    rintro _ (hs | hs) s - rfl
    · exact aux (fun t ht ↦ (mem_memberSubfamily.1 ht).2) hs <| mem_insert_self _ _
    · exact aux (fun t ht ↦ (mem_nonMemberSubfamily.1 ht).2) hs <| mem_insert_self _ _

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

Goal state before:
pp: case succ
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
      ↑(#(falling (Fintype.card α - k) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ∑ x ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - x))) / ↑((Fintype.card α).choose (Fintype.card α - x)) +
      ↑(#(𝒜 # (Fintype.card α - (k + 1)))) / ↑((Fintype.card α).choose (Fintype.card α - (k + 1))) ≤
    (↑(#(𝒜 # (Fintype.card α - (k + 1)))) + ↑(#(∂ (falling (Fintype.card α - (k + 1) + 1) 𝒜)))) /
      ↑((Fintype.card α).choose (Fintype.card α - (k + 1)))

Tactic:
_root_.add_div,

Goal state after:
case succ
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
      ↑(#(falling (Fintype.card α - k) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ∑ x ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - x))) / ↑((Fintype.card α).choose (Fintype.card α - x)) +
      ↑(#(𝒜 # (Fintype.card α - (k + 1)))) / ↑((Fintype.card α).choose (Fintype.card α - (k + 1))) ≤
    ↑(#(𝒜 # (Fintype.card α - (k + 1)))) / ↑((Fintype.card α).choose (Fintype.card α - (k + 1))) +
      ↑(#(∂ (falling (Fintype.card α - (k + 1) + 1) 𝒜))) / ↑((Fintype.card α).choose (Fintype.card α - (k + 1)))
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3.refine_1
α : 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 : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : insert a v ∈ 𝒜 ∧ a ∉ v
hsv : s ∩ v = {a}
⊢ False

Tactic:
← singleton_subset_iff (a := a),

Goal state after:
case refine_3.refine_1
α : 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 : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : insert a v ∈ 𝒜 ∧ ¬{a} ⊆ v
hsv : s ∩ v = {a}
⊢ False
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
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 α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₃ (s ∩ t) * f₄ (s ∪ t) + f₃ (s ∩ insert a t) * f₄ (s ∪ insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
collapse_of_mem ‹_› (union_mem_sups ‹_› ‹_›) (union_mem_sups ‹_› ‹_›) rfl
        (union_insert _ _ _),

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
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 α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₃ (s ∩ t) * f₄ (s ∪ t) + f₃ (s ∩ insert a t) * f₄ (s ∪ insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * (f₄ (s ∪ t) + f₄ (s ∪ insert a t))
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case mpr
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : x ∈ {x | (mkClasses c H) x y}
b' : Set α
right✝ : ∀ (y : Set α), (fun b ↦ b ∈ c ∧ x ∈ b) y → y = b'
hc : b' ∈ c
hb' : x ∈ b'
⊢ x ∈ s

Tactic:
eq_of_mem_eqv_class H hs hy hc (hx b' hc hb')

Goal state after:
case mpr
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : x ∈ {x | (mkClasses c H) x y}
b' : Set α
right✝ : ∀ (y : Set α), (fun b ↦ b ∈ c ∧ x ∈ b) y → y = b'
hc : b' ∈ c
hb' : x ∈ b'
⊢ x ∈ b'
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case inl
V : Type u
u : V
⊢ (completeGraph V).Reachable u u

pp: case inr
V : Type u
u v : V
huv : u ≠ v
⊢ (completeGraph V).Reachable u v

Tactic:
· simp

Goal state after:
case inr
V : Type u
u v : V
huv : u ≠ v
⊢ (completeGraph V).Reachable u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
⊢ v ∈ c.supp ↔ w ∈ c.supp

Tactic:
simp only [ConnectedComponent.mem_supp_iff] at *
  constructor <;> intro h <;> simp only [← h] <;> apply connectedComponentMk_eq_of_adj
  · exact hadj.symm
  · exact hadj

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
⊢ range (hs.piecewise f) = ⋃ i, f i '' s i

Tactic:
refine ext fun x => ⟨?_, fun ⟨t, ⟨i, hi⟩, ht⟩ ↦ ?_⟩
  · rintro ⟨x, rfl⟩
    exact mem_iUnion_of_mem (hs.index x) ⟨x, hs.mem_index x, rfl⟩
  · simp only [← hi, mem_image] at ht
    obtain ⟨a, ha1, ha2⟩ := ht
    refine ⟨a, ?_⟩
    simp only [hs.mem_iff_index_eq] at ha1
    simpa [hs.mem_iff_index_eq, ← ha1] using! ha2

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ Pairwise fun c c' ↦ Disjoint c.supp c'.supp

Tactic:
by
  simp_rw [Set.disjoint_left]
  intro _ _ h a hsx hsy
  rw [ConnectedComponent.mem_supp_iff] at hsx hsy
  rw [hsx] at hsy
  exact h hsy

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.reverse.edges
⊢ False

Tactic:
rw [Walk.edges_reverse, List.mem_reverse] at hpq'

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp.refine_2
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(v, w) ∈ (Walk.cons ⋯ ↑p.toPath).edges

Tactic:
· simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∉ P.edges
⊢ ∀ e ∈ P.edges, e ∉ {s(x, y)}

Tactic:
by grind

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∈ P.edges
hyP : y ∈ P.support
P₁ : G.Walk w y := P.takeUntil y hyP
hxP₁ : x ∉ (P.takeUntil y hyP).support
heP₁ : s(x, y) ∉ P₁.edges
⊢ ∀ e ∈ P₁.edges, e ∉ {s(x, y)}

Tactic:
by grind

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

Goal state before:
pp: case inr
V : Type u
h✝ : Infinite V
⊢ ⊤.chromaticNumber = ENat.card V

Tactic:
· simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
⊢ (induce s G).Reachable ⟨u, hu⟩ ⟨v, hv⟩

Tactic:
obtain ⟨p, hp⟩ := hG.exists_isPath u v

Goal state after:
V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
p : G.Walk u v
hp : p.IsPath
⊢ (induce s G).Reachable ⟨u, hu⟩ ⟨v, hv⟩
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
p : G.Walk u v
hp : p.IsPath
w : V
hwp : w ∈ p.support
hws : w ∉ s
⊢ w ≠ u

Tactic:
by grind

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
p : G.Walk u v
hp : p.IsPath
w : V
hwp : w ∈ p.support
hws : w ∉ s
⊢ w ≠ v

Tactic:
by grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v w : V
p : G.Walk u v
e : Sym2 V
⊢ ∀ (a₁ a₂ : V),
    (fun v_1 w ↦ v_1 ∈ p.support ∧ w ∈ p.support) a₁ a₂ = (fun v_1 w ↦ v_1 ∈ p.support ∧ w ∈ p.support) a₂ a₁

Tactic:
by grind

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
s : Finset V
h : G.IsClique ↑s
hc : card α ≤ s.card
C : G.Coloring α
a✝¹ : α
a✝ : a✝¹ ∈ Set.univ
w✝ : ↑↑s
hx : (Hom.comp C (Embedding.induce ↑s).toHom) w✝ = ?m.37
⊢ a✝¹ ∈ ⇑C '' ↑s

Tactic:
exact ⟨_, Subtype.coe_prop _, hx⟩

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

Goal state before:
pp: case succ
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
n : ℕ
hc : (completeMultipartiteGraph V).CliqueFree (n + 1)
⊢ (completeMultipartiteGraph V).Colorable (n + 1 - 1)

Tactic:
| succ n =>

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ G.neighborFinset v = {w ∈ t | G.Adj v w}

Tactic:
by
  ext w
  rw [mem_neighborFinset, mem_filter, iff_and_self]
  exact h.mem_of_mem_adj hv

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

Goal state before:
pp: case empty.inl
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
ℬ : Finset (Finset α)
hℬ : ℬ = ∅ ∨ ℬ = {∅}
⊢ (∑ s ∈ ∅, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ ∅ ⊼ ℬ, f₃ s) * ∑ s ∈ ∅ ⊻ ℬ, f₄ s

pp: case empty.inr
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
ℬ : Finset (Finset α)
hℬ : ℬ = ∅ ∨ ℬ = {∅}
⊢ (∑ s ∈ {∅}, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ {∅} ⊼ ℬ, f₃ s) * ∑ s ∈ {∅} ⊻ ℬ, f₄ s

Tactic:
· simp

Goal state after:
case empty.inr
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
ℬ : Finset (Finset α)
hℬ : ℬ = ∅ ∨ ℬ = {∅}
⊢ (∑ s ∈ {∅}, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ {∅} ⊼ ℬ, f₃ s) * ∑ s ∈ {∅} ⊻ ℬ, f₄ s
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case empty.inr
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
ℬ : Finset (Finset α)
hℬ : ℬ = ∅ ∨ ℬ = {∅}
⊢ (∑ s ∈ {∅}, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ {∅} ⊼ ℬ, f₃ s) * ∑ s ∈ {∅} ⊻ ℬ, f₄ s

Tactic:
obtain rfl | rfl := hℬ

Goal state after:
case empty.inr.inl
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
⊢ (∑ s ∈ {∅}, f₁ s) * ∑ s ∈ ∅, f₂ s ≤ (∑ s ∈ {∅} ⊼ ∅, f₃ s) * ∑ s ∈ {∅} ⊻ ∅, f₄ s

case empty.inr.inr
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
⊢ (∑ s ∈ {∅}, f₁ s) * ∑ s ∈ {∅}, f₂ s ≤ (∑ s ∈ {∅} ⊼ {∅}, f₃ s) * ∑ s ∈ {∅} ⊻ {∅}, f₄ s
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case empty.inr.inl
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
⊢ (∑ s ∈ {∅}, f₁ s) * ∑ s ∈ ∅, f₂ s ≤ (∑ s ∈ {∅} ⊼ ∅, f₃ s) * ∑ s ∈ {∅} ⊻ ∅, f₄ s

pp: case empty.inr.inr
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
⊢ (∑ s ∈ {∅}, f₁ s) * ∑ s ∈ {∅}, f₂ s ≤ (∑ s ∈ {∅} ⊼ {∅}, f₃ s) * ∑ s ∈ {∅} ⊻ {∅}, f₄ s

Tactic:
· simp

Goal state after:
case empty.inr.inr
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
⊢ (∑ s ∈ {∅}, f₁ s) * ∑ s ∈ {∅}, f₂ s ≤ (∑ s ∈ {∅} ⊼ {∅}, f₃ s) * ∑ s ∈ {∅} ⊻ {∅}, f₄ s
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
hi : 0 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert 0) ((cons hxy i').getVert (0 + 1))

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert (n✝ + 1)) ((cons hxy i').getVert (n✝ + 1 + 1))

Tactic:
· simp

Goal state after:
case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert (n✝ + 1)) ((cons hxy i').getVert (n✝ + 1 + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ (a₁ : V × V)
    (ha₁ :
      a₁ ∈
        {x |
          match x with
          | (x, y) => G.Adj x y})
    (a₂ : V × V)
    (ha₂ :
      a₂ ∈
        {x |
          match x with
          | (x, y) => G.Adj x y}),
    ((match a₁, ha₁ with
        | (v, w), x => s(Sum.inl v, Sum.inr w)) =
        match a₂, ha₂ with
        | (v, w), x => s(Sum.inl v, Sum.inr w)) →
      a₁ = a₂

Tactic:
by grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v w : V
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
by
  cases eq_or_ne (G.edist u v) ⊤ with
  | inl huv => simp [huv]
  | inr huv =>
    cases eq_or_ne (G.edist v w) ⊤ with
    | inl hvw => simp [hvw]
    | inr hvw =>
      obtain ⟨p, hp⟩ := exists_walk_of_edist_ne_top huv
      obtain ⟨q, hq⟩ := exists_walk_of_edist_ne_top hvw
      rw [← hp, ← hq, ← Nat.cast_add, ← Walk.length_append]
      exact edist_le _

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

Goal state before:
pp: 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
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
by_cases! he : i = 0 ∨ i = p.length

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
⊢ (p.toSubgraph.neighborSet v).ncard = 2

case neg
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
⊢ (p.toSubgraph.neighborSet v).ncard = 2
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
x✝ : ↑(G ⊕g H).edgeSet
e : Sym2 (V ⊕ W)
he : e ∈ (G ⊕g H).edgeSet
⊢ ∀ (a b : V ⊕ W) (h : (G ⊕g H).Adj a b),
    (match a, b, h with
      | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
      | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
      | Sum.inl u, Sum.inr v, h => False.elim ⋯
      | Sum.inr u, Sum.inl v, h => False.elim ⋯) =
      match b, a, ⋯ with
      | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
      | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
      | Sum.inl u, Sum.inr v, h => False.elim ⋯
      | Sum.inr u, Sum.inl v, h => False.elim ⋯

Tactic:
by grind

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

Goal state before:
pp: case zero
n : ℕ
hm : 0 ≤ n + 3
⊢ (cycle n).getVert 0 = ⟨(n + 3 - 0) % (n + 3), ⋯⟩

pp: case succ
n n✝ : ℕ
hm : n✝ + 1 ≤ n + 3
⊢ (cycle n).getVert (n✝ + 1) = ⟨(n + 3 - (n✝ + 1)) % (n + 3), ⋯⟩

Tactic:
· simp

Goal state after:
case succ
n n✝ : ℕ
hm : n✝ + 1 ≤ n + 3
⊢ (cycle n).getVert (n✝ + 1) = ⟨(n + 3 - (n✝ + 1)) % (n + 3), ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case refine_2.patches
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ s' ⊆ ↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset),
    ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩

Tactic:
refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩

Goal state after:
case refine_2.patches.refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ {x | x ∈ (Nonempty.some ⋯).support} ⊆ ↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset)

case refine_2.patches.refine_2
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ (hu' : u ∈ {x | x ∈ (Nonempty.some ⋯).support}) (hv' : v ∈ {x | x ∈ (Nonempty.some ⋯).support}),
    (induce {x | x ∈ (Nonempty.some ⋯).support} G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: 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
m : Fin n
⊢ ↑m.succ < p.support.length

Tactic:
by grind

Goal state after: