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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g t → x ∈ A

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d k : ℕ
⊢ ThreeAPFree ↑(sphere n d k)

Tactic:
set f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
    { toFun := fun f => toLp 2 (((↑) : ℕ → ℝ) ∘ f)
      map_zero' := PiLp.ext fun _ => cast_zero
      map_add' := fun _ _ => PiLp.ext fun _ => cast_add _ _ }

Goal state after:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f ↦ toLp 2 (Nat.cast ∘ f), map_zero' := ⋯, map_add' := ⋯ }
⊢ ThreeAPFree ↑(sphere n d k)
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
h : s.prod = t.prod
hf : IsMulFreimanHom (0 + 1) A B f
hs : s.card = 0
x✝ : t.card = 0
⊢ (map f s).prod = (map f t).prod

Tactic:
aesop

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
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U ≠ ∅ ∧ U ∈ B.powerset
hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(#(U * A)) / ↑(#U) ≤ ↑(#(x' * A)) / ↑(#x')
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)

Tactic:
mem_powerset,

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U ≠ ∅ ∧ U ⊆ B
hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(#(U * A)) / ↑(#U) ≤ ↑(#(x' * A)) / ↑(#x')
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: 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
hC : C ≠ ∅ ∧ C ∈ A.powerset
hCmin : ∀ x' ∈ A.powerset.erase ∅, ↑(#(C * B)) / ↑(#C) ≤ ↑(#(x' * B)) / ↑(#x')
⊢ ↑(#(B ^ m / B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ (m + n) * ↑(#A)

Tactic:
mem_powerset,

Goal state after:
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
hC : C ≠ ∅ ∧ C ⊆ A
hCmin : ∀ x' ∈ A.powerset.erase ∅, ↑(#(C * B)) / ↑(#C) ≤ ↑(#(x' * B)) / ↑(#x')
⊢ ↑(#(B ^ m / B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ (m + n) * ↑(#A)
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
⊢ minOrder (ZMod n) = ↑n.minFac

Tactic:
refine ((minOrder_le_natCard (zmultiples_eq_bot.not.2 this) <| toFinite _).trans ?_).antisymm <|
    le_minOrder_iff_forall_addSubgroup.2 fun s hs _ ↦ ?_

Goal state after:
case refine_1
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
⊢ ↑(Nat.card ↥(zmultiples ↑(n / n.minFac))) ≤ ↑n.minFac

case refine_2
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
s : AddSubgroup (ZMod n)
hs : s ≠ ⊥
x✝ : (↑s).Finite
⊢ ↑n.minFac ≤ ↑(Nat.card ↥s)
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:
exact ruzsa_triangle_inequality_invMul_mul_mul ..

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

Goal state before:
pp: case h
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (SimpleGraph.map (⇑f) G).Adj x✝ y✝ ↔ s(x✝, y✝) ∈ ⇑f.sym2Map '' G.edgeSet

Tactic:
map_adj,

Goal state after:
case h
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝) ↔ s(x✝, y✝) ∈ ⇑f.sym2Map '' G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ Fintype.card ↑Sym2.diagSetᶜ = (Fintype.card V).choose 2

Tactic:
← Sym2.card_diagSet_compl

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.minDegree = d

Tactic:
simp [minDegree, h.degree_eq, Finset.image_const]

Goal state after:
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
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage Subtype.val ⋯
i : Subtype Pr
hi : i ∈ P.parts.preimage Subtype.val ⋯
hi' : i ∉ t
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ Disjoint (id i) (t.sup id)

Tactic:
rw [disjoint_subtype_iff Prinf Prbot, sup_coe, this, ← sup_image t Subtype.val id]

Goal state after:
α : 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
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage Subtype.val ⋯
i : Subtype Pr
hi : i ∈ P.parts.preimage Subtype.val ⋯
hi' : i ∉ t
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ Disjoint (↑(id i)) ((image Subtype.val t).sup id)

α : 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
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage Subtype.val ⋯
i : Subtype Pr
hi : i ∈ P.parts.preimage Subtype.val ⋯
hi' : i ∉ t
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ ∀ ⦃x y : α⦄, Pr x → Pr y → Pr (x ⊔ y)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst✝ : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
hinj : ∀ x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, ∀ y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, x ⊓ b = y ⊓ b → x = y
heq : (image (fun x ↦ x ⊓ b) P.parts).erase ⊥ = image (fun x ↦ x ⊓ b) ({x ∈ P.parts | x ⊓ b ≠ ⊥})
x : α
hx : x ∈ {x ∈ P.parts | ¬x ⊓ b ≠ ⊥}
⊢ f (x ⊓ b) = 0

Tactic:
simp only [ne_eq, Decidable.not_not, Finset.mem_filter] at hx
    rw [hx.2, hf]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
h : a ∉ s
⊢ P.part a = ∅

Tactic:
by simp [part, h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} →
      ∃ a ∈ (F.erase t).powerset, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = x

Tactic:
mem_powerset,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} → ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = x
Module: Mathlib.Combinatorics.SimpleGraph.Density

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

Tactic:
edgeDensity_add_edgeDensity_compl _ (hs₂.mono hs) (ht₂.mono ht),

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

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

Tactic:
rw [← card_product, interedges_def, interedges_def]

Goal state after:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ #({e ∈ s ×ˢ t | G.Adj e.1 e.2}) + #({e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2}) = #(s ×ˢ t)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

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

Tactic:
mul_right_comm _ ε,

Goal state after:
case calc_2
α : 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 ε
⊢ ↑(#P.parts * (#P.parts - 1)) * ↑(#A / #P.parts + 1) ^ 2 * ε < ε * (↑(#A) + ↑(#P.parts)) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:

Tactic:
_ ≤ ∑ i ∈ P.nonUniforms G ε, (#i.1 * #i.2 : 𝕜) := by
        norm_cast; simp_rw [← card_product]; exact card_biUnion_le
    _ < _ := hP.sum_nonUniforms_lt' hA hε hG
    _ ≤ ε * (#A + #A) ^ 2 := by gcongr; exact P.card_parts_le_card
    _ = _ := by ring

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts) /
      ↑(#P.parts) ^ 2 =
    (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) /
      ↑(#(increment hP G ε).parts) ^ 2

Tactic:
card_increment hPα hPG,

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts) /
      ↑(#P.parts) ^ 2 =
    (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) /
      ↑(stepBound #P.parts) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
v₁ v₂ : ↑s
⊢ G.Adj ↑v₁ ↑v₂ ∧ ↑v₁ ≠ x ∧ ↑v₂ ≠ x ↔ G.Adj ↑v₁ ↑v₂

Tactic:
and_iff_left_iff_imp

Goal state after:
V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
v₁ v₂ : ↑s
⊢ G.Adj ↑v₁ ↑v₂ → ↑v₁ ≠ x ∧ ↑v₂ ≠ x
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
v w : V
s : Set V
G : SimpleGraph ↑s
hadj : G.spanningCoe.Adj v w
⊢ v ∈ s

Tactic:
aesop

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ w✝ : V
hadj : G.Adj v✝ w✝
v w : V
⊢ (G.subgraphOfAdj hadj).spanningCoe.Adj v w ↔ (fromEdgeSet {s(v✝, w✝)}).Adj v w

Tactic:
aesop

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ Function.Injective fun G' ↦ (G'.verts, G'.spanningCoe)

Tactic:
by
  intro G₁ G₂ h
  rw [Prod.ext_iff] at h
  exact Subgraph.ext h.1 (spanningCoe_inj.1 h.2)

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G.Copy H
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : Fintype ↑(H.neighborSet (f v))
⊢ G.degree v ≤ H.degree (f v)

Tactic:
simpa [card_neighborSet_eq_degree] using
    Fintype.card_le_of_injective _ (f.mapNeighborSet v).injective

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : x✝ = t
h✝ : ¬y✝ = t
⊢ G.Adj s y✝ ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s

Tactic:
aesop

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : y✝ = t
⊢ G.Adj s x✝ ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s

Tactic:
aesop

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : x✝ = t
h✝ : ¬y✝ = t
⊢ G.Adj s y✝ ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}

Tactic:
aesop

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : y✝ = t
⊢ G.Adj s x✝ ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}

Tactic:
aesop

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset \ G.incidenceFinset t
this : t ∉ e
⊢ ∀ b ∈ image (fun x ↦ s(x, t)) (G.neighborFinset s), e ≠ b

Tactic:
aesop

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

Goal state before:
pp: case e_a.e_a.H
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ ∀ ⦃a₁ a₂ : V⦄, (fun x ↦ s(x, t)) a₁ = (fun x ↦ s(x, t)) a₂ → a₁ = a₂

Tactic:
aesop

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

Goal state before:
pp: case e_a.e_a.H
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ ∀ ⦃a₁ a₂ : V⦄, (fun x ↦ s(x, t)) a₁ = (fun x ↦ s(x, t)) a₂ → a₁ = a₂

Tactic:
aesop

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
h' : ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∈ s
⊢ False

Tactic:
exact h' _ hs rfl

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : G.Subgraph
s✝ s' s : Set V
h : s ⊆ G'.verts
x✝ : ↑(G'.induce s).verts
v : V
hv✝ : v ∈ (G'.induce s).verts
hv : v ∈ s
⊢ ⟨v, ⋯⟩ ∈ {v | ↑v ∈ s}

Tactic:
aesop

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : G.Subgraph
s✝ s' s : Set V
h : s ⊆ G'.verts
x✝ : ↑(G'.induce s).verts
v : V
hv : v ∈ (G'.induce s).verts
⊢ ⟨v, ⋯⟩ ∈ {v | ↑v ∈ s}

Tactic:
by simp at hv; aesop

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

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

Tactic:
aesop

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s✝ s : Set V
x✝ : ↑(G'.deleteVerts s).verts
v : V
hv : v ∈ (G'.deleteVerts s).verts
⊢ ⟨v, ⋯⟩ ∈ {v | ↑v ∉ s}

Tactic:
aesop

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
⊢ w ∈ nil.support ↔ w = u✝ ∨ ∃ e ∈ nil.edges, w ∈ e

Tactic:
aesop

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : w ∈ p✝.support ↔ w = w✝ ∨ ∃ e ∈ p✝.edges, w ∈ e
⊢ w ∈ (cons h✝ p✝).support ↔ w = w✝ ∨ ∃ e ∈ (cons h✝ p✝).edges, w ∈ e

Tactic:
aesop

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

Goal state before:
pp: case cons.nil
V : Type u
G : SimpleGraph V
u v w u✝ v✝ : V
h : G.Adj u✝ v✝
ih : ¬nil.Nil → (w ∈ nil.support ↔ ∃ e ∈ nil.edges, w ∈ e)
hnil : ¬(cons h nil).Nil
⊢ w ∈ (cons h nil).support ↔ ∃ e ∈ (cons h nil).edges, w ∈ e

Tactic:
aesop

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

Goal state before:
pp: case cons.cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝¹ w✝ : V
h : G.Adj u✝ v✝¹
v✝ : V
h✝ : G.Adj v✝¹ v✝
p✝ : G.Walk v✝ w✝
ih : ¬(cons h✝ p✝).Nil → (w ∈ (cons h✝ p✝).support ↔ ∃ e ∈ (cons h✝ p✝).edges, w ∈ e)
hnil : ¬(cons h (cons h✝ p✝)).Nil
⊢ w ∈ (cons h (cons h✝ p✝)).support ↔ ∃ e ∈ (cons h (cons h✝ p✝)).edges, w ∈ e

Tactic:
aesop

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

Goal state before:
pp: case refine_2.refine_3
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₂.support = ((((p₂.take s.length).copy ⋯ ⋯).append p₁).append ((p₂.drop (s.length + p₁.length)).copy ⋯ ⋯)).support

Tactic:
simp only [← h, support_append, support_copy, support_take,
      List.take_append, drop_support_eq_support_drop_min, List.tail_drop]

Goal state after:
case refine_2.refine_3
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s ++ p₁.support ++ t =
    List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) p₁.support ++
          List.take (s.length + 1 - (s ++ p₁.support).length) t ++
        p₁.support.tail ++
      List.drop (min (s.length + p₁.length) p₂.length + 1) (s ++ p₁.support ++ t)
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ h.toWalk.IsPath

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) *
      ((1 - ε ^ 5 / 50) / (↑(#(A.sup id)) * ↑(#(B.sup id))) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y)))) ≤
    ↑(#(G.interedges x y))

Tactic:
refine mul_le_of_le_one_right (cast_nonneg _) ?_
    rw [div_mul_eq_mul_div, ← mul_assoc, mul_assoc]
    refine div_le_one_of_le₀ ?_ (by positivity)
    refine (mul_le_mul_of_nonneg_right (one_sub_le_m_div_m_add_one_sq hPα hPε) ?_).trans ?_
    · exact_mod_cast _root_.zero_le
    rw [sq, mul_mul_mul_comm, mul_comm ((m : ℝ) / _), mul_comm ((m : ℝ) / _)]
    gcongr
    · apply le_sum_card_subset_chunk_parts hA hx
    · apply le_sum_card_subset_chunk_parts hB hy

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : n = 0
hm0 : ¬m = 0
hnm : v = p.getVert (m - 1)
⊢ v ∉ p.support

Tactic:
aesop

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

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
h✝ : x = v
⊢ Sym2.ToRel {s(v, w)} x y

Tactic:
aesop

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

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
h✝ : ¬x = v
⊢ Sym2.ToRel {s(v, w)} x y

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a e ∧ G.Adj b e ∧ {a, b, e} = {a, b, e}

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ ¬(#t ≤ 1 ∧ #t = n)

Tactic:
by rintro ⟨h', rfl⟩; exact h'.not_gt hn

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj a d
hce : G.Adj a b
hde : G.Adj b d
⊢ G.Adj a d ∧ G.Adj b d ∧ {a, d, b} = {a, b, d}

Tactic:
aesop

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ i = 0 ∨ i = p.length → p.getVert i = u

Tactic:
aesop

Goal state after: