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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ ∑ s ∈ (range (#univ + 1)).disjiUnion (fun i ↦ powersetCard i univ) ⋯,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
sum_disjiUnion

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ ∑ i ∈ range (#univ + 1), ∑ x ∈ powersetCard i univ, ↑(card α) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case a
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ∃ x, ∀ ⦃x_1 : ℕ⦄, 0 < x_1 → x_1 ≤ m → x_1 % m = 1 → x_1 = x

Tactic:
use 1

Goal state after:
case h
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ∀ ⦃x : ℕ⦄, 0 < x → x ≤ m → x % m = 1 → x = 1
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
a : α
⊢ a ∈ map { toFun := compl, inj' := ⋯ } s ↔ a ∈ sᶜˢ

Tactic:
compls

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ lowerClosure ↑s ⊓ lowerClosure ↑t ↔ a ∈ lowerClosure ↑s ∧ a ∈ lowerClosure ↑t

Tactic:
LowerSet.mem_inf_iff

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ lowerClosure ↑s ∧ a ∈ lowerClosure ↑t ↔ a ∈ lowerClosure ↑s ∧ a ∈ lowerClosure ↑t
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
ha : a ∉ upperClosure ↑s ⊔ upperClosure ↑t
⊢ a ∉ upperClosure ↑(s ⊻ t)

Tactic:
by rwa [coe_sups, upperClosure_sups]

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : Finite α
a : α
⊢ SupIrred (Iic a)

Tactic:
exact supIrred_Iic _

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

Goal state before:
pp: case empty.inl
α : Type u_1
inst✝ : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑∅
⊢ #∅ * #ℬ ≤ 2 ^ #∅ * #(∅ ∩ ℬ)

pp: case empty.inr
α : Type u_1
inst✝ : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑{∅}
⊢ #{∅} * #ℬ ≤ 2 ^ #∅ * #({∅} ∩ ℬ)

Tactic:
· simp only [card_empty, zero_mul, empty_inter, mul_zero, le_refl]

Goal state after:
case empty.inr
α : Type u_1
inst✝ : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑{∅}
⊢ #{∅} * #ℬ ≤ 2 ^ #∅ * #({∅} ∩ ℬ)
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
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
⊢ False

Tactic:
apply m z (disjoint_right.1 hsv hz)

Goal state after:
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 α) := ⋯
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
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
⊢ insert z s ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inr.cons.refine_2
ι : 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)
⊢ IsLowerSet ↑(f' i)ᶜ

Tactic:
coe_compl

Goal state after:
case inr.cons.refine_2
ι : 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)
⊢ IsLowerSet (↑(f' i))ᶜ
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ∅ ∉ 𝒜

Tactic:
rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ¬𝒜 = {∅}
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr.inr.inr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
ha : k ∈ s
⊢ k ∈ insert j t

pp: case mpr.inr.inr.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
gt : a < k
⊢ a ∈ insert j t

Tactic:
· rw [r₁]; apply mem_insert_self

Goal state after:
case mpr.inr.inr.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
gt : a < k
⊢ a ∈ insert j t
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr.refine_1
α : 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
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ #(U.erase x) = #(V.erase (V.min' hV))

pp: case inr.refine_2
α : 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
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ (U.erase x).Nonempty

pp: case inr.refine_3
α : 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
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ (V.erase (V.min' hV)).Nonempty

pp: case inr.refine_4
α : 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
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ (U.erase x).max' ?inr.refine_2 < (V.erase (V.min' hV)).max' ?inr.refine_3

Tactic:
· rw [card_erase_of_mem (min'_mem _ _), card_erase_of_mem Hx, same_size]

Goal state after:
case inr.refine_2
α : 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
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ (U.erase x).Nonempty

case inr.refine_3
α : 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
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ (V.erase (V.min' hV)).Nonempty

case inr.refine_4
α : 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
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ (U.erase x).max' ?inr.refine_2 < (V.erase (V.min' hV)).max' ?inr.refine_3
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
⊢ False

Tactic:
have hV : (B \ A).Nonempty :=
    sdiff_nonempty.2 fun h ↦ hAB.symm <| eq_of_subset_of_card_le h hAB'.le

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case e'_1
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)

Tactic:
rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]

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

Goal state before:
pp: case e'_2
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk a✝

Tactic:
rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]

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

Goal state before:
pp: case e'_4.e'_3
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝¹ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
e_3✝ : (fun x ↦ V') ≍ fun x ↦ V'
e_1✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (G.connectedComponentMk b✝).toSimpleGraph.Adj ≍ (G.connectedComponentMk a✝).toSimpleGraph.Adj

Tactic:
rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]

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

Goal state before:
pp: case e'_5
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
⊢ G.connectedComponentMk b✝ = G.connectedComponentMk a✝

Tactic:
rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]

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

Goal state before:
pp: case e'_6
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk a✝

Tactic:
rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]

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) * f₂ (insert a t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
exact (h ‹_› ‹_›).trans <| mul_le_mul (le_collapse_of_insert_mem ‹_› h₃
        (insert_inter_distrib _ _ _).symm <| inter_mem_infs ‹_› ‹_›) (le_collapse_of_insert_mem ‹_›
        h₄ (insert_union_distrib _ _ _).symm <| union_mem_sups ‹_› ‹_›) (h₄ _) <|
        collapse_nonneg h₃ _

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

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

Tactic:
by
  ext v
  rw [mem_neighborFinset, adj_comm, mem_filter, iff_and_self]
  exact h.mem_of_mem_adj' hw

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
inst✝ : Nontrivial ↑H.verts
h : H.Preconnected
v : ↑H.verts
⊢ ∃ u, H.Adj (↑v) u

Tactic:
have := h.coe.exists_adj_of_nontrivial v

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
inst✝ : Nontrivial ↑H.verts
h : H.Preconnected
v : ↑H.verts
this : ∃ u, H.coe.Adj v u
⊢ ∃ u, H.Adj (↑v) u
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : ¬w.Nil
⊢ w.toSubgraph.Adj w.penultimate v

Tactic:
rw [not_nil_iff_lt_length] at h

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : 0 < w.length
⊢ w.toSubgraph.Adj w.penultimate v
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 ≤ ↑(Nat.card V)
⊢ 4 * (s.encard * t.encard) ≤ ↑(Nat.card V) ^ 2

Tactic:
← s.toFinite.cast_ncard_eq,

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.encard ≤ ↑(Nat.card V)
⊢ 4 * (↑s.ncard * t.encard) ≤ ↑(Nat.card V) ^ 2
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)

Tactic:
Pi.mul_apply,

Goal state after:
case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ g a * (μ b * f b) ≤ f (a ⊓ b) * (μ (a ⊔ b) * g (a ⊔ b))
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ μ b * (g a * f b) ≤ μ (a ⊔ b) * (f (a ⊓ b) * g (a ⊔ b))

Tactic:
mul_comm (g _)

Goal state after:
case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ μ b * (f b * g a) ≤ μ (a ⊔ b) * (f (a ⊓ b) * g (a ⊔ b))
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n : ℕ
m : Fin (n + 3)
i : ℕ
hi : i ≤ ↑m
⊢ ↑((cycleCons n m).getVert i) = (↑m - i) % (n + 3)

Tactic:
by
  obtain ⟨m, hm⟩ := m
  induction i generalizing m
  · simp [Nat.mod_eq_of_lt hm]
  · cases m <;> grind +locals [getVert_cons_succ]

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

Goal state before:
pp: case refine_2.refine_2.inr
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
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
this :
  ∀ {V : Type u_1} {G : SimpleGraph V} {n : ℕ},
    2 < n →
      ∀ (a : V) (p : G.Walk a a),
        p.IsCycle →
          ∀ (hp₂ : p.length = n) (x : ℕ) (hx : x < n) (y : ℕ) (hy : y < n),
            (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩ → x ≠ y → x > y → G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]
hle : ¬x > y
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

pp: V✝ : Type u_1
G✝ : SimpleGraph V✝
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
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
hle : x > y
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
· exact this hn a p hp₁ hp₂ y hy x hx hab.symm hne.symm (by lia) |>.symm

Goal state after:
V✝ : Type u_1
G✝ : SimpleGraph V✝
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
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
hle : x > y
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
x : V
⊢ adjMatrix α G x v = adjMatrix α G v x

Tactic:
rw [← transpose_apply (adjMatrix α G) x v, transpose_adjMatrix]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsTree ↔ Nonempty V ∧ Maximal IsAcyclic G

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨_, h⟩ ↦ G.maximal_isAcyclic_iff_isTree.mp h⟩
  have := h.nonempty
  exact ⟨this, G.maximal_isAcyclic_iff_isTree.mpr h⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
x y : V
h : G.Adj x y
hbr : ¬G.IsBridge s(x, y)
⊢ Fintype.card ↑(G.deleteEdges {s(x, y)}).edgeSet + 1 < Nat.card V

Tactic:
← edgeFinset_card,

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
x y : V
h : G.Adj x y
hbr : ¬G.IsBridge s(x, y)
⊢ (G.deleteEdges {s(x, y)}).edgeFinset.card + 1 < Nat.card V
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
x y : V
h : G.Adj x y
hbr : ¬G.IsBridge s(x, y)
⊢ (G.deleteEdges {s(x, y)}).edgeFinset.card + 1 < Fintype.card ↑G.edgeSet + 1

Tactic:
← edgeFinset_card,

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
x y : V
h : G.Adj x y
hbr : ¬G.IsBridge s(x, y)
⊢ (G.deleteEdges {s(x, y)}).edgeFinset.card + 1 < G.edgeFinset.card + 1
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case map_rel'
α : 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
⊢ False

Tactic:
apply h _ <| (((c.connected_toSimpleGraph ⟨_, hv⟩ a).some.concat hab).append
                 (c.connected_toSimpleGraph ⟨_, hv⟩ b).some.reverse).map c.toSimpleGraph_hom

Goal state after:
case map_rel'
α : 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
⊢ Odd (Walk.map c.toSimpleGraph_hom (((Nonempty.some ⋯).concat hab).append (Nonempty.some ⋯).reverse)).length