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 : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
hA : 0 < expansion K S ∅
⊢ False

Tactic:
simp at hA

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
one_sub_K_pos : 0 < 1 - K
⊢ False

Tactic:
let t := Nat.floor ((κ + 1) / (1 - K))

Goal state after:
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
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
⊢ False
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case refine_2
⊢ Nat.cast =O[atTop] fun n ↦ ↑((n - 3) / 6)

Tactic:
rw [IsBigO_def]
      refine ⟨12, ?_⟩
      simp only [IsBigOWith, norm_natCast, eventually_atTop]
      exact ⟨15, fun x hx ↦ by norm_cast; lia⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hG : G.Loopless
hle : H ≤ G
⊢ H.Loopless

Tactic:
loopless_iff_forall_ne_of_adj

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hG : ∀ (u v : α), G.Adj u v → u ≠ v
hle : H ≤ G
⊢ ∀ (u v : α), H.Adj u v → u ≠ v
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case tail'
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
ih : ∃ n, ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a

Tactic:
obtain ⟨n, hn⟩ := ih

Goal state after:
case tail'
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case cons'
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
ih : ∃ n, ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), a.head * m * m' ∈ FP a

Tactic:
obtain ⟨n, hn⟩ := ih

Goal state after:
case cons'
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), a.head * m * m' ∈ FP a
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case refine_5
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
h : ∃ m ∈ S, m * m = m
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a

Tactic:
rcases h with ⟨U, hU, U_idem⟩

Goal state after:
case refine_5
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : U ∈ S
U_idem : U * U = U
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D C : Set α
⊢ M.IsCircuit C → Disjoint C D → C ⊆ M.E

Tactic:
exact fun h _ ↦ h.subset_ground

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: 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ᶜ
n : Fin (Fintype.card X)
hn : ↑n < #s
⊢ ↑n < Fintype.card ↥s

Tactic:
simpa using hn

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X ⊆ (M ／ C).closure X \ X ∪ M.closure (C ∪ X) \ C ∩ X ∧ M.closure (C ∪ X) \ C ∩ X ⊆ (M ／ C).closure X

Tactic:
← sdiff_subset_iff

Goal state after:
α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X \ ((M ／ C).closure X \ X) ⊆ M.closure (C ∪ X) \ C ∩ X ∧
    M.closure (C ∪ X) \ C ∩ X ⊆ (M ／ C).closure X
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.right.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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
⊢ ¬m.degree (b i) ≤ c

Tactic:
by_cases hc' : c ∈ r'.support

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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
hc' : c ∈ r'.support
⊢ ¬m.degree (b i) ≤ c

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' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
hc' : c ∉ r'.support
⊢ ¬m.degree (b i) ≤ c
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : IsStronglyConnected V
a b : Symmetrify V
⊢ Nonempty (Path a b)

Tactic:
obtain ⟨p⟩ := h a b

Goal state after:
V : Type u_2
inst✝ : Quiver V
h : IsStronglyConnected V
a b : Symmetrify V
p : Path a b
⊢ Nonempty (Path a b)
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
n : ℕ
hn : n ≤ nil.length
⊢ n = 0

Tactic:
simpa using hn

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

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

Tactic:
simp [comp_nil]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case inr
A : Finset ℕ
ε : ℝ
hε : 0 < ε
this : ∀ (ε : ℝ), 0 < ε → ε ≤ 1 → ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε
hε₁ : ¬ε ≤ 1
⊢ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε

pp: A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
⊢ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε

Tactic:
· obtain ⟨n, hn, hn'⟩ := this 1 zero_lt_one le_rfl
    exact ⟨n, hn, hn'.trans_le (le_of_not_ge hε₁)⟩

Goal state after:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
⊢ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: 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

Tactic:
exact ⟨0, hA, n, ⟨hnB, by simp⟩⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∩ t).powerset = s.powerset ⊼ t.powerset

Tactic:
ext u
  simp only [mem_infs, mem_powerset, inf_eq_inter]
  refine ⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩
  · rwa [← inter_inter_distrib_right, inter_eq_right]
  · rintro ⟨v, hv, w, hw, rfl⟩
    exact inter_subset_inter hv hw

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

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
p : α → Prop
⊢ (∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)

Tactic:
refine ⟨fun h a ha b hb hab => h _ ⟨_, ha, _, hb, hab, rfl⟩, ?_⟩

Goal state after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
p : α → Prop
⊢ (∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)) → ∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ lowerClosure ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

Tactic:
by_cases hℬ : s ∈ lowerClosure (ℬ : Set <| Finset α)

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ lowerClosure ↑𝒜
hℬ : s ∈ lowerClosure ↑ℬ
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ lowerClosure ↑𝒜
hℬ : s ∉ lowerClosure ↑ℬ
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

Tactic:
by_cases hℬ : s ∈ lowerClosure (ℬ : Set <| Finset α)

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure ↑𝒜
hℬ : s ∈ lowerClosure ↑ℬ
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure ↑𝒜
hℬ : s ∉ lowerClosure ↑ℬ
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
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 a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ Disjoint v a

Tactic:
← hba

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

Goal state before:
pp: case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : #t + k = #s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : #t = #u + 1
⊢ #u + (k + 1) = #u + 1 + k

Tactic:
add_right_comm

Goal state after:
case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : #t + k = #s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : #t = #u + 1
⊢ #u + (k + 1) = #u + k + 1
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : #t + (k + 1) = #s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : #u = #t + 1
⊢ #t + 1 + k = #t + (k + 1)

Tactic:
add_right_comm

Goal state after:
case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : #t + (k + 1) = #s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : #u = #t + 1
⊢ #t + k + 1 = #t + (k + 1)
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
hu : u = ⊥
hv : v = ⊥
⊢ (b ⊔ ⊥) \ ⊥ ∈ s

Tactic:
sup_bot_eq,

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 = ⊥
hv : v = ⊥
⊢ b \ ⊥ ∈ s
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 a : α
inst✝ : DecidableEq α
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hva : v = ⊥
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ (b ⊔ ⊥) \ ⊥ ∈ s

Tactic:
sup_bot_eq,

Goal state after:
case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hva : v = ⊥
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ b \ ⊥ ∈ s
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ #𝒜 * #ℬ ≤ 2 ^ (#s + 1) * #(𝒜 ∩ ℬ)

Tactic:
← card_memberSubfamily_add_card_nonMemberSubfamily a 𝒜,

Goal state after:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ (#(Finset.memberSubfamily a 𝒜) + #(Finset.nonMemberSubfamily a 𝒜)) * #ℬ ≤ 2 ^ (#s + 1) * #(𝒜 ∩ ℬ)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
s : Set (Sym2 V)
⊢ (fromEdgeSet s).Reachable = Relation.ReflTransGen (Sym2.ToRel s)

Tactic:
by
  rw [reachable_eq_reflTransGen, ← Relation.transGen_reflGen, ← Relation.transGen_reflGen]
  congr 1
  ext
  simpa [Relation.reflGen_iff] using by tauto

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : Fintype ↑(G.neighborSet v)
huv : u ≠ v
hu : G.degree v = 0
⊢ ¬G.Reachable u v

Tactic:
by
  rw [reachable_comm]
  exact not_reachable_of_left_degree_zero huv.symm hu

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
⊢ G.Adj v w ∧ (G.deleteEdges {s(v, w)}).Reachable v w ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
reachable_deleteEdges_iff_exists_walk

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
⊢ (G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges) ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ 0 * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
zero_mul

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
hG : G.Colorable n
⊢ G.chromaticNumber = ↑n ↔ ∀ (C : G.Coloring (Fin n)), Surjective ⇑C

Tactic:
by
  rw [← hG.chromaticNumber_le.ge_iff_eq, le_chromaticNumber_iff_forall_surjective]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s = ∑ s ∈ 𝒜, f s

Tactic:
calc
    _ = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ u.powerset.image (insert a) ∩ 𝒜, f s := ?_
    _ = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ ((insert a u).powerset \ u.powerset) ∩ 𝒜, f s := ?_
    _ = ∑ s ∈ 𝒜, f s := ?_
  · rw [← Finset.sum_ite_mem, ← Finset.sum_ite_mem, sum_image, ← sum_add_distrib]
    · exact sum_congr rfl fun s hs ↦ collapse_eq (notMem_mono (mem_powerset.1 hs) hu) _ _
    · exact (insert_erase_invOn.2.injOn).mono fun s hs ↦ notMem_mono (mem_powerset.1 hs) hu
  · congr with s
    simp only [mem_image, mem_powerset, mem_sdiff, subset_insert_iff]
    refine ⟨?_, fun h ↦ ⟨_, h.1, ?_⟩⟩
    · rintro ⟨s, hs, rfl⟩
      exact ⟨subset_insert_iff.1 <| insert_subset_insert _ hs, fun h ↦
        hu <| h <| mem_insert_self _ _⟩
    · rw [insert_erase (erase_ne_self.1 fun hs ↦ ?_)]
      rw [hs] at h
      exact h.2 h.1
  · rw [← sum_union (disjoint_sdiff_self_right.mono inf_le_left inf_le_left),
      ← union_inter_distrib_right, union_sdiff_of_subset (powerset_mono.2 <| subset_insert _ _),
      inter_eq_right.2 h𝒜]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.IsBipartiteWith ↑s ↑t
hsub : G.support.toFinset ⊆ s ∪ t
v : V
a✝ : v ∈ s ∪ t
hv : v ∉ G.support.toFinset
⊢ G.degree v = 0

Tactic:
Set.mem_toFinset,

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.IsBipartiteWith ↑s ↑t
hsub : G.support.toFinset ⊆ s ∪ t
v : V
a✝ : v ∈ s ∪ t
hv : v ∉ G.support
⊢ G.degree v = 0
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
s₁ s₂ : α ⊕ β
p₁ : α
p₂ : β
⊢ Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inl p₁) =
      Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inr p₂) →
    Sum.inl p₁ = Sum.inr p₂

Tactic:
simpa using (h (fα p₁).prop (fβ p₂).prop).symm.ne'

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha✝ : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb✝ : b ∈ (G.subgraphOfAdj hvw).verts
ha : a = v ∨ a = w
hb : b = v ∨ b = w
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha✝⟩ ⟨b, hb✝⟩

Tactic:
obtain rfl | rfl := ha <;> obtain rfl | rfl := hb <;>
    first | rfl | (apply Adj.reachable; simp)

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

Goal state before:
pp: case inr
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isRight = true
hs₂ : s₂.isLeft = true
⊢ G.Adj (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₁) (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₂)

Tactic:
· rw [← Sum.inr_getRight s₁ hs₁, ← Sum.inl_getLeft s₂ hs₂,
      Sum.elim_inl, Sum.elim_inr, adj_comm]
    exact h (by simp) (by simp)

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

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v = ⊤
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
| inl huv =>

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf (Set.range fun x ↦ ↑x.length) = G.edist v u

Tactic:
← edist_eq_sInf

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.IsPath

Tactic:
by
  classical
  have : p.bypass = p := by
    apply bypass_eq_self_of_length_le_length_bypass
    calc p.length
      _ = G.dist u v := hp
      _ ≤ p.bypass.length := dist_le p.bypass
  rw [← this]
  apply Walk.bypass_isPath

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ (G □ H).edist x y ≤ ↑w_app.length

Tactic:
by exact edist_le _

Goal state after: