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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
A : Set α
B : Set β
n : ℕ
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
hfAB : BijOn (⇑f) A B
s t : Multiset α
x✝³ : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
x✝² : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
x✝¹ : s.card = n
x✝ : t.card = n
⊢ (map (⇑f) s).prod = (map (⇑f) t).prod ↔ s.prod = t.prod

Tactic:
by
    rw [← map_multiset_prod, ← map_multiset_prod, EquivLike.apply_eq_iff_eq]

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

Goal state before:
pp: k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → x ∈ Iic ↑k
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → x ∈ Iic ↑k
hs : s.card = m
ht : t.card = m
⊢ (map val s).sum = (map val t).sum ↔ s.sum = t.sum

Tactic:
by
    have (u : Multiset (Fin (n + 1))) : Nat.castRingHom _ (u.map val).sum = u.sum := by simp
    rw [← this, ← this]
    have {u : Multiset (Fin (n + 1))} (huk : ∀ x ∈ u, x ≤ k) (hu : card u = m) :
        (u.map val).sum < (n + 1) := Nat.lt_succ_iff.2 <| hkmn.trans' <| by
      rw [← hu, ← card_map]
      refine sum_le_card_nsmul (u.map val) k ?_
      simpa [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, aux hm hkmn] using huk
    exact ⟨congr_arg _, CharP.natCast_injOn_Iio _ (n + 1) (this hsA hs) (this htA ht)⟩

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

Goal state before:

Tactic:
(#F * #B : ℝ) = #(F * B) := by
        rw [card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hF, Nat.cast_mul]
      _ ≤ #(A * B) := by gcongr
      _ ≤ K * #B := hK

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

Goal state before:
pp: case h₁
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin : ∀ x' ∈ A.powerset.erase ∅, ↑(#(C * B)) / ↑(#C) ≤ ↑(#(x' * B)) / ↑(#x')
hC : C.Nonempty
hCA : C ⊆ A
⊢ ↑(#(C * B ^ m)) ≤ (↑(#(C * B)) / ↑(#C)) ^ m * ↑(#C)

Tactic:
exact card_mul_pow_le (mul_aux hC hCA hCmin) _

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

Goal state before:
pp: case h₂
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin : ∀ x' ∈ A.powerset.erase ∅, ↑(#(C * B)) / ↑(#C) ≤ ↑(#(x' * B)) / ↑(#x')
hC : C.Nonempty
hCA : C ⊆ A
⊢ ↑(#(C * B ^ n)) ≤ (↑(#(C * B)) / ↑(#C)) ^ n * ↑(#C)

Tactic:
exact card_mul_pow_le (mul_aux hC hCA hCmin) _

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A : Set G
⊢ (∃ H, ↑H = A) → IsApproximateSubgroup 1 A

Tactic:
by rintro ⟨H, rfl⟩; exact .subgroup

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

Goal state before:
pp: case h₁
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 := ⋯
V : Finset G := ⋯
W : Finset G := ⋯
⊢ ↑(#(π ![1, -ε 1, -ε 0])) ≤ k * ↑(#A)

Tactic:
exact h ![1, -ε 1, -ε 0] fun i ↦ by fin_cases i <;> simp [hε]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Nontrivial V
⊢ Nonempty ⊤.Dart

Tactic:
obtain ⟨v, w, h⟩ := exists_pair_ne V

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Nontrivial V
v w : V
h : v ≠ w
⊢ Nonempty ⊤.Dart
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case inr.inr.inr.inr
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 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = -1
⊢ ↑(#(A⁻¹ * A⁻¹ * A⁻¹)) ≤ K ^ 3 * ↑(#A)

Tactic:
simp [*, pow_succ', ← mul_inv_rev] at hA ⊢

Goal state after:
case inr.inr.inr.inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
ε : 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 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = -1
hA : ↑(#(A * (A * A))) ≤ K * ↑(#A)
⊢ ↑(#(A * (A * A))) ≤ K * (K * K) * ↑(#A)
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 : V
⊢ ∀ ⦃w : V⦄, G.Adj v w → (SimpleGraph.comap f G').Adj v w

Tactic:
w

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 W
f : ⊤ →g G'
v : V
⊢ ∀ ⦃a₂ : V⦄, f v = f a₂ → v = a₂

Tactic:
w

Goal state after:
V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : ⊤ →g G'
v w : V
⊢ f v = f w → v = w
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd #{w | Odd (G.degree w) ∧ w ≠ v}

Tactic:
← filter_filter,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd #({w ∈ {w | Odd (G.degree w)} | w ≠ v})
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd #({w ∈ {w | Odd (G.degree w)} | w ≠ v})

Tactic:
filter_ne',

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd #({w | Odd (G.degree w)}.erase v)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * 4 ^ #P.parts + a
⊢ (4 ^ #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u

Tactic:
have : m * 4 ^ #P.parts ≤ card α / #P.parts := by
    rw [stepBound, ← Nat.div_div_eq_div_mul]
    exact Nat.div_mul_le_self _ _
  rw [Nat.add_sub_of_le this] at hucard
  rw [(hP.card_parts_eq_average hu).resolve_left hucard, mul_add, mul_one, ← add_assoc, ← add_mul,
    Nat.sub_add_cancel a_add_one_le_four_pow_parts_card, ← add_assoc, mul_comm,
    Nat.add_sub_of_le this, card_univ]

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

Goal state before:
pp: ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
⊢ x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2

Tactic:
apply h₁.trans

Goal state after:
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
⊢ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
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
inst✝ : IsTriangulated C
a b : EInt
hab : a ≤ b
X✝ : C
⊢ IsIso ((t.eTruncGEToGEGE a b).app X✝)

Tactic:
simp only [eTruncGEToGEGE_app]

Goal state after:
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
inst✝ : IsTriangulated C
a b : EInt
hab : a ≤ b
X✝ : C
⊢ IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X✝))
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ↑(#{a}) * ε ≤ ↑(#s')
ht : ↑(#{b}) * ε ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
card_singleton,

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ↑1 * ε ≤ ↑(#s')
ht : ↑1 * ε ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity {a} {b})| < ε
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 (G.nonuniformWitnesses ε t s).2 (G.nonuniformWitnesses ε t s).1 - G.edgeDensity s t|

Tactic:
edgeDensity_comm,

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).1 (G.nonuniformWitnesses ε t s).2 - G.edgeDensity s t|
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case calc_1
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ∀ x ∈ P.nonUniforms G ε, ↑(#x.1) * ↑(#x.2) ≤ ↑(#A / #P.parts + 1) ^ 2

Tactic:
simp only [Prod.forall, Finpartition.mk_mem_nonUniforms, and_imp]
    rintro U V hU hV - -
    rw [sq, ← Nat.cast_mul, ← Nat.cast_mul, Nat.cast_le]
    exact Nat.mul_le_mul (hP.card_part_le_average_add_one hU)
      (hP.card_part_le_average_add_one hV)

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

Goal state before:
pp: case right
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : G'.Subgraph
h : H ≤ H'
v : V
⊢ ∀ ⦃w : V⦄, (Subgraph.comap f H).Adj v w → (Subgraph.comap f H').Adj v w

Tactic:
w

Goal state after:
case right
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : G'.Subgraph
h : H ≤ H'
v w : V
⊢ (Subgraph.comap f H).Adj v w → (Subgraph.comap f H').Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ (⋃ i, {↑i}) \ Sym2.diagSet = G.edgeSet

Tactic:
Set.iUnion_coe_set,

Goal state after:
V : Type u_1
G : SimpleGraph V
⊢ (⋃ i ∈ G.edgeSet, {i}) \ Sym2.diagSet = G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ (⋃ i ∈ G.edgeSet, {i}) \ Sym2.diagSet = G.edgeSet

Tactic:
Set.biUnion_of_singleton

Goal state after:
V : Type u_1
G : SimpleGraph V
⊢ G.edgeSet \ Sym2.diagSet = G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.deleteEdges (s ∩ G'.edgeSet) = G'.deleteEdges s

Tactic:
by
  ext <;> simp +contextual [imp_false]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
v : ↑(G'.deleteEdges s).verts
⊢ ∀ ⦃w : ↑(G'.deleteEdges s).verts⦄, (G'.deleteEdges s).coe.Adj v w → G'.coe.Adj v w

Tactic:
w

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
v w : ↑(G'.deleteEdges s).verts
⊢ (G'.deleteEdges s).coe.Adj v w → G'.coe.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v : V
⊢ ∀ ⦃w : V⦄, H.spanningCoe.Adj v w → G.Adj v w

Tactic:
w

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
⊢ H.spanningCoe.Adj v w → G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v : V
⊢ ∀ ⦃w : V⦄, v ∈ s → w ∈ s → G'.Adj v w → v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w

Tactic:
w

Goal state after:
case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v w : V
⊢ v ∈ s → w ∈ s → G'.Adj v w → v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : n ≤ p.length
⊢ some (p.getVert n) = p.support[n]?

Tactic:
getVert_eq_support_getElem p h,

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : n ≤ p.length
⊢ some p.support[n] = p.support[n]?
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
u : Set V
h : G ≤ G'
v : ↑(⊤.deleteVerts u).verts
⊢ ∀ ⦃w : ↑(⊤.deleteVerts u).verts⦄, (⊤.deleteVerts u).coe.Adj v w → (⊤.deleteVerts u).coe.Adj v w

Tactic:
w

Goal state after:
V : Type u
G G' : SimpleGraph V
u : Set V
h : G ≤ G'
v w : ↑(⊤.deleteVerts u).verts
⊢ (⊤.deleteVerts u).coe.Adj v w → (⊤.deleteVerts u).coe.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
q : G.Walk u' v'
hpq : p.IsSubwalk q
h : G.Adj v' w
⊢ p.IsSubwalk (q.concat h)

Tactic:
obtain ⟨r₁, r₂, rfl⟩ := hpq

Goal state after:
V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
h : G.Adj v' w
r₁ : G.Walk u' u
r₂ : G.Walk v v'
⊢ p.IsSubwalk (((r₁.append p).append r₂).concat h)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Tactic:
rw [Nat.eq_add_of_sub_eq (Nat.sub_pos_of_lt hi') rfl, Nat.sub_eq_zero_of_le hi']

Goal state after:
case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length - Nat.succ 0 + Nat.succ 0) = (cons h p).getVert 0
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ t ∈ (p.append p').support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail

Tactic:
rw [tail_support_append, List.mem_append]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
p : G.Walk u v
h : n ≤ k
⊢ (p.take n).IsSubwalk (p.take k)

Tactic:
induction k, h using Nat.le_induction with

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
p : G.Walk u v
h : n ≤ k
⊢ (p.drop k).IsSubwalk (p.drop n)

Tactic:
induction k, h using Nat.le_induction with

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

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
m : ℕ
⊢ (nil.take 0).getVert m = nil.getVert (min 0 m)

Tactic:
cases m

Goal state after:
case nil.zero.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.take 0).getVert 0 = nil.getVert (min 0 0)

case nil.zero.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take 0).getVert (n✝ + 1) = nil.getVert (min 0 (n✝ + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
m n✝ : ℕ
⊢ (nil.take (n✝ + 1)).getVert m = nil.getVert (min (n✝ + 1) m)

Tactic:
cases m

Goal state after:
case nil.succ.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).getVert 0 = nil.getVert (min (n✝ + 1) 0)

case nil.succ.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝¹ n✝ : ℕ
⊢ (nil.take (n✝¹ + 1)).getVert (n✝ + 1) = nil.getVert (min (n✝¹ + 1) (n✝ + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

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✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
m : ℕ
⊢ ((cons h✝ p✝).take 0).getVert m = (cons h✝ p✝).getVert (min 0 m)

Tactic:
cases m

Goal state after:
case cons.zero.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
⊢ ((cons h✝ p✝).take 0).getVert 0 = (cons h✝ p✝).getVert (min 0 0)

case cons.zero.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n✝ : ℕ
⊢ ((cons h✝ p✝).take 0).getVert (n✝ + 1) = (cons h✝ p✝).getVert (min 0 (n✝ + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
m n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).getVert m = (cons h✝ p✝).getVert (min (n✝ + 1) m)

Tactic:
cases m

Goal state after:
case cons.succ.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).getVert 0 = (cons h✝ p✝).getVert (min (n✝ + 1) 0)

case cons.succ.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n✝¹ n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝¹ + 1)).getVert (n✝ + 1) = (cons h✝ p✝).getVert (min (n✝¹ + 1) (n✝ + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.length < k
⊢ p.support[k]? = q.support[k]?

Tactic:
| inr hk =>

Goal state after:
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
⊢ (⇑f '' (↑s ∩ ↑t)).Subsingleton

Tactic:
exact (hG hs ht hst).image _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
⊢ x✝ ≠ y✝ → G.Adj x✝ y✝

Tactic:
nh

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
nh : x✝ ≠ y✝
⊢ G.Adj x✝ y✝
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
is3Clique_triple_iff.symm,

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.IsNClique 3 {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case refine_3
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ (p.append q).support.tail.Nodup

Tactic:
rw [tail_support_append, List.nodup_append']
    exact ⟨hp.support_nodup.tail, hq.support_nodup.tail, h⟩

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : ∀ (x : Fin n), φ x ≠ t
| ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b

Tactic:
enter [a, b]

Goal state after:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : ∀ (x : Fin n), φ x ≠ t
a b : Fin n
| (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ G.CliqueFreeOn s 2 ↔ s.Pairwise G.Adjᶜ

Tactic:
by
  classical
  refine ⟨fun h a ha b hb _ hab => h ?_ ⟨by simpa [hab.ne], card_pair hab.ne⟩, ?_⟩
  · push_cast
    exact Set.insert_subset_iff.2 ⟨ha, Set.singleton_subset_iff.2 hb⟩
  simp only [CliqueFreeOn, isNClique_iff, card_eq_two, not_and, not_exists]
  rintro h t hst ht a b hab rfl
  simp only [coe_insert, coe_singleton, Set.insert_subset_iff, Set.singleton_subset_iff] at hst
  refine h hst.1 hst.2 hab (ht ?_ ?_ hab) <;> simp

Goal state after: