mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b : α
hb : b = a ∨ b ∈ s
c : α
hc : c = a ∨ c ∈ s
d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
⊢ b = c

Tactic:
obtain rfl | hb := hb <;> obtain rfl | hc := hc

Goal state after:
case inl.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
c d : α
h : c * d = c * c
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c
hd : d = c ∨ d ∈ s
⊢ c = c

case inl.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1
ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b
hd : d = b ∨ d ∈ s
hc : c ∈ s
⊢ b = c

case inr.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c
hd : d = c ∨ d ∈ s
⊢ b = c

case inr.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
⊢ b = c
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a : E
ha : a ∈ frontier s
b : E
hb : b ∈ frontier s
c : E
hc : c ∈ frontier s
habc : a + c = b + b
⊢ (1 / 2) • a + (1 / 2) • c = b

Tactic:
← smul_add,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a : E
ha : a ∈ frontier s
b : E
hb : b ∈ frontier s
c : E
hc : c ∈ frontier s
habc : a + c = b + b
⊢ (1 / 2) • (a + c) = b
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ 2 / rexp 1 < 1

Tactic:
div_lt_one (exp_pos _)

Goal state after:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ 2 < rexp 1
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case h
N : ℕ
hN : 4096 ≤ N
⊢ 2 / rexp 1 < 1

Tactic:
div_lt_one (exp_pos _)

Goal state after:
case h
N : ℕ
hN : 4096 ≤ N
⊢ 2 < rexp 1
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:

Tactic:
A ^ m ∩ B ^ n ⊆ (F₁ ^ (m - 1) * A) ∩ (F₂ ^ (n - 1) * B) := by
        gcongr <;> apply pow_subset_pow_mul_of_sq_subset_mul <;> norm_cast <;> lia
      _ = ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), a • A ∩ b • B := by
        simp_rw [← smul_eq_mul, ← iUnion_smul_set, iUnion₂_inter_iUnion₂]; norm_cast
      _ ⊆ ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), f a b • (A⁻¹ * A ∩ (B⁻¹ * B)) := by
        gcongr; exact hf ..
      _ = (Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) * (A ^ 2 ∩ B ^ 2) := by
        simp_rw [hA.inv_eq_self, hB.inv_eq_self, ← sq]
        rw [Finset.coe_image₂, ← smul_eq_mul, ← iUnion_smul_set, biUnion_image2]
        simp_rw [Finset.mem_coe]

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

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A ^ 2 ⊆ ↑{x} • A
⊢ ∃ x, A * A ⊆ x • A

Tactic:
· rw [Finset.coe_singleton, singleton_smul, sq] at hKA
        use x

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ (A <• s).convolution B x = A.convolution (s •> B) x

Tactic:
nth_rw 1 [← inv_inv B, ← inv_inv (s • B), inv_smul_finset_distrib s B, ← card_inter_smul,
    ← card_inter_smul, smul_comm]
  simp [← card_smul_finset (op s) (A ∩ _), smul_finset_inter]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ 2 * #G.edgeFinset =
    #{x |
        match x with
        | (x, y) => G.Adj x y}

Tactic:
rw [← dart_card_eq_twice_card_edges, ← card_univ]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #univ =
    #{x |
        match x with
        | (x, y) => G.Adj x y}
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V ↪ W
inst✝ : Subsingleton V
⊢ SimpleGraph.map (⇑f) G ≤ G'

Tactic:
by
  rw [map_le_iff_le_comap]; apply le_comap_of_subsingleton

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
e : Sym2 V
h : e ∈ G.edgeSet
⊢ Sym2.map (fun x ↦ { toFun := ⇑f.symm.toEquiv, map_rel' := ⋯ } ({ toFun := ⇑f.toEquiv, map_rel' := ⋯ } x)) e = e

Tactic:
convert! congr_fun Sym2.map_id e

Goal state after:
case e'_2
V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
e : Sym2 V
h : e ∈ G.edgeSet
x✝ : V
a✝ : x✝ ∈ e
⊢ { toFun := ⇑f.symm.toEquiv, map_rel' := ⋯ } ({ toFun := ⇑f.toEquiv, map_rel' := ⋯ } x✝) = id x✝
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
e : Sym2 W
h : e ∈ G'.edgeSet
⊢ Sym2.map (fun x ↦ { toFun := ⇑f.toEquiv, map_rel' := ⋯ } ({ toFun := ⇑f.symm.toEquiv, map_rel' := ⋯ } x)) e = e

Tactic:
convert! congr_fun Sym2.map_id e

Goal state after:
case e'_2
V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
e : Sym2 W
h : e ∈ G'.edgeSet
x✝ : W
a✝ : x✝ ∈ e
⊢ { toFun := ⇑f.toEquiv, map_rel' := ⋯ } ({ toFun := ⇑f.symm.toEquiv, map_rel' := ⋯ } x✝) = id x✝
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
⊢ RightInverse (Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom)
    (Hom.mapEdgeSet (RelIso.toRelEmbedding f).toRelHom)

Tactic:
by
    rintro ⟨e, h⟩
    simp only [Hom.mapEdgeSet, RelEmbedding.toRelHom, Sym2.map_map, comp_apply, Subtype.mk.injEq]
    convert! congr_fun Sym2.map_id e
    exact RelIso.apply_symm_apply _ _

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
v : V
hv : G.minDegree = G.degree v
⊢ k ≤ G.minDegree

Tactic:
rw [hv]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
v : V
hv : G.minDegree = G.degree v
⊢ k ≤ G.degree v
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.minDegree = G.degree v
⊢ G.minDegree < Fintype.card V

Tactic:
rw [hv]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.minDegree = G.degree v
⊢ G.degree v < Fintype.card V
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.maxDegree < Fintype.card V

Tactic:
rw [hv]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.degree v < Fintype.card V
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ (insert b P.parts).sup id = c

Tactic:
by rwa [sup_insert, P.sup_parts, id, _root_.sup_comm]

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

Goal state before:
pp: case ha
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(#(interedges r s t))

Tactic:
exact mod_cast Nat.zero_le _

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

Goal state before:
pp: case hb
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(#s) * ↑(#t)

Tactic:
exact mod_cast Nat.zero_le _

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

Goal state before:
pp: case refine_2.refine_2.ha
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ 0 ≤ ↑(#t₂)

Tactic:
exact mod_cast Nat.zero_le _

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

Goal state before:
pp: case hb
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ 0 ≤ ↑(#t₁)

Tactic:
exact mod_cast Nat.zero_le _

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case pos
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
h✝ : WellOrderingRel s t
⊢ ↑(#s) * ε ≤ ↑(#(G.nonuniformWitnesses ε s t).1)

Tactic:
exact G.left_nonuniformWitnesses_card h

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

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2

Tactic:
have hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ) := by ring

Goal state after:
case inr.inr
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ε / 2 * ↑(#A) ^ 2

Tactic:
apply hP.card_biUnion_offDiag_le'.trans

Goal state after:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts) ≤ ε / 2 * ↑(#A) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
⊢ u ∈ (G.subgraphOfAdj hvw).neighborSet v ↔ u ∈ {w}

Tactic:
suffices w = u ↔ u = w by simpa [hvw.ne.symm] using this

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
⊢ w = u ↔ u = w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).neighborSet w = {v}

Tactic:
by
  rw [subgraphOfAdj_symm hvw.symm]
  exact neighborSet_fst_subgraphOfAdj hvw.symm

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

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
⊢ (∃ (hv : x✝¹ ∈ H.verts) (hw : x✝ ∈ H.verts), (Subgraph.restrict H').Adj ⟨x✝¹, hv⟩ ⟨x✝, hw⟩) ↔ (H ⊓ H').Adj x✝¹ x✝

Tactic:
restrict_adj

Goal state after:
case Adj
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
⊢ (∃ (_ : x✝¹ ∈ H.verts) (_ : x✝ ∈ H.verts), H.Adj x✝¹ x✝ ∧ H'.Adj x✝¹ x✝) ↔ (H ⊓ H').Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, p✝.length ≤ i → p✝.getVert i = w✝
n✝ : ℕ
hi : (cons h✝ p✝).length ≤ n✝ + 1
⊢ (cons h✝ p✝).getVert (n✝ + 1) = w✝

Tactic:
· exact ih (Nat.succ_le_succ_iff.1 hi)

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

Goal state before:
pp: case hp
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ ∀ e ∈ (toDeleteEdges s p hp).edges, e ∈ G.edgeSet

Tactic:
apply edges_transfer _ _ ▸ p.edges_subset_edgeSet

Goal state after:
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
h : p.support = q.support
⊢ (List.map Dart.toProd p.darts).unzip = (List.map Dart.toProd q.darts).unzip

Tactic:
have : Prod.fst ∘ Dart.toProd = fun d : G.Dart ↦ d.fst := rfl

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : p.support = q.support
this : Prod.fst ∘ Dart.toProd = fun d ↦ d.toProd.1
⊢ (List.map Dart.toProd p.darts).unzip = (List.map Dart.toProd q.darts).unzip
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
⊢ (∃ s, G.IsClique s ∧ ⇑f '' s = t) → (SimpleGraph.map (⇑f) G).IsClique t

Tactic:
rintro ⟨x, hs, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
x : Set α
hs : G.IsClique x
ht : (⇑f '' x).Nontrivial
⊢ (SimpleGraph.map (⇑f) G).IsClique (⇑f '' x)
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
⊢ Set.InjOn q.getVert {i | i ≤ q.length}

Tactic:
by
      intro n hn m hm hnm
      simp only [Set.mem_ofPred_eq] at hn hm
      have := hinj
        (by rw [length_cons]; lia : n + 1 ≤ (q.cons h).length)
        (by rw [length_cons]; lia : m + 1 ≤ (q.cons h).length)
        (by simpa [getVert_cons] using hnm)
      lia

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.IsNClique n ∅ ↔ n = 0

Tactic:
by simp [isNClique_iff, eq_comm]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
a : α
⊢ G.IsNClique n {a} ↔ n = 1

Tactic:
by simp [isNClique_iff, eq_comm]

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

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ (cons hadj (p.takeUntil u hup)).IsSubwalk (cons hadj p)

pp: case refine_2
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ (cons hadj (p.takeUntil u hup)).IsCycle

Tactic:
· rw [isSubwalk_iff_support_isInfix, support_cons, support_cons]
      exact (List.prefix_cons_inj u |>.mpr <| p.support_takeUntil_prefix_support hup).isInfix

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ (cons hadj (p.takeUntil u hup)).IsCycle
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
sm : G.IsMaximumClique s
⊢ #s = G.cliqueNum

Tactic:
obtain ⟨sc, sm⟩ := sm
  obtain ⟨t, tc, tcard⟩ := G.exists_isNClique_cliqueNum
  exact eq_of_le_of_not_lt sc.card_le_cliqueNum (by simp [← tcard, sm t tc])

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
B : Finset G
⊢ δₘ[∅, B] = 0

Tactic:
simp [divConst]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
⊢ δₘ[A, ∅] = 0

Tactic:
simp [divConst]

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

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

Tactic:
simp [divConst]

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: ε : ℝ
hε : 0 < ε
n : ℕ
hn : cornersTheoremBound (ε / 3) ≤ n
⊢ ↑(rothNumberNat n) ≤ ε * ↑n

Tactic:
obtain ⟨A, hs₁, hs₂, hs₃⟩ := rothNumberNat_spec n

Goal state after:
ε : ℝ
hε : 0 < ε
n : ℕ
hn : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hs₁ : A ⊆ range n
hs₂ : #A = rothNumberNat n
hs₃ : ThreeAPFree ↑A
⊢ ↑(rothNumberNat n) ≤ ε * ↑n
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ toColex s ≤ toColex {a} ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)

Tactic:
simp only [toColex_le_toColex, mem_singleton, exists_eq_left]

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (∀ ⦃a_1 : α⦄, a_1 ∈ s → ¬a_1 = a → a ∉ s ∧ a_1 ≤ a) ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ⇑f ⊆ {a} ∧ a ∈ fixedPoints ⇑f ↔ fixedPoints ⇑f = {a}

Tactic:
Set.eq_singleton_iff_unique_mem,

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ⇑f ⊆ {a} ∧ a ∈ fixedPoints ⇑f ↔ a ∈ fixedPoints ⇑f ∧ ∀ x ∈ fixedPoints ⇑f, x = a
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q ↦ ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq ↦ ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
h2 : ∀ (l : { l // p ∈ l }), Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L
⊢ Fintype.card { l // p ∈ l } • order P L + 1 = order P L ^ 2 + order P L + 1

Tactic:
← Nat.card_eq_fintype_card,

Goal state after:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q ↦ ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq ↦ ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
h2 : ∀ (l : { l // p ∈ l }), Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L
⊢ Nat.card { l // p ∈ l } • order P L + 1 = order P L ^ 2 + order P L + 1
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: n : ℕ
this : ↑(catalan n) = ↑n.centralBinom / (↑n + 1)
⊢ catalan n = n.centralBinom / (n + 1)

Tactic:
have h := Nat.succ_dvd_centralBinom n
    exact mod_cast this

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

Goal state before:
pp: case e_a
m : Multiset ℕ
⊢ (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!

Tactic:
rw [← Finset.prod_mul_distrib]

Goal state after:
case e_a
m : Multiset ℕ
⊢ ∏ x ∈ m.toFinset.erase 0,
      x ! ^ count x m * ((count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1)) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case pos
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a = b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 1

pp: case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : ¬a = b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0

Tactic:
· simp [hab]

Goal state after:
case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : ¬a = b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case pos
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a = b
⊢ ∑ x ∈ Icc a b, (mu' 𝕜) x b = 1

pp: case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : ¬a = b
⊢ ∑ x ∈ Icc a b, (mu' 𝕜) x b = 0

Tactic:
· simp [hab]

Goal state after:
case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : ¬a = b
⊢ ∑ x ∈ Icc a b, (mu' 𝕜) x b = 0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case tail
p q b✝ c✝ : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p b✝
mq : b✝ = c✝.insidePart ∨ b✝ = c✝.outsidePart
ih : ↑p <:+: ↑b✝
⊢ ↑p <:+: ↑c✝

Tactic:
| tail _pm mq ih =>

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

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

Tactic:
exact hsum.mul_left _

Goal state after:
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 ∈ lowerBounds (Set.range fun A ↦ expansion K S ↑A)

Tactic:
simp [lowerBounds, *]

Goal state after: