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

Goal state before:
pp: case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
i : ι
hi : i ∈ s
⊢ x = ↑(↑l ⟨x, xs⟩ i)

Tactic:
hs,

Goal state after:
case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
i : ι
hi : i ∈ {i | l.idxFun i = none}
⊢ x = ↑(↑l ⟨x, xs⟩ i)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
i : ι
hi : i ∈ sᶜ
⊢ (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0 = ↑(↑l ⟨x, xs⟩ i)

Tactic:
hs,

Goal state after:
case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
i : ι
hi : i ∈ {i | l.idxFun i = none}ᶜ
⊢ (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0 = ↑(↑l ⟨x, xs⟩ i)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
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 τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
this : (rename ⇑e.symm) P = 0
⊢ P = 0

Tactic:
have that := MvPolynomial.rename_injective (R := R) e.symm (e.symm.injective)

Goal state after:
R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
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 τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
this : (rename ⇑e.symm) P = 0
that : Injective ⇑(rename ⇑e.symm)
⊢ P = 0
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 : (eval default) (C (constantCoeff P)) = 0
this : P = C (constantCoeff P)
⊢ P = 0

Tactic:
eval_C

Goal state after:
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 : constantCoeff P = 0
this : P = C (constantCoeff P)
⊢ P = 0
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : 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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
hc' : c ∉ r'.support
this : c ∉ r'.support → c ∈ ((monomial (m.degree f)) (m.leadingCoeff f)).support
⊢ c = m.degree f

Tactic:
simpa only [Finset.mem_singleton] using support_monomial_subset (this hc')

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.right.right
σ : 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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∀ c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
intro c hc i
        by_cases hc' : c ∈ r'.support
        · exact H'.2.2 c hc' i
        · convert! hf i
          classical
          have := MvPolynomial.support_add hc
          rw [Finset.mem_union, Classical.or_iff_not_imp_left] at this
          simpa only [Finset.mem_singleton] using support_monomial_subset (this hc')

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
hj : ¬j = i
⊢ (mapDomain (fun x ↦ i) e) j = (single i (e ())) j

Tactic:
rw [mapDomain_of_notMem_range, single_eq_of_ne hj]
      simp [Set.range_const, Set.mem_singleton_iff, hj]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Weight

Goal state before:
pp: V : Type u_1
inst✝¹ : Quiver V
R : Type u_2
inst✝ : Monoid R
w : {i j : V} → (i ⟶ j) → R
a b c : V
p : Path a b
q : Path b c
⊢ weight (fun {i j} ↦ w) (p.comp q) = weight (fun {i j} ↦ w) p * weight (fun {i j} ↦ w) q

Tactic:
induction q with
  | nil => simp
  | cons _ _ ih => simp [ih, mul_assoc]

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case neg
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
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : Finsupp.degree (degLex.degree (h i * Alon.P (S i) i)) ≤ f.totalDegree
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0

Tactic:
degree_mul_of_isRegular_right hi (by simp only [(Alon.monic_P ..).leadingCoeff_eq_one,
      isRegular_one]),

Goal state after:
case neg
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
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : Finsupp.degree (degLex.degree (h i) + degLex.degree (Alon.P (S i) i)) ≤ f.totalDegree
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ schnirelmannDensity A = 1 ↔ A = Set.univ

Tactic:
rw [schnirelmannDensity_eq_one_iff]

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ {0}ᶜ ⊆ A ↔ A = Set.univ
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized (r - k) ↑(∂^[k] 𝒜)

Tactic:
simp_rw [Set.Sized, mem_coe, mem_shadow_iterate_iff_exists_sdiff]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ ∀ ⦃x : Finset α⦄, (∃ s ∈ 𝒜, x ⊆ s ∧ #(s \ x) = k) → #x = r - k
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 a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
hba : compress u v b = a
⊢ u ≤ a

Tactic:
unfold compress at hba

Goal state after:
case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
hba : (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) = a
⊢ u ≤ a
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 a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
hba : compress u v b = a
⊢ Disjoint v a

Tactic:
unfold compress at hba

Goal state after:
case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
hba : (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) = a
⊢ Disjoint v a
Module: Mathlib.Order.Birkhoff

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

Tactic:
by
  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.Compression.UV

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
hba : compress u v b = a
⊢ (a ⊔ v) \ u ∈ s

Tactic:
unfold compress at hba

Goal state after:
case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
hba : (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) = a
⊢ (a ⊔ v) \ u ∈ s
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
⊢ (if h : IsEmpty α then ofIsEmpty
      else
        have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊔ b) =
    (if h : IsEmpty α then ofIsEmpty
        else
          have this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∪
      (if h : IsEmpty α then ofIsEmpty
        else
          have this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b

Tactic:
split

Goal state after:
case isTrue
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : IsEmpty α
⊢ ofIsEmpty (a ⊔ b) = ofIsEmpty a ∪ ofIsEmpty b

case isFalse
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : ¬IsEmpty α
⊢ (have this := Fintype.toOrderBot α;
      RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
        { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊔ b) =
    (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∪
      (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
⊢ (if h : IsEmpty α then ofIsEmpty
      else
        have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊓ b) =
    (if h : IsEmpty α then ofIsEmpty
        else
          have this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∩
      (if h : IsEmpty α then ofIsEmpty
        else
          have this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b

Tactic:
split

Goal state after:
case isTrue
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : IsEmpty α
⊢ ofIsEmpty (a ⊓ b) = ofIsEmpty a ∩ ofIsEmpty b

case isFalse
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : ¬IsEmpty α
⊢ (have this := Fintype.toOrderBot α;
      RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
        { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊓ b) =
    (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∩
      (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case refine_2
α : 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 ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 ↦ x1 ⊆ x2) 𝒜 s) ≤ #(image (fun a ↦ insert a s) sᶜ)

Tactic:
refine card_le_card fun t ht => ?_

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ bipartiteAbove (fun x1 x2 ↦ x1 ⊆ x2) 𝒜 s
⊢ t ∈ image (fun a ↦ insert a s) sᶜ
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

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

Tactic:
r₁

Goal state after:
case mpr.inr.inr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
ha : k ∈ s
⊢ k ∈ insert k t
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
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ 1 < #V

Tactic:
rwa [← same_size]

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

Goal state before:
pp: n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
⊢ familyMeasure ({a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜}) < familyMeasure 𝒜

Tactic:
have ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty := by
    contrapose! a
    rw [filter_image, a, image_empty, union_empty]
    rwa [a, union_empty] at uA

Goal state after:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
⊢ familyMeasure ({a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜}) < familyMeasure 𝒜
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
u : Finset α
hu : u ∈ 𝒜 ∧ a ∉ u
hsu : s ∩ u = t.erase a
⊢ insert a s ∩ u = t

Tactic:
insert_inter_of_notMem hu.2,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
u : Finset α
hu : u ∈ 𝒜 ∧ a ∉ u
hsu : s ∩ u = t.erase a
⊢ s ∩ u = t
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
obtain ⟨v, hv, hsv⟩ := hs <| insert_subset ha ht
    rw [Down.mem_compression] at hv
    obtain hv | hv := hv
    · refine ⟨erase v a, hv.2, ?_⟩
      rw [inter_erase, hsv, erase_insert]
      rintro ha
      rw [insert_eq_self.2 (mem_inter.1 ha).2] at hu
      exact hu.1 hu.2
    rw [insert_eq_self.2 <| inter_subset_right (s₁ := s) ?_] at hv
    cases hv.1 hv.2
    rw [hsv]
    exact mem_insert_self _ _

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : G.connectedComponentMk v = c
hc' : G.connectedComponentMk v = c'
⊢ c = c'

Tactic:
rw [← hc, ← hc']

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.IsBridge s(u, v)
hreach : G.Reachable u v
⊢ G.deleteEdges {s(u, v)} ≠ G

Tactic:
by grind [isBridge_iff]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
⊢ ∀ (i : ℕ), G'.Colorable i → ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑i

Tactic:
intro m hc

Goal state after:
V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
m : ℕ
hc : G'.Colorable m
⊢ ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑m
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ v ∈ s.attach, #(bipartiteAbove G.Adj t ↑v) = ∑ x ∈ t.attach, #(G.neighborFinset ↑x)

Tactic:
conv_rhs =>
    rhs; intro w
    rw [isBipartiteWith_bipartiteBelow h w.prop]

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ v ∈ s.attach, #(bipartiteAbove G.Adj t ↑v) = ∑ w ∈ t.attach, #(bipartiteBelow G.Adj s ↑w)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: case neg.inl
V : Type u_1
G : SimpleGraph V
u v : V
huv : G.Adj u v
hc : ¬G.IsEdgeReachable 2 u v
hr : (G.deleteEdges {s(u, v)}).Reachable (u, v).1 (u, v).2
hs₂ : {s(u, v)}.encard < ↑2
hs₁ : {s(u, v)}.encard = ↑1
⊢ (G.deleteEdges {s(u, v)}).Reachable u v

Tactic:
exact hr

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected
v : ↑H.verts
inst✝ : Fintype ↑(H.neighborSet ↑v)
⊢ H.degree ↑v = 0 ↔ H.verts.Subsingleton

Tactic:
refine ⟨fun hv ↦ Set.not_nontrivial_iff.mp fun hn ↦ ?_, (degree_eq_zero_of_subsingleton H _ ·)⟩
  have := hn.coe_sort
  simpa [hv] using h.coe.degree_pos_of_nontrivial v

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.dropUntil u h).toSubgraph ⊔ (c.takeUntil u h).toSubgraph = c.toSubgraph

Tactic:
sup_comm,

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.takeUntil u h).toSubgraph ⊔ (c.dropUntil u h).toSubgraph = c.toSubgraph
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

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

Tactic:
sup_comm,

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