mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
pb : IsPullback (𝟙 G.obj) χ'.hom (χ'.hom ≫ (closedSieves J).ι) (closedSieves J).ι
⊢ IsPullback m.hom ((isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F.obj) (χ'.hom ≫ (closedSieves J).ι)
    (Presheaf.truth C)

Tactic:
have : IsPullback m.hom ?_ χ'.hom <| (truth J).hom := by
    simpa using hχ'.map (sheafToPresheaf J _)

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
pb : IsPullback (𝟙 G.obj) χ'.hom (χ'.hom ≫ (closedSieves J).ι) (closedSieves J).ι
this : IsPullback m.hom ((isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F.obj) χ'.hom (truth J).hom
⊢ IsPullback m.hom ((isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F.obj) (χ'.hom ≫ (closedSieves J).ι)
    (Presheaf.truth C)
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
⊢ #s ≤ #t

Tactic:
rw [← mul_one #s, ← mul_one #t]

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
⊢ #s * 1 ≤ #t * 1
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
ha : a ≠ 0
hs : ThreeGPFree (a • s)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * d = c * c
⊢ a • b * a • d = a * c * (a * c)

Tactic:
rw [smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h, mul_mul_mul_comm]

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

Goal state before:
pp: n d : ℕ
a : Fin (n + 1) → ℕ
⊢ (map d) a = a 0 + (∑ x, a x.succ * d ^ ↑x) * d

Tactic:
by
  simp [map, Fin.sum_univ_succ, _root_.pow_succ, ← mul_assoc, ← sum_mul]

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

Goal state before:
pp: case hd
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑⌈√(log ↑N)⌉₊

pp: case hx
N : ℕ
hN : 4096 ≤ N
⊢ 50 / 19 ≤ √(log ↑N)

Tactic:
· rw [cast_pos, lt_ceil, cast_zero, Real.sqrt_pos]
      refine log_pos ?_
      rw [one_lt_cast]
      exact hN.trans_lt' (by norm_num1)

Goal state after:
case hx
N : ℕ
hN : 4096 ≤ N
⊢ 50 / 19 ≤ √(log ↑N)
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
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
hA₀ : 0 < ↑(#A)
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

Tactic:
have hA₀' : (0 : ℚ≥0) < #A' := cast_pos.2 hA'.card_pos

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
hA₀ : 0 < ↑(#A)
hA₀' : 0 < ↑(#A')
⊢ #(A * C) * #A' ≤ #(A' * C) * #A
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: case h
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
a : G
h✝¹ : a ∈ F₁ ^ (m - 1)
b : G
h✝ : b ∈ F₂ ^ (n - 1)
⊢ a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))

Tactic:
exact hf ..

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Defs

Goal state before:
pp: case e'_2.e'_2.e'_2
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
hf' : InjOn (fun x ↦ (f x.1, f x.2)) (s ×ˢ s)
⊢ f x₁ + f y₂ = f x₂ + f y₁ ↔ x₁ + y₂ = x₂ + y₁

Tactic:
· exact hf.add_eq_add hx₁ hy₂ hx₂ hy₁

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

Goal state before:
pp: case h
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
⊢ v ∈ {v | Odd (G.degree v)}

Tactic:
mem_filter_univ

Goal state after:
case h
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
⊢ Odd (G.degree 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
⊢ v ∈ {w | Odd (G.degree w)}

Tactic:
mem_filter_univ

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 (G.degree v)
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #{w | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
hg' : 0 < #{w | w ≠ v ∧ Odd (G.degree w)}
w : V
hw : w ∈ {w | w ≠ v ∧ Odd (G.degree w)}
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Tactic:
mem_filter_univ

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #{w | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
hg' : 0 < #{w | w ≠ v ∧ Odd (G.degree w)}
w : V
hw : w ≠ v ∧ Odd (G.degree w)
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Set α
f : α → ℕ
x✝ : ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
x y : α
hx : x ∈ s
hy : y ∈ s
b : ℕ
hb : ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
⊢ f x ≤ f y + 1

Tactic:
by grw [(hb x hx).2, (hb y hy).1]

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semiring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
s : Set α
hs : s.Subsingleton
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f i ≤ f j + 1

Tactic:
by
  rw [hs hi hj]
  exact le_add_of_nonneg_right zero_le_one

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ G.degree v = 0 ↔ ¬G.degree v ≠ 0

Tactic:
not_ne_iff

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ G.degree v = 0 ↔ G.degree v = 0
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
⊢ ∃ c ∈ P.parts, c ≤ b

Tactic:
by_contra H
  refine Q.ne_bot hb (disjoint_self.1 <| Disjoint.mono_right (Q.le hb) ?_)
  have : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q := by grind [h _]
  have : P.parts.sup id ≤ (Q.parts.erase b).sup id := by grind [Finset.le_sup, Finset.sup_le_iff]
  grw [← P.sup_parts, this]
  exact Q.supIndep (erase_subset _ _) hb (notMem_erase _ _)

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

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
parts : Finset α
hdisjoint : (↑parts).PairwiseDisjoint id
X : Type u_2
inst✝ : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
⊢ ∑ p ∈ (ofPairwiseDisjoint parts hdisjoint).parts, f p = ∑ p ∈ parts, f p

Tactic:
by_cases hbot : ⊥ ∈ parts
  · simp only [Finpartition.ofPairwiseDisjoint]
    rw [← erase_union_eq ⊥ parts hbot, union_comm, sum_union_eq_right]
    · simp
    grind
  · simp_all

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a✝ : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
a : Finset α
ha : a ∈ ↑parts
b : Finset α
hb : b ∈ ↑parts
hab : a ≠ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ id a → a_1 ∉ id b

Tactic:
intro x hx hx'

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a✝ : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
a : Finset α
ha : a ∈ ↑parts
b : Finset α
hb : b ∈ ↑parts
hab : a ≠ b
x : α
hx : x ∈ id a
hx' : x ∈ id b
⊢ False
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts > 0
⊢ #s % #P.parts ≤ #P.parts

Tactic:
· exact (Nat.mod_lt _ h).le

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
ε : 𝕜
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})| < ε

Tactic:
one_mul

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 : ε ≤ ↑(#s')
ht : ε ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity {a} {b})| < ε
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: case refine_1
α : 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₂ - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁)) * edgeDensity r s₂ t₂ ≤
    1 * edgeDensity r s₂ t₂ - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁)) * edgeDensity r s₂ t₂

Tactic:
one_mul

Goal state after:
case refine_1
α : 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₂ - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁)) * edgeDensity r s₂ t₂ ≤
    edgeDensity r s₂ t₂ - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁)) * edgeDensity r s₂ t₂
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : 0 < a
⊢ 0 < m ∧ m ≤ m + 1 ∧ m ≤ a * m + b * (m + 1) ∧ a * m - 1 * m + b * (m + 1) = a * m + b * (m + 1) - m

Tactic:
one_mul

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : 0 < a
⊢ 0 < m ∧ m ≤ m + 1 ∧ m ≤ a * m + b * (m + 1) ∧ a * m - m + b * (m + 1) = a * m + b * (m + 1) - m
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : ¬0 < a
⊢ 0 < m + 1 ∧
    m + 1 ≤ m + 1 ∧ m + 1 ≤ a * m + b * (m + 1) ∧ a * m + (b * (m + 1) - 1 * (m + 1)) = a * m + b * (m + 1) - (m + 1)

Tactic:
one_mul

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : ¬0 < a
⊢ 0 < m + 1 ∧
    m + 1 ≤ m + 1 ∧ m + 1 ≤ a * m + b * (m + 1) ∧ a * m + (b * (m + 1) - (m + 1)) = a * m + b * (m + 1) - (m + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case a
α : 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
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ #P.parts ≤ #A

Tactic:
exact P.card_parts_le_card

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(#P.parts * #P.parts - #P.parts) ≤ 1 * ↑(#P.parts) ^ 2

Tactic:
one_mul

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(#P.parts * #P.parts - #P.parts) ≤ ↑(#P.parts) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case a
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ #P.parts ≤ #A

Tactic:
exact P.card_parts_le_card

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

Goal state before:
pp: case a
α : 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 ≤ #A

Tactic:
exact P.card_parts_le_card

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
h : 0 < a
⊢ #({i ∈ R.parts | #i = m + 1}) = b

Tactic:
rw [hR₃, if_pos h]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G✝ G₁ G₂ G₃ : SimpleGraph V
H✝ : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
G : SimpleGraph V
H : SimpleGraph W
⊢ SimpleGraph V

Tactic:
exact
  if hH : H = ⊥ then G
  else G.deleteEdges <| ⋃ (G' : G.Subgraph) (hG' : Nonempty (H ≃g G'.coe)), {(aux hH hG').some}

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

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝ : V
⊢ x✝ ∈ H.verts ↔ x✝ ∈ (G.singletonSubgraph v).verts

pp: case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ H.Adj x✝¹ x✝ ↔ (G.singletonSubgraph v).Adj x✝¹ x✝

Tactic:
· rw [h, singletonSubgraph_verts]

Goal state after:
case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ H.Adj x✝¹ x✝ ↔ (G.singletonSubgraph v).Adj x✝¹ x✝
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
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #(G.edgeFinset \ G.incidenceFinset t ∪ image (fun x ↦ s(x, t)) (G.neighborFinset s)) =
    #G.edgeFinset + G.degree s - G.degree t

Tactic:
card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image,

Goal state after:
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
⊢ #(G.edgeFinset \ G.incidenceFinset t) + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) =
    #G.edgeFinset + G.degree s - G.degree t
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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 1 ≤ 2 ^ #P.parts * ε ^ 2 / 10

Tactic:
refine (one_le_sq_iff₀ <| by positivity).1 ?_
        rw [div_pow, mul_pow, pow_right_comm, ← pow_mul ε, one_le_div (by positivity)]
        calc
          (↑10 ^ 2) = 100 := by norm_num
          _ ≤ ↑4 ^ #P.parts * ε ^ 5 := hPε
          _ ≤ ↑4 ^ #P.parts * ε ^ 4 := by
            gcongr _ * ?_
            exact pow_le_pow_of_le_one (by sz_positivity) hε₁ (by decide)
          _ = (↑2 ^ 2) ^ #P.parts * ε ^ (2 * 2) := by norm_num

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
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #(G.edgeFinset \ G.incidenceFinset t ∪ image (fun x ↦ s(x, t)) (G.neighborFinset s)) - #{s(t, t)} =
    #G.edgeFinset + G.degree s - G.degree t - 1

Tactic:
card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image,

Goal state after:
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
⊢ #(G.edgeFinset \ G.incidenceFinset t) + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) - #{s(t, t)} =
    #G.edgeFinset + G.degree s - G.degree t - 1
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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
⊢ 1 * ↑(#(G.nonuniformWitness ε U V)) - 2 ^ #P.parts * ↑m / (↑(#U) * ε) * ↑(#(G.nonuniformWitness ε U V)) =
    ↑(#(G.nonuniformWitness ε U V)) - 2 ^ #P.parts * ↑m / (↑(#U) * ε) * ↑(#(G.nonuniformWitness ε U V))

Tactic:
one_mul

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
⊢ ↑(#(G.nonuniformWitness ε U V)) - 2 ^ #P.parts * ↑m / (↑(#U) * ε) * ↑(#(G.nonuniformWitness ε U V)) =
    ↑(#(G.nonuniformWitness ε U V)) - 2 ^ #P.parts * ↑m / (↑(#U) * ε) * ↑(#(G.nonuniformWitness ε U V))
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).coe ≤ G'.coe

Tactic:
by
  intro v w
  simp +contextual

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.support.tail ~ p.support.dropLast

Tactic:
cases p with | nil => rfl | cons h p
  simpa using support_tail_perm_support_dropLast <| p.cons h

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

Goal state before:
pp: α : Type u_1
⊢ ⊥.EdgeDisjointTriangles

Tactic:
by
  simp [EdgeDisjointTriangles]

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

Goal state before:
pp: case pos
α : 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
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : ¬x ≠ y
⊢ completeGraph (Fin n) ⊑ G

Tactic:
not_ne_iff

Goal state after:
case pos
α : 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
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : x = y
⊢ completeGraph (Fin n) ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ Gᶜ.CliqueFree n ↔ G.IndepSetFree n

Tactic:
by
  simp [IndepSetFree, CliqueFree]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ Gᶜ.IndepSetFree n ↔ G.CliqueFree n

Tactic:
by
  simp [IndepSetFree, CliqueFree]

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v : V
⊢ Injective (Path.map f hinj)

Tactic:
rintro ⟨p, hp⟩ ⟨p', hp'⟩ h

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v : V
p : G.Walk u v
hp : p.IsPath
p' : G.Walk u v
hp' : p'.IsPath
h : Path.map f hinj ⟨p, hp⟩ = Path.map f hinj ⟨p', hp'⟩
⊢ ⟨p, hp⟩ = ⟨p', hp'⟩
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
x : α × β × γ
hx : x ∈ t
⊢ (graph t).IsNClique 3 (toTriangle x)

Tactic:
exact toTriangle_is3Clique hx

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

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 ≤ x
⊢ (#A).choose 2 ≤ (#(A.erase 0) + 1).choose 2

Tactic:
by grw [tsub_le_iff_right.1 <| pred_card_le_card_erase]

Goal state after: