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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ (↑(Finset.map f (s ∩ t))).Subsingleton

Tactic:
coe_map,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ (⇑f '' ↑(s ∩ t)).Subsingleton
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
v w : α
s : Finset α
n : ℕ
hc : (G ⊔ edge v w).IsNClique n s
hx : v ∈ s
⊢ #(s.erase v) = n - 1

Tactic:
rw [card_erase_of_mem hx, hc.2]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝ : Fintype β
f : ⊤.Copy G
⊢ G.IsClique ↑(map f.toEmbedding univ) ∧ Fintype.card β = Fintype.card β

Tactic:
coe_map,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝ : Fintype β
f : ⊤.Copy G
⊢ G.IsClique (⇑f.toEmbedding '' ↑univ) ∧ Fintype.card β = Fintype.card β
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hd : p.support.tail.Disjoint q.support.tail
hl : p.length ≠ 1
⊢ p.edges.Disjoint q.edges

Tactic:
simp only [List.disjoint_left] at hd ⊢

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hl : p.length ≠ 1
hd : ∀ ⦃a : V⦄, a ∈ p.support.tail → a ∉ q.support.tail
⊢ ∀ ⦃a : Sym2 V⦄, a ∈ p.edges → a ∉ q.edges
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hl : p.length ≠ 1
hd : ∃ a ∈ p.edges, a ∈ q.edges
⊢ ∃ a ∈ p.support.tail, a ∈ q.support.tail

Tactic:
obtain ⟨⟨a, b⟩, hep, heq⟩ := hd

Goal state after:
case mk
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hl : p.length ≠ 1
w✝ : Sym2 V
a b : V
hep : Quot.mk (Sym2.Rel V) (a, b) ∈ p.edges
heq : Quot.mk (Sym2.Rel V) (a, b) ∈ q.edges
⊢ ∃ a ∈ p.support.tail, a ∈ q.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → G = ⊥

Tactic:
simp_rw [← edgeSet_eq_empty, Set.eq_empty_iff_forall_notMem, Sym2.forall, mem_edgeSet]
    exact fun h a b hab => h _ ⟨by simpa [hab.ne], card_pair hab.ne⟩

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
⊢ G.CliqueFreeOn (s ∩ G.neighborSet a) n

Tactic:
by
  classical
  refine fun t hts ht => hs ?_ (ht.insert fun b hb => (hts hb).2)
  push_cast
  exact Set.insert_subset_iff.2 ⟨ha, hts.trans Set.inter_subset_left⟩

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ (SimpleGraph.map (⇑f) G).cliqueSet n → s ∈ map f '' G.cliqueSet n

pp: case mpr
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ map f '' G.cliqueSet n → s ∈ (SimpleGraph.map (⇑f) G).cliqueSet n

Tactic:
· rintro ⟨hs, rfl⟩
    have hs' : (s.preimage f f.injective.injOn).map f = s := by
      classical
      rw [map_eq_image, image_preimage, filter_true_of_mem]
      rintro a ha
      obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
      obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm
      exact ⟨c, hc⟩
    refine ⟨s.preimage f f.injective.injOn, ⟨?_, by rw [← card_map f, hs']⟩, hs'⟩
    rw [coe_preimage]
    exact fun a ha b hb hab => map_adj_apply.1 (hs ha hb <| f.injective.ne hab)

Goal state after:
case mpr
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ map f '' G.cliqueSet n → s ∈ (SimpleGraph.map (⇑f) G).cliqueSet n
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
n : ℕ
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α ↪ β
hn : n ≠ 1
⊢ map f '' G.cliqueSet n = ↑(map { toFun := map f, inj' := ⋯ } (G.cliqueFinset n))

Tactic:
coe_map,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
n : ℕ
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α ↪ β
hn : n ≠ 1
⊢ map f '' G.cliqueSet n = ⇑{ toFun := map f, inj' := ⋯ } '' ↑(G.cliqueFinset n)
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).IsCycle
⊢ p.IsCycle

Tactic:
rw [isCycle_def, ne_eq, eq_nil_iff_nil]
  rw [isCycle_def, ne_eq, eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail] at hp
  exact hp.imp .of_map <| .imp_right <| .of_map f

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

Goal state before:
pp: case refl.refl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
Z' : Finset α
hZ' : Z' ∈ P.parts
zZ' : z ∈ Z'
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
nYZ : Y ≠ Z'
uYZ : G.IsUniform (ε / 8) Y Z'
dYZ : ε / 4 ≤ ↑(G.edgeDensity Y Z')
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
cases P.disjoint.elim hZ hZ' (not_disjoint_iff.2 ⟨z, zZ, zZ'⟩)

Goal state after:
case refl.refl.refl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))
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}
this : 0 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ ↑(#s) - 2 * ε * ↑(#s) ≤ ↑(#s) - ↑(#(G.badVertices ε s t ∪ G.badVertices ε s u))

Tactic:
sub_le_sub_iff_left,

Goal state after:
α : 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}
this : 0 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ ↑(#(G.badVertices ε s t ∪ G.badVertices ε s u)) ≤ 2 * ε * ↑(#s)
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case refine_1.H
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ ∀ (a_1 b : ℕ), a_1 ∈ L → b ∈ L → (a_1 - (a + 1) < b - (a + 1) ↔ a_1 < b)

Tactic:
exact fun x y hx _ ↦ by rw [tsub_lt_tsub_iff_right (haL _ hx)]

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

Goal state before:
pp: case refine_2
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
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ (↑ℬ).PairwiseDisjoint fun x ↦ x

Tactic:
exact h𝒜disj.mono hℬ𝒜

Goal state after:
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : (s : Set α) → s.Finite → (a : α) → β a
⊢ ∃ χ, ∀ (s : Set α), s.Finite → ∃ t, ∃ (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x

Tactic:
by
  obtain ⟨χ, hχ⟩ := Finset.rado_selection (fun s ↦ g s s.finite_toSet)
  refine ⟨χ, fun s hs ↦ ?_⟩
  obtain ⟨t, ht, ht'⟩ := hχ hs.toFinset
  exact ⟨t, by simp_all⟩

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
⊢ 𝒜 = initSeg (𝒜.sup' h𝒜₀ ⇑toColex)

Tactic:
ext t

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
⊢ t ∈ 𝒜 ↔ t ∈ initSeg (𝒜.sup' h𝒜₀ ⇑toColex)
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₃ : #sᶜ = 0
⊢ #(s.biUnion t)ᶜ = 0

Tactic:
rw [Finset.card_compl, tsub_eq_zero_iff_le, (Finset.card_le_univ _).ge_iff_eq', eq_comm,
        Finset.card_eq_iff_eq_univ] at hs₃ ⊢

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₃ : s = univ
⊢ s.biUnion t = univ
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
⊢ a * b * (c * d) ∈ A⁻¹ * A

Tactic:
have h₂ : (1 / 2 : ℚ) * #A < #(A ∩ (a * b)⁻¹ • A) := by
      refine (h₁ b hb _ ha).trans_le ?_
      rw [← card_smul_finset b⁻¹]
      simp [smul_smul, smul_finset_inter]

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))
⊢ a * b * (c * d) ∈ A⁻¹ * A
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
⊢ 1 < order P L

Tactic:
obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, -, -, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := @exists_config P L _ _

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
⊢ 1 < order P L
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
⊢ #(A⁻¹ * A) < 2 * #A

Tactic:
have h₂ : ∀ x ∈ A ×ˢ A, (fun ⟨x, y⟩ => x * y⁻¹) x ∈ A⁻¹ * A := by
    rw [← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h)]
    simp only [mem_product, Prod.forall, mem_mul, and_imp, mem_inv]
    intro a b ha hb
    exact ⟨a, ha, b⁻¹, by simp [hb], rfl⟩

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ #(A⁻¹ * A) < 2 * #A
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
⊢ a •> ((A⁻¹ * A) <• a) ⊆ A * A

Tactic:
intro z hz

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z : G
hz : z ∈ a •> ((A⁻¹ * A) <• a)
⊢ z ∈ A * A
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: x : BinaryTree Unit
n : ℕ
⊢ x ∈ treesOfNumNodesEq n ↔ x.numNodes = n

Tactic:
induction x using BinaryTree.unitRecOn generalizing n <;> cases n

Goal state after:
case base.zero
⊢ nil ∈ treesOfNumNodesEq 0 ↔ nil.numNodes = 0

case base.succ
n✝ : ℕ
⊢ nil ∈ treesOfNumNodesEq (n✝ + 1) ↔ nil.numNodes = n✝ + 1

case ind.zero
x✝ y✝ : BinaryTree Unit
a✝¹ : ∀ {n : ℕ}, x✝ ∈ treesOfNumNodesEq n ↔ x✝.numNodes = n
a✝ : ∀ {n : ℕ}, y✝ ∈ treesOfNumNodesEq n ↔ y✝.numNodes = n
⊢ node () x✝ y✝ ∈ treesOfNumNodesEq 0 ↔ (node () x✝ y✝).numNodes = 0

case ind.succ
x✝ y✝ : BinaryTree Unit
a✝¹ : ∀ {n : ℕ}, x✝ ∈ treesOfNumNodesEq n ↔ x✝.numNodes = n
a✝ : ∀ {n : ℕ}, y✝ ∈ treesOfNumNodesEq n ↔ y✝.numNodes = n
n✝ : ℕ
⊢ node () x✝ y✝ ∈ treesOfNumNodesEq (n✝ + 1) ↔ (node () x✝ y✝).numNodes = n✝ + 1
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∑ u ∈ antidiagonal n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)) =
    ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2

Tactic:
apply sum_congr rfl
      rintro ⟨i, j⟩ H
      rw [card_map, card_product, ih _ (fst_le H), ih _ (snd_le H)]

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

Goal state before:
pp: case neg
m : Multiset ℕ
this :
  (∏ 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)!
hm : 0 ∉ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
nth_rewrite 1 [← Finset.erase_eq_of_notMem hm]

Goal state after:
case neg
m : Multiset ℕ
this :
  (∏ 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)!
hm : 0 ∉ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset.erase 0, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ i ≤ ([U] ++ ↑p).length

Tactic:
rw [singleton_append, length_cons]

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ i ≤ (↑p).length + 1
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Preorder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f g : IncidenceAlgebra 𝕜 α
h : IncidenceAlgebra 𝕝 α
⊢ (f + g) • h = f • h + g • h

Tactic:
ext; exact Eq.trans (sum_congr rfl fun x _ ↦ add_smul _ _ _) sum_add_distrib

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

Goal state before:
pp: case e'_2.e'_5.e'_6
m n : ℕ
hn : n ≠ 0
⊢ n ! ^ m = (map (fun j ↦ j !) (replicate m n)).prod

pp: case e'_2.e'_6
m n : ℕ
hn : n ≠ 0
⊢ m ! = ∏ j ∈ (replicate m n).toFinset.erase 0, (count j (replicate m n))!

pp: case e'_3
m n : ℕ
hn : n ≠ 0
⊢ m * n = (replicate m n).sum

Tactic:
· simp only [map_replicate, prod_replicate]

Goal state after:
case e'_2.e'_6
m n : ℕ
hn : n ≠ 0
⊢ m ! = ∏ j ∈ (replicate m n).toFinset.erase 0, (count j (replicate m n))!

case e'_3
m n : ℕ
hn : n ≠ 0
⊢ m * n = (replicate m n).sum
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
⊢ ↑({ toList := List.take (p.firstReturn + 1) ↑(p + q), count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }.denest ⋯) =
    ↑({ toList := List.take (p.firstReturn + 1) ↑p, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }.denest ⋯)

Tactic:
congr 3

Goal state after:
p q : DyckWord
h : p ≠ 0
⊢ List.take (p.firstReturn + 1) ↑(p + q) = List.take (p.firstReturn + 1) ↑p
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁵ : Ring 𝕜
inst✝⁴ : Preorder α
inst✝³ : Preorder β
f₁ f₂ : IncidenceAlgebra 𝕜 α
g₁ g₂ : IncidenceAlgebra 𝕜 β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
h :
  ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    f₁ a₁ a₂ * g₁ b₁ b₂ * (f₂ a₂ a₃ * g₂ b₂ b₃) = f₁ a₁ a₂ * f₂ a₂ a₃ * (g₁ b₁ b₂ * g₂ b₂ b₃)
x y : α × β
a✝ : x ≤ y
⊢ (f₁.prod g₁ * f₂.prod g₂) x y = ((f₁ * f₂).prod (g₁ * g₂)) x y

Tactic:
simp [Icc_prod_def, sum_mul_sum, h, sum_product]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case e'_5
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ (fun i ↦ if p (i + 1) then ∑' (j : ℕ), X ^ ((i + 1) * j) else 1) = fun i ↦
    1 + ∑' (j : ℕ), (if p (i + 1) then 1 else 0) • X ^ ((i + 1) * (j + 1))

pp: case e'_6
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ (PowerSeries.mk fun n ↦ ↑(#(restricted n p))) = genFun fun i c ↦ if p i then 1 else 0

Tactic:
· ext1 i
    split_ifs
    · rw [tsum_eq_zero_add' ?_]
      · simp
      simp_rw [pow_mul, pow_add]
      apply Summable.mul_right
      exact summable_pow_of_constantCoeff_eq_zero (by simp)
    · simp

Goal state after:
case e'_6
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ (PowerSeries.mk fun n ↦ ↑(#(restricted n p))) = genFun fun i c ↦ if p i then 1 else 0
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
a b : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
h : (fun i ↦ (↑i + 1) * m - 1) a = (fun i ↦ (↑i + 1) * m - 1) b
⊢ 1 ≤ (↑a + 1) * m

Tactic:
by nlinarith

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
a b : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
h : (fun i ↦ (↑i + 1) * m - 1) a = (fun i ↦ (↑i + 1) * m - 1) b
⊢ 1 ≤ (↑b + 1) * m

Tactic:
by nlinarith

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∏' (n : ℕ), (1 - X ^ (n + 1)) = pentagonalSeries R

Tactic:
rw [pentagonalSeries_eq_tsum_pow_pentagonal_sub]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∏' (n : ℕ), (1 - X ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ ↑(#((↑H).toFinset * Z)) / ↑(#(↑H).toFinset) = ↑(#((↑H).toFinset * S)) / ↑(#(↑H).toFinset)

Tactic:
congr 3

Goal state after:
case e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ (↑H).toFinset * Z = (↑H).toFinset * S
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 G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ (e : β), e ∈ edgeSet ↔ ∃ x y, IsLink e x y

Tactic:
simp_rw [← hIsLink, ← hedgeSet]
    exact G.edge_mem_iff_exists_isLink

Goal state after: