mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case inl
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → t ∈ tris → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : ↥tris → Sym2 α := fun t ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩
i : (↑t₁ ∩ ↑t₂).Subsingleton
t : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯
⊢ False

pp: case inr
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → t ∈ tris → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : ↥tris → Sym2 α := fun t ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩
i : (↑t₁ ∩ ↑t₂).Subsingleton
t : fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯
⊢ False

Tactic:
· exact hfne _ (i ⟨hfx ht₁, t.1.symm ▸ hfx ht₂⟩ ⟨hfy ht₁, t.2.symm ▸ hfy ht₂⟩)

Goal state after:
case inr
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → t ∈ tris → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : ↥tris → Sym2 α := fun t ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩
i : (↑t₁ ∩ ↑t₂).Subsingleton
t : fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:

Tactic:
_ ≤ card α / (2 * #P.parts : ℝ) := by gcongr
    _ ≤ ↑(card α / #P.parts) :=
      (div_le_iff₀' (by positivity)).2 <| mod_cast (aux ‹_› P.card_parts_le_card).le
    _ ≤ (#s : ℝ) := mod_cast hP₁.average_le_card_part hX

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) := ⋯
B : Finset (α × α) := ⋯
C : Finset (α × α) := ⋯
⊢ ↑(#B) ≤ ε / 2 * ↑(Fintype.card α) ^ 2

Tactic:
exact hP.card_biUnion_offDiag_le hε hP'

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A * A)) * ↑(#(A * A)) = σₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
rw [← mulConst_mul_card]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ σₘ[A] * ↑(#A) * (σₘ[A] * ↑(#A)) = σₘ[A] ^ 2 * (↑(#A) * ↑(#A))
Module: Mathlib.Combinatorics.Additive.Randomisation

Goal state before:
pp: G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
⊢ 𝔼 a, ∏ ψ ∈ t, (d ψ * ψ a + (starRingEnd ℂ) (d ψ * ψ a)) / 2 = 0

Tactic:
simp only [map_mul, prod_div_distrib, prod_add, prod_const, ← expect_div, expect_sum_comm,
    div_eq_zero_iff, pow_eq_zero_iff', OfNat.ofNat_ne_zero, ne_eq, card_eq_zero,
    false_and, or_false]

Goal state after:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
⊢ ∑ j ∈ t.powerset, 𝔼 i, (∏ i_1 ∈ j, d i_1 * i_1 i) * ∏ i_1 ∈ t \ j, (starRingEnd ℂ) (d i_1) * (starRingEnd ℂ) (i_1 i) =
    0
Module: Mathlib.Combinatorics.Additive.SubsetSum

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 ≤ x
⊢ (#A).choose 2 < #A.subsetSum

Tactic:
calc (#A).choose 2
    _ ≤ (#(A.erase 0) + 1).choose 2 := by grw [tsub_le_iff_right.1 <| pred_card_le_card_erase]
    _ < #(A.erase 0).subsetSum :=
        card_succ_choose_two_lt_card_subsetSum_of_pos fun x hx =>
          (A_pos x (mem_of_mem_erase hx)).lt_of_ne (ne_of_mem_erase hx).symm
    _ = #A.subsetSum := by rw [subsetSum_erase_zero]

Goal state after:
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
⊢ some (f x) ≠ some x

Tactic:
(Option.some_injective α).ne_iff

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
⊢ f x ≠ x
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)

Tactic:
obtain ⟨f, hf1, hf2⟩ := Nondegenerate.exists_injective_of_card_le (ge_of_eq h)
  have hf3 := (Fintype.bijective_iff_injective_and_card f).mpr ⟨hf1, h.symm⟩
  exact ⟨f, hf3, fun l ↦ (sum_eq_sum_iff_of_le fun l _ ↦ pointCount_le_lineCount (hf2 l)).1
        ((hf3.sum_comp _).trans (sum_lineCount_eq_sum_pointCount P L)).symm _ <| mem_univ _⟩

Goal state after:
Module: Mathlib.Combinatorics.Digraph.Basic

Goal state before:
pp: V : Type u_1
adj adj' : V → V → Bool
h : (fun v w ↦ adj v w = true) = fun v w ↦ adj' v w = true
⊢ adj = adj'

Tactic:
funext v w

Goal state after:
V : Type u_1
adj adj' : V → V → Bool
h : (fun v w ↦ adj v w = true) = fun v w ↦ adj' v w = true
v w : V
⊢ adj v w = adj' v w
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
⊢ A ⊆ a •> (A⁻¹ * A)

Tactic:
by
  rw [← smul_mul_assoc]
  exact subset_mul_right _ (by simp [← inv_smul_mem_iff, inv_mem_inv ha])

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

Goal state before:
pp: case e_val
p q a b : DyckWord
h : a + b = 0
neg_val✝ : b + a = 0
ha : ↑a = []
hb : ↑b = []
⊢ a = 0

Tactic:
exact toList_eq_nil.mp ha

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ A⁻¹ * (A⁻¹ * A * A) = A⁻¹ * A

Tactic:
rw [← mul_inv_eq_inv_mul_of_doubling_lt_two <| weaken_doubling h]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ A⁻¹ * (A * A⁻¹ * A) = A * A⁻¹
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ ∑ x ∈ Icc a b, (mu' 𝕜) x b = if a = b then 1 else 0

Tactic:
sum_Icc_mu'_left

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (if a = b then 1 else 0) = if a = b then 1 else 0
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
⊢ (∑ x ∈ Icc a b, if x ≤ b then mud a x else 0) = if a = b then 1 else 0

Tactic:
calc
    ∑ x ∈ Icc a b, (if x ≤ b then mud a x else 0) = ∑ x ∈ Icc a b, mud a x := by
      congr! with x hx; exact if_pos (mem_Icc.1 hx).2
    _ = ∑ x ∈ Icc (ofDual b) (ofDual a), mu 𝕜 x (ofDual a) := by simp [Icc_orderDual_def, mud]
    _ = if ofDual b = ofDual a then 1 else 0 := sum_Icc_mu_left ..
    _ = if a = b then 1 else 0 := by simp [eq_comm]

Goal state after:
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
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
⊢ Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))

Tactic:
apply Summable.comp_nat_add (k := 1)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
⊢ Summable fun n ↦ x ^ (n + 1 + 1) * ∏ n ∈ Finset.range (n + 1), (1 - x ^ (n + 1))
Module: Mathlib.Combinatorics.Enumerative.Schroder

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 2 * (n + 1).smallSchroder = n.largeSchroder

Tactic:
rw [smallSchroder_succ_eq_largeSchroder_div_two hn,
    Nat.mul_div_cancel_left' (even_largeSchroder hn).two_dvd]

Goal state after:
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
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
H : Subgroup G := { carrier := n⁻¹ •> ↑N, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
⊢ IsAtom K S (↑H).toFinset

Tactic:
· simpa [Set.toFinset_smul_set, toFinset_coe, H] using! IsAtom.smul_finset n⁻¹ hN

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : CommRing α
s : Finset α
inst✝¹ : Fact (IsUnit 2)
hs : ThreeAPFree ↑s
inst✝ : DecidableEq α
this : NoAccidental (triangleIndices s)
⊢ #(graph (triangleIndices s)).edgeFinset = 3 * Fintype.card α * #s

Tactic:
rw [(locallyLinear hs).card_edgeFinset, card_triangles, card_triangleIndices, mul_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
F : Set β
⊢ (G.deleteEdges F).IsLoopAt e x ↔ G.IsLoopAt e x ∧ e ∉ F

Tactic:
simp only [← restrict_edgeSet_sdiff_eq_deleteEdges, restrict_isLoopAt, mem_sdiff,
    and_congr_right_iff, and_iff_right_iff_imp]
  exact fun h _ ↦ h.edge_mem

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
x y : α'
f : α → α'
⊢ (map f G).Adj x y ↔ Relation.Map G.Adj f f x y

Tactic:
simp only [Adj, map_isLink, map_apply]

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
x y : α'
f : α → α'
⊢ (∃ e a b, G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ a b, (∃ e, G.IsLink e a b) ∧ f a = x ∧ f b = y
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ ＼ D₂ = M ＼ (D₁ ∪ D₂)

Tactic:
by
  rw [← restrict_compl, ← restrict_compl, ← restrict_compl, restrict_restrict_eq,
    restrict_ground_eq, sdiff_sdiff]
  simp

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ＼ ∅ = M

Tactic:
by
  rw [delete_eq_self_iff]
  exact empty_disjoint _

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M N : Matroid α
X : Set α
h : N ≤r M
hX : Disjoint X N.E
⊢ N ≤r M ＼ X

Tactic:
obtain ⟨D, hD, rfl⟩ := isRestriction_iff_exists_eq_delete.1 h
  refine isRestriction_iff_exists_eq_delete.2 ⟨D \ X, sdiff_subset_sdiff_left hD, ?_⟩
  rwa [delete_delete, union_sdiff_self, union_comm, ← delete_delete, eq_comm,
    delete_eq_self_iff]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case H.inl
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) = ∅
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)

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
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
· rw [h, Finset.prod_empty, mul_one]
    exact FP.head _

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
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
hx : x ∈ s
⊢ ↑({ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
          invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
          left_inv := ⋯, right_inv := ⋯ }
        x) <
    #s

Tactic:
simpa [hx, -Fin.is_lt] using (g _).is_lt

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h_empty
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
⊢ P = 0

Tactic:
suffices P = C (constantCoeff P) by
      specialize Heval default (fun i ↦ PEmpty.elim i)
      rw [this, eval_C] at Heval
      rw [this, Heval, C_0]
    ext m
    suffices m = 0 by simp [this, ← constantCoeff_eq]
    ext d; exact PEmpty.elim d

Goal state after:
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
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
use g', r' + monomial (m.degree f) (m.leadingCoeff f)

Goal state after:
case h
σ : 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
⊢ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + (r' + (monomial (m.degree f)) (m.leadingCoeff f)) ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree f)) ∧
      ∀ c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support, ∀ (i : ι), ¬m.degree (b i) ≤ c
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
B : Set (MvPolynomial σ R)
hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑B →₀ MvPolynomial σ R
r : MvPolynomial σ R
H :
  f = (Finsupp.linearCombination (MvPolynomial σ R) fun p ↦ ↑p) g + r ∧
    (∀ (i : ↑B), m.toSyn (m.degree (↑i * g i)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ (i : ↑B), ¬m.degree ↑i ≤ c
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) fun b ↦ ↑b) g + r ∧
      (∀ (b : ↑B), m.toSyn (m.degree (↑b * g b)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c

Tactic:
exact ⟨g, r, H.1, H.2.1, fun c hc b hb ↦ H.2.2 c hc ⟨b, hb⟩⟩

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

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

Tactic:
by simp [comp_nil]

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

Goal state before:
pp: case cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v c✝ : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ c✝
u'' : U
eu : u' ⟶ u''
k : φ.star u' ⟨u'', eu⟩ = ⟨c✝, ev⟩
⊢ ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, (φ.mapPath q').cons ev⟩

Tactic:
simp only [star_apply, Sigma.mk.inj_iff] at k

Goal state after:
case cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v c✝ : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ c✝
u'' : U
eu : u' ⟶ u''
k : φ.obj u'' = c✝ ∧ φ.map eu ≍ ev
⊢ ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, (φ.mapPath q').cons ev⟩
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case e'_1.e'_2.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this✝ :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
this : ∀ n ∈ range (card α + 1), ↑((card α).choose n) / ((↑(card α) - ↑n) * ↑((card α).choose n)) = (↑(card α) - ↑n)⁻¹
a : ℕ
ha : a ∈ range (card α + 1)
⊢ (↑(card α) - ↑a)⁻¹ = (↑(card α + 1 - 1 - a))⁻¹

Tactic:
rw [add_tsub_cancel_right, cast_sub (mem_range_succ_iff.mp ha)]

Goal state after:
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
b : α
hb : b ∈ s
hab : a ≤ b
⊢ id b ≤ a

Tactic:
exact (hs.eq ha hb hab).ge

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
h : u ⊆ s ∩ t
⊢ s ∩ u ∩ (t ∩ u) = u

Tactic:
rwa [← inter_inter_distrib_right, inter_eq_right]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k) → ∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
rintro ⟨s, hs, hts, rfl⟩

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
⊢ ∃ u, #u = #(s \ t) ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k) → ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
rintro ⟨s, hs, hst, rfl⟩
    exact ⟨_, rfl, sdiff_subset, by rwa [sdiff_sdiff_eq_self hst]⟩

Goal state after:
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a✝ b✝ a b c : α
⊢ a \ c ⊔ a ⊓ b ≤ a ⊓ b ⊔ a \ c

Tactic:
sup_comm

Goal state after:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a✝ b✝ a b c : α
⊢ a ⊓ b ⊔ a \ c ≤ a ⊓ b ⊔ a \ c
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ #𝒜 * #ℬ ≤ 2 ^ #(insert a s) * #(𝒜 ∩ ℬ)

Tactic:
rw [card_insert_of_notMem hs, ← card_memberSubfamily_add_card_nonMemberSubfamily a 𝒜, ←
    card_memberSubfamily_add_card_nonMemberSubfamily a ℬ, add_mul, mul_add, mul_add,
    add_comm (_ * _), add_add_add_comm]

Goal state after:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ #(Finset.memberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 ^ (#s + 1) * #(𝒜 ∩ ℬ)
Module: Mathlib.Combinatorics.SetFamily.Intersecting

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

Tactic:
Nat.le_div_iff_mul_le Nat.two_pos,

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