mathlib-initiative/mathlib-tactics huggingface dataset:
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
key : 16 ^ #P.parts = ↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts))
⊢ ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts) ^ 2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ #P.parts

Tactic:
key

Goal state after:
α : 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
key : 16 ^ #P.parts = ↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts))
⊢ ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
        ↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts))) ^
      2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) /
      ↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts))
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x

Tactic:
by_cases a ∈ s

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h✝ : a ∈ s
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x

case neg
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h✝ : a ∉ s
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case mp
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v

Tactic:
rintro ⟨a, ha⟩
    exact ⟨a, ha⟩

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ (crossProduct ((crossProduct u) v)) w = (u ⬝ᵥ w) • v - (v ⬝ᵥ w) • u

Tactic:
simp_rw [cross_apply, vec3_dotProduct]
  ext i
  fin_cases i <;>
  · simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.reduceFinMk, cons_val,
      Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
    ring

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
hx : x ∈ ↑H
⊢ x * a ∈ A

Tactic:
← smul_eq_mul,

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
hx : x ∈ ↑H
⊢ x •> a ∈ A
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
hx : x ∈ ↑H
⊢ a ∈ x⁻¹ •> A

Tactic:
inv_mem hx

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
hx : x ∈ ↑H
⊢ a ∈ A
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
⊢ ∑ y, ∑ x, lineCount L (x, y).1 = ∑ x, ∑ y, pointCount P (x, y).2

Tactic:
simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]

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
ha : a ∈ A
⊢ 1 ∈ a •> A⁻¹

Tactic:
by simp [← inv_smul_mem_iff, inv_mem_inv ha]

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

Goal state before:
pp: n : ℕ
this : ↑(catalan n) = ↑n.centralBinom / (↑n + 1)
h : n + 1 ∣ n.centralBinom
⊢ catalan n = n.centralBinom / (n + 1)

Tactic:
exact mod_cast this

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
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
⊢ 1 ∈ A⁻¹ <• a

Tactic:
by simp [← inv_smul_mem_iff, inv_mem_inv ha]

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

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∑ u ∈ antidiagonal n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)) =
    ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2

pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
· apply sum_congr rfl
      rintro ⟨i, j⟩ H
      rw [card_map, card_product, ih _ (fst_le H), ih _ (snd_le H)]

Goal state after:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! ^ (c + 1) * (c + 1)! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1)

Tactic:
by
        rw [factorial_succ, pow_succ]; ring

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).bell = ∑ i ≤ n, n.choose i * (n - i).bell

Tactic:
by
  rw [Nat.bell]

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

Goal state before:
pp: case hbc
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := ⋯
H : Subgroup G := ⋯
S_nonempty : S.Nonempty
this✝ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := ⋯
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := ⋯
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
ineq : ↑(#A) * ↑(#A) ≤ ((2 - K) * ↑l + (K - 1) * ↑(#S)) * ↑(#A)
this : 0 < #A
⊢ ↑(#A) ≤ (2 - K) * ↑l + (K - 1) * ↑(#S)

Tactic:
exact le_of_mul_le_mul_right ineq <| by positivity

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

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
⊢ (p + q).insidePart = p.insidePart

Tactic:
insidePart,

Goal state after:
p q : DyckWord
h : p ≠ 0
⊢ (if h : p + q = 0 then 0 else ((p + q).take ((p + q).firstReturn + 1) ⋯).denest ⋯) =
    if h : p = 0 then 0 else (p.take (p.firstReturn + 1) ⋯).denest ⋯
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.nest.insidePart = p

Tactic:
insidePart,

Goal state after:
p : DyckWord
⊢ (if h : p.nest = 0 then 0 else (p.nest.take (p.nest.firstReturn + 1) ⋯).denest ⋯) = p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ p.insidePart.nest + p.outsidePart = p

Tactic:
insidePart,

Goal state after:
p : DyckWord
h : p ≠ 0
⊢ (if h : p = 0 then 0 else (p.take (p.firstReturn + 1) ⋯).denest ⋯).nest + p.outsidePart = p
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
⊢ ∑ z ≥ x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z = ∑ z ≥ x, (mu 𝕜 * zeta 𝕜) x z * f z

Tactic:
by
      simp_rw [mul_apply, sum_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ EqOn H.IsLink G.IsLink E(H)

Tactic:
rintro e he
  ext x y
  exact isLink_iff hHG he

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
x' y' : α
h : G.IsLink e x y
h' : G.IsLink e x' y'
⊢ x = x' ∧ y = y' ∨ x = y' ∧ y = x'

Tactic:
obtain rfl | rfl := h.left_eq_or_eq h'
  · simp [h.right_unique h']
  simp [h'.symm.right_unique h]

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ (G.deleteEdges F₁).deleteEdges F₂ = G.deleteEdges (F₁ ∪ F₂)

Tactic:
simp only [← restrict_edgeSet_sdiff_eq_deleteEdges, sdiff_eq_compl_inter, restrict_inter_edgeSet,
    edgeSet_restrict, restrict_restrict, compl_union]
  rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.induce V(G) = G

Tactic:
refine (Compatible.of_le_le (G := G) (by simp) (by simp)).ext rfl <| Set.ext fun e ↦
    ⟨fun ⟨_, _, h⟩ ↦ h.1.edge_mem, fun h ↦ ?_⟩
  obtain ⟨x, y, h⟩ := exists_isLink_of_mem_edgeSet h
  exact ⟨x, y, h, h.left_mem, h.right_mem⟩

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
⊢ map f G = map g G

Tactic:
refine Graph.ext (by grind) fun _ _ _ ↦ ⟨fun ⟨_, _, hvw, _, _⟩ ↦ ?_, fun ⟨_, _, hvw, _, _⟩ ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
x✝³ : β
x✝² x✝¹ : α'
x✝ : (map f G).IsLink x✝³ x✝² x✝¹
w✝¹ w✝ : α
hvw : G.IsLink x✝³ w✝¹ w✝
left✝ : f w✝¹ = x✝²
right✝ : f w✝ = x✝¹
⊢ (map g G).IsLink x✝³ x✝² x✝¹

case refine_2
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
x✝³ : β
x✝² x✝¹ : α'
x✝ : (map g G).IsLink x✝³ x✝² x✝¹
w✝¹ w✝ : α
hvw : G.IsLink x✝³ w✝¹ w✝
left✝ : g w✝¹ = x✝²
right✝ : g w✝ = x✝¹
⊢ (map f G).IsLink x✝³ x✝² x✝¹
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: case inl
α : Type u_1
H : Hypergraph α
empty : V(H) = ∅ ∧ E(H) = ∅
⊢ H = ⊥ ∨ H.IsNonempty

Tactic:
| inl empty =>

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
inst✝ : M.RankPos
hD : M.Coindep D
⊢ ¬(M.IsBase ∅ ∧ Disjoint ∅ D)

Tactic:
simp [M.empty_not_isBase]

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
hx : x ∈ s
this : ↑(g ⟨x, hx⟩) < #s
⊢ (fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩))
      ((fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s)) x) =
    x

Tactic:
simp [hx, this]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
this : ∀ ⦃K : Set α⦄, Disjoint K J → M.Indep (K ∪ J) → K ⊆ X → I ⊆ K ∪ J → K ⊆ I
⊢ (M ／ J).IsBasis' (I \ J) (X \ J)

Tactic:
simpa +contextual [IsBasis', (hIX.indep.subset hJI).contract_indep_iff,
      subset_sdiff, maximal_subset_iff, disjoint_sdiff_left,
      union_eq_self_of_subset_right hJI, hIX.indep, sdiff_subset.trans hIX.subset,
      sdiff_subset_iff, subset_antisymm_iff, union_comm J]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ ∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN

Tactic:
refine ⟨_, _, hI.1, hI.2.1, h.mono inter_subset_right inter_subset_right, ?_⟩

Goal state after:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ I = I ∩ M.E ∪ I ∩ N.E
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_case₂ : v ∈ pPrev.vertices → v ≠ (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
cases hv' with
    | inl h_in_prefix =>
      by_cases h_eq_end : v = (pPrev.cons e).end
      · exact h_case₁ h_eq_end
      · exact h_case₂ h_in_prefix h_eq_end
    | inr h_eq_end => exact h_case₁ h_eq_end

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case inr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
n : ℕ
hn : n ≠ 0
⊢ schnirelmannDensity A * ↑n ≤ ↑(#({a ∈ Ioc 0 n | a ∈ A}))

Tactic:
exact (le_div_iff₀ (by positivity)).1 (schnirelmannDensity_le_div hn)

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg.inl.inl
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a✝ a : ℕ
left✝ : Sum.inl a✝ ≠ Sum.inl a
hxy : f (Sum.inl a✝) = f (Sum.inl a)
ha : (0 < a✝ ∧ a✝ ≤ n) ∧ a✝ ∈ A
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ n ∈ A + B

Tactic:
first | grind [inr_mem_disjSum] | exact ⟨a, by simp [*], b, by simp [*], by grind⟩

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg.inl.inr
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a b : ℕ
left✝ : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
ha : (0 < a ∧ a ≤ n) ∧ a ∈ A
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ n ∈ A + B

Tactic:
first | grind [inr_mem_disjSum] | exact ⟨a, by simp [*], b, by simp [*], by grind⟩

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg.inr.inl
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b a : ℕ
left✝ : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
ha : (0 < b ∧ b ≤ n) ∧ b ∈ B
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ n ∈ A + B

Tactic:
first | grind [inr_mem_disjSum] | exact ⟨a, by simp [*], b, by simp [*], by grind⟩

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg.inr.inr
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b✝ b : ℕ
left✝ : Sum.inr b✝ ≠ Sum.inr b
hxy : f (Sum.inr b✝) = f (Sum.inr b)
ha : (0 < b✝ ∧ b✝ ≤ n) ∧ b✝ ∈ B
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ n ∈ A + B

Tactic:
first | grind [inr_mem_disjSum] | exact ⟨a, by simp [*], b, by simp [*], by grind⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
a : α
⊢ a ∈ sᶜˢ ↔ aᶜ ∈ s

Tactic:
Iff.comm,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
a : α
⊢ aᶜ ∈ s ↔ a ∈ sᶜˢ
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
a : α
ha : a ∈ ↑({a ∈ s | compress u v a ∉ s})
b : α
hb : b ∈ ↑({a ∈ s | compress u v a ∉ s})
hab : compress u v a = compress u v b
⊢ a = b

Tactic:
rw [mem_coe, mem_filter] at ha hb

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
a : α
ha : a ∈ s ∧ compress u v a ∉ s
b : α
hb : b ∈ s ∧ compress u v b ∉ s
hab : compress u v a = compress u v b
⊢ a = b
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
ha : SupIrred a
⊢ a ≠ ⊥

Tactic:
by rintro rfl; exact not_supIrred_bot ha

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t✝ ≤ #t

Tactic:
exact card_mono hst

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
inst✝ : DecidableEq α
u v : α
s : Finset α
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s

Tactic:
have h : {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = ∅ :=
    filter_false_of_mem fun a ha h ↦ h <| compress_mem_compression_of_mem_compression ha
  rw [compression, filter_image, h, image_empty, ← h]
  exact filter_union_filter_not_eq _ (compression u v s)

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t✝ ≤ #t

Tactic:
exact card_mono hst

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t ≤ #t✝

Tactic:
exact card_mono hst

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t ≤ #t✝

Tactic:
exact card_mono hst

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
n : ℕ
x✝ : n ∈ range (#s + 1)
⊢ ∑ t ∈ powersetCard n s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    ↑((#s).choose n) * (↑(card α) - ↑(#s)) / ((↑(card α) - ↑n) * ↑((card α).choose n))

Tactic:
mul_div_assoc,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
n : ℕ
x✝ : n ∈ range (#s + 1)
⊢ ∑ t ∈ powersetCard n s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    ↑((#s).choose n) * ((↑(card α) - ↑(#s)) / ((↑(card α) - ↑n) * ↑((card α).choose n)))
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s

Tactic:
by_cases hs : s ∈ 𝒜.shadow

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s

case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∉ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case ind.inr.succ.h𝒜₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ 𝒜.Nonempty

Tactic:
exact h𝒜

Goal state after: