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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a e ∧ G.Adj b e ∧ {b, a, e} = {a, b, e}

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hde : G.Adj a b
hcd : G.Adj a c
hce : G.Adj b c
⊢ G.Adj a c ∧ G.Adj b c ∧ {c, a, b} = {a, b, c}

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : ∀ w ∈ s \ {b}, G.Adj a w
hb : b ∈ s
n✝ : ℕ
hs : G.IsNClique (n✝ + 1) s
w : α
h : w ∈ s.erase b
⊢ G.Adj a w

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ G.Adj a d ∧ G.Adj b d ∧ {b, d, a} = {a, b, d}

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
⊢ G.Adj a c ∧ G.Adj b c ∧ {c, b, a} = {a, b, c}

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
x✝ : ∃ s a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
w✝² : Finset α
a w✝¹ w✝ : α
hab : G.Adj a w✝¹
hac : G.Adj a w✝
hbc : G.Adj w✝¹ w✝
right✝ : w✝² = {a, w✝¹, w✝}
⊢ ((Walk.cons hab (Walk.cons hbc (Walk.cons ⋯ nil))).IsTrail ∧
      Walk.cons hab (Walk.cons hbc (Walk.cons ⋯ nil)) ≠ nil ∧
        (Walk.cons hab (Walk.cons hbc (Walk.cons ⋯ nil))).support.tail.Nodup) ∧
    (Walk.cons hab (Walk.cons hbc (Walk.cons ⋯ nil))).length = 3

Tactic:
aesop

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

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adjᶜ → G.CliqueFreeOn s 2

Tactic:
simp only [CliqueFreeOn, isNClique_iff, card_eq_two, not_and, not_exists]

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adjᶜ → ∀ ⦃t : Finset α⦄, ↑t ⊆ s → G.IsClique ↑t → ∀ (x x_1 : α), x ≠ x_1 → ¬t = {x, x_1}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t✝ u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)
hst : G.IsUniform ε s t✝
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)
utu : G.IsUniform ε t✝ u
h₁ : ↑(#(G.badVertices ε s t✝)) ≤ ↑(#s) * ε
h₂ : ↑(#(G.badVertices ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (G.badVertices ε s t✝ ∪ G.badVertices ε s u)
this :
  (X'.biUnion fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t✝ | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t✝ ×ˢ u |
      match x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
a : α
a✝¹ : a ∈ ↑X'
b : α
a✝ : b ∈ ↑X'
t : a ≠ b
⊢ ∀ (a_1 a_2 b_1 a_3 b_2 : α),
    (a_3, b_2) ∈ G.interedges ({y ∈ t✝ | G.Adj a y}) ({y ∈ u | G.Adj a y}) →
      a = a_1 →
        a_3 = a_2 →
          b_2 = b_1 →
            ∀ (a b_3 : α),
              (a, b_3) ∈ G.interedges ({y ∈ t✝ | G.Adj b y}) ({y ∈ u | G.Adj b y}) → b = a_1 → a = a_2 → ¬b_3 = b_1

Tactic:
aesop

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

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : Fintype.card α ≤ l
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
calc
      _ ≤ triangleRemovalBound ε * ↑l ^ 3 := by
        gcongr; exact (triangleRemovalBound_pos hε).le
      _ ≤ (1 : ℝ) := (triangleRemovalBound_mul_cube_lt hε).le
      _ ≤ _ := by simpa [one_le_iff_ne_zero] using (hG.cliqueFinset_nonempty hε).card_pos.ne'

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ ↑(#A) * δₘ[A, B] = ↑(#(A / B))

Tactic:
rw [mul_comm, divConst_mul_card]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A * A)) * ↑(#A) ≤ ↑(#(A / A)) * ↑(#(A / A))

Tactic:
norm_cast; exact ruzsa_triangle_inequality_mul_div_div ..

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
F : Unit → MvPolynomial σ K := ⋯
this : ∑ i, (F i).totalDegree < Fintype.card σ
x✝ : σ → K
⊢ (eval x✝) f = 0 ↔ ∀ i ∈ univ, (eval x✝) (F i) = 0

Tactic:
aesop

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

Goal state before:
pp: M : Type u_1
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : Finset M
a : M
a_notin_A : a ∉ A
B : Finset M
hB : B ⊆ A
⊢ insert a B ⊆ insert a A

Tactic:
aesop

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

Goal state before:
pp: case refine_2
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
h' : ∀ (x : ℕ), x ∈ L → ((fun x ↦ x + a + 1) ∘ fun x ↦ x - (a + 1)) x = x
⊢ L = map (fun x ↦ x + a + 1) (map (fun x ↦ x - (a + 1)) L)

Tactic:
simp [List.map_congr_left h']

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

Goal state before:
pp: case composite
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
⊢ ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i

Tactic:
rintro k hk

Goal state after:
case composite
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
k : ℕ
hk : k ≤ 2 * m - 1
⊢ ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inl
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
b : α
x✝ : b ∈ s
⊢ ¬b = b → b ∉ s ∧ b ≤ b ↔ b ≤ b ∧ (b ∈ s → b = b)

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
x✝ : b ∈ s
hba : b ≠ a
⊢ ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h✝ : a ∈ s
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h✝ : a ∉ s
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t) ∧ toColex s ≠ toColex t ↔ ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Colex (Finset α)
⊢ (∀ (h : s ≠ t), (ofColex s ∆ ofColex t).max' ⋯ ∈ ofColex t) ∧ s ≠ t ↔
    ∃ (h : s ≠ t), (ofColex s ∆ ofColex t).max' ⋯ ∈ ofColex t

Tactic:
aesop

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
v : ℙ K V
b : V
hb : b ≠ 0
x : Kˣ
ha : x • b ≠ 0
⊢ K ∙ ↑⟨x • b, ha⟩ = K ∙ ↑⟨b, hb⟩

Tactic:
exact Submodule.span_singleton_group_smul_eq _ x _

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ (crossProduct v) w = 0 → ¬LinearIndependent F ![v, w]

Tactic:
have hv' : v = ![v 0, v 1, v 2] := by simp [← List.ofFn_inj]

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
⊢ (crossProduct v) w = 0 → ¬LinearIndependent F ![v, w]
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
u : V
hu : u ≠ 0
h : (mk K u hu).submodule = v.submodule
⊢ mk K u hu = v

Tactic:
| h u hu =>

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

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
v : ℙ K V
u : V
hu : u ≠ 0
h : map f hf (mk K u hu) = map f hf v
⊢ mk K u hu = v

Tactic:
| h u hu =>

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

Goal state before:
pp: case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (n + 1 + 1))) = numDerangements (n + 1 + 1)

Tactic:
rw [numDerangements_add_two, card_derangements_fin_add_two, mul_add, hyp, hyp]

Goal state after:
case ind.succ.succ.a
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ n + 1 < n + 1 + 1

case ind.succ.succ.a
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ n < n + 1 + 1
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
⊢ a •> A ⊆ B * A ∧ b •> A ⊆ B * A

Tactic:
exact ⟨smul_finset_subset_mul ha, smul_finset_subset_mul hb⟩

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: K : Type u_3
inst✝ : Field K
a b c d : ℙ K (Fin 3 → K)
hac : a.orthogonal c
hbc : b.orthogonal c
had : a.orthogonal d
hbd : b.orthogonal d
⊢ a = b ∨ c = d

Tactic:
induction a with

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

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∀ ⦃x : ℕ × ℕ⦄,
    x ∈ ↑(antidiagonal n) →
      ∀ ⦃y : ℕ × ℕ⦄,
        y ∈ ↑(antidiagonal n) →
          x ≠ y →
            ∀ ⦃a : BinaryTree Unit⦄,
              a ∈ pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2) →
                a ∉ pairwiseNode (treesOfNumNodesEq y.1) (treesOfNumNodesEq y.2)

Tactic:
aesop

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

Goal state before:
pp: p✝ q : DyckWord
p : AddUnits DyckWord
⊢ p = default

Tactic:
obtain ⟨a, b, h, -⟩ := p
    obtain ⟨ha, hb⟩ := append_eq_nil_iff.mp (toList_eq_nil.mpr h)
    congr
    · exact toList_eq_nil.mp ha
    · exact toList_eq_nil.mp hb

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

Goal state before:
pp: case a
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
j : ℕ
hj : j ∈ ((a ::ₘ m).toFinset.erase 0).erase a
⊢ (count j m)! = (count j (a ::ₘ m))!

Tactic:
· simp [Finset.mem_erase.mp hj]

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ count U ↑p = count D ↑p

Tactic:
p.count_U_eq_count_D

Goal state after:
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ count D ↑p = count D ↑p
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ (mu 𝕜 * zeta 𝕜) a b = ∑ x ∈ Icc a b, (mu 𝕜) a x

Tactic:
rw [mul_apply]

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, (mu 𝕜) a x
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, (mu 𝕜) a x

Tactic:
congr! with x hx

Goal state after:
case a
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ (mu 𝕜) a x * (zeta 𝕜) x b = (mu 𝕜) a x
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ (zeta 𝕜 * mu' 𝕜) a b = ∑ x ∈ Icc a b, (mu' 𝕜) x b

Tactic:
rw [mul_apply]

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (mu' 𝕜) x b = ∑ x ∈ Icc a b, (mu' 𝕜) x b
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (mu' 𝕜) x b = ∑ x ∈ Icc a b, (mu' 𝕜) x b

Tactic:
congr! with x hx

Goal state after:
case a
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (mu' 𝕜) x b = (mu' 𝕜) x b
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) = ∑ x ∈ Icc a b, mud a x

Tactic:
congr! with x hx

Goal state after:
case a
𝕜 : 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 : αᵒᵈ
hx : x ∈ Icc a b
⊢ (if x ≤ b then mud a x else 0) = mud a x
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U ↑q = count D ↑q
⊢ count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)

Tactic:
rw [← h] at hq ⊢

Goal state after:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U (r' ++ ↑p) = count D (r' ++ ↑p)
⊢ count U (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)) =
    count D (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p))
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
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)⌋₊
A : Finset G
hA : t + 1 ≤ #A
⊢ (1 - K) * (↑t + 1) ≤ (1 - K) * ↑(#A)

Tactic:
norm_cast; gcongr

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

Goal state before:
pp: case e'_3.e'_4
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ G₂.IsLink = G₁.IsLink

pp: case e'_3.e'_5
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ E(G₂) = E(G₁)

Tactic:
· simp [funext_iff, h]

Goal state after:
case e'_3.e'_5
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ E(G₂) = E(G₁)
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u✝ v✝ w : α
e f : β
G H : Graph α β
vertexSet : Set α
edgeSet✝ : Set β
u v : α
edgeSet : Set β
⊢ ∀ ⦃e : β⦄ ⦃x y v_1 w : α⦄,
    e ∈ edgeSet ∧ (x = u ∧ y = v ∨ x = v ∧ y = u) → e ∈ edgeSet ∧ (v_1 = u ∧ w = v ∨ v_1 = v ∧ w = u) → x = v_1 ∨ x = w

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u✝ v✝ w : α
e f : β
G H : Graph α β
vertexSet : Set α
edgeSet✝ : Set β
u v : α
edgeSet : Set β
⊢ ∀ (e : β), e ∈ edgeSet ↔ ∃ x y, e ∈ edgeSet ∧ (x = u ∧ y = v ∨ x = v ∧ y = u)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ e ∈ edgeSet → ((∃ x_1, x = u ∧ x_1 = v ∨ x = v ∧ x_1 = u) ↔ x = u ∨ x = v)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ (e ∈ edgeSet ∧ (x = u ∨ x = v)) ∧ ¬(e ∈ edgeSet ∧ (x = u ∧ x = v ∨ x = v ∧ x = u)) ↔
    e ∈ edgeSet ∧ (x = u ∨ x = v) ∧ u ≠ v

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ e ∈ edgeSet → (x = u ∧ x = v ∨ x = v ∧ x = u ↔ x = u ∧ u = v)

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι' → α') → κ
c : κ
⊢ ∀ (a : η' → α'),
    (C fun x ↦ eα (Sum.elim id (⇑eα.symm ∘ a ∘ ⇑eη) (l.idxFun (eι.symm x)))) = c ↔
      C (⇑eα ∘ ↑l ((eη.arrowCongr eα).symm a) ∘ ⇑eι.symm) = c

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case cons'
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
ih : ∃ n, ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), a.head * m * m' ∈ FP a

Tactic:
obtain ⟨n, hn⟩ := ih
    use n + 1
    intro m' hm'
    rw [mul_assoc]
    exact FP.cons _ _ (hn _ hm')

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBasis B (M.E \ D)
hss : B ⊆ M.E ∧ Disjoint B D
hcl : M.IsBasis B M.E
⊢ M.IsBase B ∧ Disjoint B D

Tactic:
isBasis_ground_iff

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBasis B (M.E \ D)
hss : B ⊆ M.E ∧ Disjoint B D
hcl : M.IsBase B
⊢ M.IsBase B ∧ Disjoint B D
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D S : Set α
hD : M.Coindep D
⊢ S ⊆ M.E → Disjoint S D → ((∃ B, M.IsBase B ∧ Disjoint B D ∧ B ⊆ S) ↔ ∃ B, M.IsBase B ∧ B ⊆ S)

Tactic:
refine fun hSE hSD ↦ ⟨fun ⟨B, hB, hBD, hBS⟩ ↦ ⟨B, hB, hBS⟩, fun ⟨B, hB, hBS⟩ ↦ ⟨B, hB, ?_, hBS⟩⟩

Goal state after:
α : Type u_1
M : Matroid α
D S : Set α
hD : M.Coindep D
hSE : S ⊆ M.E
hSD : Disjoint S D
x✝ : ∃ B, M.IsBase B ∧ B ⊆ S
B : Set α
hB : M.IsBase B
hBS : B ⊆ S
⊢ Disjoint B D
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ e ∈ M.closure I \ I

Tactic:
hI.closure_eq_closure

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ e ∈ M.closure X \ I
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
⊢ (Matroid.sigma M).IsBasis I X ↔ ∀ (i : ι), (M i).IsBasis (Sigma.mk i ⁻¹' I) (Sigma.mk i ⁻¹' X)

Tactic:
simp only [IsBasis, sigma_indep_iff, maximal_subset_iff, and_imp, and_assoc, sigma_ground_eq,
    forall_and, and_congr_right_iff]

Goal state after:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
⊢ (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) →
    ((I ⊆ X ∧
        (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
          X ⊆ univ.sigma fun i ↦ (M i).E) ↔
      (∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X) ∧
        (∀ (x : ι) ⦃t : Set (α x)⦄,
            (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t) ∧
          ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
⊢ (Disjoint {e} I ∧ e ∈ M.closure I \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C

Tactic:
hI.closure_eq_closure

Goal state after:
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
⊢ (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ (M ／ C).IsNonloop e ↔ e ∈ M.E \ M.closure C

Tactic:
isNonloop_iff_mem_compl_loops,

Goal state after:
α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ e ∈ (M ／ C).E \ (M ／ C).loops ↔ e ∈ M.E \ M.closure C
Module: Mathlib.Combinatorics.Quiver.Path.Weight

Goal state before:
pp: V : Type u_1
inst✝³ : Quiver V
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 ≤ w e
i j : V
p : Path i j
⊢ 0 ≤ weight (fun {i j} ↦ w) p

Tactic:
by
  induction p with
  | nil =>
      simp
  | cons p e ih =>
      have he : 0 ≤ w e := hw e
      simpa [weight_cons] using mul_nonneg ih he

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

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a x✝ : α
⊢ x✝ ∈ {b | b ∈ s ⊻ t ∧ b ≤ a} ↔ x✝ ∈ {b | b ∈ s ∧ b ≤ a} ⊻ {b | b ∈ t ∧ b ≤ a}

Tactic:
aesop

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

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a x✝ : α
⊢ x✝ ∈ {b | b ∈ s ⊼ t ∧ a ≤ b} ↔ x✝ ∈ {b | b ∈ s ∧ a ≤ b} ⊼ {b | b ∈ t ∧ a ≤ b}

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ insert 0 A
⊢ ∀ n > 0, n ∈ insert 0 A ↔ n ∈ A

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ A \ {0}
⊢ ∀ n > 0, n ∈ A \ {0} ↔ n ∈ A

Tactic:
aesop

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝓓 a 𝒜 ∧ s.erase a ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜

Tactic:
exact h.1

Goal state after: