mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
i : ℕ
x✝ : i + 1 ≠ 0
⊢ p.tail.getVert i ∈ p.tail.support

Tactic:
exact getVert_mem_support ..

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.support[k]? = none
ht : q.support[k]? = none
⊢ p.support[k]? = q.support[k]?

Tactic:
rw [hk, ht]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
⊢ ∀ ⦃y : α⦄, y ∈ s → x ≠ y → (G ⊔ edge v w).Adj x y

Tactic:
y

Goal state after:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
⊢ y ∈ s → x ≠ y → (G ⊔ edge v w).Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : V
hu : u ∈ {w | w ∈ p.support}
v : V
hv : v ∈ {w | w ∈ p.support}
hf : f u = f v
⊢ u = v

Tactic:
obtain ⟨u, rfl⟩ := List.get_of_mem hu

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
v : V
hv : v ∈ {w | w ∈ p.support}
u : Fin p.support.length
hu : p.support.get u ∈ {w | w ∈ p.support}
hf : f (p.support.get u) = f v
⊢ p.support.get u = v
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : p.support.get u ∈ {w | w ∈ p.support}
v : Fin p.support.length
hv : p.support.get v ∈ {w | w ∈ p.support}
hf : f (p.support.get u) = f (p.support.get v)
⊢ p.support.get u = p.support.get v

Tactic:
congr

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : p.support.get u ∈ {w | w ∈ p.support}
v : Fin p.support.length
hv : p.support.get v ∈ {w | w ∈ p.support}
hf : f (p.support.get u) = f (p.support.get v)
⊢ u = v
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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x : Finset α
⊢ ∀ (b : Finset α),
    x ∈ A →
      b ∈ B →
        ↑(#(interedges G.Adj x b)) / (↑(#x) * ↑(#b) * (↑(#A) * ↑(#B))) ≤
          ↑(#(interedges G.Adj x b)) * ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))))

Tactic:
y

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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
⊢ x ∈ A →
    y ∈ B →
      ↑(#(interedges G.Adj x y)) / (↑(#x) * ↑(#y) * (↑(#A) * ↑(#B))) ≤
        ↑(#(interedges G.Adj x y)) * ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))))
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map (⇑f) G).IsClique ↑s
hn : #s ≠ 1
⊢ ∀ x ∈ s, x ∈ Set.range ⇑f

Tactic:
rintro a ha

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map (⇑f) G).IsClique ↑s
hn : #s ≠ 1
a : β
ha : a ∈ s
⊢ a ∈ Set.range ⇑f
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ a ∈ G.edgeFinset, 1 ≤ #(bipartiteAbove (fun e s ↦ e ∈ s.sym2) (G.cliqueFinset 3) a)

Tactic:
simpa [Sym2.forall, Nat.one_le_iff_ne_zero, -Finset.card_eq_zero, Finset.card_ne_zero,
        Finset.Nonempty]
      using hG.2

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ⊆ t
⊢ t ⊆ ↑s

Tactic:
by
      by_contra hc
      have fint := ofFinite t
      have ne : s ≠ t.toFinset := fun a ↦ by subst a; simp_all[Set.coe_toFinset, not_true_eq_false]
      have hle : #t.toFinset ≤ #s := M.maximum t.toFinset (by simp [Set.coe_toFinset, ht])
      have hlt : #s < #t.toFinset :=
        card_lt_card (ssubset_of_ne_of_subset ne (Set.subset_toFinset.mpr hsub))
      exact lt_irrefl _ (lt_of_lt_of_le hlt hle)

Goal state after:
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 × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
⊢ False

Tactic:
cornersTheoremBound,

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ + 1 ≤ Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
⊢ False
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #({x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}) =
    #((s * t).disjiUnion (fun x ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) ⋯)

Tactic:
congr

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ {x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2} =
    (s * t).disjiUnion (fun x ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) ⋯
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree ↑A
⊢ ∀ a ∈ A, a < 2 * n + 1

Tactic:
rintro a ha

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree ↑A
a : ℕ
ha : a ∈ A
⊢ a < 2 * n + 1
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:

Tactic:
(∑ x : σ → K, f.coeff d * ∏ i, x i ^ d i) = f.coeff d * ∑ x : σ → K, ∏ i, x i ^ d i :=
      (mul_sum ..).symm
    _ = 0 := (mul_eq_zero.mpr ∘ Or.inr) ?_

Goal state after:
K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
⊢ ∑ x, ∏ i, x i ^ d i = 0
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case bit
b : Bool
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
⊢ (map (fun i ↦ 2 ^ i) (bit b n).bitIndices).sum = bit b n

Tactic:
have hrw : (fun i ↦ 2 ^ i) ∘ (fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i := by
      ext i; simp [pow_add, mul_comm]

Goal state after:
case bit
b : Bool
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i
⊢ (map (fun i ↦ 2 ^ i) (bit b n).bitIndices).sum = bit b n
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: 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 : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
⊢ 2 * (m * n) - k * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t

Tactic:
tsub_right_comm,

Goal state after:
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 : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
⊢ 2 * (m * n) - 1 - k * n = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
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 w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ mk K v hv = mk K w hw ↔ ∃ a, a • w = v

Tactic:
by
  rw [mk_eq_mk_iff K v w hv hw]
  constructor
  · rintro ⟨a, ha⟩
    exact ⟨a, ha⟩
  · rintro ⟨a, ha⟩
    refine ⟨Units.mk0 a fun c => hv.symm ?_, ha⟩
    rwa [c, zero_smul] at ha

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
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : True → -w 0 = 0 ∧ v 0 = 0
h21 : True → -w 1 = 0 ∧ v 1 = 0
h22 : True → -w 2 = 0 ∧ v 2 = 0
⊢ False

Tactic:
rw [hv', cons_eq_zero_iff, cons_eq_zero_iff, cons_eq_zero_iff, zero_empty] at hv

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬(v 0 = 0 ∧ v 1 = 0 ∧ v 2 = 0 ∧ ![] = ![])
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : True → -w 0 = 0 ∧ v 0 = 0
h21 : True → -w 1 = 0 ∧ v 1 = 0
h22 : True → -w 2 = 0 ∧ v 2 = 0
⊢ False
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ (mk F v hv).cross (mk F w hw) = mk F ((crossProduct v) w) ⋯

Tactic:
rw [cross_mk_of_cross_ne_zero]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
hst : s < t
⊢ (fun s ↦ ∑ k ∈ ofColex s, n ^ k) s < (fun s ↦ ∑ k ∈ ofColex s, n ^ k) t

Tactic:
Colex.lt_iff_exists_forall_lt

Goal state after:
n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
hst : ∃ a ∈ ofColex t, a ∉ ofColex s ∧ ∀ b ∈ ofColex s, b ∉ ofColex t → b < a
⊢ (fun s ↦ ∑ k ∈ ofColex s, n ^ k) s < (fun s ↦ ∑ k ∈ ofColex s, n ^ k) t
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
⊢ #s ≤ #(s.biUnion t)

Tactic:
by_cases hs₁ : #s = 1

Goal state after:
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : #s = 1
⊢ #s ≤ #(s.biUnion t)

case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
⊢ #s ≤ #(s.biUnion t)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
p₁ p₂ : P
hp₁ : ∀ x ∈ s, p₁ ∈ x
hp₂ : ∀ x ∈ s, p₂ ∈ x
⊢ p₁ = p₂

Tactic:
obtain ⟨l₁, l₂, hl₁, hl₂, hl₃⟩ :=
        Finset.one_lt_card_iff.mp (Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hs₀, hs₁⟩)

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
p₁ p₂ : P
hp₁ : ∀ x ∈ s, p₁ ∈ x
hp₂ : ∀ x ∈ s, p₂ ∈ x
l₁ l₂ : L
hl₁ : l₁ ∈ s
hl₂ : l₂ ∈ s
hl₃ : l₁ ≠ l₂
⊢ p₁ = p₂
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case neg.intro
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this✝ : Fintype { p // p ∈ l }
val✝ : Fintype { l // p ∈ l }
this : ∀ (p' : { p // p ∈ l }), p ≠ ↑p'
⊢ Fintype.card { p // p ∈ l } ≤ Fintype.card { l // p ∈ l }

Tactic:
exact
    Fintype.card_le_of_injective (fun p' => ⟨mkLine (this p'), (mkLine_ax (this p')).1⟩)
      fun p₁ p₂ hp =>
      Subtype.ext ((eq_or_eq p₁.2 p₂.2 (mkLine_ax (this p₁)).2
            ((congr_arg (_ ∈ ·) (Subtype.ext_iff.mp hp)).mpr (mkLine_ax (this p₂)).2)).resolve_right
          fun h' => (congr_arg (p ∉ ·) h').mp h (mkLine_ax (this p₁)).1)

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
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G}, a ∈ A → a⁻¹ •> ↑A = ↑H
⊢ a •> ↑(stabilizer G A) = ↑A ∧ ↑(stabilizer G A) <• a = ↑A

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
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
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G}, a ∈ A → a⁻¹ •> ↑A = ↑H
⊢ a •> ↑(stabilizer G A) = ↑A

case refine_2
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
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G}, a ∈ A → a⁻¹ •> ↑A = ↑H
⊢ ↑(stabilizer G A) <• a = ↑A
Module: Mathlib.Combinatorics.Derangements.Exponential

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑((k + 1).ascFactorial (n - k)) / ↑n.factorial = (-1) ^ k / ↑k.factorial

Tactic:
Nat.ascFactorial_eq_div,

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑((k + (n - k)).factorial / k.factorial) / ↑n.factorial = (-1) ^ k / ↑k.factorial
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
x✝¹ x✝ : V
⊢ ⊥.toSimpleGraphInclusive.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Tactic:
exact ⟨fun ⟨_, h⟩ ↦ by tauto, False.elim⟩

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

Goal state before:
pp: V : Type u_1
x✝¹ x✝ : V
⊢ ⊥.toSimpleGraphStrict.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Tactic:
exact ⟨fun ⟨_, h⟩ ↦ by tauto, False.elim⟩

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

Goal state after:
case e_f
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ (fun x ↦ ↑(catalan ↑x) * ↑(catalan (d - ↑x))) = fun i ↦
    ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1))
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
⊢ (∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) *
      (∑ k ∈ m.toFinset, k * count k m)! =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !

Tactic:
congr

Goal state after:
case e_a
m : Multiset ℕ
⊢ (∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
      ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    ∏ i ∈ m.toFinset, (i * count i m)!

case e_a
m : Multiset ℕ
⊢ ∑ k ∈ m.toFinset, k * count k m = m.sum
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q a b : DyckWord
h : a + b = 0
neg_val✝ : b + a = 0
ha : ↑a = []
hb : ↑b = []
⊢ { val := a, neg := b, val_neg := h, neg_val := neg_val✝ } = default

Tactic:
congr

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

case e_neg
p q a b : DyckWord
h : a + b = 0
neg_val✝ : b + a = 0
ha : ↑a = []
hb : ↑b = []
⊢ b = 0
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
⊢ S.Nonempty

Tactic:
simpa [S]

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

Goal state before:
pp: case mk.mk
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Zero 𝕜
inst✝ : LE α
a b : α
toFun✝¹ : α → α → 𝕜
eq_zero_of_not_le'✝¹ : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun✝¹ a b = 0
toFun✝ : α → α → 𝕜
eq_zero_of_not_le'✝ : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun✝ a b = 0
h :
  { toFun := toFun✝¹, eq_zero_of_not_le' := eq_zero_of_not_le'✝¹ }.toFun =
    { toFun := toFun✝, eq_zero_of_not_le' := eq_zero_of_not_le'✝ }.toFun
⊢ { toFun := toFun✝¹, eq_zero_of_not_le' := eq_zero_of_not_le'✝¹ } =
    { toFun := toFun✝, eq_zero_of_not_le' := eq_zero_of_not_le'✝ }

Tactic:
congr

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

Goal state before:
pp: case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ ∏ x ∈ ∅.erase 0, (count x (replicate 0 n))! = 1

Tactic:
rw [show (∅ : Finset ℕ).erase 0 = ∅ from rfl, Finset.prod_empty]

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

Goal state before:
pp: case a
n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
i : ℕ
a✝ : i ∈ Finset.Iic n
⊢ n.choose i * (n - i).bell = ∑ q, n.choose i * q.parts.bell

Tactic:
simp [ih (n - i) _, Finset.mul_sum]

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

Goal state before:
pp: case neg
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : ¬a = b
h : ¬-∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b ↑x = 0
⊢ a ≤ b

Tactic:
rw [neg_eq_zero] at h
        obtain ⟨⟨x, hx⟩, -⟩ := exists_ne_zero_of_sum_ne_zero h
        exact (nonempty_Ioc.1 ⟨x, hx⟩).le

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
⊢ zeta 𝕜 * mu' 𝕜 = 1

Tactic:
zeta_mul_mu'

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
⊢ 1 = 1
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 : α
this✝ : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 = 1
⊢ mu 𝕜 = mud

Tactic:
← mu_mul_zeta

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 = mu 𝕜 * zeta 𝕜
⊢ mu 𝕜 = mud
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

Goal state before:
pp: x : ℤ
⊢ ∀ ⦃a₂ : ℤ⦄, pentagonal x = pentagonal a₂ → x = a₂

Tactic:
y

Goal state after:
x y : ℤ
⊢ pentagonal x = pentagonal y → x = y
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
A : Finset G
hA : A.Nonempty
hSA : IsFragment K S A
⊢ 0 < connectivity K S

Tactic:
exact (expansion_pos hK hS hA).trans_eq hSA

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum (fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) (pentagonalSeries R)
x : ℤ
hx : x ∉ Set.range Neg.neg
⊢ ↑↑x.negOnePow * X ^ pentagonal x = 0

Tactic:
by absurd hx; use -x; simp

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

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

Tactic:
congr

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum ((fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) ∘ Neg.neg) (pentagonalSeries R)
k : ℕ
⊢ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1)) =
    ((fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) ∘ Neg.neg) ↑k +
      ((fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) ∘ Neg.neg) (-(↑k + 1))

Tactic:
Function.comp_apply,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum ((fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) ∘ Neg.neg) (pentagonalSeries R)
k : ℕ
⊢ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1)) =
    ↑↑(-↑k).negOnePow * X ^ pentagonal (-↑k) + ↑↑(- -(↑k + 1)).negOnePow * X ^ pentagonal (- -(↑k + 1))
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: ⊢ (fun n ↦ 2) =o[atTop] fun n ↦ ↑n / 3

Tactic:
simpa [div_eq_inv_mul, Function.comp_def] using
        .atTop_of_const_mul₀ zero_lt_three (by simp [tendsto_natCast_atTop_atTop])

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
h : G.IsLink e x y
hHG : H ≤ G
he : e ∈ E(H)
⊢ H.IsLink e x y

Tactic:
by
  obtain ⟨u, v, huv⟩ := exists_isLink_of_mem_edgeSet he
  obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := (huv.mono hHG).eq_and_eq_or_eq_and_eq h
  · assumption
  exact huv.symm

Goal state after: