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

Goal state before:
pp: case refine_3
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝¹ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this✝ : Mono ((adj.homEquiv Z T.obj₃) h)
this : IsIso ((adj.homEquiv Z T.obj₃) h)
⊢ g ≫ (shiftFunctor C 1).map (𝟙 (G.obj T.obj₁)) =
    (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁

Tactic:
rw [Functor.map_id, comp_id, homEquiv_unit, assoc, ← G.map_comp_assoc, ← h₂,
        Functor.map_comp, Functor.map_comp, assoc, unit_naturality_assoc, assoc,
        Functor.commShiftIso_hom_naturality, ← adj.shift_unit_app_assoc,
        ← Functor.map_comp, right_triangle_components, Functor.map_id, comp_id]

Goal state after:
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
n : EInt
⊢ WithBotTop.rec (motive := fun {x} ↦
      (x ⟶ n) → (WithBotTop.rec 0 t.truncLT (𝟭 C) x ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) n))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
          (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥)) (fun b f ↦ 0) (fun f ↦ 0) n f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec 0 t.truncLT (𝟭 C) (WithBotTop.coe a) ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncLTOfLE a b ⋯) (fun f ↦ t.truncLTι a) n f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤)) n f)
      n (𝟙 n) =
    𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) n)

Tactic:
induction n using WithBotTop.rec <;> simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanIso n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ (map f₂ s).prod = (map f₂ t).prod ↔ s.prod = t.prod

Tactic:
by
    rw [map_congr rfl fun x hx => h.symm (hsA hx), map_congr rfl fun x hx => h.symm (htA hx),
      hf₁.map_prod_eq_map_prod hsA htA hs ht]

Goal state after:
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 t).card = n

Tactic:
by simp [ht]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t
⊢ mulRothNumber s < n

Tactic:
obtain ⟨t, hts, hcard, ht⟩ := mulRothNumber_spec s
  rw [← hcard, ← not_le]
  intro hn
  obtain ⟨u, hut, rfl⟩ := exists_subset_card_eq hn
  exact h _ (mem_powersetCard.2 ⟨hut.trans hts, rfl⟩) (ht.mono hut)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
A : Set α
n : ℕ
β : Type u_5
inst✝ : DivisionCommMonoid β
B₁ B₂ : Set β
f₁ f₂ : α → β
h₁ : IsMulFreimanHom n A B₁ f₁
h₂ : IsMulFreimanHom n A B₂ f₂
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
⊢ (map (f₁ / f₂) s).prod = (map (f₁ / f₂) t).prod

Tactic:
Pi.div_def,

Goal state after:
α : Type u_2
inst✝¹ : CommMonoid α
A : Set α
n : ℕ
β : Type u_5
inst✝ : DivisionCommMonoid β
B₁ B₂ : Set β
f₁ f₂ : α → β
h₁ : IsMulFreimanHom n A B₁ f₁
h₂ : IsMulFreimanHom n A B₂ f₂
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
⊢ (map (fun i ↦ f₁ i / f₂ i) s).prod = (map (fun i ↦ f₁ i / f₂ i) t).prod
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: x : ℝ
hx : 50 / 19 ≤ x
⊢ x + 1 ≤ 1.38 * x

Tactic:
← le_sub_iff_add_le',

Goal state after:
x : ℝ
hx : 50 / 19 ≤ x
⊢ 1 ≤ 1.38 * x - x
Module: Mathlib.Combinatorics.Additive.RuzsaCovering

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
⊢ ∃ F ⊆ A, ↑(#F) ≤ K ∧ A ⊆ F * (B / B)

Tactic:
by
  have : ∀ F, Decidable ((F : Set G).PairwiseDisjoint (· • B)) := fun F ↦ Classical.dec _
  set C := {F ∈ A.powerset | (SetLike.coe F).PairwiseDisjoint (· • B)}
  obtain ⟨F, hFmax⟩ := C.exists_maximal <| filter_nonempty_iff.2
    ⟨∅, empty_mem_powerset _, by simp [coe_empty]⟩
  simp only [C, mem_filter, mem_powerset] at hFmax
  obtain ⟨hFA, hF⟩ := hFmax.1
  refine ⟨F, hFA, le_of_mul_le_mul_right ?_ (by positivity : (0 : ℝ) < #B), fun a ha ↦ ?_⟩
  · calc
      (#F * #B : ℝ) = #(F * B) := by
        rw [card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hF, Nat.cast_mul]
      _ ≤ #(A * B) := by gcongr
      _ ≤ K * #B := hK
  by_cases hau : a ∈ F
  · exact subset_mul_left _ hB.one_mem_div hau
  by_cases! H : ∀ b ∈ F, Disjoint (a • B) (b • B)
  · refine (hFmax.not_gt ?_ <| ssubset_insert hau).elim
    rw [insert_subset_iff, coe_insert]
    exact ⟨⟨ha, hFA⟩, hF.insert fun _ hb _ ↦ H _ hb⟩
  simp_rw [not_disjoint_iff, ← inv_smul_mem_iff] at H
  obtain ⟨b, hb, c, hc₁, hc₂⟩ := H
  exact mem_mul.2 ⟨b, hb, b⁻¹ * a, mem_div.2 ⟨_, hc₂, _, hc₁, by simp⟩, by simp⟩

Goal state after:
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
n : EInt
⊢ WithBotTop.rec (motive := fun {x} ↦
      (x ⟶ n) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 n))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) n f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) n f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) n f)
      n (𝟙 n) =
    𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 n)

Tactic:
induction n using WithBotTop.rec <;> simp

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

Goal state before:
pp: 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
⊢ A ^ 2 ∩ B ^ 2 ⊆ A ^ m ∩ B ^ n

Tactic:
gcongr; exacts [hA.one_mem, hB.one_mem]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e⁻¹ • (e • x.2 * x.1) ⊆ x.1 * x.2

Tactic:
smul_mul_assoc,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e⁻¹ • e • (x.2 * x.1) ⊆ x.1 * x.2
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ∞
⊢ n ≤ minOrder G ↔ ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)

Tactic:
by
  rw [le_minOrder]
  refine ⟨fun h s hs hs' ↦ ?_, fun h a ha ha' ↦ ?_⟩
  · obtain ⟨a, has, ha⟩ := s.bot_or_exists_ne_one.resolve_left hs
    exact
      (h ha <| finite_zpowers.1 <| hs'.subset <| zpowers_le.2 has).trans
        (WithTop.coe_le_coe.2 <| s.orderOf_le_card hs' has)
  · simpa using h (zpowers_ne_bot.2 ha) ha'.finite_zpowers

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : Mul α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ s * {t.min' ht} ∩ ({s.max' hs} * t), x = s.max' hs * t.min' ht

Tactic:
simp only [mem_inter, and_imp, mem_mul, mem_singleton, exists_eq_left,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mul_left_inj]

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : Mul α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ a ∈ s, ∀ x ∈ t, s.max' hs * x = a * t.min' ht → a = s.max' hs
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ ⊥.nonUniforms G ε = ∅

Tactic:
rw [eq_empty_iff_forall_notMem]

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ ∀ (x : Finset α × Finset α), x ∉ ⊥.nonUniforms G ε
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Disjoint H H' → Disjoint H.verts H'.verts

Tactic:
intro hdisj S h₀ h₁ v hvS

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
v : V
hvS : v ∈ S
⊢ v ∈ ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
⊢ Set.range toSubgraph = {B' | Nonempty (A ≃g B'.coe)}

Tactic:
ext H'

Goal state after:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
⊢ H' ∈ Set.range toSubgraph ↔ H' ∈ {B' | Nonempty (A ≃g B'.coe)}
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
⊢ Subgraph.comap f ⊤ = ⊤

Tactic:
ext <;> simp +contextual [f.map_adj]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ G'.induce s ≤ G'.induce (s ∪ s')

Tactic:
by
  exact (sup_le_iff.mp le_induce_union).1

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
d : G.Dart
v w : V
h : d.toProd.2 = v
p : G.Walk v w
⊢ List.IsChain G.DartAdj (d :: p.darts)

Tactic:
by
  induction p generalizing d with
  | nil => exact .singleton _
  | cons h' p ih => exact .cons_cons h (ih rfl)

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.deleteEdges s).edgeSet

Tactic:
simp only [edgeSet_deleteEdges, Set.mem_sdiff]

Goal state after:
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
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
x u✝ : V
q : G.Walk u✝ w
hx : x ∈ nil.support
⊢ (nil.append q).takeUntil x ⋯ = nil.takeUntil x hx

Tactic:
rw [mem_support_nil_iff] at hx

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
x u✝ : V
q : G.Walk u✝ w
hx✝ : x ∈ nil.support
hx : x = u✝
⊢ (nil.append q).takeUntil x ⋯ = nil.takeUntil x hx✝
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
h : p.IsCycle
hn : 0 < n
⊢ (p.drop n).IsPath

Tactic:
by
  replace h : (p.drop 1).IsPath := h.isPath_tail
  rw [← Nat.add_sub_of_le hn, drop_add_eq]
  simp [h.drop (n - 1), -drop_drop]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
f : α ↪ β
inst✝ : Nonempty α
⊢ (SimpleGraph.map (⇑f) G).CliqueFree n ↔ G.CliqueFree n

Tactic:
by
  obtain (hle | hlt) := le_or_gt n 1
  · obtain (rfl | rfl) := Nat.le_one_iff_eq_zero_or_eq_one.1 hle
    · simp [CliqueFree]
    simp [CliqueFree, show ∃ (_ : β), True from ⟨f (Classical.arbitrary _), trivial⟩]
  simp [CliqueFree, isNClique_map_iff hlt]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ∑ x ∈ G.badVertices ε s t, ↑(#({y ∈ t | G.Adj x y})) ≤ #(G.badVertices ε s t) • ↑(#t) * (↑(G.edgeDensity s t) - ε)

Tactic:
smul_mul_assoc,

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ∑ x ∈ G.badVertices ε s t, ↑(#({y ∈ t | G.Adj x y})) ≤ #(G.badVertices ε s t) • (↑(#t) * (↑(G.edgeDensity s t) - ε))
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
⊢ False

Tactic:
have hε₁ : ε ≤ 1 := by
    have := hAε.trans (Nat.cast_le.2 A.card_le_univ)
    simp only [sq, Nat.cast_mul, Fintype.card_prod] at this
    rwa [mul_le_iff_le_one_left] at this
    positivity

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
⊢ False
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∉ t
hau : a ∈ u
⊢ a ∈ s'.mulSpan

Tactic:
have : a = (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b := by
      rw [prod_erase_eq_div hau, htu.2.2, div_div_self']
    rw [this]
    exact prod_div_prod_mem_mulSpan ht (subset_insert_iff.1 hu)

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s : Finset α
⊢ Eₘ[s, univ] = Fintype.card α * #s ^ 2

Tactic:
by
  rw [mulEnergy_comm, mulEnergy_univ_left]

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
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
insert_subset : insert 0 A ⊆ (insert a A).subsetSum
vadd_subset : a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum
⊢ #(insert 0 A ∪ (a +ᵥ A.subsetSum)) ≤ #(insert a A).subsetSum

Tactic:
by grw [union_subset insert_subset vadd_subset]

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Tactic:
by_cases hf : Infinite { p : P // p ∈ l }
  · simp [pointCount]
  have := fintypeOfNotInfinite hf
  cases nonempty_fintype { l : L // p ∈ l }
  rw [lineCount, pointCount, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
  have : ∀ p' : { p // p ∈ l }, p ≠ p' := fun p' hp' => h ((congr_arg (· ∈ l) hp').mpr p'.2)
  exact
    Fintype.card_le_of_injective (fun p' => ⟨mkLine (this p'), (mkLine_ax (this p')).1⟩)
      fun p₁ p₂ hp =>
      Subtype.ext ((eq_or_eq p₁.2 p₂.2 (mkLine_ax (this p₁)).2
            ((congr_arg (_ ∈ ·) (Subtype.ext_iff.mp hp)).mpr (mkLine_ax (this p₂)).2)).resolve_right
          fun h' => (congr_arg (p ∉ ·) h').mp h (mkLine_ax (this p₁)).1)

Goal state after:
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
⊢ some (f x) ≠ (Equiv.swap none (some a)) (some x)

Tactic:
rw [swap_apply_of_ne_of_ne ne_1 ne_2, (Option.some_injective α).ne_iff]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
⊢ f x ≠ x
Module: Mathlib.Combinatorics.Digraph.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
⊢ Bijective ⇑Digraph.mk'

Tactic:
refine ⟨Embedding.injective _, ?_⟩
    intro G
    use fun v w ↦ G.Adj v w
    ext v w
    simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: ⊢ catalan 1 = 1

Tactic:
simp [catalan_succ]

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
hAB : Fintype.card (Fin (Nat.succ 0).succ) + B.rank ≤ Fintype.card (Fin 3)
⊢ False

Tactic:
h.2.rank_matrix,

Goal state after:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
hAB : Fintype.card (Fin (Nat.succ 0).succ) + Fintype.card (Fin (Nat.succ 0).succ) ≤ Fintype.card (Fin 3)
⊢ False
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ a •> ((A⁻¹ * A) <• a) = (a •> (A⁻¹ * A) * (A⁻¹ * A)) <• a

Tactic:
smul_mul_assoc,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A * (A⁻¹ * A)) <• a
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i, (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i) = ↑d.succ.centralBinom / (↑d.succ + 1)

Tactic:
rw [← sum_range fun i => gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i,
            sum_range_sub, Nat.succ_eq_add_one]
        rw [gosper_catalan_sub_eq_central_binom_div d]
        norm_cast

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
⊢ l ∪ r ⊆ a •> (A⁻¹ * A)

Tactic:
rw [union_subset_iff, hl]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
⊢ A ⊆ a •> (A⁻¹ * A) ∧ r ⊆ a •> (A⁻¹ * A)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ 0 + p = p

Tactic:
ext1; rfl

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ A⁻¹ * (A⁻¹ * A) <• a ⊆ A⁻¹ * (A⁻¹ * A * A)

Tactic:
by grw [op_smul_finset_subset_mul (by simpa)]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: n : ℕ
x : (i : Fin n.succ) × { p // ↑i + 1 ∈ p.parts }
⊢ ↑x.fst + 1 ∈ (↑x.snd).parts.toFinset

Tactic:
simpa using x.2.2

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false

Tactic:
cons_append,

Goal state after:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (List.take (j + 1) (U :: (↑p ++ [D]))) = count D (List.take (j + 1) (U :: (↑p ++ [D])))) = false
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ x_1 ∈ (Ici x).sigma fun y ↦ Ici y, (mu 𝕜) x x_1.fst * (zeta 𝕜) x_1.fst x_1.snd * f x_1.snd =
    ∑ z ≥ x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z

Tactic:
rw [sum_sigma' (Ici x) fun z ↦ Icc x z]

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ x_1 ∈ (Ici x).sigma fun y ↦ Ici y, (mu 𝕜) x x_1.fst * (zeta 𝕜) x_1.fst x_1.snd * f x_1.snd =
    ∑ x_1 ∈ (Ici x).sigma fun z ↦ Icc x z, (mu 𝕜) x x_1.snd * (zeta 𝕜) x_1.snd x_1.fst * f x_1.fst
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x y : α × β
a✝ : x ≤ y
⊢ (IncidenceAlgebra.prod 1 1) x y = 1 x y

Tactic:
simp [Prod.ext_iff, ← ite_and, and_comm]

Goal state after: