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

Goal state before:
pp: case mpr
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
⊢ (∀ ⦃e : Sym2 α⦄,
      ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton) →
    ∀ ⦃x : Finset α⦄ (x_1 x_2 x_3 : α),
      G.Adj x_1 x_2 →
        G.Adj x_1 x_3 →
          G.Adj x_2 x_3 →
            x = {x_1, x_2, x_3} →
              ∀ ⦃y : Finset α⦄ (x_4 x_5 x_6 : α),
                G.Adj x_4 x_5 →
                  G.Adj x_4 x_6 →
                    G.Adj x_5 x_6 → y = {x_4, x_5, x_6} → ∀ x_7 ∈ x, x_7 ∈ y → ∀ x_8 ∈ x, x_8 ∈ y → ¬x_7 = x_8 → x = y

Tactic:
rintro hG _ a b c hab hac hbc rfl _ d e f hde hdf hef rfl g hg₁ hg₂ h hh₁ hh₂ hgh

Goal state after:
case mpr
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ {a, b, c} = {d, e, f}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #G.edgeFinset ≤ 3 * #(G.cliqueFinset 3)

Tactic:
rw [← mul_comm, ← mul_one #_]

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #G.edgeFinset * 1 ≤ #(G.cliqueFinset 3) * 3
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hp : (Walk.map f p).IsTrail
⊢ p.IsTrail

Tactic:
isTrail_def

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hp : (Walk.map f p).IsTrail
⊢ p.edges.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ 3 / 4 * ε ≤
    |(∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) /
          (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U))) -
        (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
          (4 ^ #P.parts * 4 ^ #P.parts)|

Tactic:
set p : ℝ :=
    (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), (G.edgeDensity ab.1 ab.2 : ℝ)) /
      (#(star hP G ε hU V) * #(star hP G ε hV U))

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
p : ℝ :=
  (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) /
    (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)))
⊢ 3 / 4 * ε ≤
    |p -
        (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
          (4 ^ #P.parts * 4 ^ #P.parts)|
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
⊢ y₁ - x₂ + (y₂ - x₁) = y₁ - x₁ + (y₁ - x₁)

Tactic:
sub_add_sub_comm,

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
⊢ y₁ + y₂ - (x₂ + x₁) = y₁ - x₁ + (y₁ - x₁)
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
⊢ #({x ∈ univ ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2}) = #(univ ×ˢ t ×ˢ t)

Tactic:
← card_image_of_injOn this

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
⊢ #({x ∈ univ ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2}) = #(image f (univ ×ˢ t ×ˢ t))
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : A ⊆ range n
hAε : ε * ↑n ≤ ↑(#A)
⊢ ¬ThreeAPFree ↑A

Tactic:
rintro hA
  rw [← coe_subset, coe_range] at hAn
  have : A = Fin.val '' (Nat.cast '' A : Set (Fin (2 * n).succ)) := by
    rw [Set.image_image, Set.image_congr, Set.image_id]
    simp only [mem_coe, Nat.succ_eq_add_one, Fin.val_natCast, id_eq, Nat.mod_succ_eq_iff_lt]
    rintro a ha
    have := hAn ha
    simp at this
    lia
  rw [this] at hA
  have := Fin.isAddFreimanIso_Iio two_ne_zero (le_refl (2 * n))
  have := hA.of_image this.isAddFreimanHom Fin.val_injective.injOn <| Set.image_subset_iff.2 <|
      hAn.trans fun x hx ↦ Fin.natCast_strictMono (by lia) <| by
        simpa only [coe_range, Set.mem_Iio] using hx
  rw [← coe_image] at this
  refine roth_3ap_theorem (ε / 3) (by positivity) (by simp; lia) _ ?_ this
  calc
    _ = ε / 3 * (2 * n + 1) := by simp
    _ ≤ ε / 3 * (2 * n + n) := by gcongr; simp; unfold cornersTheoremBound at hG; lia
    _ = ε * n := by ring
    _ ≤ #A := hAε
    _ = _ := by
      rw [card_image_of_injOn]
      exact (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono <| hAn.trans <| by
        simp; lia

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case cons
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
haL : ∀ (a' : ℕ), a' ∈ L → a < a'
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
⊢ (map (fun i ↦ 2 ^ i) (a :: L)).sum.bitIndices = a :: L

Tactic:
simp_rw [Nat.lt_iff_add_one_le] at haL

Goal state after:
case cons
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ (map (fun i ↦ 2 ^ i) (a :: L)).sum.bitIndices = a :: L
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun a ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology (β a)
e : Finset α → Set ((a : α) → β a) := fun s ↦ {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this : ∀ (s : Finset α), s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ (x : ↥s), f x = g t ↑x} = e s
he' : ∀ (s : Finset α), IsClosed (e s)
he'' : ∀ (B : Finset (Finset α)), (⋂ i ∈ B, e i).Nonempty
⊢ ∃ χ, ∀ (s : Finset α), ∃ t, s ⊆ t ∧ ∀ x ∈ s, χ x = g t x

Tactic:
simpa using! CompactSpace.iInter_nonempty he' he''

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
α : Type u_3
f : { v // v ≠ 0 } → α
hf : ∀ (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → f a = f b
x : ℙ K V
⊢ ∀ (a b : { v // v ≠ 0 }), a ≈ b → f a = f b

Tactic:
rintro ⟨-, hv⟩ ⟨w, hw⟩ ⟨⟨t, -⟩, rfl⟩; exact hf ⟨_, hv⟩ ⟨w, hw⟩ t rfl

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
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
x a : G
ha : a ∈ A
⊢ x * a ∈ A ↔ a * x ∈ A

Tactic:
rw [← smul_mem_smul_finset_iff a, smul_A_eq_A_smul ha, ← op_smul_eq_mul, smul_comm,
      smul_mem_smul_finset_iff, smul_eq_mul]

Goal state after:
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
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
by_cases hl₂ : p ∈ l₂

Goal state after:
case pos
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
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∈ l₂
⊢ ∃ p ∈ l₁, p ∈ l₂

case neg
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
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
⊢ ∃ p ∈ l₁, p ∈ l₂
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
hAB : (Nat.succ 0).succ + (Nat.succ 0).succ ≤ 3
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ x, ↑(catalan ↑x) * ↑(catalan (d - ↑x)) =
    ∑ i, ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1))

Tactic:
congr
      ext1 x
      have m_le_d : x.val ≤ d := by lia
      have d_minus_x_le_d : (d - x.val) ≤ d := tsub_le_self
      rw [hd _ m_le_d, hd _ d_minus_x_le_d]
      norm_cast

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

Goal state before:
pp: p q r : DyckWord
⊢ p + q + r = p + (q + r)

Tactic:
by ext1; apply append_assoc

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

Goal state before:
pp: case refine_1
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 [subset_smul_finset_iff, ← op_inv]

Goal state after:
case refine_1
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: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
⊢ 0 * f = 0

Tactic:
ext; exact sum_eq_zero fun x _ ↦ zero_mul _

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

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
⊢ p.parts.bell = ∑ a ∈ p.parts.toFinset, n.choose (a - 1) * (p.parts.erase a).bell

Tactic:
apply Nat.eq_of_mul_eq_mul_left n.succ_pos
  calc
  _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * p.parts.bell := by
    rw [succ_eq_add_one, mul_eq_mul_right_iff]
    left
    simpa [smul_eq_mul, p.parts_sum] using Finset.sum_multiset_count p.parts
  _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * p.parts.bell) := by grind [Finset.sum_mul]
  _ = ∑ a ∈ p.parts.toFinset, (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell) := by
    congr! 1 with a ha
    have ha0 : a ≠ 0 := by grind
    have hsum : (p.parts.erase a).sum + a = n + 1 := by
      simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (cons_erase (mem_dedup.mp ha))
    grind [Nat.add_one_mul_choose_eq, cons_erase, bell_cons_mul_count]
  _ = _ := by rw [Finset.mul_sum]

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

Goal state before:
pp: n : ℕ
⊢ Fintype.card { p // p.semilength = n } = catalan n

Tactic:
rw [← Fintype.ofEquiv_card (equivTreesOfNumNodesEq n), ← treesOfNumNodesEq_card_eq_catalan]
  convert! Fintype.card_coe _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hV : V(H) = V(G)
h : H ≤i G
e : β
he : e ∈ E(G)
⊢ e ∈ E(H)

Tactic:
by
    obtain ⟨_, _, hxy⟩ := G.exists_isLink_of_mem_edgeSet he
    exact h.isLink_of_mem_mem hxy (hV ▸ hxy.left_mem) (hV ▸ hxy.right_mem) |>.edge_mem

Goal state after:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case h
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N ∩ {m' | m' * m = m}
scaling_eq_self : (fun x ↦ x * m) '' N = N
absorbing_eq_self : N ∩ {m' | m' * m = m} = N
⊢ m * m = m

Tactic:
exact hm.2

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
hlm : ↑l = ↑m
⊢ l = m

Tactic:
ext i a

Goal state after:
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
hlm : ↑l = ↑m
i : ι
a : α
⊢ l.idxFun i = some a ↔ m.idxFun i = some a
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
⊢ ↑l.toSubspaceUnit a = ↑l (a ())

Tactic:
ext i; cases h : l.idxFun i <;> simp [toSubspaceUnit, h, Subspace.coe_apply]

Goal state after:
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
i : ι
hb0 : m.degree (b i) = 0
⊢ m.leadingCoeff (b i) • f = C (m.leadingCoeff (b i)) * f

Tactic:
smul_eq_C_mul

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
i : ι
hb0 : m.degree (b i) = 0
⊢ C (m.leadingCoeff (b i)) * f = C (m.leadingCoeff (b i)) * f
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
⊢ M.disjointSum N h = N.disjointSum M ⋯

Tactic:
by
  ext
  · simp [union_comm]
  repeat simpa [union_comm] using ⟨fun ⟨m, n, h⟩ ↦ ⟨n, m, M.E.union_comm N.E ▸ h⟩,
    fun ⟨n, m, h⟩ ↦ ⟨m, n, M.E.union_comm N.E ▸ h⟩⟩

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

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
⊢ ∀ ⦃a b c : WideSubquiver.toType V (geodesicSubtree r)⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f

Tactic:
rintro a b c ⟨e, p, h⟩ ⟨f, q, j⟩

Goal state after:
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h : shortestPath r c = p.cons e
f : b ⟶ c
q : Path r b
j : shortestPath r c = q.cons f
⊢ a = b ∧ ⟨e, ⋯⟩ ≍ ⟨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
g : (Fin 2 → D) → D
h✝ : g ∈ ω
⊢ (fun i ↦ g (swap ![![a, b], ![b, a]] i)) ∈ ω.tt ![![a, b], ![b, a]]

Tactic:
simp only [FractionalOperation.tt, Multiset.mem_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
g : (Fin 2 → D) → D
h✝ : g ∈ ω
⊢ ∃ a_1 ∈ ω, (fun i ↦ a_1 (swap ![![a, b], ![b, a]] i)) = fun i ↦ g (swap ![![a, b], ![b, a]] i)
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: case mp
V : Type u_2
inst✝ : Quiver V
v : V
h_singleton : ∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v
hw_ne : v ≠ v
hab hba : Nonempty (Path v v)
h_same_scc : StronglyConnectedComponent.mk v = StronglyConnectedComponent.mk v
⊢ False

Tactic:
contradiction

Goal state after:
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
⊢ P S i = (rename fun x ↦ i) (P S ())

Tactic:
simp [Alon.P]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
q : MvPolynomial σ R := g ⟨b, ⋯⟩
h1 : m.toSyn (m.degree (b * q)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ (g.sum fun i c ↦ c * ↑i) = q * b

Tactic:
rw [Finsupp.sum_eq_single ⟨b, by simp⟩ _ (by simp)]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
q : MvPolynomial σ R := g ⟨b, ⋯⟩
h1 : m.toSyn (m.degree (b * q)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ ∀ (b_1 : ↑{b}), g b_1 ≠ 0 → b_1 ≠ ⟨b, ⋯⟩ → g b_1 * ↑b_1 = 0
Module: Mathlib.Combinatorics.Quiver.Schreier

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
a b : M
x : SchreierGraph V ι
⊢ (a * b) • x = a • b • x

Tactic:
ext
    exact mul_smul a b x.toVertex

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 b✝ c✝ : V
p' : Path (φ.obj u) b✝
ev : b✝ ⟶ c✝
ih : ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨b✝, p'⟩
⊢ ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, p'.cons ev⟩

Tactic:
obtain ⟨⟨u', q'⟩, h⟩ := ih

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 b✝ c✝ : V
p' : Path (φ.obj u) b✝
ev : b✝ ⟶ c✝
u' : U
q' : Path u u'
h : (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u', q'⟩ = ⟨b✝, p'⟩
⊢ ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, p'.cons ev⟩
Module: Mathlib.Data.Set.Sups

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
c : α
⊢ c ∈ s ⊼ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ b = c

Tactic:
simp [(· ⊼ ·)]

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

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ ↑(lowerClosure (s ⊼ t)) ↔ a ∈ ↑(lowerClosure s ⊓ lowerClosure t)

Tactic:
simp only [SetLike.mem_coe, mem_lowerClosure, Set.mem_infs]

Goal state after:
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) ↔ a ∈ lowerClosure s ⊓ lowerClosure t
Module: Mathlib.Data.Set.Sups

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
hab : a ≤ b
c : α
hc : c ∈ t
hac : a ≤ c
⊢ ∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1

Tactic:
exact ⟨_, ⟨b, hb, c, hc, rfl⟩, le_inf hab hac⟩

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case right
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊↑(#A) / ε⌋₊ + 1
hn : 0 < n
⊢ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) < ε * ↑n

Tactic:
← div_lt_iff₀' hε,

Goal state after:
case right
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊↑(#A) / ε⌋₊ + 1
hn : 0 < n
⊢ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ε < ↑n
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(𝓓 a 𝒜) = #𝒜

Tactic:
by
  rw [compression, card_disjUnion, filter_image,
    card_image_of_injOn ((erase_injOn' _).mono fun s hs => _), ← card_union_of_disjoint]
  · conv_rhs => rw [← filter_union_filter_not_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]
  · exact disjoint_filter_filter_not 𝒜 𝒜 (fun s => (erase s a ∈ 𝒜))
  intro s hs
  rw [mem_coe, mem_filter] at hs
  exact not_imp_comm.1 erase_eq_of_notMem (ne_of_mem_of_not_mem hs.1 hs.2).symm

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∈ A
⊢ n ∈ A

Tactic:
by simp [hnA]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : SemilatticeInf α
s t : Finset α
c : α
⊢ c ∈ s ⊼ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ b = c

Tactic:
simp [(· ⊼ ·)]

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

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ (∃ x, ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ x, x ∈ s

Tactic:
exact fun ⟨_, a, ha, _⟩ => ⟨a, ha⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ sᶜˢ ⊼ t = t \\ s

Tactic:
by
  rw [infs_comm, infs_compls_eq_diffs]

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

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
inst✝ : DecidableEq α
u v : α
s : Finset α
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s

Tactic:
by
  have h : {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = ∅ :=
    filter_false_of_mem fun a ha h ↦ h <| compress_mem_compression_of_mem_compression ha
  rw [compression, filter_image, h, image_empty, ← h]
  exact filter_union_filter_not_eq _ (compression u v s)

Goal state after: