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

Goal state before:
pp: α : Type u_5
α' : Type u_6
ι : Type u_7
f : α → α'
l : Line α ι
x : α
⊢ ↑(map f l) (f x) = f ∘ ↑l x

Tactic:
by
  simp only [Line.apply_def, Line.map, Option.getD_map, comp_def]

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

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

Tactic:
disjoint_comm

Goal state after:
α : Type u_1
M : Matroid α
D : Set α
⊢ Disjoint D M.E ↔ Disjoint D M.E
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h.cons'
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m : M
b : Stream' M
n : M
h : FP b.tail n
ih : ∀ (p : { s // s ∈ U }), b.tail = Stream'.corec elem succ p → n ∈ ↑p
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → b.head * n ∈ ↑p

Tactic:
| cons' b n h ih =>

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s : Finset X
inst✝ : DecidableEq X
⊢ f ∈ prefixed s ↔ f.IsPrefix s

Tactic:
simp [prefixed]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
h : ∃ p ∈ s.lines, p.color = C' s.focus
⊢ (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l

Tactic:
obtain ⟨p, p_mem, hp⟩ := h
      refine Or.inr (mono_of_mono ⟨p.line, p.color, ?_⟩)
      rintro (_ | _)
      · rw [hp, s.is_focused p p_mem]
      · apply p.has_color

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

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

Tactic:
disjoint_comm

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ X \ I ⊆ (M ／ I).loops

Tactic:
rw [sdiff_subset_iff, contract_loops_eq, union_sdiff_self,
    union_eq_self_of_subset_left (M.subset_closure I)]
  exact hIX.subset_closure

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

Goal state before:
pp: α✝ α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
I : Set α
hI : M.IsBasis I C
⊢ M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (M.closure C \ C ∪ C \ I)

Tactic:
sdiff_union_sdiff_cancel (M.subset_closure C) hI.subset

Goal state after:
α✝ α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
I : Set α
hI : M.IsBasis I C
⊢ M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (M.closure C \ I)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case heval
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
y : R
hy : y ∈ S none
⊢ Polynomial.eval y (Polynomial.map (eval x) Q) = 0

Tactic:
rw [← optionEquivLeft_elim_eval]

Goal state after:
case heval
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
y : R
hy : y ∈ S none
⊢ (eval fun x_1 ↦ x_1.elim y x) P = 0
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
hC : (M ／ K).IsCircuit C
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

Tactic:
by
  wlog hKi : M.Indep K generalizing K with aux
  · obtain ⟨I, hI⟩ := M.exists_isBasis' K
    rw [hI.contract_eq_contract_delete, delete_isCircuit_iff] at hC
    obtain ⟨C', hC', hCC', hC'ss⟩ := aux hC.1 hI.indep
    exact ⟨C', hC', hCC', hC'ss.trans (union_subset_union_right _ hI.subset)⟩
  obtain ⟨hCE : C ⊆ M.E, hCK : Disjoint C K⟩ := subset_sdiff.1 hC.subset_ground
  obtain ⟨C', hC'ss, hC'⟩ := (hKi.contract_dep_iff.1 hC.dep).2.exists_isCircuit_subset
  refine ⟨C', hC', ?_, hC'ss⟩
  have hdep2 : (M ／ K).Dep (C' \ K) := by
    rw [hKi.contract_dep_iff, and_iff_right disjoint_sdiff_left]
    refine hC'.dep.superset (by simp)
  rw [← (hC.eq_of_dep_subset hdep2 (sdiff_subset_iff.2 (union_comm _ _ ▸ hC'ss)))]
  exact sdiff_subset

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
m : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some m).update none d
hn : n = (embDomain Embedding.some m).update none d
⊢ coeff m (((optionEquivLeft R σ) P).coeff d) = 0

Tactic:
rw [eq_option_embedding_update_none_iff] at hn

Goal state after:
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
m : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some m).update none d
hn : n none = d ∧ n.some = m
⊢ coeff m (((optionEquivLeft R σ) P).coeff d) = 0
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
⊢ (Matroid.sum' M).Indep I ↔ ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)

Tactic:
by
  simp only [Matroid.sum', mapEquiv_indep_iff, Equiv.sigmaEquivProd_symm_apply, sigma_indep_iff]
  convert! Iff.rfl
  ext
  simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i ↦ (M i).E)
I X : Set α
⊢ (Matroid.disjointSigma M h).IsBasis I X ↔
    (∀ (i : ι), (M i).IsBasis (I ∩ (M i).E) (X ∩ (M i).E)) ∧ I ⊆ X ∧ X ⊆ ⋃ i, (M i).E

Tactic:
by
  simp [Matroid.disjointSigma, Function.Embedding.sigmaSet_preimage h]

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
he : ¬coeff e (Q.coeff m) = 0
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
hn : n = (embDomain Embedding.some e).update none m
⊢ e i ≤ P.support.sup fun m ↦ m (Option.some i)

Tactic:
rw [eq_option_embedding_update_none_iff] at hn

Goal state after:
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
he : ¬coeff e (Q.coeff m) = 0
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
hn : n none = m ∧ n.some = e
⊢ e i ≤ P.support.sup fun m ↦ m (Option.some i)
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

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

Tactic:
filter_inter_distrib,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ image (fun s ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s} ∩ {s ∈ ℬ | a ∈ s}) =
    image (fun s ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s}) ∩ image (fun s ↦ s.erase a) ({s ∈ ℬ | a ∈ s})
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) ↑s
ha : a ∈ s
⊢ s.truncatedInf a = a

Tactic:
by
  refine le_antisymm truncatedInf_le ?_
  simp_rw [truncatedInf_of_mem (subset_upperClosure ha), le_inf'_iff, mem_filter]
  rintro b ⟨hb, hba⟩
  exact (hs.eq hb ha hba).ge

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

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

Tactic:
rw [infs_comm, infs_compls_eq_diffs]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ ∂ {{a}} = {∅}

Tactic:
by
  simp [shadow]

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 a : α
inst✝ : DecidableEq α
h : a ∈ 𝓒 u v s
ha : a ∉ s
⊢ u ≤ a

Tactic:
rw [mem_compression] at h

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
ha : a ∉ s
⊢ u ≤ a
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
⊢ Set.Sized r ↑(∂ 𝒜) ↔ Set.Sized (r + 1) ↑𝒜

Tactic:
refine ⟨fun h𝒜 s hs => ?_, Set.Sized.shadow⟩

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
h𝒜 : Set.Sized r ↑(∂ 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
⊢ #s = r + 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 a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
hba : (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) = a
⊢ u ≤ a

Tactic:
split_ifs at hba with h

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
⊢ u ≤ a

case neg
α : 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 = a
⊢ u ≤ a
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
h : a ∈ 𝓒 u v s
ha : a ∉ s
⊢ Disjoint v a

Tactic:
rw [mem_compression] at h

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
ha : a ∉ s
⊢ Disjoint v a
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
s : UpperSet α
inst✝ : Finite α
⊢ (∃ a, Ici a = s) → InfIrred s

Tactic:
· rintro ⟨a, rfl⟩
    exact infIrred_Ici _

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 a : α
inst✝ : DecidableEq α
h : a ∈ 𝓒 u v s
ha : a ∉ s
⊢ (a ⊔ v) \ u ∈ s

Tactic:
rw [mem_compression] at h

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
ha : a ∉ s
⊢ (a ⊔ v) \ u ∈ s
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 a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
hba : (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) = a
⊢ (a ⊔ v) \ u ∈ s

Tactic:
split_ifs at hba with h

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
⊢ (a ⊔ v) \ u ∈ s

case neg
α : 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 = a
⊢ (a ⊔ v) \ u ∈ s
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
⊢ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s

Tactic:
refine ⟨u, hu, hut.trans hts, ?_⟩

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) = #s
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 ∈ image (fun t ↦ s ∩ t) 𝒜
⊢ ∃ u ∈ 𝒜, s ∩ u = t

Tactic:
mem_image

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : image (fun t ↦ s ∩ t) 𝒜 = s.powerset
t : Finset α
ht : ∃ a ∈ 𝒜, s ∩ a = t
⊢ ∃ u ∈ 𝒜, s ∩ u = t
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))⁻¹ =
    ∑ r ∈ range (Fintype.card α + 1), ∑ s ∈ 𝒜 with #s = r, (↑((Fintype.card α).choose r))⁻¹

Tactic:
rw [sum_fiberwise_of_maps_to']; simp [card_le_univ]

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

Goal state before:
pp: α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ : Set α
⊢ ∀ (y₂ : Set α), b₁ ∈ s ∧ a ∈ b₁ → y₂ ∈ s ∧ a ∈ y₂ → b₁ = y₂

Tactic:
b₂

Goal state after:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
⊢ b₁ ∈ s ∧ a ∈ b₁ → b₂ ∈ s ∧ a ∈ b₂ → b₁ = b₂
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u : V
hu : u ∈ C
v : V
hv : v ∈ C
⊢ C.toSimpleGraph.Reachable ⟨u, hu⟩ ⟨v, hv⟩

Tactic:
exact C.reachable_toSimpleGraph hu hv

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

Goal state before:
pp: case mpr
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 A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ #B + i = #A

Tactic:
← card_sdiff_i,

Goal state after:
case mpr
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 A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ #B + #(A \ B) = #A
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) := ⋯
𝒞 : Finset (Finset (Fin n)) := ⋯
this✝ : Set.Sized r ↑𝒞
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ : toColex B < toColex A
HB₂ : #B = r
t : Fin n
ht : t ∈ B
this : toColex (image Fin.val B) < toColex (image Fin.val A)
⊢ ∀ b ∈ image Fin.val A, b < k

Tactic:
mem_image

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 ↑𝒞
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ : toColex B < toColex A
HB₂ : #B = r
t : Fin n
ht : t ∈ B
this : toColex (image Fin.val B) < toColex (image Fin.val A)
⊢ ∀ (b : ℕ), (∃ a ∈ A, ↑a = b) → b < k
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
e : Sym2 V
he : e ∈ G.edgeSet
⊢ G.IsBridge e ↔ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges

Tactic:
obtain ⟨v, w⟩ := e

Goal state after:
case mk
V : Type u
G : SimpleGraph V
e : Sym2 V
v w : V
he : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
⊢ G.IsBridge (Quot.mk (Sym2.Rel V) (v, w)) ↔
    ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → Quot.mk (Sym2.Rel V) (v, w) ∉ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
i : α
hi : ∀ (a : V), C a ≠ i
⊢ False

Tactic:
let D : G.Coloring {a // a ≠ i} := ⟨fun v ↦ ⟨C v, hi v⟩, (C.valid · <| congr_arg Subtype.val ·)⟩

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
i : α
hi : ∀ (a : V), C a ≠ i
D : G.Coloring { a // a ≠ i } := { toFun := fun v ↦ ⟨C v, ⋯⟩, map_rel' := ⋯ }
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
h : ¬G.Reachable u v
hb : G.IsBridge e
he : e ∈ G.edgeSet
w : V
p : (G ⊔ edge u v).Walk w w
hp : p.IsCycle
hpe : e ∈ p.edges
e' : Sym2 V
he' : e' ∈ p.edges
⊢ e' ∈ G.edgeSet

Tactic:
refine edgeSet_sup .. ▸ Walk.edges_subset_edgeSet _ he' |>.elim id fun h' ↦ h ?_ |>.elim

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
h : ¬G.Reachable u v
hb : G.IsBridge e
he : e ∈ G.edgeSet
w : V
p : (G ⊔ edge u v).Walk w w
hp : p.IsCycle
hpe : e ∈ p.edges
e' : Sym2 V
he' : e' ∈ p.edges
h' : e' ∈ (edge u v).edgeSet
⊢ G.Reachable u v
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet w)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ G.neighborFinset w = bipartiteBelow G.Adj s w

Tactic:
isBipartiteWith_neighborFinset' h hw,

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet w)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ {v ∈ s | G.Adj v w} = bipartiteBelow G.Adj s w
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
⊢ ∃ c, H.verts = c.supp

Tactic:
SimpleGraph.ConnectedComponent.exists

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
⊢ ∃ v, H.verts = (G.connectedComponentMk v).supp
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
⊢ ∃ c, H.verts = c.supp

Tactic:
rw [SimpleGraph.ConnectedComponent.exists]
  obtain ⟨v, hv⟩ := hc.nonempty
  use v
  ext w
  simp only [ConnectedComponent.mem_supp_iff, ConnectedComponent.eq]
  exact ⟨fun hw ↦ by simpa using (hc ⟨w, hw⟩ ⟨v, hv⟩).map H.hom,
    fun a ↦ a.symm.mem_subgraphVerts h hv⟩

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hμ : Monotone μ
hf : 0 < f
hg : 0 ≤ 0
hfg : ∑ a, f a = ∑ a, 0 a
h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)
⊢ ∑ a, μ a * f a ≤ ∑ a, μ a * 0 a

Tactic:
simp only [Pi.zero_apply, sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hμ : Monotone μ
hf : 0 < f
hg : 0 ≤ 0
h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)
hfg : f = 0
⊢ ∑ a, μ a * f a ≤ ∑ a, μ a * 0 a