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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ K * ↑(#A) ∈ K •> map Nat.castEmbedding (Icc 1 t)

Tactic:
· apply smul_mem_smul_finset
      apply mem_map_of_mem
      exact mem_Icc.2 ⟨Nat.one_le_iff_ne_zero.mpr hA.card_ne_zero, hAt⟩

Goal state after:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
⊢ 0 < connectivity K S

Tactic:
obtain ⟨A, hA, hSA⟩ := exists_nonempty_isFragment hK hS
  exact (expansion_pos hK hS hA).trans_eq hSA

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: case succ
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
⊢ (n + 1) * 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2

Tactic:
mul_one,

Goal state after:
case succ
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
⊢ n + 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: case succ
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
⊢ (n + 1) * 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2

Tactic:
mul_one,

Goal state after:
case succ
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
⊢ n + 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ A, #S ≤ #A ∧ ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
⊢ ∃ H x Z, ↑(Fintype.card ↥H) ≤ (2 / ε - 1) * ↑(#S) ∧ ↑(#Z) ≤ 2 / ε - 1 ∧ ↑S ⊆ ↑H * ↑Z

Tactic:
obtain ⟨Z, hZS, hHZS, hZinj⟩ := exists_subset_mul_eq_mul_injOn H S

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ A, #S ≤ #A ∧ ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
⊢ ∃ H x Z, ↑(Fintype.card ↥H) ≤ (2 / ε - 1) * ↑(#S) ∧ ↑(#Z) ≤ 2 / ε - 1 ∧ ↑S ⊆ ↑H * ↑Z
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun n ↦ x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))
hlhs : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hrhs : Summable fun k ↦ (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
htail :
  Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
    atTop (𝓝 0)
h :
  ∀ (n : ℕ),
    ∏' (n : ℕ), (1 - x ^ (n + 1)) -
        (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x =
      ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))
h1 : ∀ (k : ℕ), pentagonal (↑k + 1) = (k + 1) * (3 * k + 2) / 2
⊢ Tendsto ((fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * (x ^ pentagonal (-↑i) - x ^ pentagonal (↑i + 1))) ∘ fun a ↦ a + 1)
    atTop (𝓝 (∏' (n : ℕ), (1 - x ^ (n + 1))))

Tactic:
have h2 (k : ℕ) : pentagonal (-k) = (k * (3 * k + 1) / 2) := by grind [pentagonal_neg]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun n ↦ x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))
hlhs : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hrhs : Summable fun k ↦ (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
htail :
  Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
    atTop (𝓝 0)
h :
  ∀ (n : ℕ),
    ∏' (n : ℕ), (1 - x ^ (n + 1)) -
        (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x =
      ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))
h1 : ∀ (k : ℕ), pentagonal (↑k + 1) = (k + 1) * (3 * k + 2) / 2
h2 : ∀ (k : ℕ), pentagonal (-↑k) = k * (3 * k + 1) / 2
⊢ Tendsto ((fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * (x ^ pentagonal (-↑i) - x ^ pentagonal (↑i + 1))) ∘ fun a ↦ a + 1)
    atTop (𝓝 (∏' (n : ℕ), (1 - x ^ (n + 1))))
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ EqOn H.Inc G.Inc E(H)

Tactic:
rintro e he
  ext x
  exact hHG.inc_congr he

Goal state after:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case hab
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ ↑(#((↑H).toFinset * S)) ≤ (1 - ε / 2) * ↑(#(↑H).toFinset) + K * ↑(#((↑H).toFinset * S))

Tactic:
calc
          (#(Set.toFinset H * S) : ℝ)
      _ = K * #(H : Set G).toFinset + (#(Set.toFinset H * S) - K * #(H : Set G).toFinset) := by ring
      _ = K * #(H : Set G).toFinset + ex (Set.toFinset H)                 := rfl
      _ ≤ K * #(H : Set G).toFinset + (1 - ε / 2) * #(Set.toFinset H * S) := by
        grw [calc₁]
        gcongr
        · linarith
        · simp only [Set.mem_toFinset, SetLike.mem_coe, H.one_mem, subset_mul_right]

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
⊢ (ofSimpleGraph G).toSimpleGraph ≃g G

Tactic:
use Equiv.Set.univ α

Goal state after:
case map_rel_iff'
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
⊢ ∀ {a b : ↑V(ofSimpleGraph G)},
    G.Adj ((Equiv.Set.univ α) a) ((Equiv.Set.univ α) b) ↔ (ofSimpleGraph G).toSimpleGraph.Adj a b
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case none
η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
h : l.idxFun ie.1 = none
⊢ ↑l.toSubspace a ie = ↑l a ie.1 ie.2

Tactic:
simp [toSubspace, h, coe_apply, Subspace.coe_apply]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case some
η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
val✝ : η → α
h : l.idxFun ie.1 = some val✝
⊢ ↑l.toSubspace a ie = ↑l a ie.1 ie.2

Tactic:
simp [toSubspace, h, coe_apply, Subspace.coe_apply]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU : U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)}
⊢ ∀ a_1 ∈ FP (Stream'.drop (n + 1) a), a_1 ∈ FP (Stream'.drop n a)

Tactic:
← Stream'.drop_drop,

Goal state after:
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU : U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)}
⊢ ∀ a_1 ∈ FP (Stream'.drop 1 (Stream'.drop n a)), a_1 ∈ FP (Stream'.drop n a)
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
d : ℕ
hd : (s.erase (s.min' hs)).min' h = s.min' hs + 1 + d
⊢ FP (Stream'.drop (s.min' hs + 1 + d) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)

Tactic:
← Stream'.drop_drop,

Goal state after:
case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
d : ℕ
hd : (s.erase (s.min' hs)).min' h = s.min' hs + 1 + d
⊢ FP (Stream'.drop d (Stream'.drop (s.min' hs + 1) a)) ⊆ FP (Stream'.drop (1 + s.min' hs) a)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ (M ／ I).Indep J ↔ Disjoint J I ∧ M.Indep (J ∪ I)

Tactic:
simp_rw [indep_iff, hI.contract_isBase_iff, union_subset_iff]

Goal state after:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ (∃ B, (M.IsBase (B ∪ I) ∧ Disjoint B I) ∧ J ⊆ B) ↔ Disjoint J I ∧ ∃ B, M.IsBase B ∧ J ⊆ B ∧ I ⊆ B
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ (M ／ I).Dep J ↔ Disjoint J I ∧ M.Dep (J ∪ I)

Tactic:
rw [dep_iff, hI.contract_indep_iff, dep_iff, contract_ground, subset_sdiff, disjoint_comm,
    union_subset_iff, and_iff_left hI.subset_ground]

Goal state after:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
⊢ (M ／ I).Indep J ∧ Disjoint J (X \ I) ↔ M.Indep (J ∪ I) ∧ Disjoint X J

Tactic:
hI.indep.contract_indep_iff,

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
⊢ (Disjoint J I ∧ M.Indep (J ∪ I)) ∧ Disjoint J (X \ I) ↔ M.Indep (J ∪ I) ∧ Disjoint X J
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C D C' : Set α
h : Disjoint C' D
⊢ M ／ (C ∪ C' \ D) ＼ D = M ／ (C ∪ C') ＼ D

Tactic:
sdiff_eq_left.mpr h

Goal state after:
α : Type u_1
M : Matroid α
C D C' : Set α
h : Disjoint C' D
⊢ M ／ (C ∪ C') ＼ D = M ／ (C ∪ C') ＼ D
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C D C' D' : Set α
h : Disjoint C' D
⊢ M ／ (C ∪ C' \ D) ＼ (D ∪ D') = M ／ (C ∪ C') ＼ (D ∪ D')

Tactic:
sdiff_eq_left.mpr h

Goal state after:
α : Type u_1
M : Matroid α
C D C' D' : Set α
h : Disjoint C' D
⊢ M ／ (C ∪ C') ＼ (D ∪ D') = M ／ (C ∪ C') ＼ (D ∪ D')
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
D C D' : Set α
h : Disjoint C D
⊢ M ／ (C \ D) ＼ (D ∪ D') = M ／ C ＼ (D ∪ D')

Tactic:
sdiff_eq_left.mpr h

Goal state after:
α : Type u_1
M : Matroid α
D C D' : Set α
h : Disjoint C D
⊢ M ／ C ＼ (D ∪ D') = M ／ C ＼ (D ∪ D')
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
a✝ :
  ∀ (y : MvPolynomial σ R),
    (invImage (fun x ↦ ⋯.wrap (m.toSyn (m.degree x))) Acc.wfRel).1 y f →
      ∃ g r,
        y = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
          (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree y)) ∧
            ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
hb' : ¬∃ i, m.degree (b i) = 0
hf0 : ¬f = 0
hf✝ : ∃ i, m.degree (b i) ≤ m.degree f
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
⊢ ↑(⋯.wrap (m.toSyn (m.degree (m.reduce ⋯ f)))) < ↑(⋯.wrap (m.toSyn (m.degree f)))

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
a✝ :
  ∀ (y : MvPolynomial σ R),
    (invImage (fun x ↦ ⋯.wrap (m.toSyn (m.degree x))) Acc.wfRel).1 y f →
      ∃ g r,
        y = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
          (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree y)) ∧
            ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
hb' : ¬∃ i, m.degree (b i) = 0
hf0 : ¬f = 0
hf : ¬∃ i, m.degree (b i) ≤ m.degree f
hf'0 : ¬m.subLTerm f = 0
⊢ ↑(⋯.wrap (m.toSyn (m.degree (m.subLTerm f)))) < ↑(⋯.wrap (m.toSyn (m.degree f)))

Tactic:
· exact deg_reduce

Goal state after:
σ : 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
a✝ :
  ∀ (y : MvPolynomial σ R),
    (invImage (fun x ↦ ⋯.wrap (m.toSyn (m.degree x))) Acc.wfRel).1 y f →
      ∃ g r,
        y = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
          (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree y)) ∧
            ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
hb' : ¬∃ i, m.degree (b i) = 0
hf0 : ¬f = 0
hf : ¬∃ i, m.degree (b i) ≤ m.degree f
hf'0 : ¬m.subLTerm f = 0
⊢ ↑(⋯.wrap (m.toSyn (m.degree (m.subLTerm f)))) < ↑(⋯.wrap (m.toSyn (m.degree f)))
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
sharp :
  2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ False

Tactic:
have impos : 2 • (ω.map (fun _ => f ![a, b])).sum < ω.size • 2 • f ![a, b] := by
    convert! lt_of_lt_of_le sharp contr
    simp [FractionalOperation.tt, Multiset.map_map]

Goal state after:
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
sharp :
  2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • (Multiset.map (fun x ↦ f ![a, b]) ω).sum < ω.size • 2 • f ![a, b]
⊢ False
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) (h.sum fun i a ↦ a • Alon.P (S i) i) = 0

Tactic:
map_finsuppSum,

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
⊢ (h.sum fun a b ↦ (eval x) (b • Alon.P (S a) a)) = 0
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : u ⟶ v
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ Symmetrify.of.obj u) ⟨v, Sum.inl f⟩)

Tactic:
Equiv.sigmaSumDistrib_apply

Goal state after:
case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : u ⟶ v
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map (Sigma.mk ⟨v, Sum.inl f⟩.fst) (Sigma.mk ⟨v, Sum.inl f⟩.fst) ⟨v, Sum.inl f⟩.snd)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : v ⟶ u
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ Symmetrify.of.obj u) ⟨v, Sum.inr g⟩)

Tactic:
Equiv.sigmaSumDistrib_apply

Goal state after:
case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : v ⟶ u
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map (Sigma.mk ⟨v, Sum.inr g⟩.fst) (Sigma.mk ⟨v, Sum.inr g⟩.fst) ⟨v, Sum.inr g⟩.snd)
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
this : p.length + q.length = 0
⊢ q.length = 0

Tactic:
exact Nat.eq_zero_of_add_eq_zero_left this

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

Goal state before:
pp: case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : v ⟶ u
⊢ Sum.map (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.costar u) (φ.star u)
      ((Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj u) (Hom (Symmetrify.of.obj u))) ⟨v, Sum.inl f⟩)

Tactic:
Equiv.sigmaSumDistrib_apply

Goal state after:
case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : v ⟶ u
⊢ Sum.map (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.costar u) (φ.star u)
      (Sum.map (Sigma.mk ⟨v, Sum.inl f⟩.fst) (Sigma.mk ⟨v, Sum.inl f⟩.fst) ⟨v, Sum.inl f⟩.snd)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : u ⟶ v
⊢ Sum.map (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.costar u) (φ.star u)
      ((Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj u) (Hom (Symmetrify.of.obj u))) ⟨v, Sum.inr g⟩)

Tactic:
Equiv.sigmaSumDistrib_apply

Goal state after:
case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : u ⟶ v
⊢ Sum.map (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.costar u) (φ.star u)
      (Sum.map (Sigma.mk ⟨v, Sum.inr g⟩.fst) (Sigma.mk ⟨v, Sum.inr g⟩.fst) ⟨v, Sum.inr g⟩.snd)
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
have h_case₁ : v = (pPrev.cons e).end → ∃ (p₁ : Path a v) (p₂ : Path v (pPrev.cons e).end),
        pPrev.cons e = p₁.comp p₂ ∧ v ∉ p₂.vertices.tail := by
      rintro rfl
      exact ⟨pPrev.cons e, Path.nil, by simp [comp_nil], by simp [vertices_nil]⟩

Goal state after:
case cons
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case inl
hm : 0 ≠ 1
⊢ schnirelmannDensity {n | n % 0 = 1} = (↑0)⁻¹

pp: case inr
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ schnirelmannDensity {n | n % m = 1} = (↑m)⁻¹

Tactic:
· simp only [Nat.cast_zero, inv_zero]
    refine schnirelmannDensity_finite ?_
    simp

Goal state after:
case inr
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ schnirelmannDensity {n | n % m = 1} = (↑m)⁻¹
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 α
h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
ha : a ∉ s
⊢ u ≤ a

Tactic:
obtain h | ⟨-, b, hb, hba⟩ := h

Goal state after:
case inl
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
h : a ∈ s ∧ compress u v a ∈ s
⊢ u ≤ a

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
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 α
h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
ha : a ∉ s
⊢ Disjoint v a

Tactic:
obtain h | ⟨-, b, hb, hba⟩ := h

Goal state after:
case inl
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
h : a ∈ s ∧ compress u v a ∈ s
⊢ Disjoint v a

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