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

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

Tactic:
exact (h'.mono h).edge_mem

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ V(H.restrict F) ⊆ V(G.restrict F)

pp: case refine_2
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ E(H.restrict F) ⊆ E(G.restrict F)

Tactic:
· simpa using h.vertexSet_mono

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ E(H.restrict F) ⊆ E(G.restrict F)
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ G₁ = G₂

Tactic:
rw [← G₁.mk_eq_self G₁.edge_mem_iff_exists_isLink, ← G₂.mk_eq_self G₂.edge_mem_iff_exists_isLink]
  convert! rfl using 2
  · exact hV.symm
  · simp [funext_iff, h]
  simp [edgeSet_eq_setOfPred_exists_isLink, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
e e' f✝ : Set α
H✝ H : Hypergraph α
f : α → β
⊢ ∀ ⦃e : Set β⦄, e ∈ image f '' E(H) → e ⊆ f '' V(H)

Tactic:
rintro - ⟨e, he, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
e✝ e' f✝ : Set α
H✝ H : Hypergraph α
f : α → β
e : Set α
he : e ∈ E(H)
⊢ f '' e ⊆ f '' V(H)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : s.lines.card = Fintype.card κ + 1
⊢ (Fintype.card κ).succ ≤ Fintype.card κ

Tactic:
← Nat.add_one,

Goal state after:
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : s.lines.card = Fintype.card κ + 1
⊢ Fintype.card κ + 1 ≤ Fintype.card κ
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ (M✶ ＼ I)✶.IsBase B ↔ M.IsBase (B ∪ I) ∧ Disjoint B I

Tactic:
dual_isBase_iff',

Goal state after:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ (M✶ ＼ I).IsBase ((M✶ ＼ I).E \ B) ∧ B ⊆ (M✶ ＼ I).E ↔ M.IsBase (B ∪ I) ∧ Disjoint B I
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ Disjoint B I → (M✶✶✶.IsBasis ((M✶✶.E \ I) \ B) (M✶✶✶.E \ I) ∧ B ⊆ M✶✶.E ↔ M✶✶.IsBase (B ∪ I))

Tactic:
dual_isBase_iff',

Goal state after:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ Disjoint B I → (M✶✶✶.IsBasis ((M✶✶.E \ I) \ B) (M✶✶✶.E \ I) ∧ B ⊆ M✶✶.E ↔ M✶.IsBase (M✶.E \ (B ∪ I)) ∧ B ∪ I ⊆ M✶.E)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.left
σ : 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
i : ι
hb0 : m.degree (b i) = 0
⊢ f = (Finsupp.linearCombination (MvPolynomial σ R) b) (Finsupp.single i (⋯.unit⁻¹ • f)) + 0

Tactic:
simp only [Finsupp.linearCombination_single, smul_eq_mul, add_zero]
      simp only [smul_mul_assoc, ← smul_eq_iff_eq_inv_smul, Units.smul_isUnit]
      nth_rewrite 2 [eq_C_of_degree_eq_zero hb0]
      rw [mul_comm, smul_eq_C_mul]

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ univ.sigma fun i ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ univ.sigma fun i ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk i ⁻¹' X
hII₀ : Sigma.mk i ⁻¹' I ⊆ I₀
h : (∀ (i_1 : ι), (M i_1).Indep (Sigma.mk i_1 ⁻¹' I ∪ Sigma.mk i_1 ⁻¹' Sigma.mk i '' I₀)) → I = I ∪ Sigma.mk i '' I₀
⊢ I₀ ⊆ Sigma.mk i ⁻¹' I ∪ I₀

pp: case refine_1
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ univ.sigma fun i ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ univ.sigma fun i ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk i ⁻¹' X
hII₀ : Sigma.mk i ⁻¹' I ⊆ I₀
h : (∀ (i_1 : ι), (M i_1).Indep (Sigma.mk i_1 ⁻¹' I ∪ Sigma.mk i_1 ⁻¹' Sigma.mk i '' I₀)) → I = I ∪ Sigma.mk i '' I₀
⊢ ∀ (i_1 : ι), (M i_1).Indep (Sigma.mk i_1 ⁻¹' I ∪ Sigma.mk i_1 ⁻¹' Sigma.mk i '' I₀)

Tactic:
· exact subset_union_right

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ univ.sigma fun i ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ univ.sigma fun i ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk i ⁻¹' X
hII₀ : Sigma.mk i ⁻¹' I ⊆ I₀
h : (∀ (i_1 : ι), (M i_1).Indep (Sigma.mk i_1 ⁻¹' I ∪ Sigma.mk i_1 ⁻¹' Sigma.mk i '' I₀)) → I = I ∪ Sigma.mk i '' I₀
⊢ ∀ (i_1 : ι), (M i_1).Indep (Sigma.mk i_1 ⁻¹' I ∪ Sigma.mk i_1 ⁻¹' Sigma.mk i '' I₀)
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
hf'0 : ¬m.subLTerm f = 0
⊢ ∃ g' r',
    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

Tactic:
exact (div hb) (m.subLTerm f)

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg.inl.inl
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
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a✝ : ℕ
ha : Sum.inl a✝ ∈ sA.disjSum sB
a : ℕ
hb : Sum.inl a ∈ sA.disjSum sB
left✝ : Sum.inl a✝ ≠ Sum.inl a
hxy : f (Sum.inl a✝) = f (Sum.inl a)
⊢ n ∈ A + B

Tactic:
simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb

Goal state after:
case neg.inl.inl
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
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a✝ a : ℕ
left✝ : Sum.inl a✝ ≠ Sum.inl a
hxy : f (Sum.inl a✝) = f (Sum.inl a)
ha : (0 < a✝ ∧ a✝ ≤ n) ∧ a✝ ∈ A
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ n ∈ A + B
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg.inl.inr
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
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a : ℕ
ha : Sum.inl a ∈ sA.disjSum sB
b : ℕ
hb : Sum.inr b ∈ sA.disjSum sB
left✝ : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
⊢ n ∈ A + B

Tactic:
simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb

Goal state after:
case neg.inl.inr
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
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a b : ℕ
left✝ : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
ha : (0 < a ∧ a ≤ n) ∧ a ∈ A
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ n ∈ A + B
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg.inr.inl
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
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b : ℕ
ha : Sum.inr b ∈ sA.disjSum sB
a : ℕ
hb : Sum.inl a ∈ sA.disjSum sB
left✝ : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
⊢ n ∈ A + B

Tactic:
simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb

Goal state after:
case neg.inr.inl
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
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b a : ℕ
left✝ : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
ha : (0 < b ∧ b ≤ n) ∧ b ∈ B
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ n ∈ A + B
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg.inr.inr
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
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b✝ : ℕ
ha : Sum.inr b✝ ∈ sA.disjSum sB
b : ℕ
hb : Sum.inr b ∈ sA.disjSum sB
left✝ : Sum.inr b✝ ≠ Sum.inr b
hxy : f (Sum.inr b✝) = f (Sum.inr b)
⊢ n ∈ A + B

Tactic:
simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb

Goal state after:
case neg.inr.inr
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
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b✝ b : ℕ
left✝ : Sum.inr b✝ ≠ Sum.inr b
hxy : f (Sum.inr b✝) = f (Sum.inr b)
ha : (0 < b✝ ∧ b✝ ≤ n) ∧ b✝ ∈ B
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ n ∈ A + B
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeInf α
inst✝² : OrderTop α
inst✝¹ : Finite α
s : { s // InfIrred s }
inst✝ : Fintype ↥↑s
⊢ infIrredUpperSet.symm s = (↑↑s).toFinset.inf id

Tactic:
by
  classical
  obtain ⟨s, hs⟩ := s
  obtain ⟨a, rfl⟩ := infIrred_iff_of_finite.1 hs
  cases nonempty_fintype α
  have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
  simp [symm_apply_eq]

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:
by
  rw [mem_compression] at h
  obtain h | ⟨-, b, hb, hba⟩ := h
  · cases ha h.1
  unfold compress at hba
  split_ifs at hba with h
  · rwa [← hba, sdiff_sup_cancel (le_sup_of_le_left h.2), sup_sdiff_right_self,
      h.1.symm.sdiff_eq_left]
  · cases ne_of_mem_of_not_mem hb ha hba

Goal state after:
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:
← mem_powerset,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : image (fun t ↦ s ∩ t) 𝒜 = s.powerset
t : Finset α
ht : t ∈ s.powerset
⊢ ∃ u ∈ 𝒜, s ∩ u = t
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case mp.inr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ #(s.erase a) = k

Tactic:
card_erase_of_mem ha,

Goal state after:
case mp.inr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ #s - 1 = k
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : c.PairwiseDisjoint id
a : α
⊢ a ∈ Set.univ

Tactic:
exact Set.mem_univ a

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : hs.Quotient
x : α
⊢ hs.proj ⁻¹' {Quotient.mk'' x} = s (hs.equivQuotient.symm (Quotient.mk'' x))

Tactic:
ext y

Goal state after:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : hs.Quotient
x y : α
⊢ y ∈ hs.proj ⁻¹' {Quotient.mk'' x} ↔ y ∈ s (hs.equivQuotient.symm (Quotient.mk'' x))
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)
hBk : B ⊆ range'k
hB : #B = r - i
⊢ i + (r - i) ≤ k

Tactic:
← Nat.add_sub_assoc hir,

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)
hBk : B ⊆ range'k
hB : #B = r - i
⊢ i + r - i ≤ k
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mp
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)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = i + (r - i)
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i

Tactic:
← Nat.add_sub_assoc hir,

Goal state after:
case mp
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)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = i + r - i
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
⊢ x ∈ range (hs.piecewise f) → x ∈ ⋃ i, f i '' s i

Tactic:
rintro ⟨x, rfl⟩
    exact mem_iUnion_of_mem (hs.index x) ⟨x, hs.mem_index x, rfl⟩

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
v w v' w' : V
⊢ (G.deleteEdges {s(v, w)}).Reachable v' w' → ∃ p, s(v, w) ∉ p.edges

Tactic:
rintro ⟨p⟩

Goal state after:
case mp
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ ∃ p, s(v, w) ∉ p.edges
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr
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) < #𝒜
this✝¹ : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this✝ : r ≤ n
this : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
⊢ False

Tactic:
have h𝒜bar : (𝒜ᶜˢ : Set (Finset (Fin n))).Sized (n - r) := by simpa using h₂.compls

Goal state after:
case inr
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) < #𝒜
this✝¹ : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this✝ : r ≤ n
this : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
⊢ ¬(G.deleteEdges {s(y, x)}).Reachable u x

Tactic:
rintro ⟨p⟩

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
p : (G.deleteEdges {s(y, x)}).Walk u x
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
⊢ ¬(G.deleteEdges {s(y, x)}).Reachable v x

Tactic:
rintro ⟨p⟩

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
p : (G.deleteEdges {s(y, x)}).Walk v x
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet v)
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ Disjoint (G.neighborFinset v) s

Tactic:
neighborFinset_def,

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet v)
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ Disjoint (G.neighborSet v).toFinset s
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)
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ Disjoint (G.neighborFinset w) t

Tactic:
neighborFinset_def,

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet w)
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ Disjoint (G.neighborSet w).toFinset t
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
⊢ (∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length) ↔
    v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
refine ⟨?_, by aesop⟩

Goal state after:
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
⊢ (∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length) →
    v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ 2 ≤ G.edist u v

Tactic:
← one_add_one_eq_two

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ 1 + 1 ≤ G.edist u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
⊢ (∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length) ↔
    v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
refine ⟨?_, by aesop⟩

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
⊢ (∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length) →
    v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
u v : V ⊕ W
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) u) ((f.sumCongr g.toEquiv) v) ↔ (G ⊕g H).Adj u v

Tactic:
cases u <;> cases v <;> simp [f.map_rel_iff, g.map_rel_iff]

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

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

Tactic:
rintro x y
  obtain ⟨w₁⟩ := hG x.1 y.1
  obtain ⟨w₂⟩ := hH x.2 y.2
  exact ⟨(w₁.boxProdLeft _ _).append (w₂.boxProdRight _ _)⟩

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

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
⊢ ¬(G ⊕g H).Reachable (Sum.inl v) (Sum.inr w)

Tactic:
rintro ⟨p⟩

Goal state after:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
p : (G ⊕g H).Walk (Sum.inl v) (Sum.inr w)
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ Walk.nil.toSubgraph.Connected

Tactic:
apply singletonSubgraph_connected

Goal state after: