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

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

Tactic:
rw [← subset_singleton_iff', subset_singleton_iff] at hu

Goal state after:
case empty
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : 𝒜 = ∅ ∨ 𝒜 = {∅}
⊢ p 𝒜
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ {s ∈ 𝒜 | s.erase a ∈ 𝒜}.disjUnion ({s ∈ image (fun s ↦ s.erase a) 𝒜 | s ∉ 𝒜}) ⋯ ↔
    s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜

Tactic:
mem_disjUnion,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ {s ∈ 𝒜 | s.erase a ∈ 𝒜} ∨ s ∈ {s ∈ image (fun s ↦ s.erase a) 𝒜 | s ∉ 𝒜} ↔
    s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℝ
⊢ schnirelmannDensity A < x ↔ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < x

Tactic:
← not_le,

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℝ
⊢ ¬x ≤ schnirelmannDensity A ↔ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < x
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁ : i < n + 1
⊢ f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))

Tactic:
have h₁ := le_of_lt_succ h₁

Goal state after:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
⊢ f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case succ
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
⊢ n ∈ A + B

Tactic:
by_cases hnA : n ∈ A

Goal state after:
case pos
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 + B

case neg
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 + B
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq β
inst✝³ : SemilatticeInf α
inst✝² : SemilatticeInf β
inst✝¹ : FunLike F α β
inst✝ : InfHomClass 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:
simpa [map_eq_image] using image_infs f s t

Goal state after:
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 : α
⊢ b ⊓ c ≤ a → b ≤ a ∨ c ≤ a

Tactic:
← sup_eq_left,

Goal state after:
α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ a ⊔ b ⊓ c = a → a ⊔ b = a ∨ a ⊔ c = a
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : Disjoint u a ∧ v ⊆ a
⊢ #(a ∪ u) - #v = #a

Tactic:
card_union_of_disjoint h.1.symm,

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : Disjoint u a ∧ v ⊆ a
⊢ #a + #u - #v = #a
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 ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∉ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s

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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s

Tactic:
· obtain ⟨hus, hvs, h, _⟩ := H _ hs' hs
      exact Or.inr ⟨hs, _, h, compress_of_disjoint_of_le' hvs hus⟩

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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

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

Tactic:
inter_comm,

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
h : ∃ t, (↑t).Intersecting ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting

Tactic:
obtain ⟨t, ht, hst⟩ := h

Goal state after:
case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
t : Finset α
ht : (↑t).Intersecting
hst : s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case refine_1
α : 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 ∈ 𝒜
⊢ r ≤ #(bipartiteBelow (fun x1 x2 ↦ x1 ⊆ x2) (∂ 𝒜) s)

Tactic:
rw [← h𝒜 hs, ← card_image_of_injOn s.erase_injOn]

Goal state after:
case refine_1
α : 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 ∈ 𝒜
⊢ #(image s.erase s) ≤ #(bipartiteBelow (fun x1 x2 ↦ x1 ⊆ x2) (∂ 𝒜) s)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : 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
⊢ #s = #t + 1

Tactic:
← ‹_ = #t›,

Goal state after:
α : 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
⊢ #s = #(s.erase (s.min' hs)) + 1
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : compress U V s ≠ s
⊢ toColex (compress U V s) < toColex s

Tactic:
compress,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (if Disjoint U s ∧ V ⊆ s then (s ⊔ U) \ V else s) ≠ s
⊢ toColex (compress U V s) < toColex s
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ⊆ s) ∧ (s ⊔ U) \ V ≠ s
⊢ toColex (compress U V s) < toColex s

Tactic:
compress,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ⊆ s) ∧ (s ⊔ U) \ V ≠ s
⊢ toColex (if Disjoint U s ∧ V ⊆ s then (s ⊔ U) \ V else s) < toColex s
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : 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 𝒜)) ≤ #(∂ 𝒜)

Tactic:
refine card_shadow_compression_le _ _ fun x Hx ↦ ⟨min' V hV, min'_mem _ _, ?_⟩

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
x : α
Hx : x ∈ U
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s))⁻¹ =
    ∑ r ∈ range (Fintype.card α + 1), ∑ s ∈ 𝒜 with #s = r, (↑((Fintype.card α).choose r))⁻¹

Tactic:
by
      rw [sum_fiberwise_of_maps_to']; simp [card_le_univ]

Goal state after:
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:
eq_of_mem_eqv_class H hs' hx' hs hx

Goal state after:
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
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber ≤ ↑n + 1 ∧ ↑n < G.chromaticNumber ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n

Tactic:
← not_le,

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber ≤ ↑n + 1 ∧ ¬G.chromaticNumber ≤ ↑n ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
this : card V ≤ card V - 1
⊢ False

Tactic:
have := Fintype.one_lt_card_iff_nontrivial.mpr <| SimpleGraph.nontrivial_iff.mp ⟨_, _, hh⟩

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
this✝ : card V ≤ card V - 1
this : 1 < card V
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
⊢ ∃ a, C a = b

Tactic:
have w := Classical.arbitrary W

Goal state after:
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
⊢ ∃ a, C a = b
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case neg
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
he' : ¬C (Sum.inr w) = b
⊢ ∃ a, C a = b

Tactic:
· simpa using two_lt_card_iff.2 ⟨_, _, _, C.valid h, he, he'⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s✝ t✝ : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s✝ ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s✝
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
s t : Finset β
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 s * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (s ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (s ∪ t)

Tactic:
obtain ⟨a, rfl⟩ | hs := em (∃ a, g a = s)

Goal state after:
case refine_1.inl
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t✝ : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
t : Finset β
a : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ∪ t)

case refine_1.inr
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s✝ t✝ : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s✝ ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s✝
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
s t : Finset β
hs : ¬∃ a, g a = s
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 s * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (s ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (s ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ p.toSubgraph.neighborSet v = {p.penultimate}

Tactic:
simpa using IsPath.neighborSet_toSubgraph_startpoint hp.reverse
      (by rw [Walk.not_nil_iff_lt_length, Walk.length_reverse]; exact
        Walk.not_nil_iff_lt_length.mp hnp)

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
hne : u ≠ v
hnadj : ¬G.Adj u v
⊢ ¬1 = G.dist u v

Tactic:
by_contra hc
    obtain ⟨p, hp⟩ := Reachable.exists_walk_length_eq_dist h
    exact hnadj (Walk.exists_length_eq_one_iff.mp ⟨p, hc ▸ hp⟩)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
this : p.bypass = p
⊢ p.bypass.IsPath

Tactic:
apply Walk.bypass_isPath

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

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
h : ∃ x ∈ s, x ∈ p.support
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅

Tactic:
obtain ⟨x, hxs, hx⟩ := h

Goal state after:
case h
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : ↑(G.subgraphOfAdj h).verts
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this✝ : s(u, v) = s(↑w, ↑p.snd)
this : s(u, v) = s(↑p.penultimate, ↑w)
⊢ False

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. The original proof was:
  `grind [Sym2.eq_iff, IsCycle.snd_ne_penultimate]` -/

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : ↑(G.subgraphOfAdj h).verts
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this✝ : s(u, v) = s(↑w, ↑p.snd)
this : s(u, v) = s(↑p.penultimate, ↑w)
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e
v : V
c : G.Walk v v
hc : c.IsCycle
⊢ c.edges ≠ []

Tactic:
by simp [hc.not_nil]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∈ q.support
⊢ q = p.concat hadj

Tactic:
by
  have hw : w ∉ p.support := hG.ne_mem_support_of_support_of_adj_of_isPath hq hp hadj.symm hv
  exact Subtype.mk.inj <| hG.subsingleton_path u w |>.elim ⟨q, hq⟩ ⟨_, hp.concat hw hadj⟩

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : AddZeroClass α
inst✝¹ : One α
H : SimpleGraph V
inst✝ : DecidableRel H.Adj
h : IsCompl G H
this : Gᶜ = H
⊢ adjMatrix α G + adjMatrix α H = adjMatrix α G + adjMatrix α Gᶜ

Tactic:
subst this

Goal state after:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : AddZeroClass α
inst✝¹ : One α
inst✝ : DecidableRel Gᶜ.Adj
h : IsCompl G Gᶜ
⊢ adjMatrix α G + adjMatrix α Gᶜ = adjMatrix α G + adjMatrix α Gᶜ
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
hr : 0 < r
⊢ (turanGraph n r).CliqueFree (r + 1)

Tactic:
by
  rw [cliqueFree_iff]
  by_contra! ⟨f⟩
  obtain ⟨x, y, d, c⟩ := exists_ne_map_eq_of_card_lt (fun x ↦
    (⟨(f x).1 % r, Nat.mod_lt _ hr⟩ : Fin r)) (by simp)
  rw [Fin.mk.injEq] at c
  exact absurd c <| f.toHom.map_adj d

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
⊢ Odd p.length ↔ (¬c u = true ↔ c v = true)

Tactic:
rw [← Nat.not_even_iff_odd, c.even_length_iff_congr p]
  tauto

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

Goal state before:
pp: n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : u - v = 1
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (Even x ↔ Even y)

Tactic:
simp [Nat.even_iff]; lia

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

Goal state before:
pp: n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : v - u = 1
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (Even x ↔ Even y)

Tactic:
simp [Nat.even_iff]; lia

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
⊢ Nonempty (G ≃g turanGraph (Fintype.card V) r)

Tactic:
obtain ⟨zm, zp⟩ := h.isEquipartition.exists_partPreservingEquiv
  use (Equiv.subtypeUnivEquiv mem_univ).symm.trans zm
  intro a b
  simp_rw [turanGraph_adj, Equiv.trans_apply, Equiv.subtypeUnivEquiv_symm_apply]
  have := zp ⟨a, mem_univ a⟩ ⟨b, mem_univ b⟩
  rw [← h.not_adj_iff_part_eq] at this
  rw [← not_iff_not, not_ne_iff, this, card_parts]
  rcases le_or_gt r (card V) with c | c
  · rw [min_eq_right c]; rfl
  · have lc : ∀ x, zm ⟨x, _⟩ < card V := fun x ↦ (zm ⟨x, mem_univ x⟩).2
    rw [min_eq_left c.le, Nat.mod_eq_of_lt (lc a), Nat.mod_eq_of_lt (lc b),
      ← Nat.mod_eq_of_lt ((lc a).trans c), ← Nat.mod_eq_of_lt ((lc b).trans c)]; rfl

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

Goal state before:
pp: case e_a
n r : ℕ
⊢ (∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0) = ∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0

pp: case e_a
n r : ℕ
⊢ (∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
      ((∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
        ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
· simp [← Fin.sum_univ_eq_sum_range]

Goal state after:
case e_a
n r : ℕ
⊢ (∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
      ((∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
        ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.ediam = ⊤
⊢ G.diam = 0

Tactic:
rw [diam, h, ENat.toNat_top]

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

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

Tactic:
radius_bot

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