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

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
⊢ φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₂, p₂⟩

Tactic:
simp only [Prefunctor.pathStar_apply, Sigma.mk.inj_iff]

Goal state after:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
⊢ φ.obj x₁ = φ.obj x₂ ∧ φ.mapPath p₁ ≍ φ.mapPath p₂
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(𝓓 a 𝒜) = #𝒜

Tactic:
rw [compression, card_disjUnion, filter_image,
    card_image_of_injOn ((erase_injOn' _).mono fun s hs => _), ← card_union_of_disjoint]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #𝒜

α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Disjoint ({s ∈ 𝒜 | s.erase a ∈ 𝒜}) ({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})

α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ∀ s ∈ ↑({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}), s ∈ {s | a ∈ s}
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case pos
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
h : a ∈ upperClosure ↑s
⊢ {b ∈ s | b ≤ a}.inf' ⋯ id ≤ a

pp: case neg
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
h : a ∉ upperClosure ↑s
⊢ ⊥ ≤ a

Tactic:
· obtain ⟨b, hb, hba⟩ := h
    exact hba.trans' <| inf'_le id <| mem_filter.2 ⟨hb, ‹_›⟩

Goal state after:
case neg
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
h : a ∉ upperClosure ↑s
⊢ ⊥ ≤ a
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
a : α
⊢ aᶜ ∈ s ↔ a ∈ sᶜˢ

Tactic:
← mem_map' ⟨compl, compl_injective⟩,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
a : α
⊢ { toFun := compl, inj' := ⋯ } aᶜ ∈ map { toFun := compl, inj' := ⋯ } s ↔ a ∈ sᶜˢ
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ≤ b ⊔ c → a ≤ b ∨ a ≤ c

Tactic:
simp_rw [← inf_eq_left, inf_sup_left]; exact @h _ _

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

Goal state before:
pp: case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
u : Finset α
hau : a ∉ u
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ u_1, #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
hut : a ∈ t ∧ u ⊆ t
htu : t \ insert a u ∈ 𝒜
⊢ ∃ a ∈ t, ∃ u_1, #u_1 = #u ∧ (u_1 ⊆ t ∧ a ∉ u_1) ∧ t \ insert a u_1 ∈ 𝒜

Tactic:
exact ⟨a, hut.1, _, rfl, ⟨hut.2, hau⟩, htu⟩

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜

Tactic:
refine mem_shadow_iff.2
        ⟨(t ⊔ u) \ v,
          sup_sdiff_mem_of_mem_compression Ht hvt <| disjoint_of_erase_right hau huvs.1, a, ?_, ?_⟩

Goal state after:
case neg.refine_1
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ a ∈ (t ⊔ u) \ v

case neg.refine_2
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ ((t ⊔ u) \ v).erase a = (t.erase a ⊔ u) \ v
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: 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)

Tactic:
shadow_initSeg (card_pos.1 hr),

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.erase (s.min' ⋯))) (#s - 1)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₁ : UsefulCompression U V
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
⊢ #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)

Tactic:
obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
⊢ #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)
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 α
⊢ ↑(#(𝒜 # (Fintype.card α - k - 1))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1)) +
      ↑(#(falling (Fintype.card α - k) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - k)) ≤
    ↑(#(𝒜 # (Fintype.card α - k - 1))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1)) +
      ↑(#(∂ (falling (Fintype.card α - k) 𝒜))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1))

Tactic:
local_lubell_yamamoto_meshalkin_inequality_div
      (tsub_pos_iff_lt.2 <| Nat.succ_le_iff.1 hk).ne' <| sized_falling _ _

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 α
⊢ ↑(#(𝒜 # (Fintype.card α - k - 1))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1)) +
      ↑(#(∂ (falling (Fintype.card α - k) 𝒜))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1)) ≤
    ↑(#(𝒜 # (Fintype.card α - k - 1))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1)) +
      ↑(#(∂ (falling (Fintype.card α - k) 𝒜))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1))
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∉ 𝒜 ∧ insert a v ∈ 𝒜
⊢ a ∈ s ∩ v

Tactic:
rw [hsv]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∉ 𝒜 ∧ insert a v ∈ 𝒜
⊢ a ∈ insert a (s ∩ u)
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case mp
α : 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 ∈ s
_s' : Set α
hs' : _s' ∈ c
hx' : x ∈ _s'
⊢ y ∈ _s'

Tactic:
rwa [eq_of_mem_eqv_class H hs' hx' hs hx]

Goal state after:
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 * 0 + f₁ s * f₂ (insert a t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [mul_zero, zero_add]

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 * f₂ (insert a t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.IsUniversal u
⊢ G.Reachable u v

Tactic:
by
  by_cases! h' : u = v
  · exact h' ▸ Reachable.rfl
  · exact (h h').reachable

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

Goal state before:
pp: α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
hb₁ : b₁ ∈ s ∧ a ∈ b₁
⊢ b₂ ∈ s ∧ a ∈ b₂ → b₁ = b₂

Tactic:
hb₂

Goal state after:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
hb₁ : b₁ ∈ s ∧ a ∈ b₁
hb₂ : b₂ ∈ s ∧ a ∈ b₂
⊢ b₁ = b₂
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : ¬G.Reachable u w
⊢ Gᶜ.Reachable u w

Tactic:
exact G.reachable_or_compl_adj .. |>.resolve_left huw |>.reachable

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

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
m : ℕ
⊢ m ∈ range k → m < n

Tactic:
rw [mem_range]

Goal state after:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
m : ℕ
⊢ m < k → m < n
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case mp
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ (mkClasses c ⋯).classes → s ∈ c

Tactic:
rintro ⟨y, rfl⟩
    obtain ⟨b, ⟨hb, hy⟩, _⟩ := hc.2 y
    rwa [← eq_eqv_class_of_mem _ hb hy]

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

Goal state before:
pp: case mpr.refine_2
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
⊢ ∀ {v w : V}, G.Adj v w → ⟨C v, ⋯⟩ ≠ ⟨C w, ⋯⟩

Tactic:
rintro v w hvw
      simp only [Fin.mk_eq_mk, Ne]
      exact C.valid hvw

Goal state after:
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₁ (insert a s) * 0 + f₁ (insert a s) * f₂ (insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [mul_zero, zero_add]

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₁ (insert a s) * f₂ (insert a t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
s : Set (Sym2 V)
huv : ∀ e ∈ s, e ∉ w.edges
⊢ (G.deleteEdges s).Reachable u v

Tactic:
exact ⟨w.toDeleteEdges _ fun _ ↦ imp_not_comm.1 <| huv _⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsChordless ↔ ∀ ⦃u' v' : V⦄, u' ∈ p.support → v' ∈ p.support → G.Adj u' v' → s(u', v') ∈ p.edges

Tactic:
by
  simp [IsChordless, Sym2.forall, isChord_sym2Mk]; grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hx : ∀ (i : G.Walk u v), False
⊢ False

Tactic:
exact h.elim hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a : α
b₁ b₂ : β
⊢ (G □ H).Adj (a, b₁) (a, b₂) ↔ H.Adj b₁ b₂

Tactic:
by
  simp only [boxProd_adj, SimpleGraph.irrefl, false_and, and_true, false_or]

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

Goal state before:
pp: case hle
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Preconnected
tconn : (⊤.induce t).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ ⊤.induce {v, w} ⊔ ⊤.induce s ⊔ ⊤.induce t ≤ ⊤.induce (s ∪ t)

Tactic:
simp only [sup_le_iff, Subgraph.le_induce_union_left,
      Subgraph.le_induce_union_right, and_true, ← Subgraph.subgraphOfAdj_eq_induce ha]
    apply subgraphOfAdj_le_of_adj
    simp [hv, hw, ha]

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ {s | G.IsNClique r s} = ∅

Tactic:
filter_eq_empty_iff,

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ∀ ⦃x : Finset V⦄, x ∈ univ → ¬G.IsNClique r x
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
h : ¬Even K.supp.ncard
⊢ Even (K.supp \ s).ncard

Tactic:
have : K.supp.ncard ≠ 0 := Nat.ne_of_odd_add (Nat.not_even_iff_odd.mp h)
    rw [hrep.ncard_sdiff_of_mem (Nat.not_even_iff_odd.mp h), Nat.even_sub (by lia)]
    simpa [Nat.even_sub] using Nat.not_even_iff_odd.mp h

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
v : α
⊢ G.Adj u v ∨ u = v

Tactic:
exact or_iff_not_imp_right.mpr (hall v)

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.ediam.toNat = 1 ↔ G = ⊤

Tactic:
ENat.toNat_eq_iff one_ne_zero,

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.ediam = ↑1 ↔ G = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
| r * (r - 1)

Tactic:
enter [1]; rw [← card_range r]

Goal state after:
n r : ℕ
| #(range r)
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)
⊢ G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G →
    #G.edgeFinset ≤ {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
⟨h_le, h_free⟩

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
⊢ #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)
⊢ G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G →
    #G.edgeFinset ≤
      {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
        #x.edgeFinset

Tactic:
⟨h_le, h_free⟩

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
⊢ #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.Matching

Goal state before:
pp: case mk
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
val✝ : Sym2 V
x y : V
he : Quot.mk (Sym2.Rel V) (x, y) ∈ M.edgeSet
⊢ ∃ a, h.toEdge a = ⟨Quot.mk (Sym2.Rel V) (x, y), he⟩

Tactic:
exact ⟨⟨x, M.edge_vert he⟩, h.toEdge_eq_of_adj he⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
left✝ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
x : V
⊢ x ∈ p₁ ∪ p₂

Tactic:
have := h₁.mem_of_adj <| G.mem_neighborFinset _ _ |>.mp (hf₂ x)

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
left✝ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
x : V
this : x ∈ p₁ ∧ f x ∈ p₂ ∨ x ∈ p₂ ∧ f x ∈ p₁
⊢ x ∈ p₁ ∪ p₂
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
⊢ ↑t < ↑t' * (↑r * ε)

Tactic:
← div_lt_iff₀ (by positivity),

Goal state after:
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
⊢ ↑t / (↑r * ε) < ↑t'