mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #(G.cliqueFinset 3) = #(G.cliqueFinset 3)

Tactic:
by congr

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommRing α
s : Finset α
x : α × α × α
inst✝ : Fact (IsUnit 2)
⊢ ∀ ⦃a b c a' : α⦄, (a, b, c) ∈ triangleIndices s → (a', b, c) ∈ triangleIndices s → a = a'

Tactic:
simp only [mem_triangleIndices, Prod.mk_inj, forall_exists_index, and_imp]
    rintro _ _ _ _ x a ha rfl rfl rfl y b hb rfl h₁ h₂
    linear_combination 2 * h₁.symm - h₂.symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
⊢ G₁.Inc e = G₂.Inc f ↔ G₁.IsLink e = G₂.IsLink f

Tactic:
constructor <;> rintro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
⊢ G₁.IsLink e = G₂.IsLink f

case mpr
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.IsLink e = G₂.IsLink f
⊢ G₁.Inc e = G₂.Inc f
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case h
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x ↦ x * m) '' N = N
absorbing_eq_self : N ∩ {m' | m' * m = m} = N
⊢ m * m = m

Tactic:
rw [← absorbing_eq_self] at hm

Goal state after:
case h
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N ∩ {m' | m' * m = m}
scaling_eq_self : (fun x ↦ x * m) '' N = N
absorbing_eq_self : N ∩ {m' | m' * m = m} = N
⊢ m * m = m
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case refine_1.inr.convert_1
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ Directed (fun x1 x2 ↦ x1 ⊇ x2) Subtype.val

pp: case refine_1.inr.convert_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ∀ (i : ↑c), (↑i).Nonempty

pp: case refine_1.inr.convert_3
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ∀ (i : ↑c), IsCompact ↑i

pp: case refine_1.inr.convert_4
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ∀ (i : ↑c), IsClosed ↑i

Tactic:
· refine DirectedOn.directed_val (IsChain.directedOn hc.symm)

Goal state after:
case refine_1.inr.convert_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ∀ (i : ↑c), (↑i).Nonempty

case refine_1.inr.convert_3
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ∀ (i : ↑c), IsCompact ↑i

case refine_1.inr.convert_4
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ∀ (i : ↑c), IsClosed ↑i
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
x : η' → α'
i : ι'
⊢ ↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))

Tactic:
by
  cases h : l.idxFun (eι.symm i) <;> simp [h, reindex, coe_apply]

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
g : Numbering ↥s × Numbering ↥sᶜ
⊢ (fun f ↦
        ({ toFun := fun x ↦ ⟨↑(↑f ↑x), ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n, ⋯⟩, ⋯⟩, left_inv := ⋯,
            right_inv := ⋯ },
          { toFun := fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩, left_inv := ⋯,
            right_inv := ⋯ }))
      ((fun x ↦
          match x with
          | (g, g') =>
            ⟨{ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
                invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
                left_inv := ⋯, right_inv := ⋯ },
              ⋯⟩)
        g) =
    g

Tactic:
by simp +contextual [Prod.ext_iff, DFunLike.ext_iff]

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

Goal state before:
pp: case inr
ι : 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₁
j : ι
hne : i ≠ j
⊢ (M j).IsBase (Sigma.mk j ⁻¹' B₁ \ Sigma.mk j ⁻¹' {⟨i, e⟩} ∪ Sigma.mk j ⁻¹' {⟨i, f⟩})

Tactic:
preimage_singleton_eq_empty.2 (by simpa),

Goal state after:
case inr
ι : 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₁
j : ι
hne : i ≠ j
⊢ (M j).IsBase (Sigma.mk j ⁻¹' B₁ \ ∅ ∪ Sigma.mk j ⁻¹' {⟨i, f⟩})
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case inr
ι : 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₁
j : ι
hne : i ≠ j
⊢ (M j).IsBase (Sigma.mk j ⁻¹' B₁ \ ∅ ∪ Sigma.mk j ⁻¹' {⟨i, f⟩})

Tactic:
preimage_singleton_eq_empty.2 (by simpa),

Goal state after:
case inr
ι : 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₁
j : ι
hne : i ≠ j
⊢ (M j).IsBase (Sigma.mk j ⁻¹' B₁ \ ∅ ∪ ∅)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ Y \ X ⊆ Y \ I

Tactic:
refine sdiff_subset_sdiff_right hIX.subset

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.closure (X ∪ C) \ C

Tactic:
by
  rw [← sdiff_union_inter (M.closure (X ∪ C) \ C) X, sdiff_sdiff, union_comm C, ← contract_loops_eq,
    union_comm X, ← contract_contract, contract_loops_eq, subset_antisymm_iff, union_subset_iff,
    and_iff_right sdiff_subset, ← sdiff_subset_iff]
  simp only [sdiff_sdiff_right_self, subset_inter_iff, inter_subset_right, and_true]
  refine ⟨fun e ⟨he, he'⟩ ↦ ⟨mem_closure_of_mem' _ (.inr he') (mem_ground_of_mem_closure he).1,
    (closure_subset_ground _ _ he).2⟩, fun e ⟨⟨he, heC⟩, he'⟩ ↦
    mem_closure_of_mem' _ he' ⟨M.closure_subset_ground _ he, heC⟩⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
h : M.Spanning (X ∪ C ∩ M.E)
hdj : Disjoint X (C ∩ M.E)
⊢ Disjoint X (C \ M.E)

Tactic:
exact disjoint_sdiff_right.mono_left (subset_union_left.trans h.subset_ground)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K D : Set α
hK : M.IsCocircuit K
hD : D ⊂ K
⊢ (M ＼ D).IsCocircuit (K \ D)

Tactic:
rw [isCocircuit_def, dual_delete]

Goal state after:
α : Type u_1
M : Matroid α
K D : Set α
hK : M.IsCocircuit K
hD : D ⊂ K
⊢ (M✶ ／ D).IsCircuit (K \ D)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : M.IsCocircuit K
hXK : X ⊆ K
hX : X.Nonempty
⊢ (M ＼ (K \ X)).IsCocircuit X

Tactic:
rw [isCocircuit_def, dual_delete]

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : M.IsCocircuit K
hXK : X ⊆ K
hX : X.Nonempty
⊢ (M✶ ／ (K \ X)).IsCircuit X
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
⊢ coeff t (∑ a ∈ h.support, h a • ∏ r ∈ S a, (X a - C r)) = 0

Tactic:
coeff_sum

Goal state after:
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
⊢ ∑ x ∈ h.support, coeff t (h x • ∏ r ∈ S x, (X x - C r)) = 0
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
⊢ (if h : a ∈ lowerClosure ↑s then {b ∈ s | a ≤ b}.sup' ⋯ (⇑e ∘ id) else e ⊤) =
    if h : e a ∈ lowerClosure ↑(map e.toEmbedding s) then {b ∈ map e.toEmbedding s | e a ≤ b}.sup' ⋯ id else ⊤

Tactic:
map_top,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
⊢ (if h : a ∈ lowerClosure ↑s then {b ∈ s | a ≤ b}.sup' ⋯ (⇑e ∘ id) else ⊤) =
    if h : e a ∈ lowerClosure ↑(map e.toEmbedding s) then {b ∈ map e.toEmbedding s | e a ≤ b}.sup' ⋯ id else ⊤
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 ∧ (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

Tactic:
split_ifs at hb hab with hbs

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

case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
a b : α
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s
hbs : ¬(Disjoint u b ∧ v ≤ b)
hb : b ∈ s ∧ b ∉ s
hab : (a ⊔ u) \ v = b
⊢ a = b
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ s \\ tᶜˢ = s ⊼ t

Tactic:
rw [← infs_compls_eq_diffs, compls_compls]

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

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

Tactic:
simp_rw [← sub_eq_of_eq_add (Fintype.sum_div_mul_card_choose_card α), eq_sub_iff_add_eq,
    ← eq_sub_iff_add_eq', supSum, ← sum_sub_distrib, ← sub_div]

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
⊢ 1 = ∑ x, (↑(card α) - ↑(#({s}.truncatedSup x))) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x))
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
⊢ ∀ ⦃x : Finset α⦄, (x ∈ 𝒜 ∧ compress u v x ∈ 𝒜 ∨ x ∉ 𝒜 ∧ ∃ b ∈ 𝒜, compress u v b = x) → #x = r

Tactic:
rintro s (hs | ⟨huvt, t, ht, rfl⟩)

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
s : Finset α
hs : s ∈ 𝒜 ∧ compress u v s ∈ 𝒜
⊢ #s = r

case inr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
t : Finset α
ht : t ∈ 𝒜
huvt : compress u v t ∉ 𝒜
⊢ #(compress u v t) = r
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr.inr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ a ∈ t

Tactic:
z lt

Goal state after:
case mpr.inr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ a ∈ s.erase (s.min' hs)
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : image (fun t ↦ s ∩ t) 𝒜 = s.powerset
t : Finset α
ht : t ⊆ s
⊢ ∃ u ∈ 𝒜, s ∩ u = t

Tactic:
by rwa [← mem_powerset, ← h, mem_image] at ht

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

Goal state before:
pp: case refine_3.refine_1
α : 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 : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : v ∈ memberSubfamily a 𝒜
hsv : s ∩ v = {a}
⊢ False

Tactic:
rw [mem_memberSubfamily] at hv

Goal state after:
case refine_3.refine_1
α : 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 : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : insert a v ∈ 𝒜 ∧ a ∉ v
hsv : s ∩ v = {a}
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
x y : V
h : ¬x = y
⊢ ⊤.Reachable x y

Tactic:
else

Goal state after:
V : Type u
x y : V
h : ¬x = y
⊢ ⊤.Reachable x y
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
m : ℕ
⊢ m ∈ range k → m < n

Tactic:
rw [mem_range]; apply forall_lt_iff_le.2 hkn

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

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ B ∈ powersetCard (r - i) range'k ↔ B ∈ ∂^[i] 𝒞

Tactic:
rw [mem_powersetCard, mem_shadow_iterate_iff_exists_sdiff]

Goal state after:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ B ⊆ range'k ∧ #B = r - i ↔ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
this : ∃ n, G.Colorable n
⊢ G.Colorable n

Tactic:
obtain ⟨m, hm⟩ := this

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
m : ℕ
hm : G.Colorable m
⊢ G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
⊢ G.neighborSet w ⊆ (between s sᶜ G).neighborSet w ∪ sᶜ

Tactic:
intro v hadj

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
⊢ v ∈ (between s sᶜ G).neighborSet w ∪ sᶜ
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂ : α
b₁ b₂ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂, b₂)
⊢ w.length = w.ofBoxProdLeft.length + w.ofBoxProdRight.length

Tactic:
by
  match w with
  | .nil => simp [ofBoxProdLeft, ofBoxProdRight]
  | .cons x w' => next c =>
    unfold ofBoxProdLeft ofBoxProdRight
    rw [length_cons, length_boxProd w']
    have disj : (G.Adj a₁ c.1 ∧ b₁ = c.2) ∨ (H.Adj b₁ c.2 ∧ a₁ = c.1) := by simp_all
    rcases disj with h₁ | h₂
    · simp only [h₁, and_self, ↓reduceDIte, length_cons, Or.by_cases]
      rw [add_comm, add_comm w'.ofBoxProdLeft.length 1, add_assoc]
      congr <;> simp [h₁.2.symm]
    · simp only [h₂, add_assoc, Or.by_cases]
      congr <;> simp [h₂.2.symm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
⊢ (G □ H).Connected

Tactic:
have := hG.nonempty

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
this : Nonempty α
⊢ (G □ H).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h : {x ∈ s | x ∈ p.support}.Nonempty
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅

Tactic:
induction hp : p.length + #s using Nat.strong_induction_on generalizing s v with | _ n ih

Goal state after:
case h
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
h : {x ∈ s | x ∈ p.support}.Nonempty
hp : p.length + #s = n
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
⊢ ({G | H.Free G}.sup fun x ↦ #x.edgeFinset) ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
rw [Finset.sup_le_iff]
  intro G h
  have h' : G.map e ∈ univ.filter (H.Free ·) := by
    rw [mem_filter, ← free_congr .refl (.map e G)]
    simpa using h
  rw [Iso.card_edgeFinset_eq (.map e G)]
  convert! @le_sup _ _ _ _ {G | H.Free G} (#·.edgeFinset) _ h'

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
⊢ ({G | H.Free G}.sup fun x ↦ #x.edgeFinset) ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
rw [Finset.sup_le_iff]
  intro G h
  have h' : G.map e ∈ univ.filter (H.Free ·) := by
    rw [mem_filter, ← free_congr .refl (.map e G)]
    simpa using h
  rw [Iso.card_edgeFinset_eq (.map e G)]
  convert! @le_sup _ _ _ _ {G | H.Free G} (#·.edgeFinset) _ h'

Goal state after: