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
⊢ (map g s).prod = (map g t).prod ↔ s.prod = t.prod

Tactic:
← hf.map_prod_eq_map_prod _ _ (by simp [hs]) (by simp [ht]),

Goal state after:
α : 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
⊢ (map f (map g s)).prod = (map f (map g t)).prod ↔ s.prod = t.prod

α : 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 s → x ∈ A

α : 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
Module: Mathlib.Combinatorics.Additive.CovBySMul

Goal state before:
pp: M : Type u_1
N : Type u_2
X : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : MulAction M X
inst✝² : MulAction N X
K L : ℝ
A B C : Set X
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : ↑(#F₁) ≤ K
hFAB : A ⊆ ↑F₁ • B
F₂ : Finset N
hF₂ : ↑(#F₂) ≤ L
hFBC : B ⊆ ↑F₂ • C
⊢ CovBySMul N (K * L) A C

Tactic:
refine ⟨F₁ • F₂, ?_, ?_⟩

Goal state after:
case refine_1
M : Type u_1
N : Type u_2
X : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : MulAction M X
inst✝² : MulAction N X
K L : ℝ
A B C : Set X
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : ↑(#F₁) ≤ K
hFAB : A ⊆ ↑F₁ • B
F₂ : Finset N
hF₂ : ↑(#F₂) ≤ L
hFBC : B ⊆ ↑F₂ • C
⊢ ↑(#(F₁ • F₂)) ≤ K * L

case refine_2
M : Type u_1
N : Type u_2
X : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : MulAction M X
inst✝² : MulAction N X
K L : ℝ
A B C : Set X
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : ↑(#F₁) ≤ K
hFAB : A ⊆ ↑F₁ • B
F₂ : Finset N
hF₂ : ↑(#F₂) ≤ L
hFBC : B ⊆ ↑F₂ • C
⊢ A ⊆ ↑(F₁ • F₂) • C
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
⊢ (2 * d + 1) ^ n - 1 = (∑ i, d * (2 * d + 1) ^ ↑i) * 2

Tactic:
← sum_range fun i => d * (2 * d + 1) ^ (i : ℕ),

Goal state after:
n d : ℕ
⊢ (2 * d + 1) ^ n - 1 = (∑ i ∈ range n, d * (2 * d + 1) ^ i) * 2
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: k n✝¹ n✝ : ℕ
⊢ Set.InjOn ⇑(map (2 * (n✝ + 1) - 1)) ↑(sphere (n✝¹ + 1) (n✝ + 1) k)

Tactic:
apply map_injOn.mono fun x => ?_

Goal state after:
k n✝¹ n✝ : ℕ
x : Fin (n✝¹ + 1) → ℕ
⊢ x ∈ ↑(sphere (n✝¹ + 1) (n✝ + 1) k) → x ∈ {x | ∀ (i : Fin (n✝¹ + 1)), x i < 2 * (n✝ + 1) - 1}
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
this✝ : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1))) (map val u).sum = u.sum
this : ∀ {u : Multiset (Fin (n + 1))}, (∀ x ∈ u, x ≤ ↑k) → u.card = m → (map val u).sum < n + 1
⊢ (map val s).sum = (map val t).sum ↔
    (Nat.castRingHom (Fin (n + 1))) (map val s).sum = (Nat.castRingHom (Fin (n + 1))) (map val t).sum

Tactic:
exact ⟨congr_arg _, CharP.natCast_injOn_Iio _ (n + 1) (this hsA hs) (this htA ht)⟩

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

Goal state before:
pp: ⊢ log 2 ^ 2 * 2 ^ 2 ≤ 3 * log 2

Tactic:
sq (log 2),

Goal state after:
⊢ log 2 * log 2 * 2 ^ 2 ≤ 3 * log 2
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Tactic:
have hN₀ : 0 < (N : ℝ) := cast_pos.2 (hN.trans' <| by norm_num1)

Goal state after:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case refine_1.refine_1
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
b : G
hb : b ∈ ↑B
⊢ (fun b ↦ (a / b, c / b)) b ∈
    ↑(bipartiteAbove
        (fun b x ↦
          match x with
          | (a, c) => a / c = b)
        ((A / B) ×ˢ (C / B)) (a / c))

Tactic:
rw [mem_coe, mem_bipartiteAbove]

Goal state after:
case refine_1.refine_1
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
b : G
hb : b ∈ ↑B
⊢ (fun b ↦ (a / b, c / b)) b ∈ (A / B) ×ˢ (C / B) ∧
    match (fun b ↦ (a / b, c / b)) b with
    | (a_1, c_1) => a_1 / c_1 = a / c
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ 64 = 2 ^ ↑6

Tactic:
rw [rpow_natCast]; norm_num1

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

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A ^ 2 ⊆ ↑∅ • A
⊢ ∃ x, A * A ⊆ x • A

Tactic:
simp [hA.nonempty.ne_empty] at hKA

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 y : G
⊢ Set.MapsTo (fun ab' ↦ x •> ab'.1) ↑({ab ∈ A ×ˢ B⁻¹ | ab.1 * ab.2 = x⁻¹ * y}) ↑(x •> A ∩ y •> B)

Tactic:
simp +contextual [Set.MapsTo, Set.mem_smul_set_iff_inv_smul_mem]
        simp +contextual [← eq_mul_inv_iff_mul_eq, mul_assoc]

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

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

Tactic:
simpa [mul_assoc] using small_pos_neg_pos_mul (A := A) (K := K) (by simpa)

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe = G
v : V
hv : v ∈ (induce s G).spanningCoe.support
⊢ v ∈ s

Tactic:
support_spanningCoe

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe = G
v : V
hv : v ∈ Subtype.val '' (induce s G).support
⊢ v ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
W : Type u_2
inst✝² : Fintype W
inst✝¹ : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ #(SimpleGraph.map (⇑f) G).edgeFinset = #G.edgeFinset

Tactic:
rw [edgeFinset_map]
  exact G.edgeFinset.card_map f.sym2Map

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
⊢ b ∈ P.parts

Tactic:
obtain ⟨c, hc, hbc⟩ := hQP hb
        obtain ⟨d, hd, hcd⟩ := hPQ hc
        rwa [hbc.antisymm]
        rwa [Q.disjoint.eq_of_le hb hd (Q.ne_bot hb) (hbc.trans hcd)]

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

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (P.parts.sup fun i ↦ Q.parts.sup fun i' ↦ i ⊓ i') = P.parts.sup fun i ↦ id i ⊓ Q.parts.sup id

Tactic:
Finset.sup_inf_distrib_left

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (P.parts.sup fun i ↦ Q.parts.sup fun i' ↦ i ⊓ i') = P.parts.sup fun i ↦ Q.parts.sup fun i_1 ↦ id i ⊓ id i_1
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case mpr.ht
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ P.part a ∈ P.parts

Tactic:
simp [*, P.le ht hat]

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

Goal state before:
pp: case mpr.hu
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ t ∈ P.parts

Tactic:
simp [*, P.le ht hat]

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

Goal state before:
pp: case mpr.hat
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ a ∈ P.part a

Tactic:
simp [*, P.le ht hat]

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

Goal state before:
pp: case mpr.hau
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ a ∈ t

Tactic:
simp [*, P.le ht hat]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (atomise s ∅).parts = {s}

Tactic:
by
  simp only [atomise, powerset_empty, image_singleton, notMem_empty, IsEmpty.forall_iff,
    imp_true_iff, filter_true]
  exact erase_eq_of_notMem (notMem_singleton.2 hs.ne_empty.symm)

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

Goal state before:
pp: case inr
ι : 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
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
h₃ : ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, (f i - (∑ j ∈ t, f j) / ↑(#t)) ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 * ↑(#t) + ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, f i ^ 2

Tactic:
grw [h₃]

Goal state after:
case inr
ι : 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
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
h₃ : ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, (f i - (∑ j ∈ t, f j) / ↑(#t)) ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 * ↑(#t) + ∑ i ∈ t, (f i - (∑ j ∈ t, f j) / ↑(#t)) ^ 2 ≤ ∑ i ∈ t, f i ^ 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
a' b' : EInt
hab' : a' ≤ b'
φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')
X : C
⊢ (t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X)) ≫
        (t.eTruncLT.obj b').map ((t.eTruncGE.obj a').map ((t.eTruncLTι b).app X)) ≫
          (t.eTruncLTGEIsoGELT a' b').hom.app X =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X) ≫
        (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)

Tactic:
← t.eTruncLT_map_app_eTruncLTι_app (φ.app 1) X

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
a' b' : EInt
hab' : a' ≤ b'
φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')
X : C
⊢ (t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X)) ≫
        (t.eTruncLT.obj b').map
            ((t.eTruncGE.obj a').map
              ((t.eTruncLT.map (φ.app 1)).app X ≫ (t.eTruncLTι ((mk₁ (homOfLE hab')).obj 1)).app X)) ≫
          (t.eTruncLTGEIsoGELT a' b').hom.app X =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X) ≫
        (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).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
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (if h : ¬G.IsUniform ε s t then (⋯.choose, ⋯.choose) else (s, t)).1 ⊆ s

Tactic:
dif_pos h

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
⊢ (⋯.choose, ⋯.choose).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) * ε ≤ ↑(#(if h : ¬G.IsUniform ε s t then (⋯.choose, ⋯.choose) else (s, t)).1)

Tactic:
dif_pos h

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) * ε ≤ ↑(#(⋯.choose, ⋯.choose).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
⊢ (if h : ¬G.IsUniform ε s t then (⋯.choose, ⋯.choose) else (s, t)).2 ⊆ t

Tactic:
dif_pos h

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
⊢ (⋯.choose, ⋯.choose).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) * ε ≤ ↑(#(if h : ¬G.IsUniform ε s t then (⋯.choose, ⋯.choose) else (s, t)).2)

Tactic:
dif_pos h

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) * ε ≤ ↑(#(⋯.choose, ⋯.choose).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 (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|

Tactic:
dif_pos h

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 (⋯.choose, ⋯.choose).1 (⋯.choose, ⋯.choose).2 - G.edgeDensity s t|
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
huniform : ¬P.IsUniform G ε
⊢ ∃ P,
    P.IsEquipartition ∧
      t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i + 1] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(i + 1) ≤ ↑(P.energy G))

Tactic:
replace hP₄ := hP₄.resolve_left huniform

Goal state after:
case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
⊢ ∃ P,
    P.IsEquipartition ∧
      t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i + 1] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(i + 1) ≤ ↑(P.energy G))
Module: Mathlib.Combinatorics.SimpleGraph.Copy

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

Tactic:
by
  constructor
  · rintro ⟨f⟩
    refine ⟨f.toCopy.toSubgraph, f.toCopy.isoToSubgraph, ?_⟩
    simp [Subgraph.IsInduced, Relation.map_apply_apply, f.injective]
  · rintro ⟨H', e, hH'⟩
    exact e.isIndContained.trans hH'.isIndContained

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
w : V
hw : w ≠ t
⊢ (G.replaceVertex s t).Adj s w ↔ G.Adj s w

Tactic:
by simp [replaceVertex, hw]

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
w : V
hw : w ≠ t
⊢ (G.replaceVertex s t).Adj t w ↔ G.Adj s w

Tactic:
by simp [replaceVertex, hw]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.length ≤ 1
hq : q.length ≤ 1
⊢ p = q

Tactic:
grind [cases Walk, length_cons, Adj.ne]

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

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v✝ u' v' w✝ : V
p✝ : G.Walk u v✝
H : SimpleGraph V
s✝ s' : Set V
s : Set (Sym2 V)
v w : V
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∈ G.edgeSet ∧ e ∉ s

Tactic:
exact fun e ep => ⟨edges_subset_edgeSet p ep, hp e ep⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ ⋯ ▸ Hconcat p.reverse.reverse ⋯ (concatRecAux Hnil Hconcat p.reverse) ≍
    Hconcat p h (⋯ ▸ concatRecAux Hnil Hconcat p.reverse)

Tactic:
eqRec_heq_iff

Goal state after:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ Hconcat p.reverse.reverse ⋯ (concatRecAux Hnil Hconcat p.reverse) ≍
    Hconcat p h (⋯ ▸ concatRecAux Hnil Hconcat p.reverse)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case cons.tail
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), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
⊢ List.count u (if hx : u✝ = u then hx ▸ nil else cons h✝ (p✝.takeUntil u ⋯)).support = 1

Tactic:
split_ifs with h' <;> rw [eq_comm] at h' <;> 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), List.count u✝ (p✝.takeUntil u✝ h).support = 1
a✝ : List.Mem u✝ p✝.support
h' : u✝ = u✝
⊢ List.count u✝ (⋯ ▸ nil).support = 1

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), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h'✝ : ¬u✝ = u
h' : ¬u = u✝
⊢ List.count u (cons h✝ (p✝.takeUntil u ⋯)).support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).IsPath
hi : i ≤ (cons h✝ p✝).length
⊢ (cons h✝ p✝).getVert i = u ↔ i = 0

Tactic:
exact hp.getVert_eq_start_iff_of_not_nil not_nil_cons

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ∈ {i | i ≤ q.length}
m : ℕ
hm : m ∈ {i | i ≤ q.length}
hnm : q.getVert n = q.getVert m
⊢ n = m

Tactic:
simp only [Set.mem_ofPred_eq] at hn hm

Goal state after:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
u v : α
hyt : f u ∈ t
hxt : f v ∈ t
hyne : f u ≠ f v
⊢ f v ∈ Set.range ⇑f

Tactic:
exact Set.mem_range_self _

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.tail.support ~ p.dropLast.support

Tactic:
cases p with | nil => rfl | cons h p
  grw [← List.perm_cons u, List.perm_comm, ← List.perm_append_singleton,
    cons_support_tail not_nil_cons, support_dropLast_concat not_nil_cons]

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 : α ↪ β
⊢ (SimpleGraph.map (⇑f) G).IsNClique n t ↔ ∃ s, G.IsNClique n s ∧ map f s = t

Tactic:
rw [isNClique_iff, isClique_map_finset_iff, or_and_right,
    or_iff_right (by rintro ⟨h', rfl⟩; exact h'.not_gt hn)]
  constructor
  · rintro ⟨⟨s, hs, rfl⟩, rfl⟩
    simp [isNClique_iff, hs]
  rintro ⟨s, hs, rfl⟩
  simp [hs.card_eq, hs.isClique]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
k✝ : ℕ
hl : k✝ ≤ p.length
⊢ p.getVert k✝ = ⋯.toWalk.getVert k✝

Tactic:
cases Nat.le_one_iff_eq_zero_or_eq_one.mp (hp.length_eq_one_of_mem_edges h ▸ hl) with
  | inl hl => simp [hl]
  | inr hl =>
    rw [hl, getVert_cons_succ, getVert_zero, ← hp.length_eq_one_of_mem_edges h, getVert_length]

Goal state after: