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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
b c d : α
hcd : c ∈ t ∧ d ∈ t
⊢ ((f (b, c, d)).2.1 ∈ t ∧ (f (b, c, d)).2.2 ∈ t) ∧
    (f (b, c, d)).1.1 * (f (b, c, d)).2.1 = (f (b, c, d)).1.2 * (f (b, c, d)).2.2

Tactic:
simpa [f, mul_right_comm]

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

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ ↑(#A) = ↑(#(image (fun x ↦ ↑x) A))

Tactic:
card_image_of_injOn

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ ↑(#A) = ↑(#A)

n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ Set.InjOn (fun x ↦ ↑x) ↑A
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: x : BinaryTree Unit
n : ℕ
⊢ x ∈ treesOfNumNodesEq n ↔ x.numNodes = n

Tactic:
induction x using BinaryTree.unitRecOn generalizing n

Goal state after:
case base
n : ℕ
⊢ nil ∈ treesOfNumNodesEq n ↔ nil.numNodes = n

case ind
x✝ y✝ : BinaryTree Unit
a✝¹ : ∀ {n : ℕ}, x✝ ∈ treesOfNumNodesEq n ↔ x✝.numNodes = n
a✝ : ∀ {n : ℕ}, y✝ ∈ treesOfNumNodesEq n ↔ y✝.numNodes = n
n : ℕ
⊢ node () x✝ y✝ ∈ treesOfNumNodesEq n ↔ (node () x✝ y✝).numNodes = n
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ≠ 0

Tactic:
← Nat.pos_iff_ne_zero

Goal state after:
m : Multiset ℕ
⊢ 0 < (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : n ≤ m
a✝ : Nontrivial R
⊢ ↑n < (X ^ ((i + 1) * (m + 1))).order

Tactic:
rw [order_X_pow]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : n ≤ m
a✝ : Nontrivial R
⊢ ↑n < ↑((i + 1) * (m + 1))
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
⊢ ∑ y ≥ x, (mu 𝕜) x y * g y = ∑ y ≥ x, (mu 𝕜) x y * ∑ z ≥ y, f z

Tactic:
by simp_rw [h]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
⊢ ↑(#(A * S)) - K * ↑(#A) ≤ (2 - ε) * ↑(#S) - (1 - ε / 2) * ↑(#S)

Tactic:
gcongr; linarith

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
⊢ ∃ a, FP a ⊆ s₀

Tactic:
by
  /- Informally: given a `U`-large set `s₀`, the set `s₀ ∩ { m | ∀ᶠ m' in U, m * m' ∈ s₀ }` is also
  `U`-large (since `U` is idempotent). Thus in particular there is an `a₀` in this intersection. Now
  let `s₁` be the intersection `s₀ ∩ { m | a₀ * m ∈ s₀ }`. By choice of `a₀`, this is again
  `U`-large, so we can repeat the argument starting from `s₁`, obtaining `a₁`, `s₂`, etc.
  This gives the desired infinite sequence. -/
  have exists_elem : ∀ {s : Set M} (_hs : s ∈ U), (s ∩ { m | ∀ᶠ m' in U, m * m' ∈ s }).Nonempty :=
    fun {s} hs => Ultrafilter.nonempty_of_mem (inter_mem hs <| by rwa [← U_idem] at hs)
  let elem : { s // s ∈ U } → M := fun p => (exists_elem p.property).some
  let succ : {s // s ∈ U} → {s // s ∈ U} := fun (p : {s // s ∈ U}) =>
        ⟨p.val ∩ {m : M | elem p * m ∈ p.val},
         inter_mem p.property
           (show (exists_elem p.property).some ∈ {m : M | ∀ᶠ (m' : M) in ↑U, m * m' ∈ p.val} from
              p.val.inter_subset_right (exists_elem p.property).some_mem)⟩
  use Stream'.corec elem succ (Subtype.mk s₀ sU)
  suffices ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ p, a = Stream'.corec elem succ p → m ∈ p.val by
    intro m hm
    exact this _ m hm ⟨s₀, sU⟩ rfl
  clear sU s₀
  intro a m h
  induction h with
  | head' b =>
    rintro p rfl
    rw [Stream'.corec_eq, Stream'.head_cons]
    exact Set.inter_subset_left (Set.Nonempty.some_mem _)
  | tail' b n h ih =>
    rintro p rfl
    refine Set.inter_subset_left (ih (succ p) ?_)
    rw [Stream'.corec_eq, Stream'.tail_cons]
  | cons' b n h ih =>
    rintro p rfl
    have := Set.inter_subset_right (ih (succ p) ?_)
    · simpa only using! this
    rw [Stream'.corec_eq, Stream'.tail_cons]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
⊢ (Disjoint J (X \ I) ∧ Disjoint J I) ∧ M.Indep (J ∪ I) ↔ M.Indep (J ∪ I) ∧ Disjoint X J

Tactic:
← disjoint_union_right,

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
⊢ Disjoint J (X \ I ∪ I) ∧ M.Indep (J ∪ I) ↔ M.Indep (J ∪ I) ∧ Disjoint X J
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
⊢ (Disjoint D (X \ I) ∧ Disjoint D I) ∧ M.Dep (D ∪ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D

Tactic:
← disjoint_union_right,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
⊢ Disjoint D (X \ I ∪ I) ∧ M.Dep (D ∪ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : f = 0
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
refine ⟨0, 0, by simp [hf0], ?_, by simp⟩

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : f = 0
⊢ ∀ (i : ι), m.toSyn (m.degree (b i * 0 i)) ≤ m.toSyn (m.degree f)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : f = 0
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
refine ⟨0, 0, by simp [hf0], ?_, by simp⟩
    intro b
    simp only [Finsupp.coe_zero, Pi.zero_apply, mul_zero, degree_zero, map_zero]
    exact bot_le

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.left
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ f =
    (Finsupp.linearCombination (MvPolynomial σ R) b)
        (g' + Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) +
      r'

pp: case h.right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ (∀ (i_1 : ι),
      m.toSyn
          (m.degree
            (b i_1 *
              (g' + Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) i_1)) ≤
        m.toSyn (m.degree f)) ∧
    ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
· rw [map_add, add_assoc, add_comm _ r', ← add_assoc, ← H'.1]
      simp [reduce]

Goal state after:
case h.right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ (∀ (i_1 : ι),
      m.toSyn
          (m.degree
            (b i_1 *
              (g' + Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) i_1)) ≤
        m.toSyn (m.degree f)) ∧
    ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h_empty
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval : ∀ (x : PEmpty.{u_2 + 1} → R), (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) → (eval x) P = 0
⊢ P = 0

Tactic:
suffices P = C (constantCoeff P) by
      specialize Heval default (fun i ↦ PEmpty.elim i)
      rw [this, eval_C] at Heval
      rw [this, Heval, C_0]

Goal state after:
case h_empty
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval : ∀ (x : PEmpty.{u_2 + 1} → R), (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) → (eval x) P = 0
⊢ P = C (constantCoeff P)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
⊢ (M ／ C).Spanning X ↔ M.Spanning (X ∪ C) ∧ Disjoint X C

Tactic:
rw [spanning_iff, contract_closure_eq, contract_ground, spanning_iff, union_subset_iff,
    subset_sdiff, ← and_assoc, and_congr_left_iff, and_comm (a := X ⊆ _), ← and_assoc,
    and_congr_left_iff]
  refine fun hdj hX ↦ ⟨fun h ↦ ⟨?_, hC⟩, fun h ↦ by simp [h]⟩
  rwa [← union_sdiff_cancel (M.subset_closure_of_subset' subset_union_right hC), h,
    union_sdiff_cancel]

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • (f ![a, b] + f ![b, a])
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ False

Tactic:
← mcfab.left,

Goal state after:
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • (f ![a, b] + f ![a, b])
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ False
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ b
p : Path r a
h : shortestPath r b = p.cons e
⊢ (shortestPath r a).length < p.length + 1

Tactic:
Nat.lt_succ_iff

Goal state after:
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ b
p : Path r a
h : shortestPath r b = p.cons e
⊢ (shortestPath r a).length ≤ p.length
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ p.vertices.head? = some a

Tactic:
induction p with
  | nil => simp only [vertices_nil, head?_cons]
  | cons p' e ih => simp [ih]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : v ⟶ u
⊢ (⇑(symmetrifyCostar (φ.obj u)) ∘ φ.symmetrify.costar u) ⟨v, Sum.inl f⟩ =
    (Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)) ⟨v, Sum.inl f⟩

Tactic:
simp only [Quiver.symmetrifyCostar, Function.comp_apply]

Goal state after:
case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : v ⟶ u
⊢ (Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj (φ.obj u)) (Hom (Symmetrify.of.obj (φ.obj u))))
      (φ.symmetrify.costar u ⟨v, Sum.inl f⟩) =
    Sum.map (φ.costar u) (φ.star u)
      ((Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj u) (Hom (Symmetrify.of.obj u))) ⟨v, Sum.inl f⟩)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : u ⟶ v
⊢ (⇑(symmetrifyCostar (φ.obj u)) ∘ φ.symmetrify.costar u) ⟨v, Sum.inr g⟩ =
    (Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)) ⟨v, Sum.inr g⟩

Tactic:
simp only [Quiver.symmetrifyCostar, Function.comp_apply]

Goal state after:
case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : u ⟶ v
⊢ (Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj (φ.obj u)) (Hom (Symmetrify.of.obj (φ.obj u))))
      (φ.symmetrify.costar u ⟨v, Sum.inr g⟩) =
    Sum.map (φ.costar u) (φ.star u)
      ((Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj u) (Hom (Symmetrify.of.obj u))) ⟨v, Sum.inr g⟩)
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(image (fun s ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s})) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜

Tactic:
card_image_of_injOn

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜

α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Set.InjOn (fun s ↦ s.erase a) ↑({s ∈ 𝒜 | a ∈ s})
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ s.erase a ∈ 𝓓 a 𝒜

Tactic:
simp_rw [mem_compression, erase_idem, and_self_iff]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ↑(#({a ∈ Ioc 0 m | a ∈ {n | n % m = 1}})) / ↑m ≤ (↑m)⁻¹

Tactic:
rw [← one_div, ← @Nat.cast_one ℝ]
    gcongr
    simp only [Set.mem_ofPred_eq, card_le_one_iff_subset_singleton, subset_iff,
      mem_filter, mem_Ioc, mem_singleton, and_imp]
    use 1
    intro x _ hxm h
    rcases eq_or_lt_of_le hxm with rfl | hxm'
    · simp at h
    rwa [Nat.mod_eq_of_lt hxm'] at h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
⊢ ↑(card α) * ∑ i ∈ range (card α + 1), ↑((card α).choose i) / ((↑(card α) - ↑i) * ↑((card α).choose i)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
← mul_inv_cancel₀ (cast_ne_zero.mpr card_ne_zero : (card α : ℚ) ≠ 0),

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
⊢ ↑(card α) * ∑ i ∈ range (card α + 1), ↑((card α).choose i) / ((↑(card α) - ↑i) * ↑((card α).choose i)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + ↑(card α) * (↑(card α))⁻¹
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : compress u v b ∉ s
⊢ (compress u v b ⊔ u) \ v ∈ s

Tactic:
have hu : u = ⊥ := by
    suffices Disjoint u (u \ v) by rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this
    refine hua.mono_right ?_
    rw [← compress_idem, compress_of_disjoint_of_le hua hva]
    exact sdiff_le_sdiff_right le_sup_right

Goal state after:
case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : compress u v b ∉ s
hu : u = ⊥
⊢ (compress u v b ⊔ u) \ v ∈ s
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
⊢ ∑ j ∈ range (#s + 1), ∑ t ∈ powersetCard j s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    ∑ i ∈ range (#s + 1), ↑((#s).choose i) * (↑(card α) - ↑(#s)) / ((↑(card α) - ↑i) * ↑((card α).choose i))

Tactic:
refine sum_congr rfl fun n _ ↦ ?_

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.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
⊢ False

Tactic:
have hAB' : #A = #B := (h₁ hA).trans sizeA.symm

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
⊢ False
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
u : Finset α
hu : u ∈ nonMemberSubfamily a 𝒜
hsu : s ∩ u = t.erase a
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
rw [mem_nonMemberSubfamily] at hu

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
u : Finset α
hu : u ∈ 𝒜 ∧ a ∉ u
hsu : s ∩ u = t.erase a
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
⊢ 𝒜.Shatters s

Tactic:
intro t ht
  obtain ⟨u, hu, rfl⟩ := hs ht
  rw [Down.mem_compression] at hu
  obtain hu | hu := hu
  · exact ⟨u, hu.1, rfl⟩
  by_cases ha : a ∈ s
  · obtain ⟨v, hv, hsv⟩ := hs <| insert_subset ha ht
    rw [Down.mem_compression] at hv
    obtain hv | hv := hv
    · refine ⟨erase v a, hv.2, ?_⟩
      rw [inter_erase, hsv, erase_insert]
      rintro ha
      rw [insert_eq_self.2 (mem_inter.1 ha).2] at hu
      exact hu.1 hu.2
    rw [insert_eq_self.2 <| inter_subset_right (s₁ := s) ?_] at hv
    cases hv.1 hv.2
    rw [hsv]
    exact mem_insert_self _ _
  · refine ⟨insert a u, hu.2, ?_⟩
    rw [inter_insert_of_notMem ha]

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c
c : Set α
z : α
hz : c = {x | r x z}
hx : x ∈ c
hy : y ∈ c
⊢ r x y

Tactic:
subst c
    exact r.trans' hx (r.symm' hy)

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
⊢ (∃ v, ∀ (w : V), G.Reachable v w) → G.Preconnected ∧ Nonempty V

Tactic:
· rintro ⟨v, h⟩
    exact ⟨fun u w => (h u).symm.trans (h w), ⟨v⟩⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
h : ∀ (x : V), G.Reachable x v ↔ G.Reachable x w
⊢ G.Reachable v w

Tactic:
rw [reachable_comm, h]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
h' : m < Nat.succ 0
⊢ False

Tactic:
obtain ⟨i, hi⟩ := hm.some (Classical.arbitrary V)

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
h' : m < Nat.succ 0
i : ℕ
hi : i < m
⊢ False