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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A) (↑B) f
hf' : Set.BijOn f ↑A ↑B
⊢ mulRothNumber B ≤ mulRothNumber A

Tactic:
obtain ⟨s, hsB, hcard, hs⟩ := mulRothNumber_spec B

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A) (↑B) f
hf' : Set.BijOn f ↑A ↑B
s : Finset β
hsB : s ⊆ B
hcard : #s = mulRothNumber B
hs : ThreeGPFree ↑s
⊢ mulRothNumber B ≤ mulRothNumber A
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case refine_2
n d : ℕ
⊢ #(range (n * (d - 1) ^ 2 + 1)) • (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1)) ≤ ↑(#(box n d))

Tactic:
card_range,

Goal state after:
case refine_2
n d : ℕ
⊢ (n * (d - 1) ^ 2 + 1) • (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1)) ≤ ↑(#(box n d))
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 / ↑6 < log 2

pp: N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < ↑6

Tactic:
· exact log_two_gt_d9.trans_le' (by norm_num1)

Goal state after:
N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < ↑6
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ 4 / ↑6 < log 2

pp: ⊢ 0 < ↑6

Tactic:
· exact log_two_gt_d9.trans_le' (by norm_num1)

Goal state after:
⊢ 0 < ↑6
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : c ∈ a⁻¹ • ↑s
⊢ c * g⁻¹ ∈ a⁻¹ • ↑s

Tactic:
← op_smul_eq_mul,

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : c ∈ a⁻¹ • ↑s
⊢ op g⁻¹ • c ∈ a⁻¹ • ↑s
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x y : G
⊢ ∀ (a b : G), a ∈ A → b⁻¹ ∈ B → a * b = x⁻¹ * y → y⁻¹ * (x * a) ∈ B

Tactic:
simp +contextual [← eq_mul_inv_iff_mul_eq, mul_assoc]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#(A * A)) * ↑(#(A * (A * A))) = ↑(#(A ^ 2)) * ↑(#(A ^ 3))

Tactic:
by simp [pow_succ']

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ ↑(#(A * (A * A⁻¹))) * ↑(#(A * A)) = ↑(#(A * A * A⁻¹)) * ↑(#(A ^ 2))

Tactic:
by simp [pow_succ, mul_assoc]

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

Goal state before:
pp: 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✝

Tactic:
exact RelIso.apply_symm_apply _ _

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : Fintype ↑(Gᶜ.neighborSet v)
inst✝ : Fintype V
⊢ Gᶜ.degree v = Fintype.card V - 1 - G.degree v

Tactic:
rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]
    simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v)),
      card_neighborSet_eq_degree]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
⊢ G.minDegree = G'.minDegree

Tactic:
have : (G'.degree ·) ∘ f = (G.degree ·) := funext (f.degree_eq ·)

Goal state after:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
this : (fun x ↦ G'.degree x) ∘ ⇑f = fun x ↦ G.degree x
⊢ G.minDegree = G'.minDegree
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
⊢ G.maxDegree = G'.maxDegree

Tactic:
have : (G'.degree ·) ∘ f = (G.degree ·) := funext (f.degree_eq ·)

Goal state after:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
this : (fun x ↦ G'.degree x) ∘ ⇑f = fun x ↦ G.degree x
⊢ G.maxDegree = G'.maxDegree
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ a = ⊥

Tactic:
exact parts_eq_empty_iff

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : EInt
hab✝ : a ⟶ b
hab : a ≤ b
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 b =
    WithBotTop.rec 0 t.truncGEδLT 0 a ≫ (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

Tactic:
induction a using WithBotTop.rec

Goal state after:
case bot
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
b : EInt
hab✝ : ⊥ ⟶ b
hab : ⊥ ≤ b
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 b =
    WithBotTop.rec 0 t.truncGEδLT 0 ⊥ ≫ (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

case coe
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
b : EInt
a✝ : ℤ
hab✝ : WithBotTop.coe a✝ ⟶ b
hab : WithBotTop.coe a✝ ≤ b
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 b =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

case top
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
b : EInt
hab✝ : ⊤ ⟶ b
hab : ⊤ ≤ b
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 b =
    WithBotTop.rec 0 t.truncGEδLT 0 ⊤ ≫ (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∃ f, ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst

Tactic:
by
  use P.equivSigmaParts.trans ((Equiv.refl _).sigmaCongr (fun t ↦ t.1.equivFin))
  simp [equivSigmaParts, Equiv.sigmaCongr, Equiv.sigmaCongrLeft]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ ↑(#(interedges r s t)) / (↑(#s) * ↑(#t)) + ↑(#(interedges (fun x y ↦ ¬r x y) s t)) / (↑(#s) * ↑(#t)) = 1

Tactic:
← add_div,

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ (↑(#(interedges r s t)) + ↑(#(interedges (fun x y ↦ ¬r x y) s t))) / (↑(#s) * ↑(#t)) = 1
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: 𝕜 : 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δ₁ : δ < 1
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2

Tactic:
have hδ' : 0 ≤ 2 * δ - δ ^ 2 := by
    rw [sub_nonneg, sq]
    gcongr
    exact hδ₁.le.trans (by simp)

Goal state after:
𝕜 : 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δ₁ : δ < 1
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|

Tactic:
if_neg (asymm gt),

Goal state after:
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
⊢ ε ≤
    ↑|G.edgeDensity (G.nonuniformWitnesses ε t s).2
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ ↑(#(G.interedges s t)) / (↑(#s) * ↑(#t)) + ↑(#(Gᶜ.interedges s t)) / (↑(#s) * ↑(#t)) = 1

Tactic:
← add_div,

Goal state after:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ (↑(#(G.interedges s t)) + ↑(#(Gᶜ.interedges s t))) / (↑(#s) * ↑(#t)) = 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : 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
this✝ : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
this : 1 ≤ ε / 4 * ↑(#P.parts)
⊢ 2 * ↑(#A) ^ 2 ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)

Tactic:
convert! mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜)) using 1
      <;> ring

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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
⊢ #(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id) ≤ 2 ^ (#P.parts - 1) * m

Tactic:
have hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U :=
    nonuniformWitness_mem_nonuniformWitnesses h₂ hV hUV

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
⊢ #(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id) ≤ 2 ^ (#P.parts - 1) * m
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := ⋯
M : G.Subgraph
h : v ∈ M.verts
⊢ M'.verts ⊆ M.verts

Tactic:
simp [h, M']

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

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := ⋯
M : G.Subgraph
h : v ∈ M.verts
⊢ ∀ ⦃v w : V⦄, M'.Adj v w → M.Adj v w

Tactic:
simp [h, M']

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : G ⊑ H
⊢ G.maxDegree ≤ H.maxDegree

Tactic:
by
  have ⟨f⟩ := h
  exact f.maxDegree_mono

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G✝ G₁ G₂ G₃ : SimpleGraph V
H✝ : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
inst✝¹ : Fintype V
inst✝ : Fintype W
G : SimpleGraph V
H : SimpleGraph W
⊢ ℕ

Tactic:
by
  classical exact Fintype.card (Copy H G)

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
hG : G'.verts.Subsingleton
hv : v ∉ G'.verts
⊢ G'.degree v = 0

Tactic:
· exact degree_of_notMem_verts hv

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

Goal state before:
pp: case cons.zero
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✝
hi : (cons h✝ p✝).length ≤ 0
⊢ (cons h✝ p✝).getVert 0 = w✝

Tactic:
cases hi

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
i : ℕ
hi : i < nil.length
⊢ G.Adj (nil.getVert i) (nil.getVert (i + 1))

Tactic:
cases hi

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 : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#𝒜) * ↑(#s) * ↑m ≤ ↑(#(𝒜.sup id)) * (↑m + 1)

Tactic:
mul_right_comm

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#𝒜) * ↑m * ↑(#s) ≤ ↑(#(𝒜.sup id)) * (↑m + 1)
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 : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#(𝒜.biUnion id)) * ↑m ≤ ↑(#𝒜) * ↑(#s) * (↑m + 1)

Tactic:
mul_right_comm

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#(𝒜.biUnion id)) * ↑m ≤ ↑(#𝒜) * (↑m + 1) * ↑(#s)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case nil.mpr
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ (∃ (hu : u' = u) (hv : u' = u), nil = nil.copy hu hv) → nil.IsSubwalk nil

Tactic:
rintro ⟨rfl, _, _⟩
      simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ nil.support
⊢ (nil.takeUntil u h).append (nil.dropUntil u h) = nil

Tactic:
rw [mem_support_nil_iff] at h
    subst u
    rfl

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : u✝ = u
⊢ List.count s(u, x) (h' ▸ nil).edges ≤ 1

pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
⊢ List.count s(u, x) (cons ha (p'.takeUntil u ⋯)).edges ≤ 1

Tactic:
· subst h'
        simp

Goal state after:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
⊢ List.count s(u, x) (cons ha (p'.takeUntil u ⋯)).edges ≤ 1
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 : ∀ (k : ℕ), p.getVert k = q.getVert k
⊢ p = q

Tactic:
wlog hpq : p.length ≤ q.length generalizing p q
  · exact (this (h · |>.symm) (le_of_not_ge hpq)).symm
  refine ext_getVert_le_length (hpq.antisymm ?_) fun k _ ↦ h k
  by_contra!
  exact (q.adj_getVert_succ this).ne (by simp [← h, getVert_of_length_le])

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
hw : ∃ w ∈ p.support, w ∈ q.support ∧ w ≠ u ∧ w ≠ v
w : V
hwp : w ∈ p.support
hwq : w ∈ q.support
hwu : w ≠ u
hwv : w ≠ v
h✝ : p.takeUntil w hwp ≠ q.takeUntil w hwq
this :
  p.takeUntil w hwp ≠ q.takeUntil w hwq →
    (p.takeUntil w hwp).length = (p.takeUntil w hwp).length →
      ∃ u' v' p' q',
        p'.IsSubwalk (p.takeUntil w hwp) ∧ q'.IsSubwalk (q.takeUntil w hwq) ∧ (p'.append q'.reverse).IsCycle
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
grind [isSubwalk_takeUntil, IsSubwalk.trans]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
⊢ (SimpleGraph.map (⇑e) G).cliqueSet n = map e.toEmbedding '' G.cliqueSet n

Tactic:
obtain rfl | hn := eq_or_ne n 1
  · ext
    simp [e.exists_congr_left]
  · simpa using cliqueSet_map hn G e.toEmbedding

Goal state after:
Module: Mathlib.Data.Finset.CastCard

Goal state before:
pp: α : Type u_1
R : Type u_2
s : Finset α
a : α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
hs : a ∈ s
⊢ ↑(#(s.erase a)) = ↑(#(s.erase a)) + ↑1 - 1

Tactic:
cast_one,

Goal state after:
α : Type u_1
R : Type u_2
s : Finset α
a : α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
hs : a ∈ s
⊢ ↑(#(s.erase a)) = ↑(#(s.erase a)) + 1 - 1
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
x y : α ⊕ β ⊕ γ
h : Rel t x y
⊢ Rel t y x

Tactic:
cases h <;> constructor <;> assumption

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 : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ + 1 ≤ Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
⊢ False

Tactic:
Nat.add_one_le_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommGroup α
inst✝ : CommGroup β
s : Set α
e : β ≃* α
⊢ MulDissociated (⇑e ⁻¹' s) ↔ MulDissociated s

Tactic:
simp [MulDissociated, InjOn, ← e.finsetCongr.forall_congr_right, ← e.apply_eq_iff_eq,
    (Finset.map_injective _).eq_iff]

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
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
⊢ ∃ x₁ y₁ x₂ y₂, y₁ - x₁ ∈ A ∧ y₂ - x₁ ∈ A ∧ y₁ - x₂ ∈ A ∧ x₁ + y₂ = x₂ + y₁ ∧ x₁ ≠ x₂

Tactic:
by
    simpa [IsCornerFree, isCorner_iff, B, -exists_and_left, -exists_and_right]
      using corners_theorem ε hε hG B this

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))
hF : ∀ (x : σ → K), (eval x) F = if x ∈ S then 1 else 0
⊢ ∑ x, (eval x) F = ↑(Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 })

Tactic:
rw [Fintype.card_of_subtype S hS, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one, ←
      Fintype.sum_extend_by_zero S, sum_congr rfl fun x _ => hF x]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : Finset M
a : M
a_notin_A : a ∉ A
B : Finset M
hB : B ⊆ A
⊢ ∃ B_1 ⊆ insert a A, ∑ b ∈ B_1, b = a +ᵥ ∑ b ∈ B, b

Tactic:
exact ⟨insert a B, by aesop, by rw [sum_insert (fun h => a_notin_A (hB h))]; simp⟩

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

Goal state before:
pp: i n : ℕ
⊢ i ∈ n.bitIndices ↔ n.testBit i = true

Tactic:
by
  induction n using Nat.binaryRec generalizing i with
  | zero => simp
  | bit b n ih => cases b <;> cases i <;> simp_all [Nat.testBit_add_one, Nat.mul_add_div]

Goal state after: