mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ IsZero (Triangle.mk (𝟙 ((shiftFunctor C 1).obj (ι.obj X₁))) 0 0).obj₃

Tactic:
by
      dsimp
      rw [IsZero.iff_id_eq_zero, ← ι.map_id, id_zero, ι.map_zero]

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

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁵ : Preadditive A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι f₁
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ (shiftFunctor C 1).obj (ι.obj I)
hI : Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ ∈ distinguishedTriangles
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : (shiftFunctor C 1).map (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ (shiftFunctor C 1).obj (ι.obj K)
hm₃ : (shiftFunctor C 1).map m₃ = H.m₃
⊢ (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃)).rotate ∈ distinguishedTriangles

Tactic:
← Triangle.shift_distinguished_iff _ 1

Goal state after:
C : Type u_1
A : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁵ : Preadditive A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι f₁
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ (shiftFunctor C 1).obj (ι.obj I)
hI : Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ ∈ distinguishedTriangles
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : (shiftFunctor C 1).map (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ (shiftFunctor C 1).obj (ι.obj K)
hm₃ : (shiftFunctor C 1).map m₃ = H.m₃
⊢ (shiftFunctor (Triangle C) 1).obj (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃)).rotate ∈ distinguishedTriangles
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case inr.inr.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ b = c

pp: case inr.inr.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
⊢ b = c

Tactic:
· obtain rfl := ha hc hb ((mul_comm _ _).trans h)
    exact ha' hb hc h

Goal state after:
case inr.inr.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
⊢ b = c
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ ∑ a ∈ s, #(bipartiteAbove r t a) = ∑ b ∈ t, #(bipartiteBelow r s b)

Tactic:
simp_rw [card_eq_sum_ones, sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow]

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

Goal state before:
pp: case g2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this✝ : (map (g ∘ f) s).prod = (map g (map f t)).prod
this : s.prod = (map (g ∘ f) t).prod
x : α
hx : x ∈ t
⊢ (g ∘ f) x = id x

pp: case g1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : (map (g ∘ f) s).prod = (map g (map f t)).prod
x : α
hx : x ∈ s
⊢ (g ∘ f) x = id x

Tactic:
case g1 => exact h.1 (hsA hx)

Goal state after:
case g2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this✝ : (map (g ∘ f) s).prod = (map g (map f t)).prod
this : s.prod = (map (g ∘ f) t).prod
x : α
hx : x ∈ t
⊢ (g ∘ f) x = id x
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < dValue N

Tactic:
dValue,

Goal state after:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ⌊↑N ^ (↑(nValue N))⁻¹ / 2⌋₊
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case insert
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
⊢ #(insert x C * A * B) * #A ≤ #(A * B) * #(insert x C * A)

Tactic:
set C' := insert x C with hC'

Goal state after:
case insert
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
⊢ #(C' * A * B) * #A ≤ #(A * B) * #(C' * A)
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

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

Tactic:
by rw [sq, ← one_mul 1]; exact Set.mul_mem_mul hA₁ hA₁

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B x⁻¹ = B⁻¹.convolution A⁻¹ x

Tactic:
nth_rw 1 [← inv_inv B]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B⁻¹⁻¹ x⁻¹ = B⁻¹.convolution A⁻¹ x
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ SimpleGraph.map id G = G

Tactic:
ext
  dsimp [SimpleGraph.map, Relation.Map]
  grind [SimpleGraph.Adj.ne]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
f : V → W
g : W → X
⊢ SimpleGraph.map g (SimpleGraph.map f G) = SimpleGraph.map (g ∘ f) G

Tactic:
ext
  dsimp [SimpleGraph.map, Relation.Map]
  grind [SimpleGraph.Adj.ne]

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

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

Tactic:
rw [coe_toFinset, hn.pairwise_coe]

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.degree v = Fintype.card V - 1
⊢ G.IsUniversal v

Tactic:
rw [← G.insert_neighborFinset_eq_univ v, ← Finset.card_eq_iff_eq_univ]

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.degree v = Fintype.card V - 1
⊢ #(insert v (G.neighborFinset v)) = Fintype.card V
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this✝ : Lattice (Subtype Pr) := Subtype.lattice Prsup Prinf
this : OrderBot (Subtype Pr) := Subtype.orderBot Prbot
⊢ (P.parts.preimage Subtype.val ⋯).sup id = ⟨s, hs⟩

Tactic:
by
      simpa [Finset.sup_preimage_val_id Prsup Prbot hP] using P.sup_parts

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ ∃! t, t ∈ P.parts ∧ a ∈ t

Tactic:
obtain ⟨t, ht, ht'⟩ := P.exists_mem ha

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
ht' : a ∈ t
⊢ ∃! t, t ∈ P.parts ∧ a ∈ t
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
⊢ a ∈ P.part b ↔ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p

Tactic:
by
  constructor
  · intro h
    have : b ∈ s := P.part_nonempty.1 ⟨a, h⟩
    refine ⟨_, ?_, h, ?_⟩ <;> simp [this]
  · rintro ⟨p, hp, hap, hbp⟩
    obtain rfl : P.part b = p := P.part_eq_of_mem hp hbp
    exact hap

Goal state after:
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
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (G.nonuniformWitnesses ε s t).1 ⊆ s

Tactic:
nonuniformWitnesses,

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (if h : ¬G.IsUniform ε s t then (⋯.choose, ⋯.choose) else (s, t)).1 ⊆ s
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
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#s) * ε ≤ ↑(#(G.nonuniformWitnesses ε s t).1)

Tactic:
nonuniformWitnesses,

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#s) * ε ≤ ↑(#(if h : ¬G.IsUniform ε s t then (⋯.choose, ⋯.choose) else (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 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (G.nonuniformWitnesses ε s t).2 ⊆ t

Tactic:
nonuniformWitnesses,

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (if h : ¬G.IsUniform ε s t then (⋯.choose, ⋯.choose) else (s, t)).2 ⊆ t
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
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#t) * ε ≤ ↑(#(G.nonuniformWitnesses ε s t).2)

Tactic:
nonuniformWitnesses,

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#t) * ε ≤ ↑(#(if h : ¬G.IsUniform ε s t then (⋯.choose, ⋯.choose) else (s, t)).2)
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
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ε ≤ ↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t|

Tactic:
nonuniformWitnesses,

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ε ≤
    ↑|G.edgeDensity (if h : ¬G.IsUniform ε s t then (⋯.choose, ⋯.choose) else (s, t)).1
            (if h : ¬G.IsUniform ε s t then (⋯.choose, ⋯.choose) else (s, t)).2 -
          G.edgeDensity s t|
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
inst✝ : Nonempty ι
f : ι → G.Subgraph
⊢ (sInf (Set.range fun i ↦ f i)).Adj a b ↔ ∀ (i : ι), (f i).Adj a b

Tactic:
sInf_adj_of_nonempty (Set.range_nonempty _)

Goal state after:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
inst✝ : Nonempty ι
f : ι → G.Subgraph
⊢ (∀ G' ∈ Set.range fun i ↦ f i, G'.Adj a b) ↔ ∀ (i : ι), (f i).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case mp
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ G ⊴ H → ∃ H' _e, H'.IsInduced

Tactic:
rintro ⟨f⟩

Goal state after:
case mp
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ↪g H
⊢ ∃ H' _e, H'.IsInduced
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
⊢ H = G.singletonSubgraph v ↔ H.verts = {v}

Tactic:
refine ⟨fun h ↦ by rw [h, singletonSubgraph_verts], fun h ↦ ?_⟩

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
⊢ H = G.singletonSubgraph v
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : H.Adj x✝¹ x✝
ha1 : x✝¹ = v
ha2 : x✝ = v
⊢ False

Tactic:
subst_vars

Goal state after:
case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
x✝ : V
ha : H.Adj x✝ x✝
h : H.verts = {x✝}
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : u = v
h✝ : u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ {v}

Tactic:
subst_vars

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
w : V
hvw : G.Adj w w
⊢ (G.subgraphOfAdj hvw).neighborSet w = {w} ∪ {w}
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : u = v
h✝ : ¬u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ ∅

Tactic:
subst_vars

Goal state after:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w : V
hvw : G.Adj v w
h✝ : ¬v = w
⊢ (G.subgraphOfAdj hvw).neighborSet v = {w} ∪ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : ¬u = v
h✝ : u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ {v}

Tactic:
subst_vars

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w : V
hvw : G.Adj v w
h✝ : ¬w = v
⊢ (G.subgraphOfAdj hvw).neighborSet w = ∅ ∪ {v}
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : ¬u = v
h✝ : ¬u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ ∅

Tactic:
subst_vars

Goal state after:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : ¬u = v
h✝ : ¬u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
x✝ : V
⊢ x✝ ∈ Set.range p.getVert → x✝ ∈ Set.range p.support.get

Tactic:
by grind [Set.range_list_get, getVert_mem_support]

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ Walk.map f (p.copy hu hv) = (Walk.map f p).copy ⋯ ⋯

Tactic:
subst_vars

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u' v' : V
p : G.Walk u' v'
⊢ Walk.map f (p.copy ⋯ ⋯) = (Walk.map f p).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : G.Walk u v
f f' : G →g G'
h : f = f'
⊢ Walk.map f p = (Walk.map f' p).copy ⋯ ⋯

Tactic:
subst_vars

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : G.Walk u v
f' : G →g G'
⊢ Walk.map f' p = (Walk.map f' p).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' u'' v'' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ (p.copy hu hv).copy hu' hv' = p.copy ⋯ ⋯

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u'' v'' : V
p : G.Walk u'' v''
⊢ (p.copy ⋯ ⋯).copy ⋯ ⋯ = p.copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u u' : V
hu : u = u'
⊢ nil.copy hu hu = nil

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u' : V
⊢ nil.copy ⋯ ⋯ = nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w u' w' : V
h : G.Adj u v
p : G.Walk v w
hu : u = u'
hw : w = w'
⊢ (cons h p).copy hu hw = cons ⋯ (p.copy ⋯ hw)

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
v u' w' : V
h : G.Adj u' v
p : G.Walk v w'
⊢ (cons h p).copy ⋯ ⋯ = cons ⋯ (p.copy ⋯ ⋯)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w v' w' : V
h : G.Adj u v
p : G.Walk v' w'
hv : v' = v
hw : w' = w
⊢ cons h (p.copy hv hw) = (cons ⋯ p).copy ⋯ hw

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u v' w' : V
p : G.Walk v' w'
h : G.Adj u v'
⊢ cons h (p.copy ⋯ ⋯) = (cons ⋯ p).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w u' v' w' : V
p : G.Walk u v
q : G.Walk v w
hu : u = u'
hv : v = v'
hw : w = w'
⊢ (p.copy hu hv).append (q.copy hv hw) = (p.append q).copy hu hw

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u' v' w' : V
p : G.Walk u' v'
q : G.Walk v' w'
⊢ (p.copy ⋯ ⋯).append (q.copy ⋯ ⋯) = (p.append q).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).reverse = p.reverse.copy hv hu

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).reverse = p.reverse.copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).length = p.length

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).length = p.length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
h' : u✝ = u
⊢ (h' ▸ nil).append (Eq.rec (motive := fun x x_1 ↦ x ∈ u✝ :: p✝.support → G.Walk x w✝) (fun h ↦ cons h✝ p✝) h' ⋯) =
    cons h✝ p✝

Tactic:
subst_vars

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u✝ ∈ p✝.support), (p✝.takeUntil u✝ h).append (p✝.dropUntil u✝ h) = p✝
a✝ : List.Mem u✝ p✝.support
⊢ (⋯ ▸ nil).append (Eq.rec (motive := fun x x_1 ↦ x ∈ u✝ :: p✝.support → G.Walk x w✝) (fun h ↦ cons h✝ p✝) ⋯ ⋯) =
    cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
h' : ¬u✝ = u
⊢ (cons h✝ (p✝.takeUntil u ⋯)).append (p✝.dropUntil u ⋯) = cons h✝ p✝

Tactic:
subst_vars

Goal state after:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
h' : ¬u✝ = u
⊢ (cons h✝ (p✝.takeUntil u ⋯)).append (p✝.dropUntil u ⋯) = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k,
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ p₂.darts[i + k]? = some p₁.darts[i]

Tactic:
rw [getElem?_pos _ _ <| by grind, Option.some_inj]

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k,
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ p₂.darts[i + k] = p₁.darts[i]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).support = p.support

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).support = p.support