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

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

Tactic:
rw [map_add, add_assoc, add_comm _ r', ← add_assoc, ← H'.1]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
⊢ (M ／ C).closure X = (M ／ C).E ∧ X ⊆ (M ／ C).E ↔ M.Spanning (X ∪ C) ∧ Disjoint X C

Tactic:
contract_closure_eq,

Goal state after:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
⊢ M.closure (X ∪ C) \ C = (M ／ C).E ∧ X ⊆ (M ／ C).E ↔ M.Spanning (X ∪ C) ∧ Disjoint X C
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
⊢ M.Spanning (X ∪ C ∩ M.E) → (Disjoint X (C ∩ M.E) ↔ Disjoint X C)

Tactic:
refine fun h ↦ ⟨fun hdj ↦ ?_, Disjoint.mono_right inter_subset_left⟩

Goal state after:
α : Type u_1
M : Matroid α
X C : Set α
h : M.Spanning (X ∪ C ∩ M.E)
hdj : Disjoint X (C ∩ M.E)
⊢ Disjoint X C
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ univ.sigma fun i ↦ (M i).E
hIX : I ⊆ X
h : ∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t
h' : X ⊆ univ.sigma fun i ↦ (M i).E
i : ι
⊢ Sigma.mk i ⁻¹' X ⊆ (M i).E

Tactic:
by simpa using preimage_mono (f := Sigma.mk i) h'

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ I = I ∩ M.E ∪ I ∩ N.E

Tactic:
rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hI.2.2]

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h_option.Heval
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
m : ℕ
d : σ →₀ ℕ
x : σ → R
Heval' : Polynomial.map (eval x) Q = 0
hx : ∀ (i : σ), x i ∈ S (Option.some i)
⊢ (eval x) (Q.coeff m) = 0

Tactic:
Polynomial.ext_iff

Goal state after:
case h_option.Heval
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
m : ℕ
d : σ →₀ ℕ
x : σ → R
Heval' : ∀ (n : ℕ), (Polynomial.map (eval x) Q).coeff n = Polynomial.coeff 0 n
hx : ∀ (i : σ), x i ∈ S (Option.some i)
⊢ (eval x) (Q.coeff m) = 0
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hm : m ∈ (P S i).support
⊢ ∃ e ≤ #S, m = single i e

Tactic:
have hP : Alon.P S i = .rename (fun _ ↦ i) (Alon.P S ()) := by simp [Alon.P]

Goal state after:
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hm : m ∈ (P S i).support
hP : P S i = (rename fun x ↦ i) (P S ())
⊢ ∃ e ≤ #S, m = single i e
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
q : Path b a
h : p.comp q = nil
hlen : (p.comp q).length = 0
⊢ p.length + q.length = 0

Tactic:
simpa [length_comp] using hlen

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

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
x v : SchreierGraph V ι
s : S
hs : ι s • v = x
⊢ (ι s)⁻¹ • ι s • v = v

Tactic:
inv_smul_smul

Goal state after:
V : Type u_1
M : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
x v : SchreierGraph V ι
s : S
hs : ι s • v = x
⊢ v = v
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ : U
p₁ : Path u v₁
⊢ ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨v₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨v₁, p₁⟩ = a₂

Tactic:
induction p₁ with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
⊢ e (if h : a ∈ lowerClosure ↑s then {b ∈ s | a ≤ b}.sup' ⋯ id else ⊤) =
    if h : e a ∈ lowerClosure ↑(map e.toEmbedding s) then {b ∈ map e.toEmbedding s | e a ≤ b}.sup' ⋯ id else ⊤

Tactic:
apply_dite e,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
⊢ (if h : a ∈ lowerClosure ↑s then e ({b ∈ s | a ≤ b}.sup' ⋯ id) else e ⊤) =
    if h : e a ∈ lowerClosure ↑(map e.toEmbedding s) then {b ∈ map e.toEmbedding s | e a ≤ b}.sup' ⋯ id else ⊤
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) ↑s
ha : a ∈ s
⊢ s.truncatedSup a = a

Tactic:
refine le_antisymm ?_ le_truncatedSup
  simp_rw [truncatedSup_of_mem (subset_lowerClosure ha), sup'_le_iff, mem_filter]
  rintro b ⟨hb, hab⟩
  exact (hs.eq ha hb hab).ge

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

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeSup α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
hs : a ∈ lowerClosure ↑s
ht : ∀ x ∈ t, ¬a ≤ x
⊢ (s ∪ t).truncatedSup a = s.truncatedSup a

Tactic:
simp only [truncatedSup_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty,
    lower_aux.2 (Or.inl hs)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeInf α
inst✝⁴ : SemilatticeInf β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE β
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
this : e a ∈ upperClosure ↑(map e.toEmbedding s) ↔ a ∈ upperClosure ↑s
⊢ e (if h : a ∈ upperClosure ↑s then {b ∈ s | b ≤ a}.inf' ⋯ id else ⊥) =
    if h : e a ∈ upperClosure ↑(map e.toEmbedding s) then {b ∈ map e.toEmbedding s | b ≤ e a}.inf' ⋯ id else ⊥

Tactic:
apply_dite e,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeInf α
inst✝⁴ : SemilatticeInf β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE β
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
this : e a ∈ upperClosure ↑(map e.toEmbedding s) ↔ a ∈ upperClosure ↑s
⊢ (if h : a ∈ upperClosure ↑s then e ({b ∈ s | b ≤ a}.inf' ⋯ id) else e ⊥) =
    if h : e a ∈ upperClosure ↑(map e.toEmbedding s) then {b ∈ map e.toEmbedding s | b ≤ e a}.inf' ⋯ id else ⊥
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
⊢ α ↪o Set { a // SupIrred a }

Tactic:
by
  by_cases! h : IsEmpty α
  · exact OrderEmbedding.ofIsEmpty
  have := Fintype.toOrderBot α
  exact OrderIso.lowerSetSupIrred.toOrderEmbedding.trans ⟨⟨_, SetLike.coe_injective⟩, Iff.rfl⟩

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

Goal state before:
pp: α : 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
this : Disjoint u (u \ v)
⊢ u = ⊥

Tactic:
rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this

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

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∈ 𝓒 u v s
hva : v ≤ a
hua : Disjoint u a
⊢ (a ⊔ u) \ v ∈ s

Tactic:
by
  rw [mem_compression, compress_of_disjoint_of_le hua hva] at ha
  obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := ha
  · exact ha
  have hu : u = ⊥ := by
    suffices Disjoint u (u \ v) by rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this
    refine hua.mono_right ?_
    rw [← compress_idem, compress_of_disjoint_of_le hua hva]
    exact sdiff_le_sdiff_right le_sup_right
  have hv : v = ⊥ := by
    rw [← disjoint_self]
    apply Disjoint.mono_right hva
    rw [← compress_idem, compress_of_disjoint_of_le hua hva]
    exact disjoint_sdiff_self_right
  rwa [hu, hv, compress_self, sup_bot_eq, sdiff_bot]

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

Goal state before:
pp: case neg.refine_2
α : 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 ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ ((t ⊔ u) \ v).erase a = (t.erase a ⊔ u) \ v

Tactic:
simp [← erase_sdiff_comm, erase_union_distrib, erase_eq_of_notMem hau]

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

Goal state before:
pp: case ind.inr.succ.h𝒜₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ 𝒜.Nonempty

pp: case ind.inr.succ.h𝒜₂
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ univ ∉ 𝒜

Tactic:
· exact h𝒜

Goal state after:
case ind.inr.succ.h𝒜₂
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ univ ∉ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Intersecting

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

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

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

Goal state before:
pp: case inr.cons.refine_1
ι : 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)
⊢ IsUpperSet ↑(s.biUnion f')

Tactic:
rw [coe_biUnion]
    exact isUpperSet_iUnion₂ fun i hi ↦ hf₂ _ <| subset_cons _ hi

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

Goal state before:
pp: case inr
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ #𝒜 * (Fintype.card α).choose (r - 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose r

Tactic:
rcases r with - | r
    · exact (hr rfl).elim
    rw [tsub_add_eq_add_tsub hr', add_tsub_add_eq_tsub_right] at h𝒜
    apply le_of_mul_le_mul_right _ (pos_iff_ne_zero.2 hr)
    convert! Nat.mul_le_mul_right ((Fintype.card α).choose r) h𝒜 using 1
    · simpa [mul_assoc, Nat.choose_succ_right_eq] using Or.inl (mul_comm _ _)
    · simp only [mul_assoc, choose_succ_right_eq, mul_eq_mul_left_iff]
      exact Or.inl (mul_comm _ _)

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

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
this : DecidableEq ι
hs : #s ≤ Fintype.card α
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)

Tactic:
induction s using Finset.cons_induction generalizing f with
  | empty => simp
  | cons i s hi ih =>
  set f' : ι → Finset (Finset α) :=
    fun j ↦ if hj : j ∈ cons i s hi then (hf j hj).exists_card_eq.choose else ∅
  have hf₁ : ∀ j, j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * #(f' j) =
      2 ^ Fintype.card α ∧ (f' j : Set (Finset α)).Intersecting := by
    rintro j hj
    simp_rw [f', dif_pos hj, ← Fintype.card_finset]
    exact Classical.choose_spec (hf j hj).exists_card_eq
  have hf₂ : ∀ j, j ∈ cons i s hi → IsUpperSet (f' j : Set (Finset α)) := by
    refine fun j hj ↦ (hf₁ _ hj).2.2.isUpperSet' ((hf₁ _ hj).2.2.is_max_iff_card_eq.2 ?_)
    rw [Fintype.card_finset]
    exact (hf₁ _ hj).2.1
  refine (card_le_card <| biUnion_mono fun j hj ↦ (hf₁ _ hj).1).trans ?_
  nth_rw 1 [cons_eq_insert i]
  rw [biUnion_insert]
  refine (card_mono <| @le_sup_sdiff _ _ (f' i) _).trans ((card_union_le _ _).trans ?_)
  rw [union_sdiff_left, sdiff_eq_inter_compl]
  refine le_of_mul_le_mul_left ?_ (pow_pos (zero_lt_two' ℕ) <| Fintype.card α + 1)
  rw [pow_succ, mul_add, mul_assoc, mul_comm _ 2, mul_assoc]
  refine (add_le_add
      ((mul_le_mul_iff_right₀ <| pow_pos (zero_lt_two' ℕ) _).2
      (hf₁ _ <| mem_cons_self _ _).2.2.card_le) <|
      (mul_le_mul_iff_right₀ <| zero_lt_two' ℕ).2 <| IsUpperSet.card_inter_le_finset ?_ ?_).trans ?_
  · rw [coe_biUnion]
    exact isUpperSet_iUnion₂ fun i hi ↦ hf₂ _ <| subset_cons _ hi
  · rw [coe_compl]
    exact (hf₂ _ <| mem_cons_self _ _).compl
  rw [mul_tsub, card_compl, Fintype.card_finset, mul_left_comm, mul_tsub,
    (hf₁ _ <| mem_cons_self _ _).2.1, two_mul, add_tsub_cancel_left, ← mul_tsub, ← mul_two,
    mul_assoc, ← add_mul, mul_comm]
  gcongr
  refine (add_le_add_right
    (ih _ (fun i hi ↦ (hf₁ _ <| subset_cons _ hi).2.2)
    ((card_le_card <| subset_cons _).trans hs)) _).trans ?_
  rw [mul_tsub, two_mul, ← pow_succ',
    ← add_tsub_assoc_of_le (pow_right_mono₀ (one_le_two : (1 : ℕ) ≤ 2) tsub_le_self),
    tsub_add_eq_add_tsub hs, card_cons, add_tsub_add_eq_tsub_right]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
s : Finset α
h₁ : s ∈ ∂ (falling n 𝒜)
h₂ : s ∈ 𝒜 # m
⊢ False

Tactic:
simp_rw [mem_shadow_iff, mem_falling] at h₁

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
s : Finset α
h₂ : s ∈ 𝒜 # m
h₁ : ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = n) ∧ ∃ a ∈ s_1, s_1.erase a = s
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
h : Nontrivial V
⊢ ¬⊥.Preconnected

Tactic:
simp [nontrivial_iff.mp h, Preconnected, reachable_bot]

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

Goal state before:
pp: n r k : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ #(∂^[k] 𝒞) ≤ #(∂^[k] 𝒜)

Tactic:
by
  induction k generalizing r 𝒜 𝒞 with
  | zero => simpa
  | succ _ ih =>
    refine ih h₁.shadow (kruskal_katona h₁ h₂ h₃) ?_
    convert! h₃.shadow

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

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
⊢ i + #B ≤ #range'k

Tactic:
by
          rwa [hB, card_attachFin, card_range, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ C.toSimpleGraph.Preconnected

Tactic:
by
    intro ⟨u, hu⟩ ⟨v, hv⟩
    exact C.reachable_toSimpleGraph hu hv

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

Goal state before:
pp: case map_rel'
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
C : G.Coloring (Fin n)
a b : β
left✝ : a ≠ b
w✝¹ w✝ : V
hadj : G.Adj w✝¹ w✝
ha : f w✝¹ = a
hb : f w✝ = b
⊢ (completeGraph (Fin n)).Adj (extend (⇑f) (⇑C) (const β default) a) (extend (⇑f) (⇑C) (const β default) b)

Tactic:
← ha,

Goal state after:
case map_rel'
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
C : G.Coloring (Fin n)
a b : β
left✝ : a ≠ b
w✝¹ w✝ : V
hadj : G.Adj w✝¹ w✝
ha : f w✝¹ = a
hb : f w✝ = b
⊢ (completeGraph (Fin n)).Adj (extend (⇑f) (⇑C) (const β default) (f w✝¹)) (extend (⇑f) (⇑C) (const β default) b)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ False

Tactic:
have : r ≤ n := h₃.trans (Nat.div_le_self n 2)

Goal state after:
case inr
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this✝ : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this : r ≤ n
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
C✝ : G.Coloring α✝
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring β
⊢ (G.recolorOfEmbedding f.toEmbedding) ((G.recolorOfEmbedding f.symm.toEmbedding) C) = C

Tactic:
by
    ext v
    apply Equiv.apply_symm_apply

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
⊢ G.Adj v w ∧ (G.deleteEdges {s(v, w)}).Reachable v w ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
rw [reachable_deleteEdges_iff_exists_walk]

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
⊢ (G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges) ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
⊢ G = ⊤

Tactic:
by
  classical
  by_contra! hh
  have : G.chromaticNumber ≤ Fintype.card V - 1 := by
    obtain ⟨a, b, hne, _⟩ := ne_top_iff_exists_not_adj.mp hh
    apply chromaticNumber_le_iff_colorable.mpr
    suffices G.Coloring (Finset.univ.erase b) by simpa using Coloring.colorable this
    apply Coloring.mk (fun x ↦ if h' : x ≠ b then ⟨x, by simp [h']⟩ else ⟨a, by simp [hne]⟩)
    grind [Adj.ne', adj_symm]
  rw [h, ← ENat.natCast_one, ← ENat.natCast_sub, ENat.natCast_le_natCast] at this
  have := Fintype.one_lt_card_iff_nontrivial.mpr <| SimpleGraph.nontrivial_iff.mp ⟨_, _, hh⟩
  grind

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

Goal state before:
pp: n : ℕ
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
hc : (completeMultipartiteGraph V).CliqueFree n
⊢ (completeMultipartiteGraph V).Colorable (n - 1)

Tactic:
cases n with
  | zero => exact absurd hc not_cliqueFree_zero
  | succ n =>
  have : Fintype ι := fintypeOfNotInfinite
    fun hinf ↦ not_cliqueFree_of_infinite V f hc
  apply (coloring V).colorable.mono
  have := not_cliqueFree_of_le_card V f le_rfl
  contrapose! this
  exact hc.mono this

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
⊢ ¬w.Nil

Tactic:
by grind [Walk.not_nil_of_ne]

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v

Tactic:
· simp only [huv, or_false]
    have h : 0 < G.edist u v := edist_pos_of_ne huv
    rw [(Order.one_le_iff_pos.mpr h).ge_iff_eq']
    exact edist_eq_one_iff_adj

Goal state after: