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

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
s t : Finset X
inst✝ : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
⊢ f.IsPrefix s → ¬f.IsPrefix t

Tactic:
hs

Goal state after:
X : Type u_1
inst✝¹ : Fintype X
s t : Finset X
inst✝ : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
⊢ ¬f.IsPrefix t
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
K : Set α
hK : M.Indep K
hKJ : J ⊆ K ∧ I ⊆ K
hKX : K ⊆ X ∪ I
⊢ K ⊆ J ∪ I

Tactic:
rw [hB.1.2 (t := K \ I) disjoint_sdiff_left (by simpa [sdiff_union_of_subset hKJ.2])
    (sdiff_subset_iff.2 (by rwa [union_comm])) (subset_sdiff.2 ⟨hKJ.1, hB.1.1.1.1⟩),
    sdiff_union_of_subset hKJ.2]

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

Goal state before:
pp: case h.refine_3
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' S)
hSX : S ⊆ X
hJS : univ.sigma Js ⊆ S
⊢ (univ.sigma fun i ↦ Sigma.mk i ⁻¹' S) ⊆ univ.sigma Js

Tactic:
refine sigma_mono rfl.subset fun i ↦ ?_

Goal state after:
case h.refine_3
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' S)
hSX : S ⊆ X
hJS : univ.sigma Js ⊆ S
i : ι
⊢ Sigma.mk i ⁻¹' S ⊆ Js i
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ X ⊆ I ∪ (M ／ I).loops

Tactic:
contract_loops_eq,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ X ⊆ I ∪ M.closure I \ I
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X = (M ／ C ／ X).loops ∪ M.closure (C ∪ X) \ C ∩ X

Tactic:
contract_loops_eq,

Goal state after:
α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X = (M ／ C).closure X \ X ∪ M.closure (C ∪ X) \ C ∩ X
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval : ∀ (x : PEmpty.{u_2 + 1} → R), (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) → (eval x) P = 0
m : PEmpty.{u_2 + 1} →₀ ℕ
this : m = 0
⊢ coeff m P = coeff m (C (constantCoeff P))

Tactic:
simp [this, ← constantCoeff_eq]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : IsStronglyConnected V
⊢ IsStronglyConnected (Symmetrify V)

Tactic:
intro a b

Goal state after:
V : Type u_2
inst✝ : Quiver V
h : IsStronglyConnected V
a b : Symmetrify V
⊢ Nonempty (Path a b)
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
⊢ (eval x) r = 0

Tactic:
rw [Iff.symm sub_eq_iff_eq_add'] at hf

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
⊢ (eval x) r = 0
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ s ∈ 𝓓 a 𝒜

Tactic:
← erase_insert ha

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ (insert a s).erase a ∈ 𝓓 a 𝒜
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
n : ℕ
s : Finset α
⊢ s ∈ powersetCard n univ →
    ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑n) * ↑((card α).choose n))

Tactic:
hs

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
n : ℕ
s : Finset α
hs : s ∈ powersetCard n univ
⊢ ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑n) * ↑((card α).choose n))
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ↑({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) → s ∈ {s | a ∈ s}

Tactic:
hs

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ ↑({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})
⊢ s ∈ {s | a ∈ s}
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case H
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ Function.Injective fun x ↦ x * m + 1

Tactic:
intro a b

Goal state after:
case H
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
a b : ℕ
⊢ (fun x ↦ x * m + 1) a = (fun x ↦ x * m + 1) b → a = b
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
⊢ ∀ (s t u : Finset α), s ○ t ○ u = s ○ (t ○ u)

Tactic:
refine (associative_of_commutative_of_le inferInstance ?_).assoc

Goal state after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
⊢ ∀ (a b c : Finset α), a ○ b ○ c ⊆ a ○ (b ○ c)
Module: Mathlib.Order.Irreducible

Goal state before:
pp: case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
i : ι
s : Finset ι
a✝ : i ∉ s
ih : s.sup f = a → ∃ i ∈ s, f i = a
h : (insert i s).sup f = a
⊢ f i = a ∨ ∃ x ∈ s, f x = a

Tactic:
rw [sup_insert] at h

Goal state after:
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
i : ι
s : Finset ι
a✝ : i ∉ s
ih : s.sup f = a → ∃ i ∈ s, f i = a
h : f i ⊔ s.sup f = a
⊢ f i = a ∨ ∃ x ∈ s, f x = a
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ birkhoffFinset (a ⊔ b) = birkhoffFinset a ∪ birkhoffFinset b

Tactic:
dsimp [OrderEmbedding.birkhoffFinset]

Goal state after:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ Fintype.finsetEquivSet.symm (birkhoffSet (a ⊔ b)) =
    Fintype.finsetEquivSet.symm (birkhoffSet a) ∪ Fintype.finsetEquivSet.symm (birkhoffSet b)
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ birkhoffFinset (a ⊓ b) = birkhoffFinset a ∩ birkhoffFinset b

Tactic:
dsimp [OrderEmbedding.birkhoffFinset]

Goal state after:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ Fintype.finsetEquivSet.symm (birkhoffSet (a ⊓ b)) =
    Fintype.finsetEquivSet.symm (birkhoffSet a) ∩ Fintype.finsetEquivSet.symm (birkhoffSet b)
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ infSum (𝒜 ∪ ℬ) + infSum (𝒜 ⊻ ℬ) = infSum 𝒜 + infSum ℬ

Tactic:
by
  unfold infSum
  rw [← sum_add_distrib, ← sum_add_distrib, Finset.sum_congr rfl fun s _ ↦ _]
  simp_rw [← add_div, ← Nat.cast_add, card_truncatedInf_union_add_card_truncatedInf_sups]
  simp

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

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : compress u v b ∉ s
hu : u = ⊥
hv : v = ⊥
⊢ (compress u v b ⊔ u) \ v ∈ s

Tactic:
hu,

Goal state after:
case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : compress u v b ∉ s
hu : u = ⊥
hv : v = ⊥
⊢ (compress ⊥ v b ⊔ ⊥) \ v ∈ s
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : #t + (k + 1) = #s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : #u = #t + 1
⊢ #u + k = #s

Tactic:
hu,

Goal state after:
case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : #t + (k + 1) = #s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : #u = #t + 1
⊢ #t + 1 + k = #s
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
⊢ s.Intersecting ↔ s = ∅

Tactic:
refine
    subsingleton_of_subsingleton.intersecting.trans
      ⟨not_imp_comm.2 fun h => subsingleton_of_subsingleton.eq_singleton_of_mem ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
h : ¬s = ∅
⊢ ⊥ ∈ s

case refine_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
⊢ s = ∅ → s ≠ {⊥}
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 = insert a s
ht : t ∈ 𝒜
⊢ f t ≤ collapse 𝒜 a f s

Tactic:
rw [collapse_eq ha, ← hts, if_pos ht]
  split_ifs
  · exact le_add_of_nonneg_left <| hf _
  · rw [zero_add]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ s ∈ 𝒜.biUnion powerset

Tactic:
mem_biUnion,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ ∃ a ∈ 𝒜, s ∈ a.powerset
Module: Mathlib.Combinatorics.SetFamily.LYM

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

Tactic:
hs

Goal state after:
case mp.inr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ k + 1 - 1 = k
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 : succ 0 = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = #U
this : U.erase x = ∅
⊢ V.erase (V.min' hV) = ∅

Tactic:
rw [← Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ← same_size]

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

Goal state before:
pp: case ha
α : 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 ∉ ℬ
⊢ 0 ≤ f₄ (s ∪ t) + f₄ (insert a s ∪ t)

pp: case hbc
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∉ ℬ
⊢ f₃ (s ∩ t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t)

Tactic:
exacts [add_nonneg (h₄ _) <| h₄ _, le_collapse_of_mem ‹_› h₃ rfl <| inter_mem_infs ‹_› ‹_›]

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
⊢ #s + 1 = k + 1

Tactic:
hs

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
⊢ k + 1 = k + 1
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

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

Tactic:
← card_pos,

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
⊢ 0 < #(U.erase x)
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case zero
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
hk : 0 ≤ Fintype.card α
⊢ ∑ r ∈ range (0 + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
    ↑(#(falling (Fintype.card α - 0) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - 0))

Tactic:
simp only [cast_one, cast_le, sum_singleton, div_one, choose_self, range_one,
      zero_add, range_one, sum_singleton,
      choose_self, cast_one, div_one, cast_le, tsub_zero]
    exact card_le_card (slice_subset_falling _ _)

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∉ ℬ
⊢ (f₁ s + f₁ (insert a s)) * (0 + 0) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
· rw [add_zero, mul_zero]
      exact mul_nonneg (collapse_nonneg h₃ _) <| collapse_nonneg h₄ _

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

Goal state before:
pp: case mpr
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ {x | (mkClasses c H) x y} → x ∈ s

Tactic:
· intro hx
    obtain ⟨b', ⟨hc, hb'⟩, _⟩ := H x
    rwa [eq_of_mem_eqv_class H hs hy hc (hx b' hc hb')]

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

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
i : α
hi : ∀ (a : V), C a ≠ i
D : G.Coloring { a // a ≠ i } := { toFun := fun v ↦ ⟨C v, ⋯⟩, map_rel' := ⋯ }
⊢ False

Tactic:
exact Nat.notMem_of_lt_sInf ((Nat.sub_one_lt_of_lt <| card_pos_iff.2 ⟨i⟩).trans_le h)
      ⟨G.recolorOfEquiv (equivOfCardEq <| by simp) D⟩

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 α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s.erase a ⊆ u ∧ ¬s ⊆ u
hs : s.erase a = s
⊢ False

Tactic:
hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s ⊆ u ∧ ¬s ⊆ u
hs : s.erase a = s
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty

Tactic:
H.connected_iff',

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.coe.Connected ↔ H.Preconnected ∧ H.verts.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hv : v ∈ s
⊢ G.degree v ≤ (between (↑s) (↑s)ᶜ G).degree v + #s

Tactic:
have h_bipartite : (G.between s sᶜ).IsBipartiteWith s ↑(sᶜ) := by
    simpa using between_isBipartiteWith disjoint_compl_right
  simp_rw [← card_neighborFinset_eq_degree,
    ← card_union_of_disjoint (isBipartiteWith_neighborFinset_disjoint h_bipartite hv)]
  exact card_le_card (neighborFinset_subset_between_union hv)

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

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

Tactic:
simpa [extend_apply' _ _ _ hs] using! mul_nonneg
      (extend_nonneg (fun a : L ↦ h₃ a) le_rfl _) (extend_nonneg (fun a : L ↦ h₄ a) le_rfl _)

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 : G.edist u v = 2
⊢ (G.commonNeighbors u v).Nonempty

Tactic:
obtain ⟨w, hw⟩ := exists_walk_of_edist_eq_coe h
    use w.getVert 1
    suffices w.getVert 1 ∈ G.commonNeighbors (w.getVert 0) (w.getVert w.length) by simpa
    refine hw ▸ G.mem_commonNeighbors.mp ?_
    exact ⟨w.adj_getVert_succ (by simp [hw]), (w.adj_getVert_succ (by simp [hw])).symm⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
p : G.Walk u v
hp : p.length = G.dist u v
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
obtain ⟨q, hq⟩ := hconn.exists_walk_length_eq_dist v w

Goal state after:
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
p : G.Walk u v
hp : p.length = G.dist u v
q : G.Walk v w
hq : q.length = G.dist v w
⊢ G.dist u w ≤ G.dist u v + G.dist v w
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n✝ : ℕ
⊢ DecidableRel (cycleGraph (n✝ + 2)).Adj

Tactic:
unfold cycleGraph

Goal state after:
n✝ : ℕ
⊢ DecidableRel
    (match n✝ + 2 with
      | 0 => ⊥
      | 1 => ⊥
      | n.succ.succ => { Adj := fun a b ↦ a - b = 1 ∨ b - a = 1, symm := ⋯, loopless := ⋯ }).Adj
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n✝ : ℕ
⊢ DecidableRel (cycleGraph (n✝ + 2)).Adj

Tactic:
by unfold cycleGraph; infer_instance

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

Goal state before:
pp: n : ℕ
u v : Fin 1
⊢ (cycleGraph 1).Adj u v ↔ ↑(u - v) = 1 ∨ ↑(v - u) = 1

Tactic:
simp [cycleGraph_one_adj]

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

Goal state before:
pp: case refine_2
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
⊢ cycleGraph n ⊑ G

Tactic:
refine ⟨⟨⟨fun n ↦ p.support[n.succ]'(?_), ?_⟩, ?_⟩⟩

Goal state after:
case refine_2.refine_1
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✝
n : Fin n✝
⊢ ↑n.succ < p.support.length

case refine_2.refine_2
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
⊢ ∀ {a_1 b : Fin n}, (cycleGraph n).Adj a_1 b → G.Adj p.support[a_1.succ] p.support[b.succ]

case refine_2.refine_3
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
⊢ Function.Injective ⇑{ toFun := fun n_1 ↦ p.support[n_1.succ], map_rel' := ?refine_2.refine_2 }
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsAdjMatrix
f : W → V
i j : W
⊢ A.submatrix f f i j = 0 ∨ A.submatrix f f i j = 1

Tactic:
by simp [h.zero_or_one]

Goal state after: