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

Goal state before:
pp: case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
⊢ (h.sum fun a b ↦ (eval x) (b • Alon.P (S a) a)) = 0

Tactic:
Finsupp.sum,

Goal state after:
case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
⊢ ∑ a ∈ h.support, (eval x) (h a • Alon.P (S a) a) = 0
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
⊢ coeff t (h.sum fun i a ↦ a • ∏ r ∈ S i, (X i - C r)) = 0

Tactic:
Finsupp.sum,

Goal state after:
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
⊢ coeff t (∑ a ∈ h.support, h a • ∏ r ∈ S a, (X a - C r)) = 0
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Finset ℕ
⊢ schnirelmannDensity ↑A = 0

Tactic:
refine le_antisymm ?_ schnirelmannDensity_nonneg

Goal state after:
A : Finset ℕ
⊢ schnirelmannDensity ↑A ≤ 0
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq β
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
hf : Injective ⇑f
s t : Finset α
⊢ map { toFun := ⇑f, inj' := hf } (s ⊻ t) = map { toFun := ⇑f, inj' := hf } s ⊻ map { toFun := ⇑f, inj' := hf } t

Tactic:
by
  simpa [map_eq_image] using image_sups f s t

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
s t : Finset α
a : α
inst✝ : DecidableEq α
⊢ a ∈ upperClosure ↑(s ∪ t) ↔ a ∈ upperClosure ↑s ∨ a ∈ upperClosure ↑t

Tactic:
rw [coe_union, upperClosure_union, UpperSet.mem_inf_iff]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ u ∈ (s ∩ t).powerset ↔ u ∈ s.powerset ⊼ t.powerset

Tactic:
simp only [mem_infs, mem_powerset, inf_eq_inter]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ u ⊆ s ∩ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ ∀ ⦃x : α⦄, x ∈ s ○ t → ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = x

Tactic:
mem_disjSups

Goal state after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ ∀ ⦃x : α⦄, (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = x
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
p : α → Prop
⊢ (∀ c ∈ s ○ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)

Tactic:
mem_disjSups

Goal state after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
p : α → Prop
⊢ (∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ (∃ x, x ∈ s ○ t) → ∃ x, x ∈ s

Tactic:
mem_disjSups

Goal state after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ (∃ x, ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ x, x ∈ s
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ (∃ x, x ∈ s ○ t) → ∃ x, x ∈ t

Tactic:
mem_disjSups

Goal state after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ (∃ x, ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ x, x ∈ t
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
⊢ SupIrred s ↔ ∃ a, Iic a = s

Tactic:
refine ⟨fun hs ↦ ?_, ?_⟩
  · obtain ⟨a, ha, has⟩ := (s : Set α).toFinite.exists_maximal (coe_nonempty.2 hs.ne_bot)
    exact ⟨a, (hs.2 <| erase_sup_Iic ha fun b hb ↦
      le_imp_eq_iff_le_imp_ge'.2 <| has hb).resolve_left (erase_lt.2 ha).ne⟩
  · rintro ⟨a, rfl⟩
    exact supIrred_Iic _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsUpperSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Tactic:
rw [← isLowerSet_compl, ← coe_compl] at h𝒜

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsLowerSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

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

Tactic:
by_cases hwu : w ∈ u

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 α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝¹ : v \ u = v
this✝ : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
⊢ False

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
⊢ s = ∅ → s ≠ {⊥}

Tactic:
rintro rfl
    exact (Set.singleton_nonempty _).ne_empty.symm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsUpperSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)

Tactic:
rw [← isLowerSet_compl, ← coe_compl] at h𝒜

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
⊢ IsInitSeg (∂ 𝒜) (r - 1)

Tactic:
by
  cases nonempty_fintype α
  obtain rfl | hr := Nat.eq_zero_or_pos r
  · have : 𝒜 ⊆ {∅} := fun s hs ↦ by rw [mem_singleton, ← Finset.card_eq_zero]; exact h₁.1 hs
    have := shadow_monotone this
    simp only [subset_empty, shadow_singleton_empty] at this
    simp [this]
  obtain rfl | h𝒜 := 𝒜.eq_empty_or_nonempty
  · simp
  obtain ⟨s, rfl, rfl⟩ := h₁.exists_initSeg h𝒜
  rw [shadow_initSeg (card_pos.1 hr), ← card_erase_of_mem (min'_mem _ _)]
  exact isInitSeg_initSeg

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

Goal state before:
pp: case inr
α : 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
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

Tactic:
refine h₂ ⟨UVd.mono (erase_subset ..) (erase_subset ..), ?_, ?_, ?_, ?_⟩ (card_erase_lt_of_mem Hx)

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

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.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : univ.PairwiseDisjoint fun i ↦ f i '' s i
x y : α
h : hs.piecewise f x = hs.piecewise f y
⊢ hs.index x = hs.index y

Tactic:
apply h_disjoint.elim trivial trivial

Goal state after:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : univ.PairwiseDisjoint fun i ↦ f i '' s i
x y : α
h : hs.piecewise f x = hs.piecewise f y
⊢ ¬Disjoint (f (hs.index x) '' s (hs.index x)) (f (hs.index y) '' s (hs.index y))
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
⊢ False

Tactic:
have : c = (puw.append pwv).append pvu := by simp [puw, pwv, pvu]

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
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: case refine_2.inr
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk : k ≠ 0
h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
s : Set (Sym2 V)
hs : s.encard < ↑(k + 1)
e : Sym2 V
he : e ∈ s
⊢ (G.deleteEdges s).Reachable u v

Tactic:
← Set.insert_sdiff_self_of_mem he,

Goal state after:
case refine_2.inr
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk : k ≠ 0
h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
s : Set (Sym2 V)
hs : s.encard < ↑(k + 1)
e : Sym2 V
he : e ∈ s
⊢ (G.deleteEdges (insert e (s \ {e}))).Reachable u v
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case inr
α : 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
⊢ ∑ a, μ a * f a ≤ ∑ a, μ a * g a

Tactic:
obtain rfl | hg := hg.eq_or_lt

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

case inr.inr
α : 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, μ a * f a ≤ ∑ a, μ a * g a
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_4
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ G.edist u v ≤ 2

Tactic:
obtain ⟨w, hw⟩ := h.2.2
    rw [mem_commonNeighbors] at hw
    have := (Walk.cons hw.1 <| .cons hw.2.symm .nil).edist_le
    simp_all

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

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

Tactic:
simp_all [edist_eq_two_iff]

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

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
p : (G ⊕g H).Walk (Sum.inl v) (Sum.inr w)
⊢ False

Tactic:
have hs : ∀ x : V ⊕ W, x ∉ Set.range .inl ↔ x ∈ Set.range .inr := by simp

Goal state after:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
p : (G ⊕g H).Walk (Sum.inl v) (Sum.inr w)
hs : ∀ (x : V ⊕ W), x ∉ Set.range Sum.inl ↔ x ∈ Set.range Sum.inr
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (induce (s ∪ t) G).Connected

Tactic:
rw [connected_induce_iff]
  rw [preconnected_induce_iff] at sconn tconn
  apply (Subgraph.connected_induce_top_sup sconn tconn hv hw ha).mono
  · 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]
  · simp only [Subgraph.verts_sup, Subgraph.induce_verts]
    rw [Set.union_assoc]
    simp [Set.insert_subset_iff, Set.singleton_subset_iff, hv, hw]

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

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

Tactic:
rw [connected_iff_exists_forall_reachable]

Goal state after:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
⊢ ∃ v, ∀ (w : ↑s), (induce s G).Reachable v w
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
u v : V
⊢ ↑(G.finsetWalkLengthLT n u v) = {p | p.length < n}

Tactic:
ext p
  simp [finsetWalkLengthLT, mem_finsetWalkLength_iff]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ ↑(G.finsetWalkLengthLT n u v) ↔ p ∈ {p | p.length < n}

Tactic:
coe_finsetWalkLengthLT_eq

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ {p | p.length < n} ↔ p ∈ {p | p.length < n}
Module: Mathlib.Combinatorics.SimpleGraph.Circulant

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s ∨ v - u ∈ s → u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
intro h1

Goal state after:
case mp
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s ∨ v - u ∈ s
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
Module: Mathlib.Combinatorics.SimpleGraph.Circulant

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0} → u - v ∈ s ∨ v - u ∈ s

Tactic:
intro h1

Goal state after:
case mpr
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
⊢ u - v ∈ s ∨ v - u ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case inr
V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
hnemp : Hs.Nonempty
⊢ (sSup Hs).IsAcyclic

Tactic:
· intro u p hp
    obtain ⟨H, hH, hpH⟩ := p.exists_mem_contains_edges_of_directed Hs hnemp h_dir
    exact h_acyc H hH (p.transfer H hpH) <| Walk.IsCycle.transfer hp hpH

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

Goal state before:
pp: case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ ↑(∑ x ∈ G.neighborFinset u, #(G.finsetWalkLength n x v)) =
    ↑(∑ u_1, #(Finset.map { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑u_1) v)))

Tactic:
simp only [Nat.cast_sum, card_map, neighborFinset_def]

Goal state after:
case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ ∑ x ∈ (G.neighborSet u).toFinset, ↑(#(G.finsetWalkLength n x v)) = ∑ x, ↑(#(G.finsetWalkLength n (↑x) v))
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case inl
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
⊢ ¬(↑(v + 1) % 2 = 0 ↔ ↑v % 2 = 0)

Tactic:
← Fin.even_iff_mod_of_even h,

Goal state after:
case inl
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
⊢ ¬(Even (v + 1) ↔ ↑v % 2 = 0)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case inl
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
⊢ ¬(Even (v + 1) ↔ ↑v % 2 = 0)

Tactic:
← Fin.even_iff_mod_of_even h,

Goal state after:
case inl
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
⊢ ¬(Even (v + 1) ↔ Even v)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case inr
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
⊢ ¬(↑u % 2 = 0 ↔ ↑(u + 1) % 2 = 0)

Tactic:
← Fin.even_iff_mod_of_even h,

Goal state after:
case inr
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
⊢ ¬(Even u ↔ ↑(u + 1) % 2 = 0)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case inr
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
⊢ ¬(Even u ↔ ↑(u + 1) % 2 = 0)

Tactic:
← Fin.even_iff_mod_of_even h,

Goal state after:
case inr
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
⊢ ¬(Even u ↔ Even (u + 1))
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 ⊂ G.edgeFinset

Tactic:
by simpa [deleteEdges, edgeFinset]

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
h : ¬G.IsCompleteMultipartite
⊢ ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂

Tactic:
by
  apply mt IsTrans.mk at h
  push Not at h
  obtain ⟨_, _, _, h1, h2, h3⟩ := h
  rw [adj_comm] at h1
  exact ⟨_, _, _, h3, h1, 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
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
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
ha : G.Adj v w
⊢ #large ≤ Fintype.card V

Tactic:
simpa using card_le_card large.subset_univ

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

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
u : α
⊢ ⊤.eccent u ≤ 1

Tactic:
eccent,

Goal state after:
α : Type u_1
inst✝ : Nontrivial α
u : α
⊢ ⨆ v, ⊤.edist u v ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inr
α : Type u_1
h✝ : Nontrivial α
u : α
⊢ 1 = ⊤.radius

Tactic:
radius_top

Goal state after:
case inr
α : Type u_1
h✝ : Nontrivial α
u : α
⊢ 1 = 1