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

Goal state before:
pp: 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 := A * A⁻¹
H : Subgroup G := stabilizer G S
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 → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * ↑(#A) < ↑(#(A ∩ z⁻¹ •> A))
hrw : (2 - K) * ↑(#A) ≤ ↑(#(A ∩ w •> A))
this✝¹ : ↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) ≤ ↑(#(z⁻¹ •> A ∩ w •> A))
this✝ : ↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) ≤ ↑(#A)
this : ↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) + ↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) = ↑(#(A ∩ z⁻¹ •> A)) + ↑(#(A ∩ w •> A))
⊢ 0 < ↑(#(z⁻¹ •> A ∩ w •> A))

Tactic:
linarith

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
b : ℕ
hb : b ≠ Multiset.count i p.parts - 1
this : Multiset.count i p.parts * i ≠ i * (b + 1)
⊢ (if Multiset.count i p.parts * i = i * (b + 1) then f i (b + 1) else 0) = 0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ ∑' (n : ℕ), powMulProdOneSubPow k n x =
    1 - x ^ (2 * k + 3) - x ^ (3 * k + 5) * ∑' (n : ℕ), powMulProdOneSubPow (k + 1) n x

Tactic:
rw [eq_sub_iff_add_eq, show 1 - x ^ (2 * k + 3) = 0 - aux k 0 x by simp [aux]]
  rw [← (hsum _).tsum_mul_left, ← (hsum _).tsum_add ((hsum _).mul_left _)]
  apply HasSum.tsum_eq
  rw [((hsum _).add ((hsum _).mul_left _)).hasSum_iff_tendsto_nat]
  simp_rw [aux_sub_aux, Finset.sum_range_sub (aux k · x)]
  apply Tendsto.sub_const
  rw [show 𝓝 0 = 𝓝 (0 * (0 - 1) * ∏' i, (1 - x ^ (k + i + 2))) by simp]
  refine (Tendsto.mul ?_ ?_).mul ?_
  · exact hx.comp (strictMono_mul_left_of_pos (by simp)).tendsto_atTop
  · exact (hx.comp (add_right_strictMono.add_monotone monotone_const).tendsto_atTop).sub_const _
  · apply Multipliable.tendsto_prod_tprod_nat
    convert h (k + 1) using 4
    ring

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : expansion K S A = connectivity K S
hB : expansion K S B = connectivity K S
hAB : (A ∩ B).Nonempty
this✝¹ : expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
this✝ : connectivity K S ≤ expansion K S (A ∩ B)
this : connectivity K S ≤ expansion K S (A ∪ B)
⊢ expansion K S (A ∩ B) = connectivity K S

Tactic:
linarith

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
⊢ 0 < 1 - K

Tactic:
linarith

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ ↑n <
    ((-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2)).order +
      (∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))).order

Tactic:
← le_order_mul

Goal state after:
case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ ↑n <
    ((-1) ^ (k + 1)).order + (X ^ ((k + 1) * (3 * k + 4) / 2)).order +
      (∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))).order
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case ha
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := ⋯
hK : K < 1
ex : Finset G → ℝ := ⋯
κ : ℝ := ⋯
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)
⊢ 0 ≤ 1 - ε / 2

Tactic:
linarith

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)
⊢ (2 - ε) * ↑(#S) - (1 - ε / 2) * ↑(#S) = (1 - ε / 2) * ↑(#S)

Tactic:
linarith

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5.h₁
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ n + 1 ≤ k + 1

Tactic:
linarith

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5.h₂
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ 2 ≤ 3 * k + 4

Tactic:
linarith

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
h : G.IsLink e x y
hHG : H ≤ G
he : e ∈ E(H)
u v : α
huv : H.IsLink e u v
⊢ H.IsLink e x y

Tactic:
obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := (huv.mono hHG).eq_and_eq_or_eq_and_eq h

Goal state after:
case inl
α : Type u_1
β : Type u_2
e : β
G H : Graph α β
hHG : H ≤ G
he : e ∈ E(H)
u v : α
huv : H.IsLink e u v
h : G.IsLink e u v
⊢ H.IsLink e u v

case inr
α : Type u_1
β : Type u_2
e : β
G H : Graph α β
hHG : H ≤ G
he : e ∈ E(H)
u v : α
huv : H.IsLink e u v
h : G.IsLink e v u
⊢ H.IsLink e v u
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
hn : 6 ≤ ↑n
⊢ 0 ≤ ↑n / 3 - 2

Tactic:
linarith

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

Goal state before:
pp: α : Type u_1
β : Type u_2
H₁ H₂ : Graph α β
hH : H₁.Compatible H₂
⊢ H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) ↔ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → x ∈ V(G) → y ∈ V(G) → G.IsLink e x y

Tactic:
tauto

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

Goal state before:
pp: case ha
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := ⋯
hK : K < 1
ex : Finset G → ℝ := ⋯
κ : ℝ := ⋯
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)
⊢ 0 ≤ 1 - ε / 2

Tactic:
linarith

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
⊢ (∃ x y, (∃ e, G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) ↔ ∃ e x y, G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)

Tactic:
tauto

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

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

Tactic:
obtain rfl | rfl := h'.eq_or_eq_of_isLink h

Goal state after:
case inl
α : Type u_1
β : Type u_2
y : α
e : β
G : Graph α β
h' : G.Inc e y
h : G.IsLoopAt e y
⊢ y = y

case inr
α : Type u_1
β : Type u_2
y : α
e : β
G : Graph α β
h' : G.Inc e y
h : G.IsLoopAt e y
⊢ y = y
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (F₁ᶜ ∩ F₂ᶜ ∩ E(G)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)

Tactic:
restrict_inter_edgeSet,

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (F₁ᶜ ∩ F₂ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
⊢ (∃ y a b, G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ v, (∃ y, G.IsLink e v y) ∧ x = f v

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
x y : α'
f : α → α'
⊢ (∃ e a b, G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ a b, (∃ e, G.IsLink e a b) ∧ f a = x ∧ f b = y

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
H : Hypergraph α
⊢ (H.image f).image g = H.image (g ∘ f)

Tactic:
by
  ext <;> simp [Set.image_image]

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

Goal state before:
pp: α : Type u_1
H : Hypergraph α
h : H.IsComplete
⊢ ¬H.IsTrivial

Tactic:
by
  intro hH
  exact hH.not_mem_edgeSet (h ∅ (Set.empty_subset _))

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D

Tactic:
tauto

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

Goal state before:
pp: case hnc
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
hf0 : f = 0
⊢ False

Tactic:
apply hf

Goal state after:
case hnc
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
hf0 : f = 0
⊢ m.degree f = 0
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E

Tactic:
tauto

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

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk i ⁻¹' B₁
⊢ (M i).IsBase (Sigma.mk i ⁻¹' B₁ \ Sigma.mk i ⁻¹' {⟨i, e⟩} ∪ Sigma.mk i ⁻¹' {⟨i, f⟩})

Tactic:
simpa only [show ∀ x, {⟨i,x⟩} = Sigma.mk i '' {x} by simp,
        preimage_image_eq _ sigma_mk_injective, union_singleton]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
h : (M ／ C).IsNonloop e
⊢ M.IsNonloop e

Tactic:
← indep_singleton

Goal state after:
α : Type u_1
M : Matroid α
e : α
C : Set α
h : (M ／ C).Indep {e}
⊢ M.Indep {e}
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: case inr
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
aux : ∀ {C : Set α}, Disjoint C D → C ⊆ M.E → M ／ C ＼ D = M ＼ D ／ C
hCE : ¬C ⊆ M.E
⊢ C ∩ (M.E ∩ (M.E \ D)) = C ∩ (M.E \ D)

Tactic:
inter_eq_self_of_subset_right sdiff_subset

Goal state after:
case inr
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
aux : ∀ {C : Set α}, Disjoint C D → C ⊆ M.E → M ／ C ＼ D = M ＼ D ／ C
hCE : ¬C ⊆ M.E
⊢ C ∩ (M.E \ D) = C ∩ (M.E \ D)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case neg
σ : 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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
⊢ ∃ 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:
· suffices ∃ (g' : ι →₀ MvPolynomial σ R), ∃ r',
        (m.subLTerm f = Finsupp.linearCombination (MvPolynomial σ R) b g' + r') ∧
        (∀ i, m.degree ((b i) * (g' i)) ≼[m] m.degree (m.subLTerm f)) ∧
        (∀ c ∈ r'.support, ∀ i, ¬ m.degree (b i) ≤ c) by
      obtain ⟨g', r', H'⟩ := this
      use g', r' + monomial (m.degree f) (m.leadingCoeff f)
      constructor
      · simp [← add_assoc, ← H'.1, subLTerm]
      constructor
      · exact fun b ↦ le_trans (H'.2.1 b) (degree_sub_LTerm_le f)
      · intro c hc i
        by_cases hc' : c ∈ r'.support
        · exact H'.2.2 c hc' i
        · convert! hf i
          classical
          have := MvPolynomial.support_add hc
          rw [Finset.mem_union, Classical.or_iff_not_imp_left] at this
          simpa only [Finset.mem_singleton] using support_monomial_subset (this hc')
    by_cases hf'0 : m.subLTerm f = 0
    · refine ⟨0, 0, by simp [hf'0], ?_, by simp⟩
      intro b
      simp only [Finsupp.coe_zero, Pi.zero_apply, mul_zero, degree_zero, map_zero]
      exact bot_le
    · exact (div hb) (m.subLTerm f)

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

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

pp: case mpr
V : Type u_2
inst✝ : Quiver V
v : V
⊢ (∀ (w : V), w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))) →
    ∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v

Tactic:
· intro h_singleton w hw_ne h_bidir
    obtain ⟨hab, hba⟩ := h_bidir
    have h_same_scc : (w : StronglyConnectedComponent V) = v :=
      stronglyConnectedComponent_eq_of_path (a := w) (b := v) hba hab
    obtain ⟨rfl⟩ := h_singleton w h_same_scc
    contradiction

Goal state after:
case mpr
V : Type u_2
inst✝ : Quiver V
v : V
⊢ (∀ (w : V), w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))) →
    ∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case nil
V : Type u_1
inst✝ : Quiver V
a : V
⊢ nil.length = 0 ↔ nil = nil

Tactic:
tauto

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ a
⊢ (a✝¹.cons a✝).length = 0 ↔ a✝¹.cons a✝ = nil

Tactic:
tauto

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
h : ε ≤ schnirelmannDensity A
⊢ False

Tactic:
linarith

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

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
b a : α
⊢ (if h : a ≤ b then {b ∈ {b} | a ≤ b}.sup' ⋯ fun x ↦ x else ⊤) = if a ≤ b then b else ⊤

Tactic:
split_ifs <;> simp [Finset.filter_true_of_mem, *]

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

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
b a : α
⊢ (if h : b ≤ a then {b ∈ {b} | b ≤ a}.inf' ⋯ fun x ↦ x else ⊥) = if b ≤ a then b else ⊥

Tactic:
split_ifs <;> simp [Finset.filter_true_of_mem, *]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #s = #t + 1

Tactic:
by
  refine mem_shadow_iff_exists_sdiff.trans <| exists_congr fun t ↦ and_congr_right fun _ ↦
    and_congr_right fun hst ↦ ?_
  rw [card_sdiff_of_subset hst, tsub_eq_iff_eq_add_of_le, add_comm]
  exact card_mono hst

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ supSum (𝒜 ∪ ℬ) + supSum (𝒜 ⊼ ℬ) = supSum 𝒜 + supSum ℬ

Tactic:
unfold supSum
  rw [← sum_add_distrib, ← sum_add_distrib, Finset.sum_congr rfl fun s _ ↦ _]
  simp_rw [← add_div, ← Nat.cast_add, card_truncatedSup_union_add_card_truncatedSup_infs]
  simp

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

Goal state before:
pp: L L' : Set ℕ
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Set (Finset α)
h : L ⊆ L'
hL : L.IsIntersectingOf 𝒜
⊢ L'.IsIntersectingOf 𝒜

Tactic:
tauto

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

Goal state before:
pp: L : Set ℕ
α : Type u_1
inst✝ : DecidableEq α
⊢ L.IsIntersectingOf ∅

Tactic:
tauto

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - #s

Tactic:
← card_compl,

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 ↦ x1 ⊆ x2) 𝒜 s) ≤ #sᶜ
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
cards' : #(s.erase (s.min' hs)) = #(s.erase (s.min' hs))
⊢ #s = #(insert (s.min' hs) (s.erase (s.min' hs))) ∧
    (insert (s.min' hs) (s.erase (s.min' hs)) = s ∨
      ∃ w ∈ s,
        w ∉ insert (s.min' hs) (s.erase (s.min' hs)) ∧
          ∀ ⦃a : α⦄, w < a → (a ∈ insert (s.min' hs) (s.erase (s.min' hs)) ↔ a ∈ s))

Tactic:
rw [insert_erase (min'_mem _ _)]

Goal state after:
case mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
cards' : #(s.erase (s.min' hs)) = #(s.erase (s.min' hs))
⊢ #s = #s ∧ (s = s ∨ ∃ w ∈ s, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ s))
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this✝ : 𝒜 ⊆ {∅}
this : ∂ 𝒜 = ∅
⊢ IsInitSeg (∂ 𝒜) (0 - 1)

Tactic:
simp [this]

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

Goal state before:
pp: case succ
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
      ↑(#(falling (Fintype.card α - k) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ↑(#(𝒜 # (Fintype.card α - k - 1))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1)) +
      ∑ x ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - x))) / ↑((Fintype.card α).choose (Fintype.card α - x)) ≤
    ↑(#(𝒜 # (Fintype.card α - k - 1))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1)) +
      ↑(#(∂ (falling (Fintype.card α - k - 1 + 1) 𝒜))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1))

Tactic:
tsub_add_cancel_of_le (le_tsub_of_add_le_left hk)

Goal state after:
case succ
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
      ↑(#(falling (Fintype.card α - k) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ↑(#(𝒜 # (Fintype.card α - k - 1))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1)) +
      ∑ x ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - x))) / ↑((Fintype.card α).choose (Fintype.card α - x)) ≤
    ↑(#(𝒜 # (Fintype.card α - k - 1))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1)) +
      ↑(#(∂ (falling (Fintype.card α - k) 𝒜))) / ↑((Fintype.card α).choose (Fintype.card α - k - 1))
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : 𝓒 U V 𝒜 ≠ 𝒜
⊢ familyMeasure (𝓒 U V 𝒜) < familyMeasure 𝒜

Tactic:
compression

Goal state after:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
⊢ familyMeasure ({a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜}) < familyMeasure 𝒜
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
u v : V
⊢ Relation.ReflTransGen G.Adj u v → G.Reachable u v

Tactic:
intro h
    induction h with
    | refl => rfl
    | tail _ ha hr => exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩

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

Goal state before:
pp: V : Type u
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ x✝ = x✝¹ ∨ s(x✝¹, x✝) ∈ s ∧ ¬x✝¹ = x✝ ↔ x✝ = x✝¹ ∨ s(x✝¹, x✝) ∈ s

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (t ∈ c ∧ x ∈ t) ∧ ∀ (y : Set α), y ∈ c ∧ x ∈ y → y = t
⊢ t ∈ c ∧ x ∈ t

Tactic:
tauto

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
inst✝¹ : Fintype α
inst✝ : Fintype ↑C.colorClasses
⊢ card ↑(Setoid.ker ⇑C).classes ≤ card α

Tactic:
convert! Setoid.card_classes_ker_le C

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

Goal state before:
pp: n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
A : Finset (Fin n)
hAbar : A ∈ ∂^[n - 2 * r] 𝒜ᶜˢ
hA : A ∈ 𝒜
⊢ False

Tactic:
simp only [mem_shadow_iterate_iff_exists_sdiff, mem_compls] at hAbar
    obtain ⟨C, hC, hAC, _⟩ := hAbar
    exact h𝒜 hA hC (disjoint_of_subset_left hAC disjoint_compl_right)

Goal state after: