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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h₂ : p₂.IsTrail
w✝¹ : G.Walk v' v
w✝ : G.Walk w w'
h : p₂ = (w✝¹.append p₁).append w✝
⊢ p₁.IsTrail

Tactic:
rw [h] at h₂

Goal state after:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
w✝¹ : G.Walk v' v
w✝ : G.Walk w w'
h₂ : ((w✝¹.append p₁).append w✝).IsTrail
h : p₂ = (w✝¹.append p₁).append w✝
⊢ p₁.IsTrail
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h₂ : p₂.IsPath
w✝¹ : G.Walk v' v
w✝ : G.Walk w w'
h : p₂ = (w✝¹.append p₁).append w✝
⊢ p₁.IsPath

Tactic:
rw [h] at h₂

Goal state after:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
w✝¹ : G.Walk v' v
w✝ : G.Walk w w'
h₂ : ((w✝¹.append p₁).append w✝).IsPath
h : p₂ = (w✝¹.append p₁).append w✝
⊢ p₁.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
⊢ p.getVert i = u ↔ i = 0

Tactic:
cases p
  · simpa using hi
  · exact hp.getVert_eq_start_iff_of_not_nil not_nil_cons

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.length + 1 ≤ k
⊢ p.support[k]? = q.support[k]?

Tactic:
have ht : q.length + 1 ≤ k := hl ▸ hk

Goal state after:
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.length + 1 ≤ k
ht : q.length + 1 ≤ k
⊢ p.support[k]? = q.support[k]?
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: 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
⊢ p = q

Tactic:
suffices ∀ k : ℕ, p.support[k]? = q.support[k]? by
    exact ext_support <| List.ext_getElem?_iff.mpr this
  intro k
  cases le_or_gt k p.length with
  | inl hk =>
    rw [← getVert_eq_support_getElem? p hk, ← getVert_eq_support_getElem? q (hl ▸ hk)]
    exact congrArg some (h k hk)
  | inr hk =>
    replace hk : p.length + 1 ≤ k := hk
    have ht : q.length + 1 ≤ k := hl ▸ hk
    rw [← length_support, ← List.getElem?_eq_none_iff] at hk ht
    rw [hk, ht]

Goal state after:
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
| (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))

Tactic:
SimpleGraph.edgeDensity,

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
| (1 + ε ^ 5 / 49) * ↑(edgeDensity G.Adj (A.biUnion id) (B.biUnion id))
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
x : V
w : G.Walk u v
hw : w.IsTrail
hx : x ∈ w.support
⊢ ((w.takeUntil x hx).edges ++ (w.dropUntil x hx).edges).Nodup

Tactic:
by simpa [← edges_append] using hw.edges_nodup

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
⊢ ∃ w ∈ p.support, w ∈ q.support ∧ ∃ c, c.IsCycle ∧ c.support <+ p.support ++ q.support.reverse.tail

Tactic:
have ⟨u', v', p', q', hp', hq', hcyc⟩ := hp.exists_isCycle_of_ne hq h
  use u', hp'.support_subset p'.start_mem_support, hq'.support_subset q'.start_mem_support
  refine ⟨_, hcyc, ?_⟩
  rw [support_append, support_reverse]
  refine .append ?_ <| .tail <| .reverse ?_
  · exact isSubwalk_iff_support_isInfix.mp hp' |>.sublist
  · exact isSubwalk_iff_support_isInfix.mp hq' |>.sublist

Goal state after:
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:
rw [isTrail_def]
  rw [isTrail_def, edges_map] at hp
  exact hp.of_map

Goal state after:
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
p : G.Walk u u
hp : (Walk.map f p).IsTrail ∧ ¬Walk.map f p = nil
⊢ p.IsTrail ∧ ¬p.Nil

Tactic:
eq_nil_iff_nil,

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hp : (Walk.map f p).IsTrail ∧ ¬(Walk.map f p).Nil
⊢ p.IsTrail ∧ ¬p.Nil
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
p : G.Walk u u
hinj : Injective ⇑f
⊢ p.IsTrail ∧ ¬Walk.map f p = nil ↔ p.IsTrail ∧ ¬p = nil

Tactic:
eq_nil_iff_nil,

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective ⇑f
⊢ p.IsTrail ∧ ¬(Walk.map f p).Nil ↔ p.IsTrail ∧ ¬p = nil
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
p : G.Walk u u
hinj : Injective ⇑f
⊢ p.IsTrail ∧ ¬(Walk.map f p).Nil ↔ p.IsTrail ∧ ¬p = nil

Tactic:
eq_nil_iff_nil,

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective ⇑f
⊢ p.IsTrail ∧ ¬(Walk.map f p).Nil ↔ p.IsTrail ∧ ¬p.Nil
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
p : G.Walk u u
hp : (Walk.map f p).IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup
⊢ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup

Tactic:
eq_nil_iff_nil,

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hp : (Walk.map f p).IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup
⊢ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
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
p : G.Walk u u
hinj : Injective ⇑f
⊢ p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup

Tactic:
eq_nil_iff_nil,

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective ⇑f
⊢ p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
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
p : G.Walk u u
hinj : Injective ⇑f
⊢ p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup

Tactic:
eq_nil_iff_nil,

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective ⇑f
⊢ p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
⊢ ε ≤ 0

Tactic:
have := h₀ (empty_subset _)

Goal state after:
α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
this : (fun H ↦ H.CliqueFree 3) (G.deleteEdges ↑∅) → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#∅)
⊢ ε ≤ 0
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
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤
    ↑(#({x ∈ s ×ˢ t ×ˢ u |
          match x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}))

Tactic:
have h₁ : #(badVertices G ε s t) ≤ #s * ε := G.card_badVertices_le dst hst
  have h₂ : #(badVertices G ε s u) ≤ #s * ε := G.card_badVertices_le dsu usu
  let X' := s \ (badVertices G ε s t ∪ badVertices G ε s u)
  have : X'.biUnion _ ⊆ (s ×ˢ t ×ˢ u).filter fun (a, b, c) ↦ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c :=
    triangle_split_helper _
  refine le_trans ?_ (Nat.cast_le.2 <| card_le_card this)
  rw [card_biUnion, Nat.cast_sum]
  · apply le_trans _ (card_nsmul_le_sum X' _ _ <| G.good_vertices_triangle_card dst dsu dtu utu)
    rw [nsmul_eq_mul]
    have := hst.pos.le
    suffices hX' : (1 - 2 * ε) * #s ≤ #X' by
      exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)
    have i : badVertices G ε s t ∪ badVertices G ε s u ⊆ s :=
      union_subset (filter_subset _ _) (filter_subset _ _)
    rw [sub_mul, one_mul, card_sdiff_of_subset i, Nat.cast_sub (card_le_card i),
      sub_le_sub_iff_left, mul_assoc, mul_comm ε, two_mul]
    refine (Nat.cast_le.2 <| card_union_le _ _).trans ?_
    rw [Nat.cast_add]
    gcongr
  rintro a _ b _ t
  rw [Function.onFun, Finset.disjoint_left]
  simp only [Prod.forall, mem_image, not_exists, Prod.mk_inj,
    exists_imp, and_imp, not_and]
  aesop

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 σ
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₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ ∑ a, (∏ j, x₀ j ^ d ↑j) * a ^ d i = (∏ j, x₀ j ^ d ↑j) * ∑ a, a ^ d i

Tactic:
rw [mul_sum]

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx : x ∉ S
⊢ ∃ i ∈ s, (eval x) (f i) ≠ 0

Tactic:
by
        simpa [hS, not_forall, Classical.not_imp] using hx

Goal state after:
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
this : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : ↑n ∣ ∑ i ∈ t₀, a i
h : t₀ ∈ 𝒜
⊢ n = 0

Tactic:
simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id h

Goal state after:
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 : (crossProduct v) w ≠ 0
⊢ (if h : (crossProduct v) w = 0 then mk F v hv else mk F ((crossProduct v) w) h) = mk F ((crossProduct v) w) h

Tactic:
dif_neg h

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : (crossProduct v) w ≠ 0
⊢ mk F ((crossProduct v) w) h = mk F ((crossProduct v) w) h
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: 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
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : Fintype.card L ≤ #s
⊢ Fintype.card P ≤ #(s.biUnion t)

Tactic:
(Finset.card_le_univ _).ge_iff_eq',

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
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : Fintype.card L = #s
⊢ Fintype.card P = #(s.biUnion t)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c✝ d✝ x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
h₃ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (c * d) •> A))
t : G
ht : t ∈ A ∧ d⁻¹ * (c⁻¹ * t) ∈ A ∧ a * (b * t) ∈ A
⊢ a * b * (c * d) ∈ A⁻¹ * A

Tactic:
rw [← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h), mem_mul]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c✝ d✝ x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
h₃ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (c * d) •> A))
t : G
ht : t ∈ A ∧ d⁻¹ * (c⁻¹ * t) ∈ A ∧ a * (b * t) ∈ A
⊢ ∃ y ∈ A, ∃ z ∈ A⁻¹, y * z = a * b * (c * d)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: s : DyckStep
⊢ s = U ∨ s = D

Tactic:
cases s

Goal state after:
case U
⊢ U = U ∨ U = D

case D
⊢ D = U ∨ D = D
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case cons.nil
s : DyckStep
bal : count U [s] = count D [s]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i [s]) ≤ count U (take i [s])
h : { toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ 0
h' : ↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ take 1 (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).head h']

Tactic:
cases s

Goal state after:
case cons.nil.U
bal : count U [U] = count D [U]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i [U]) ≤ count U (take i [U])
h : { toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ 0
h' : ↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ take 1 (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).head h']

case cons.nil.D
bal : count U [D] = count D [D]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i [D]) ≤ count U (take i [D])
h : { toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ 0
h' : ↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ take 1 (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).head h']
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case cons.nil
q : DyckWord
i : ℕ
s : DyckStep
bal : count U [s] = count D [s]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (List.take i [s]) ≤ count U (List.take i [s])
hn : { toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h : ↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
l1 :
  List.take 1 ↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).head h]
⊢ (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 =
    (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 - 1 + 1

Tactic:
cases s

Goal state after:
case cons.nil.U
q : DyckWord
i : ℕ
bal : count U [U] = count D [U]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (List.take i [U]) ≤ count U (List.take i [U])
hn : { toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h : ↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
l1 :
  List.take 1 ↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).head h]
⊢ (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 =
    (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 - 1 + 1

case cons.nil.D
q : DyckWord
i : ℕ
bal : count U [D] = count D [D]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (List.take i [D]) ≤ count U (List.take i [D])
hn : { toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h : ↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
l1 :
  List.take 1 ↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).head h]
⊢ (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 =
    (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 - 1 + 1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case e'_6
p : DyckWord
s : DyckStep
⊢ (s == U) = decide ¬(s == D) = true

Tactic:
cases s

Goal state after:
case e'_6.U
p : DyckWord
⊢ (U == U) = decide ¬(U == D) = true

case e'_6.D
p : DyckWord
⊢ (D == U) = decide ¬(D == D) = true
Module: Mathlib.Combinatorics.Enumerative.Bell

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

Tactic:
factorial_zero,

Goal state after:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ 1 = ∏ x ∈ ∅.erase 0, (count x (replicate 0 n))!
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B

Tactic:
have : (#(A ∩ B) + #(A ∪ B) : ℝ) = #A + #B := mod_cast card_inter_add_card_union A B

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
this : ↑(#(A ∩ B)) + ↑(#(A ∪ B)) = ↑(#A) + ↑(#B)
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

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

Tactic:
obtain ⟨A, hA, hSA⟩ := exists_nonempty_isFragment hK hS

Goal state after:
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
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
k : ℕ
⊢ Multipliable fun n ↦ 1 - X ^ (n + k + 1)

Tactic:
by
  simpa [sub_eq_add_neg] using
    multipliable_one_add_of_tendsto_order_atTop_nhds_top R (tendsto_order_neg_X_pow R k)

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

Goal state before:
pp: n✝ : ℕ
x✝ : 0 < n✝ + 1
⊢ stirlingSecond 0 (n✝ + 1) = 0

Tactic:
rw [stirlingSecond]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : CommRing α
s✝ : Finset α
x : α × α × α
s : Finset α
⊢ Function.Injective fun xa ↦ (xa.1, xa.1 + xa.2, xa.1 + 2 * xa.2)

Tactic:
rintro ⟨x, a⟩ ⟨y, b⟩ h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : CommRing α
s✝ : Finset α
x✝ : α × α × α
s : Finset α
x a y b : α
h : (fun xa ↦ (xa.1, xa.1 + xa.2, xa.1 + 2 * xa.2)) (x, a) = (fun xa ↦ (xa.1, xa.1 + xa.2, xa.1 + 2 * xa.2)) (y, b)
⊢ (x, a) = (y, b)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case calc_1
n : ℕ
⊢ ↑n ≤ (2 * ↑(n / 6) + (1 + 2) - 1) * 3

Tactic:
add_sub_assoc,

Goal state after:
case calc_1
n : ℕ
⊢ ↑n ≤ (2 * ↑(n / 6) + (1 + 2 - 1)) * 3
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
M' : Type (max 0 u_1) := { m // m ∈ s }
⊢ ∃ m ∈ s, m * m = m

Tactic:
let : Semigroup M' :=
    { mul := fun p q => ⟨p.1 * q.1, s_add _ p.2 _ q.2⟩
      mul_assoc := fun p q r => Subtype.ext (mul_assoc _ _ _) }

Goal state after:
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
M' : Type (max 0 u_1) := { m // m ∈ s }
this : Semigroup M' := { mul := fun p q ↦ ⟨↑p * ↑q, ⋯⟩, mul_assoc := ⋯ }
⊢ ∃ m ∈ s, m * m = m
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
e✝ e' f✝ : Set α
H✝ H : Hypergraph α
f : α → β
e : Set α
he : e ∈ E(H)
⊢ f '' e ⊆ f '' V(H)

Tactic:
exact image_mono he.subset_vertexSet

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
e : α
he : M.IsLoop e
heN : e ∈ N.E
hNM : N ≤m M
⊢ N.IsLoop e

Tactic:
rw [← singleton_dep] at he ⊢
  exact he.of_isMinor (by simpa) hNM

Goal state after: