mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
S : Type u_2
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
H : S
⊢ ↑(#{1}) ≤ 1 ∧ ↑H ^ 2 ⊆ ↑{1} • ↑H

Tactic:
simp

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
n : ℤ
⊢ WithBotTop.coe n ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: 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
⊢ WithBotTop.rec (motive := fun {x} ↦
      (x ⟶ ⊥) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) ⊥ f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) ⊥ f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) ⊥ f)
      ⊥ (𝟙 ⊥) =
    𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)

Tactic:
simp

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

Goal state before:
pp: 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
a✝ : ℤ
⊢ WithBotTop.rec (motive := fun {x} ↦
      (x ⟶ WithBotTop.coe a✝) →
        (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a✝)))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) (WithBotTop.coe a✝) f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) (WithBotTop.coe a✝) f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) (WithBotTop.coe a✝) f)
      (WithBotTop.coe a✝) (𝟙 (WithBotTop.coe a✝)) =
    𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a✝))

Tactic:
simp

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

Goal state before:
pp: 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
⊢ WithBotTop.rec (motive := fun {x} ↦
      (x ⟶ ⊤) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) ⊤ f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) ⊤ f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) ⊤ f)
      ⊤ (𝟙 ⊤) =
    𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)

Tactic:
simp

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

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
hAA' : ∅ ⊆ A
⊢ #(A * C) * #∅ ≤ #(∅ * C) * #A

Tactic:
simp

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

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

Tactic:
have hA₀ : (0 : ℚ≥0) < #A := cast_pos.2 hA.card_pos

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
hA₀ : 0 < ↑(#A)
⊢ #(A * C) * #A' ≤ #(A' * C) * #A
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A C : Finset G
⊢ #(A * C) * #∅ ≤ #(A * ∅) * #(∅ * C)

Tactic:
simp

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

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
B : Finset G
n : ℕ
hAB : ∀ A' ⊆ ∅, #(∅ * B) * #A' ≤ #(A' * B) * #∅
⊢ ↑(#(∅ * B ^ n)) ≤ (↑(#(∅ * B)) / ↑(#∅)) ^ n * ↑(#∅)

Tactic:
simp

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

Goal state before:
pp: case inr.zero
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
⊢ ↑(#(A * B ^ 0)) ≤ (↑(#(A * B)) / ↑(#A)) ^ 0 * ↑(#A)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2

Tactic:
op_smul_finset_mul_eq_mul_smul_finset,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ x.1 * e • e⁻¹ • x.2 ⊆ x.1 * x.2
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: α : 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
⊢ op (b⁻¹ * a) • b = a

Tactic:
simp

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 : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
⊢ ∀ (i : Fin 3), |1 i| = 1

Tactic:
simp

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 : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (Fin n → ℤ) → Finset G := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ |Fin.cons 1 (tail (tail ε)) 0| = 1

Tactic:
simp

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

Goal state before:
pp: case mk.mk
V : Type u_1
G : SimpleGraph V
toProd✝¹ : V × V
adj✝¹ : G.Adj toProd✝¹.1 toProd✝¹.2
toProd✝ : V × V
adj✝ : G.Adj toProd✝.1 toProd✝.2
⊢ { toProd := toProd✝¹, adj := adj✝¹ } = { toProd := toProd✝, adj := adj✝ } ↔
    { toProd := toProd✝¹, adj := adj✝¹ }.toProd = { toProd := toProd✝, adj := adj✝ }.toProd

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
p : V × V
hp : G.Adj p.1 p.2
q : V × V
hq : G.Adj q.1 q.2
⊢ { toProd := p, adj := hp }.edge = { toProd := q, adj := hq }.edge ↔
    { toProd := p, adj := hp } = { toProd := q, adj := hq } ∨
      { toProd := p, adj := hp } = { toProd := q, adj := hq }.symm

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
p : V × V
h : G.Adj p.1 p.2
u✝ v✝ : V
⊢ { toProd := p, adj := h }.edge = s(u✝, v✝) ↔
    { toProd := p, adj := h }.toProd = (u✝, v✝) ∨ { toProd := p, adj := h }.toProd = (v✝, u✝)

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
a b : V
h : G.Adj (a, b).1 (a, b).2
u v : V
⊢ { fst := a, snd := b, adj := h }.toProd = (u, v) ∨ { fst := a, snd := b, adj := h }.toProd = (v, u) ↔
    { fst := a, snd := b, adj := h }.toProd.1 = u ∧ { fst := a, snd := b, adj := h }.toProd.2 = v ∨
      { fst := a, snd := b, adj := h }.toProd.1 = v ∧ { fst := a, snd := b, adj := h }.toProd.2 = u

Tactic:
simp

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

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
K : ℝ
hA : ↑(#(∅ ^ 3)) ≤ K * ↑(#∅)
⊢ ↑(#(∅⁻¹ * ∅ * ∅)) ≤ K ^ 2 * ↑(#∅)

Tactic:
simp

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
⊢ 2 ≤ 3

Tactic:
simp

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

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
K : ℝ
hA : ↑(#(∅ ^ 3)) ≤ K * ↑(#∅)
⊢ ↑(#(∅ * ∅⁻¹ * ∅)) ≤ K ^ 3 * ↑(#∅)

Tactic:
simp

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
⊢ 2 ≤ 3

Tactic:
simp

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
⊢ 3 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case hmn
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
hδ : (δ 0 = 1 ∨ δ 0 = -1) ∧ (δ 1 = 1 ∨ δ 1 = -1) ∧ (δ 2 = 1 ∨ δ 2 = -1)
⊢ 2 ≤ 3

Tactic:
simp

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
⊢ ↑(#(A ^ m)) ≤ K ^ (m - 2) * ↑(#A)

Tactic:
have (ε : ℤ) (hε : |ε| = 1) : A ^ ε = A := by
    obtain rfl | rfl := eq_or_eq_neg_of_abs_eq hε <;> simp [hAsymm]

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
⊢ ↑(#(A ^ m)) ≤ K ^ (m - 2) * ↑(#A)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
⊢ ↑(#(A ^ m)) = ↑(#(List.map (fun i ↦ A ^ 1) (finRange m)).prod)

Tactic:
simp

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
⊢ ∀ (i : Fin m), |1| = 1

Tactic:
simp

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
this : DecidableEq V
⊢ Set.MapsTo (fun d ↦ d.toProd.1) ↑univ ↑univ

Tactic:
simp

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

Goal state before:
pp: case e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ d ∉ {d.symm}

Tactic:
rw [mem_singleton]

Goal state after:
case e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ ¬d = d.symm
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
a b : V
⊢ (SimpleGraph.map (⇑f) G).Adj (f a) (f b) ↔ G.Adj a b

Tactic:
simp

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
⊢ ∀ x ∈ G.edgeFinset, #{a | a.edge = x} = 2

Tactic:
intro e h

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
h : e ∈ G.edgeFinset
⊢ #{a | a.edge = e} = 2
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ a ∈ univ,
    (a.toProd.1, a.toProd.2) ∈
      {x |
        match x with
        | (x, y) => G.Adj x y}

Tactic:
simp

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

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ (a : V × V)
    (ha :
      a ∈
        {x |
          match x with
          | (x, y) => G.Adj x y}),
    { toProd := a, adj := ⋯ } ∈ univ

Tactic:
simp

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

Goal state before:
pp: case refine_3
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ (a : G.Dart) (ha : a ∈ univ), { fst := a.toProd.1, snd := a.toProd.2, adj := ⋯ } = a

Tactic:
simp

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

Goal state before:
pp: case refine_4
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ (a : V × V)
    (ha :
      a ∈
        {x |
          match x with
          | (x, y) => G.Adj x y}),
    ({ toProd := a, adj := ⋯ }.toProd.1, { toProd := a, adj := ⋯ }.toProd.2) = a

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝¹ x✝ : V
⊢ (SimpleGraph.comap (⇑f) (SimpleGraph.map (⇑f) G)).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝

Tactic:
simp

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
e : V ≃ W
x✝ : SimpleGraph V
⊢ SimpleGraph.comap (⇑e) (SimpleGraph.comap (⇑e.symm) x✝) = x✝

Tactic:
simp

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
e : V ≃ W
x✝ : SimpleGraph W
⊢ SimpleGraph.comap (⇑e.symm) (SimpleGraph.comap (⇑e) x✝) = x✝

Tactic:
simp

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
G₁ G₂ : SimpleGraph V
H : SimpleGraph W
f✝ : G✝ →g G'
f : V → W
G : SimpleGraph W
⊢ ∀ {a b : V}, (SimpleGraph.comap f G).Adj a b → G.Adj (f a) (f b)

Tactic:
simp

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
H : SimpleGraph W
f : G ↪g G'
⊢ ∀ {a b : V}, (induce (Set.range ⇑f) G').Adj ((Equiv.ofInjective ⇑f ⋯) a) ((Equiv.ofInjective ⇑f ⋯) b) ↔ G.Adj a b

Tactic:
simp

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
H : SimpleGraph W
f✝ : G✝ ↪g G'
f : V ↪ W
G : SimpleGraph W
⊢ ∀ {a b : V}, G.Adj (f a) (f b) ↔ (SimpleGraph.comap (⇑f) G).Adj a b

Tactic:
simp

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
H : SimpleGraph W
f✝ : G✝ ↪g G'
f : V ↪ W
G : SimpleGraph V
⊢ ∀ {a b : V}, (SimpleGraph.map (⇑f) G).Adj (f a) (f b) ↔ G.Adj a b

Tactic:
simp

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
H : SimpleGraph W
f✝ : G ↪g G'
α : Type u_5
β : Type u_6
f : α ↪ β
⊢ ∀ {a b : α}, (completeGraph β).Adj (f a) (f b) ↔ (completeGraph α).Adj a b

Tactic:
simp

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
H : SimpleGraph W
f✝ : G ↪g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
f : G ↪g H
⊢ ∀ {a b : V}, Hᶜ.Adj (f.toEmbedding a) (f.toEmbedding b) ↔ Gᶜ.Adj a b

Tactic:
simp

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

Goal state before:
pp: case inl
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
H : SimpleGraph W
f✝ : G ↪g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
f : Gᶜ ↪g Hᶜ
v : V
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding v) ↔ G.Adj v v

Tactic:
simp

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
s s' : Set V
h✝ h : s ⊆ s'
⊢ ∀ {a b : ↑s}, (induce s' G).Adj ((s.embeddingOfSubset s' h) a) ((s.embeddingOfSubset s' h) b) ↔ (induce s G).Adj a b

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s s' : Set V
h : s ⊆ s'
x✝ : ↑s
⊢ ↑((G.induceHomOfLE h).toHom x✝) = ↑((induceHom Hom.id ⋯) x✝)

Tactic:
simp

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'
v : V
w : ↑(G.neighborSet v)
⊢ (fun w ↦ ⟨f.symm ↑w, ⋯⟩) ((fun w ↦ ⟨f ↑w, ⋯⟩) w) = w

Tactic:
simp

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'
v : V
w : ↑(G'.neighborSet (f v))
⊢ (fun w ↦ ⟨f ↑w, ⋯⟩) ((fun w ↦ ⟨f.symm ↑w, ⋯⟩) w) = w

Tactic:
simp

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'
f : V ≃ W
G : SimpleGraph W
⊢ ∀ {a b : V}, G.Adj (f a) (f b) ↔ (SimpleGraph.comap (⇑f) G).Adj a b

Tactic:
simp

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'
α : Type u_5
β : Type u_6
f : α ≃ β
⊢ ∀ {a b : α}, (completeGraph β).Adj (f a) (f b) ↔ (completeGraph α).Adj a b

Tactic:
simp

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'
G'' : SimpleGraph X
G''' : SimpleGraph Y
s : Set V
t : Set W
r : Set X
φ : G ≃g G'
φst : Set.BijOn (⇑φ) s t
ψ : G' ≃g G''
ψtr : Set.BijOn (⇑ψ) t r
v : ↑s
⊢ (fun w ↦ ⟨φ.symm ↑w, ⋯⟩) ((fun v ↦ ⟨φ ↑v, ⋯⟩) v) = v

Tactic:
simp

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'
G'' : SimpleGraph X
G''' : SimpleGraph Y
s : Set V
t : Set W
r : Set X
φ : G ≃g G'
φst : Set.BijOn (⇑φ) s t
ψ : G' ≃g G''
ψtr : Set.BijOn (⇑ψ) t r
w : ↑t
⊢ (fun v ↦ ⟨φ ↑v, ⋯⟩) ((fun w ↦ ⟨φ.symm ↑w, ⋯⟩) w) = w

Tactic:
simp

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
V₁ : Type u_5
V₂ : Type u_6
W₁ : Type u_7
W₂ : Type u_8
hV : V₁ ≃ V₂
hW : W₁ ≃ W₂
⊢ ∀ {a b : V₁ ⊕ W₁},
    (completeBipartiteGraph V₂ W₂).Adj ((hV.sumCongr hW) a) ((hV.sumCongr hW) b) ↔
      (completeBipartiteGraph V₁ W₁).Adj a b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case inl
α : Type u_1
f : α → ℕ
⊢ ∅.EquitableOn f → ∃ b, ∀ a ∈ ∅, b ≤ f a ∧ f a ≤ b + 1

Tactic:
simp

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)
⊢ v ∉ G.neighborFinset v

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
v : V
inst✝ : Fintype ↑(⊥.neighborSet v)
a✝ : V
⊢ a✝ ∈ ⊥.neighborFinset v ↔ a✝ ∈ ∅

Tactic:
simp

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✝ : Subsingleton V
⊢ G.degree v = 0

Tactic:
simp

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.edgeSet
⊢ G.degree v ≤ #G.edgeFinset

Tactic:
rw [← card_incidenceFinset_eq_degree]
  exact card_le_card (G.incidenceFinset_subset v)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
v : V
inst✝ : DecidableRel G.Adj
a✝ : V
⊢ a✝ ∈ G.neighborFinset v ↔ a✝ ∈ {w | G.Adj v w}

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
v : V
⊢ ⊥.degree v = 0

Tactic:
simp

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

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
h✝ : IsEmpty V
⊢ G.minDegree ≤ H.minDegree

Tactic:
simp

Goal state after: