mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.left
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ f =
    m.reduce ⋯ f +
      (Finsupp.linearCombination (MvPolynomial σ R) b)
        (Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f)))

Tactic:
simp [reduce]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
R C : Set α
M : Matroid α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = (M ↾ (R \ C ∪ C)) ／ C

Tactic:
simp [union_eq_self_of_subset_right hCR]

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
sharp :
  2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ Multiset.map (fun x ↦ f ![a, b]) ω = Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])

Tactic:
simp [FractionalOperation.tt, Multiset.map_map]

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
sharp :
  2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • (Multiset.map (fun x ↦ f ![a, b]) ω).sum < ω.size • 2 • f ![a, b]
rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]
distrib : (Multiset.map (fun x ↦ f ![a, b]) ω).sum = ω.size • f ![a, b]
⊢ False

Tactic:
rhs_swap,

Goal state after:
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
sharp :
  2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • (Multiset.map (fun x ↦ f ![a, b]) ω).sum < 2 • ω.size • f ![a, b]
rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]
distrib : (Multiset.map (fun x ↦ f ![a, b]) ω).sum = ω.size • f ![a, b]
⊢ False
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b b✝ c✝ : V
p' : Path a b✝
e : b✝ ⟶ c✝
ih : a ∈ p'.vertices
⊢ a ∈ (p'.cons e).vertices

Tactic:
simp [ih]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b b✝ c✝ : V
p' : Path a b✝
e : b✝ ⟶ c✝
ih : p'.vertices.head? = some a
⊢ (p'.cons e).vertices.head? = some a

Tactic:
simp [ih]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b b✝ c✝ : V
p' : Path a b✝
e : b✝ ⟶ c✝
ih : p'.vertices[0] = a
⊢ (p'.cons e).vertices[0] = a

Tactic:
simp [ih]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b c : V
p : Path a b
b✝ c✝ : V
q' : Path b b✝
e : b✝ ⟶ c✝
ih : (p.comp q').vertices = p.vertices.dropLast ++ q'.vertices
⊢ (p.comp (q'.cons e)).vertices = p.vertices.dropLast ++ (q'.cons e).vertices

Tactic:
simp [ih]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
⊢ p 𝒜

Tactic:
set u := 𝒜.sup id

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α := 𝒜.sup id
⊢ p 𝒜
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∈ A
⊢ n ∈ A

Tactic:
simp [hnA]

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

Goal state before:
pp: α : Type u_4
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
n : ℕ
h𝒜 : Set.Sized n ↑𝒜
s : Finset α
hs : s ∈ 𝒜
⊢ Fintype.card α - #s = Fintype.card α - n

Tactic:
h𝒜 hs

Goal state after:
α : Type u_4
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
n : ℕ
h𝒜 : Set.Sized n ↑𝒜
s : Finset α
hs : s ∈ 𝒜
⊢ Fintype.card α - n = Fintype.card α - n
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ Disjoint v a

pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h✝ : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ Disjoint v a

Tactic:
· rw [← hba]
    exact disjoint_sdiff_self_right

Goal state after:
case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h✝ : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ Disjoint v a
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
a : α
⊢ (fun s ↦ (↑s).toFinset.sup Subtype.val) ((fun a ↦ { carrier := {b | ↑b ≤ a}, lower' := ⋯ }) a) = a

Tactic:
refine le_antisymm (Finset.sup_le fun b ↦ Set.mem_toFinset.1) ?_

Goal state after:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
a : α
⊢ a ≤ (fun s ↦ (↑s).toFinset.sup Subtype.val) ((fun a ↦ { carrier := {b | ↑b ≤ a}, lower' := ⋯ }) a)
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
⊢ IsUpperSet ↑s

Tactic:
rintro a b hab ha
    rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]
    · exact mem_insert_self _ _
    rw [coe_insert]
    exact
      hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab

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

Goal state before:
pp: α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : (↑s).Intersecting
x : α
hx' : x ∈ s
hx : { toFun := compl, inj' := ⋯ } x ∈ s
hxc : { toFun := compl, inj' := ⋯ } x ∈ map { toFun := compl, inj' := ⋯ } s
⊢ False

Tactic:
exact hs.compl_notMem hx' hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t u : Finset α
ha : a ∉ s
ht : t ∈ 𝒜
hu : u ∈ 𝒜
hts : t = s
hus : u = insert a s
⊢ collapse 𝒜 a f s = f t + f u

Tactic:
subst hts

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t u : Finset α
ht : t ∈ 𝒜
hu : u ∈ 𝒜
ha : a ∉ t
hus : u = insert a t
⊢ collapse 𝒜 a f t = f t + f u
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = s
ht : t ∈ 𝒜
⊢ f t ≤ collapse 𝒜 a f s

Tactic:
subst hts

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
⊢ f t ≤ collapse 𝒜 a f t
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mp.left
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : toColex (insert a t) ≤ toColex s
⊢ #(insert a t) - 1 = #t

Tactic:
card_insert_of_notMem ha,

Goal state after:
case mp.left
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : toColex (insert a t) ≤ toColex s
⊢ #t + 1 - 1 = #t
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inr.cons.refine_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * Fintype.card (Finset α) + 2 * (#(s.biUnion f') * #(f' i)ᶜ) ≤
    2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))

Tactic:
mul_tsub,

Goal state after:
case inr.cons.refine_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * Fintype.card (Finset α) + 2 * (#(s.biUnion f') * #(f' i)ᶜ) ≤
    2 * 2 ^ Fintype.card α * 2 ^ Fintype.card α - 2 * 2 ^ Fintype.card α * 2 ^ (Fintype.card α - #(cons i s hi))
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inr.cons.refine_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * 2 ^ Fintype.card α + #(s.biUnion f') * (2 * (2 ^ Fintype.card α - #(f' i))) ≤
    2 * 2 ^ Fintype.card α * 2 ^ Fintype.card α - 2 * 2 ^ Fintype.card α * 2 ^ (Fintype.card α - #(cons i s hi))

Tactic:
mul_tsub,

Goal state after:
case inr.cons.refine_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * 2 ^ Fintype.card α + #(s.biUnion f') * (2 * 2 ^ Fintype.card α - 2 * #(f' i)) ≤
    2 * 2 ^ Fintype.card α * 2 ^ Fintype.card α - 2 * 2 ^ Fintype.card α * 2 ^ (Fintype.card α - #(cons i s hi))
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case h₂
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α + (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)) ≤
    2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))

Tactic:
mul_tsub,

Goal state after:
case h₂
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α + (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)) ≤
    2 * 2 ^ Fintype.card α - 2 * 2 ^ (Fintype.card α - #(cons i s hi))
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ image (fun t ↦ s ∩ t) 𝒜 = s.powerset

Tactic:
by ext t; rw [mem_image, mem_powerset, h.subset_iff]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : s ∉ 𝒜
a : α
ha : a ∉ s
hst : insert a s ⊆ t
⊢ #(insert a s) = k + 1

Tactic:
card_insert_of_notMem ha,

Goal state after:
case neg
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : s ∉ 𝒜
a : α
ha : a ∉ s
hst : insert a s ⊆ t
⊢ #s + 1 = k + 1
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:
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 : SimpleGraph V
e : Sym2 V
he : G.IsBridge e
⊢ Nontrivial V

Tactic:
cases e with | h u v =>  _ 

Goal state after:
case h
V : Type u
G : SimpleGraph V
u v : V
he : G.IsBridge s(u, v)
⊢ Nontrivial V
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

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

Tactic:
← hne

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
hc : ↑G.chromaticNumber.toNat < ↑n
hne : ↑G.chromaticNumber.toNat = G.chromaticNumber
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.chromaticNumber.toNat < n
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
w : V
⊢ G.Adj v w → w ∈ t

Tactic:
exact h.mem_of_mem_adj hv

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
w : V
⊢ G.Adj v w → w ∈ t

Tactic:
exact h.mem_of_mem_adj hv

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.IsEdgeReachable 1 u v ↔ G.Reachable u v

Tactic:
simp [IsEdgeReachable, Order.lt_one_iff]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
huy : ¬G.IsEdgeReachable 2 u x
e : Sym2 V
he : ¬(G.deleteEdges {e}).Reachable u x
⊢ x ∉ w.support

Tactic:
have he' : ¬ (G.deleteEdges {e}).Reachable v x := fun hvy ↦
    he <| (isEdgeReachable_two.1 huv _).trans hvy

Goal state after:
V : Type u_1
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
huy : ¬G.IsEdgeReachable 2 u x
e : Sym2 V
he : ¬(G.deleteEdges {e}).Reachable u x
he' : ¬(G.deleteEdges {e}).Reachable v x
⊢ x ∉ w.support
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inl
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isLeft = true
hs₂ : s₂.isRight = true
⊢ G.Adj ((Subtype.val ∘ ⇑fα) (s₁.getLeft hs₁))
    (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inr (s₂.getRight hs₂)))

Tactic:
Sum.elim_inr

Goal state after:
case inl
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isLeft = true
hs₂ : s₂.isRight = true
⊢ G.Adj ((Subtype.val ∘ ⇑fα) (s₁.getLeft hs₁)) ((Subtype.val ∘ ⇑fβ) (s₂.getRight hs₂))
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
⊢ G'.dist u v ≤ G.dist u v

Tactic:
obtain ⟨_, hw⟩ := hr.exists_walk_length_eq_dist

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : w✝.length = G.dist u v
⊢ G'.dist u v ≤ G.dist u v
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.IsExtremal H.Free ↔ H.Free G ∧ #G.edgeFinset = extremalNumber (Fintype.card V) H

Tactic:
IsExtremal,

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (H.Free G ∧ ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], H.Free G' → #G'.edgeFinset ≤ #G.edgeFinset) ↔
    H.Free G ∧ #G.edgeFinset = extremalNumber (Fintype.card V) H
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
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
⊢ False

Tactic:
apply absurd h

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 := ⋯
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
⊢ ¬G.IsTuranMaximal r
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
x✝ : ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂
w✝² w✝¹ w✝ : α
h1 : G.Adj w✝¹ w✝
h2 : ¬G.Adj w✝² w✝¹
h3 : ¬G.Adj w✝² w✝
h : G.IsCompleteMultipartite
⊢ ¬G.Adj w✝¹ w✝²

Tactic:
rwa [adj_comm] at h2

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
⊢ False

Tactic:
apply absurd h

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 := ⋯
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ¬G.IsTuranMaximal r
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩) = v

Tactic:
refine Prod.ext (Fin.ext ?_) (Fin.ext ?_)

Goal state after:
case refine_1
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑(⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).1 = ↑v.1

case refine_2
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑(⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).2 = ↑v.2