mathlib-initiative/mathlib-tactics huggingface dataset:
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 ↑A
⊢ ↑A = (fun x ↦ ↑↑x) '' ↑A

Tactic:
Set.image_congr,

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree ↑A
⊢ ↑A = ?m.72 '' ↑A

n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree ↑A
⊢ ∀ a ∈ ↑A, ↑↑a = ?m.72 a

n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree ↑A
⊢ ℕ → ℕ
Module: Mathlib.Combinatorics.Additive.SubsetSum

Goal state before:
pp: case insert
M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A✝ : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : M
A : Finset M
A_lt_a : ∀ x ∈ A, x < a
ih : (∀ x ∈ A, 0 < x) → (#A + 1).choose 2 < #A.subsetSum
A_pos : ∀ x ∈ insert a A, 0 < x
A_pos' : ∀ x ∈ A, 0 < x
⊢ (#(insert a A) + 1).choose 2 < #(insert a A).subsetSum

Tactic:
grw [card_insert_of_notMem fun ha => (A_lt_a a ha).false, Nat.choose_succ_left _ _ (by lia),
      Nat.choose_one_right, add_right_comm, add_assoc, Nat.add_one_le_iff.2 (ih A_pos')]

Goal state after:
case insert
M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A✝ : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : M
A : Finset M
A_lt_a : ∀ x ∈ A, x < a
ih : (∀ x ∈ A, 0 < x) → (#A + 1).choose 2 < #A.subsetSum
A_pos : ∀ x ∈ insert a A, 0 < x
A_pos' : ∀ x ∈ A, 0 < x
⊢ #A + #A.subsetSum < #(insert a A).subsetSum
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: k : ℕ
⊢ (2 ^ k).bitIndices = [k]

Tactic:
← mul_one (a := 2 ^ k),

Goal state after:
k : ℕ
⊢ (2 ^ k * 1).bitIndices = [k]
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case bit.false
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i
⊢ (map (fun i ↦ 2 ^ i) (bit false n).bitIndices).sum = bit false n

Tactic:
simpa [hrw, List.sum_map_mul_left]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
⊢ v.cross w = w.cross v

Tactic:
rcases eq_or_ne v w with rfl | h

Goal state after:
case inl
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : ℙ F (Fin 3 → F)
⊢ v.cross v = v.cross v

case inr
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ v.cross w = w.cross v
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ (mk F ((crossProduct v) w) ⋯).orthogonal (mk F v hv)

Tactic:
orthogonal_mk,

Goal state after:
case h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ (crossProduct v) w ⬝ᵥ v = 0
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
hst : ∃ a ∈ ofColex t, a ∉ ofColex s ∧ ∀ b ∈ ofColex s, b ∉ ofColex t → b < a
⊢ (fun s ↦ ∑ k ∈ ofColex s, n ^ k) s < (fun s ↦ ∑ k ∈ ofColex s, n ^ k) t

Tactic:
obtain ⟨a, hat, has, ha⟩ := hst

Goal state after:
n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
a : ℕ
hat : a ∈ ofColex t
has : a ∉ ofColex s
ha : ∀ b ∈ ofColex s, b ∉ ofColex t → b < a
⊢ (fun s ↦ ∑ k ∈ ofColex s, n ^ k) s < (fun s ↦ ∑ k ∈ ofColex s, n ^ k) t
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) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
a : G
ha : a ∈ A
⊢ A * A = A <• a

Tactic:
A_smul ha

Goal state after:
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
a : G
ha : a ∈ A
⊢ A * A = A * A
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ Perm.decomposeOption (Perm.decomposeOption.symm (some a, f)) = (some a, f)

Tactic:
rw [apply_symm_apply]

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)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ #(A⁻¹ * A) < 2 * #A

Tactic:
have : ((1 / 2 : ℚ) * #A) * #(A⁻¹ * A) < (#A : ℚ) ^ 2 := by
    rw [← Nat.cast_pow, sq, ← card_product, card_eq_sum_card_fiberwise h₂, Nat.cast_sum]
    refine (sum_lt_sum_of_nonempty (by simp [h₀]) h₁).trans_eq' ?_
    simp only [sum_const, nsmul_eq_mul, mul_comm]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
this : 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#A) ^ 2
⊢ #(A⁻¹ * A) < 2 * #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
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ ↑A ⊆ a •> (↑A⁻¹ * ↑A)

Tactic:
exact_mod_cast A_subset_aH a ha

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs✝ : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
⊢ ∀ i ∈ univ,
    (Multiset.toFinsupp i.parts).prod f =
      ∏ i_1 ∈ Finset.map (addRightEmbedding 1) s,
        (coeff (i.toFinsuppAntidiag i_1)) (1 + ∑' (j : ℕ), f i_1 (j + 1) • X ^ (i_1 * (j + 1)))

Tactic:
· exact fun p _ ↦ aux_prod_f_eq_prod_coeff f p hs (by simp)

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

Goal state before:
pp: case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ 2 * (i + 1).smallSchroder * (n + 1 - i).largeSchroder = 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

pp: case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ i ≠ 0

Tactic:
← two_mul_smallSchroder_succ

Goal state after:
case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ 2 * (i + 1).smallSchroder * (2 * (n + 1 - i + 1).smallSchroder) =
    2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ n + 1 - i ≠ 0

case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ i ≠ 0
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case cardH
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)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ ↑(Fintype.card ↥H) ≤ (2 / ε - 1) * ↑(#S)

pp: case cardZ
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)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ ↑(#Z) ≤ 2 / ε - 1

Tactic:
case cardH =>
    rw [← mul_le_mul_iff_right₀ (a := ε / 2) (by positivity)]
    calc
            ε / 2 * (Fintype.card H)
        _ = ε / 2 * #(H : Set G).toFinset   := by
          simp only [Set.toFinset_card, SetLike.coe_sort_coe]
        _ = (1 - K) * #(H : Set G).toFinset := by ring
        _ ≤ ex (Set.toFinset H)             := mul_card_le_expansion hS
        _ ≤ (1 - ε / 2) * #S                := calc₁
        _ = ε / 2 * ((2 / ε - 1) * #S)      := by field

Goal state after:
case cardZ
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)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ ↑(#Z) ≤ 2 / ε - 1
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case calc_1
n : ℕ
⊢ (↑n + 3) / 3 ≤ 2 * ↑(n / 6) + 1 + 2

Tactic:
rw [← div_add_one (three_ne_zero' ℝ), ← le_sub_iff_add_le, div_le_iff₀ (zero_lt_three' ℝ),
        add_assoc, add_sub_assoc, add_mul, mul_right_comm, add_sub_cancel_left]

Goal state after:
case calc_1
n : ℕ
⊢ ↑n ≤ 2 * 3 * ↑(n / 6) + 2 * 3
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
hx : G.Inc e x
hy : G.Inc e y
hz : G.Inc e z
⊢ x = y ∨ x = z ∨ y = z

Tactic:
by_contra! ⟨hxy, hxz, hyz⟩

Goal state after:
α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
hx : G.Inc e x
hy : G.Inc e y
hz : G.Inc e z
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
⊢ False
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι' → α') → κ
⊢ IsMono C (l.reindex eη eα eι) ↔ IsMono (fun x ↦ C (⇑eα ∘ x ∘ ⇑eι.symm)) l

Tactic:
simp only [IsMono, funext (reindex_apply _ _ _ _ _), coe_apply]
  exact exists_congr fun c ↦ (eη.arrowCongr eα).symm.forall_congr <| by aesop

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case refine_2.htd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ ∀ (i : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (i + 1) a)} ⊆ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}

pp: case htn
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ ∀ (i : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}.Nonempty

pp: case refine_2.ht0
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ IsCompact {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop 0 a)}

pp: case refine_2.htcl
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ ∀ (i : ℕ), IsClosed {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}

Tactic:
· intro n U hU
      filter_upwards [hU]
      rw [← Stream'.drop_drop, ← Stream'.tail_eq_drop]
      exact FP.tail _

Goal state after:
case htn
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ ∀ (i : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}.Nonempty

case refine_2.ht0
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ IsCompact {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop 0 a)}

case refine_2.htcl
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ ∀ (i : ℕ), IsClosed {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

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

Tactic:
and_iff_left_iff_imp,

Goal state after:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis' I (X \ D) → Disjoint (X \ D ∩ M.E) D
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X ∩ (M.E \ D)) ∩ (M.E \ D) ∪ ∅ = M.closure (X \ D) \ D

Tactic:
union_empty,

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X ∩ (M.E \ D)) ∩ (M.E \ D) = M.closure (X \ D) \ D
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ M ／ C = M ↔ Disjoint C M.E

Tactic:
rw [← dual_delete_dual, ← dual_inj, dual_dual, delete_eq_self_iff, dual_ground]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
⊢ (M ／ C).IsCocircuit K ↔ M.IsCocircuit K ∧ Disjoint K C

Tactic:
rw [isCocircuit_def, dual_contract, delete_isCircuit_iff]

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 • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum < (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum

Tactic:
apply Multiset.sum_lt_sum

Goal state after:
case hle
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 • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ ∀ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] ≤ f i

case hlt
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 • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: case mp
V : Type u_2
inst✝ : Quiver V
v : V
h_singleton : ∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v
w : V
hw_ne : w ≠ v
hab : Nonempty (Path v w)
hba : Nonempty (Path w v)
⊢ False

Tactic:
have h_same_scc : (w : StronglyConnectedComponent V) = v :=
      stronglyConnectedComponent_eq_of_path (a := w) (b := v) hba hab

Goal state after:
case mp
V : Type u_2
inst✝ : Quiver V
v : V
h_singleton : ∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v
w : V
hw_ne : w ≠ v
hab : Nonempty (Path v w)
hba : Nonempty (Path w v)
h_same_scc : StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v
⊢ False
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∉ s
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a

Tactic:
· exact Or.inl ⟨by rwa [insert_erase ha], notMem_erase _ _⟩

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

Goal state before:
pp: case neg
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
⊢ n ∈ A + B

Tactic:
by_cases hnB : n ∈ B

Goal state after:
case pos
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
⊢ n ∈ A + B

case neg
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
⊢ n ∈ A + B
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ s ○ t ○ (u ○ v) = s ○ u ○ (t ○ v)

Tactic:
simp_rw [← disjSups_assoc, disjSups_right_comm]

Goal state after:
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 ∈ 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

Tactic:
compress

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
a : α
ha : a ∈ s ∧ (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ∉ s
b : α
hb : b ∈ s ∧ compress u v b ∉ s
hab : (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) = compress u v b
⊢ a = b
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
a b : α
hb : b ∈ s ∧ compress u v b ∉ s
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s
hab : (a ⊔ u) \ v = compress u v b
⊢ a = b

Tactic:
compress

Goal state after:
case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
a b : α
hb : b ∈ s ∧ (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) ∉ s
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s
hab : (a ⊔ u) \ v = if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b
⊢ a = b
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
u : Finset α
hau : a ∉ u
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ u_1, #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
hut : insert a u ⊆ t
htu : t \ insert a u ∈ 𝒜
⊢ ∃ a ∈ t, ∃ u_1, #u_1 = #u ∧ (u_1 ⊆ t ∧ a ∉ u_1) ∧ t \ insert a u_1 ∈ 𝒜

Tactic:
rw [insert_subset_iff] at hut

Goal state after:
case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
u : Finset α
hau : a ∉ u
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ u_1, #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
hut : a ∈ t ∧ u ⊆ t
htu : t \ insert a u ∈ 𝒜
⊢ ∃ a ∈ t, ∃ u_1, #u_1 = #u ∧ (u_1 ⊆ t ∧ a ∉ u_1) ∧ t \ insert a u_1 ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: 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 ∈ ∂ 𝒜
⊢ compress u v s ∈ ∂ 𝒜

Tactic:
compress

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 ∈ ∂ 𝒜
⊢ (if Disjoint u s ∧ v ⊆ s then (s ⊔ u) \ v else s) ∈ ∂ 𝒜
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case inr.hd
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < (Fintype.card α).choose (r - 1)

Tactic:
exact Nat.choose_pos (r.pred_le.trans hr')

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
h : 𝒜.Shatters s
⊢ (∃ u ∈ 𝒜, s ∩ u = t) → t ⊆ s

Tactic:
by rintro ⟨u, _, rfl⟩; exact inter_subset_left

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s))⁻¹ ≤ 1

Tactic:
calc
    _ = ∑ r ∈ range (Fintype.card α + 1),
        ∑ s ∈ 𝒜 with #s = r, ((Fintype.card α).choose r : 𝕜)⁻¹ := by
      rw [sum_fiberwise_of_maps_to']; simp [card_le_univ]
    _ = ∑ r ∈ range (Fintype.card α + 1), (#(𝒜 # r) / (Fintype.card α).choose r : 𝕜) := by
      simp [slice, div_eq_mul_inv]
    _ ≤ 1 := lubell_yamamoto_meshalkin_inequality_sum_card_div_choose h𝒜

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
h : G.IsUniversal u
h' : u = v
⊢ G.Reachable u v

pp: case neg
V : Type u
G : SimpleGraph V
u v : V
h : G.IsUniversal u
h' : u ≠ v
⊢ G.Reachable u v

Tactic:
· exact h' ▸ Reachable.rfl

Goal state after:
case neg
V : Type u
G : SimpleGraph V
u v : V
h : G.IsUniversal u
h' : u ≠ v
⊢ G.Reachable u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case inr.inr
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∈ P.edges
hyP : y ∈ P.support
P₁ : G.Walk w y := P.takeUntil y hyP
hxP₁ : x ∉ (P.takeUntil y hyP).support
⊢ (G.deleteEdges {s(x, y)}).Reachable x w

Tactic:
have heP₁ : s(x, y) ∉ P₁.edges := fun h ↦ hxP₁ <| P₁.fst_mem_support_of_mem_edges h

Goal state after:
case inr.inr
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∈ P.edges
hyP : y ∈ P.support
P₁ : G.Walk w y := P.takeUntil y hyP
hxP₁ : x ∉ (P.takeUntil y hyP).support
heP₁ : s(x, y) ∉ P₁.edges
⊢ (G.deleteEdges {s(x, y)}).Reachable x w
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.Colorable 1 ∧ ¬G.Colorable 0 ↔ G = ⊥ ∧ ¬IsEmpty V

Tactic:
colorable_one_iff,

Goal state after:
V : Type u
G : SimpleGraph V
⊢ G = ⊥ ∧ ¬G.Colorable 0 ↔ G = ⊥ ∧ ¬IsEmpty V
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
i : ℕ
hi : i < w.length
⊢ w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1))

Tactic:
induction w generalizing i with
  | nil => cases hi
  | cons hxy i' ih =>
    cases i
    · simp
    · simp only [Walk.toSubgraph, getVert_cons_succ, Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq,
        Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
      right
      exact ih (Nat.succ_lt_succ_iff.mp hi)

Goal state after: