mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
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 : 2 ≤ m
⊢ m ≠ 0

Tactic:
;

Goal state after:
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 : ℕ
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 : 2 ≤ m
⊢ m ≠ 0
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 ε))
⊢ #A * #(V⁻¹ * W) ≤ #(A * V) * #(A * W)

Tactic:
;

Goal state after:
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 ε))
⊢ #A * #(V⁻¹ * W) ≤ #(A * V) * #(A * W)
Module: Mathlib.Combinatorics.SimpleGraph.Dart

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

Tactic:
;

Goal state after:
case mk
V : Type u_1
G : SimpleGraph V
d₂ : G.Dart
toProd✝ : V × V
adj✝ : G.Adj toProd✝.1 toProd✝.2
⊢ { toProd := toProd✝, adj := adj✝ } = d₂ ↔ { toProd := toProd✝, adj := adj✝ }.toProd = d₂.toProd
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:
;

Goal state after:
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
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 ε))
⊢ k * ↑(#A) * (k ^ (m - 1) * ↑(#A)) = ↑(#A) * (k ^ (m - 1) * k * ↑(#A))

Tactic:
;

Goal state after:
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 ε))
⊢ k * ↑(#A) * (k ^ (m - 1) * ↑(#A)) = ↑(#A) * (k ^ (m - 1) * k * ↑(#A))
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) * #(A * (A * A))

Tactic:
;

Goal state after:
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) * #(A * (A * A))
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)

Tactic:
;

Goal state after:
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)
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
⊢ #A ≤ #(A ^ 3)

Tactic:
;

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

Goal state after:
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
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ (∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d) → d.toProd.1 = v

Tactic:
rintro ⟨e, he, rfl⟩

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v e : V
he : e ∈ G.neighborSet v
⊢ (G.dartOfNeighborSet v ⟨e, he⟩).toProd.1 = v
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
d : G.Dart
_h : d ∈ ↑univ
⊢ d.edge ∈ G.edgeSet

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
d : G.Dart
_h : d ∈ ↑univ
⊢ d.edge ∈ G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ : W
⊢ x✝ ∈ (SimpleGraph.map (⇑f) G).support ↔ x✝ ∈ ⇑f '' G.support

Tactic:
;

Goal state after:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ : W
⊢ x✝ ∈ (SimpleGraph.map (⇑f) G).support ↔ x✝ ∈ ⇑f '' G.support
Module: Mathlib.Combinatorics.SimpleGraph.Maps

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

Tactic:
;

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
e : V ≃ W
x✝¹ x✝ : W
⊢ (SimpleGraph.comap (⇑e.symm.toEmbedding) G).Adj x✝¹ x✝ ↔ (SimpleGraph.map (⇑e.toEmbedding) G).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V → W
hf : Injective f
x✝¹ x✝ : V
⊢ (SimpleGraph.comap f (completeGraph W)).Adj x✝¹ x✝ ↔ (completeGraph V).Adj x✝¹ x✝

Tactic:
;

Goal state after:
V : Type u_1
W : Type u_2
f : V → W
hf : Injective f
x✝¹ x✝ : V
⊢ (SimpleGraph.comap f (completeGraph W)).Adj x✝¹ x✝ ↔ (completeGraph V).Adj x✝¹ x✝
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
v w : V
⊢ G.Adj v w → (SimpleGraph.comap f G').Adj v w

Tactic:
;

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V → W
inst✝ : Subsingleton V
v w : V
⊢ G.Adj v w → (SimpleGraph.comap f G').Adj v w
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
⊢ G ≤ SimpleGraph.comap (⇑f) G'

Tactic:
;

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V ↪ W
inst✝ : Subsingleton V
⊢ G ≤ SimpleGraph.comap (⇑f) G'
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
x✝² : SimpleGraph V
x✝¹ x✝ : V
⊢ ((Equiv.refl V).simpleGraph x✝²).Adj x✝¹ x✝ ↔ ((Equiv.refl (SimpleGraph V)) x✝²).Adj x✝¹ x✝

Tactic:
;

Goal state after:
V : Type u_1
x✝² : SimpleGraph V
x✝¹ x✝ : V
⊢ ((Equiv.refl V).simpleGraph x✝²).Adj x✝¹ x✝ ↔ ((Equiv.refl (SimpleGraph V)) x✝²).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
⊢ ⊤ ≤ induce {v} G

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
⊢ ⊤ ≤ induce {v} G
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ᶜ
v w : V
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding w) ↔ G.Adj v w

Tactic:
obtain rfl | hvw := eq_or_ne v w
    · simp
    · simpa [hvw, not_iff_not] using f.map_adj_iff (v := v) (w := w)

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:
;

Goal state after:
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✝)
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
⊢ ∀ {a b : ↑s},
    (induce t G').Adj
        ({ toFun := fun v ↦ ⟨φ ↑v, ⋯⟩, invFun := fun w ↦ ⟨φ.symm ↑w, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a)
        ({ toFun := fun v ↦ ⟨φ ↑v, ⋯⟩, invFun := fun w ↦ ⟨φ.symm ↑w, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b) ↔
      (induce s G).Adj a b

Tactic:
simp [map_adj_iff φ]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : (↑l.toFinset).Pairwise r
hn : l.Nodup
⊢ Pairwise r l

Tactic:
rw [coe_toFinset] at hl
  exact hn.pairwise_of_set_pairwise hl

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:
;

Goal state after:
V : Type u_1
v : V
inst✝ : Fintype ↑(⊥.neighborSet v)
a✝ : V
⊢ a✝ ∈ ⊥.neighborFinset v ↔ a✝ ∈ ∅
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:
;

Goal state after:
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}
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v : V
⊢ #(univ.erase v) = Fintype.card V - 1

Tactic:
rw [card_erase_of_mem (mem_univ v), card_univ]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : Nonempty V
inst✝ : DecidableRel G.Adj
d : ℕ
h : G.IsRegularOfDegree d
⊢ G.maxDegree = d

Tactic:
by
  simp [maxDegree, h.degree_eq, Finset.image_const]

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

Goal state before:
pp: V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x ↦ x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : ↑s
a✝ : V
⊢ a✝ ∈ map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) ↔ a✝ ∈ G.neighborFinset ↑v ∩ s.toFinset

Tactic:
;

Goal state after:
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x ↦ x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : ↑s
a✝ : V
⊢ a✝ ∈ map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) ↔ a✝ ∈ G.neighborFinset ↑v ∩ s.toFinset
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ #s / #P.parts + 1

Tactic:
by
  rw [← P.sum_card_parts]
  exact Finset.EquitableOn.le_add_one hP ht

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ a = ⊥
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : a = ⊥
⊢ Nonempty (Finpartition ⊥)

Tactic:
;

Goal state after:
case pos
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : a = ⊥
⊢ Nonempty (Finpartition ⊥)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ P.parts ⊆ s.powerset

Tactic:
;

Goal state after:
case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ P.parts ⊆ s.powerset
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ P.parts
⊢ p ∈ s.powerset

Tactic:
;

Goal state after:
case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ P.parts
⊢ p ∈ s.powerset
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ P.parts
⊢ p ⊆ s

Tactic:
;

Goal state after:
case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ P.parts
⊢ p ⊆ s
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
this✝ : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
this : P.parts.sup id ≤ (Q.parts.erase b).sup id
⊢ Disjoint b a

Tactic:
← P.sup_parts,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
this✝ : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
this : P.parts.sup id ≤ (Q.parts.erase b).sup id
⊢ Disjoint b (P.parts.sup id)
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
⊢ (𝟭 C).Additive

Tactic:
;

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
⊢ (𝟭 C).Additive
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✝ : ℤ
⊢ (t.truncGE a✝).Additive

Tactic:
;

Goal state after:
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✝ : ℤ
⊢ (t.truncGE a✝).Additive
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
⊢ Functor.Additive 0

Tactic:
;

Goal state after:
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
⊢ Functor.Additive 0
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
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✝

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
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✝

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
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✝

Tactic:
;

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✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a✝ b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ ¬∃ a_1 ∈ I, ⊥ ∈ (P a_1).parts

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a✝ b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ ¬∃ a_1 ∈ I, ⊥ ∈ (P a_1).parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a✝ b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ ∀ a_1 ∈ I, ⊥ ∉ (P a_1).parts

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a✝ b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ ∀ a_1 ∈ I, ⊥ ∉ (P a_1).parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ x✝¹ * 4 ^ x✝¹ ≤ x✝ * 4 ^ x✝

Tactic:
;

Goal state after:
x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ x✝¹ * 4 ^ x✝¹ ≤ x✝ * 4 ^ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: case ha
x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ 1 ≤ 4

Tactic:
;

Goal state after:
case ha
x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ 1 ≤ 4
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ ↑(n * 4 ^ n) = ↑n * 4 ^ n

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ ↑(n * 4 ^ n) = ↑n * 4 ^ n