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

Goal state before:
pp: case hbc
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 → ℝ := ⋯
κ : ℝ := ⋯
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⋯
A : Finset G
hA : t + 1 ≤ #A
⊢ (κ + 1) / (1 - K) < ↑t + 1

Tactic:
exact Nat.lt_floor_add_one _

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

Goal state before:
pp: case calc_1
n : ℕ
⊢ ↑n ≤ 2 * ↑(n / 6) * 3 + (1 + 2 - 1) * 3

Tactic:
mul_right_comm,

Goal state after:
case calc_1
n : ℕ
⊢ ↑n ≤ 2 * 3 * ↑(n / 6) + (1 + 2 - 1) * 3
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case ha
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := ⋯
hK : K < 1
ex : Finset G → ℝ := ⋯
κ : ℝ := ⋯
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ 0 ≤ 1 - ε / 2

pp: case a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := ⋯
hK : K < 1
ex : Finset G → ℝ := ⋯
κ : ℝ := ⋯
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ S ⊆ (↑H).toFinset * S

Tactic:
· linarith

Goal state after:
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := ⋯
hK : K < 1
ex : Finset G → ℝ := ⋯
κ : ℝ := ⋯
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ S ⊆ (↑H).toFinset * S
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
F : Set β
⊢ (G.restrict F).Inc e x ↔ G.Inc e x ∧ e ∈ F

Tactic:
simp [Inc, and_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
y z : α
hyz : z ≠ x
hy : G.IsLink e y z
⊢ False

Tactic:
← h.eq_of_inc hy.inc_right

Goal state after:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
y z : α
hyz : x ≠ x
hy : G.IsLink e y z
⊢ False
Module: Mathlib.Combinatorics.Graph.Delete

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

Tactic:
inter_comm _ F₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
F : Set β
⊢ (G.deleteEdges F).Inc e x ↔ G.Inc e x ∧ e ∉ F

Tactic:
simp [Inc, and_comm]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
⊢ (M ＼ D).IsBase B ↔ M.IsBase B ∧ Disjoint B D

Tactic:
rw [Matroid.delete_isBase_iff]

Goal state after:
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
⊢ M.IsBasis B (M.E \ D) ↔ M.IsBase B ∧ Disjoint B D
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case neg
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ᶜ
x : X
hx : x ∉ s
⊢ (fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩))
      ((fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s)) x) =
    x

Tactic:
· simp [hx]

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : X
hx : x ∈ s
⊢ ↑(↑((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 := ⋯ },
                  ⋯⟩)
            ((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 := ⋯ }))
              f))
        x) =
    ↑(↑f x)

pp: case neg
X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : X
hx : x ∉ s
⊢ ↑(↑((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 := ⋯ },
                  ⋯⟩)
            ((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 := ⋯ }))
              f))
        x) =
    ↑(↑f x)

Tactic:
· simp [hx]

Goal state after:
case neg
X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : X
hx : x ∉ s
⊢ ↑(↑((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 := ⋯ },
                  ⋯⟩)
            ((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 := ⋯ }))
              f))
        x) =
    ↑(↑f x)
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
⊢ (M.sum N).E = Sum.inl '' M.E ∪ Sum.inr '' N.E

Tactic:
by
  simp [Matroid.sum, Set.ext_iff, mapEquiv, mapEmbedding, Equiv.ulift, Equiv.sumEquivSigmaBool]

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 : σ →₀ ℕ
this : Q.coeff m = 0
⊢ coeff d (Q.coeff m) = 0

Tactic:
simp only [this, coeff_zero]

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
⊢ (M.disjointSum N h).Indep I ↔ M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E

Tactic:
by
  simp [disjointSum, and_assoc]

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
⊢ (M.disjointSum N h).IsBase B ↔ M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E

Tactic:
by
  simp [disjointSum, and_assoc]

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I X : Set α
⊢ (M.disjointSum N h).IsBasis I X ↔
    M.IsBasis (I ∩ M.E) (X ∩ M.E) ∧ N.IsBasis (I ∩ N.E) (X ∩ N.E) ∧ I ⊆ X ∧ X ⊆ M.E ∪ N.E

Tactic:
by
  simp [disjointSum, and_assoc]

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: case inr
D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i ↦ a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
ha1 : a = r 1
hb0 : b = r 0
⊢ r 0 ≠ r 1

Tactic:
· rw [ha1, hb0] at hab
      exact hab.symm

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

Goal state before:
pp: case cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
b✝ c✝ : V
p : Path r b✝
e : b✝ ⟶ c✝
ih : ∀ (q : Path r b✝), p = q
q : Path r c✝
⊢ p.cons e = q

Tactic:
rcases q with _ | ⟨q, f⟩
        · exact False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le p) (height_lt e)))
        · rcases unique_arrow e f with ⟨⟨⟩, ⟨⟩⟩
          rw [ih]

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: case hlt
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
g : (Fin 2 → D) → D
h✝ : g ∈ ω
this : (fun i ↦ g (swap ![![a, b], ![b, a]] i)) ∈ ω.tt ![![a, b], ![b, a]]
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i

Tactic:
exact ⟨_, this, mcfab.rows_lt_aux hab symmega this⟩

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

Goal state before:
pp: case pos
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : c ∈ S
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e_1 p₁ p₂, p'.cons e = p₁.comp (e_1.toPath.comp p₂)

Tactic:
have p'_len : p'.length = n := by simp_all

Goal state after:
case pos
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : c ∈ S
p'_len : p'.length = n
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e_1 p₁ p₂, p'.cons e = p₁.comp (e_1.toPath.comp p₂)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ ⇑(symmetrifyCostar (φ.obj u)) ∘ φ.symmetrify.costar u = Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)

Tactic:
ext ⟨v, f | g⟩ <;>
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [Quiver.symmetrifyCostar]`
    simp only [Quiver.symmetrifyCostar, Function.comp_apply] <;>
    erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply]

Goal state after:
case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : v ⟶ u
⊢ Sum.map (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.costar u) (φ.star u)
      (Sum.map (Sigma.mk ⟨v, Sum.inl f⟩.fst) (Sigma.mk ⟨v, Sum.inl f⟩.fst) ⟨v, Sum.inl f⟩.snd)

case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : u ⟶ v
⊢ Sum.map (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.costar u) (φ.star u)
      (Sum.map (Sigma.mk ⟨v, Sum.inr g⟩.fst) (Sigma.mk ⟨v, Sum.inr g⟩.fst) ⟨v, Sum.inr g⟩.snd)
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ schnirelmannDensity A = 1 ↔ A = Set.univ

Tactic:
schnirelmannDensity_eq_one_iff

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ {0}ᶜ ⊆ A ↔ A = Set.univ
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
h𝒜 : Set.Sized r ↑(∂ 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
a : α
ha : a ∈ s
⊢ #s = r + 1

Tactic:
rw [← h𝒜 (erase_mem_shadow hs ha), card_erase_add_one ha]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a : α
h : ∀ t ∈ 𝒜, a ∉ t
ht : 𝒜.Shatters t
⊢ a ∉ t

Tactic:
obtain ⟨u, hu, htu⟩ := ht.exists_superset; exact notMem_mono htu <| h u hu

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : v ∈ c.supp
hc' : v ∈ c'.supp
⊢ c = c'

Tactic:
by
  simp only [mem_supp_iff] at *
  rw [← hc, ← hc']

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
x✝ : x ∈ ⋃ i, f i '' s i
t : Set β
i : ι
hi : (fun i ↦ f i '' s i) i = t
ht : x ∈ t
⊢ x ∈ range (hs.piecewise f)

Tactic:
simp only [← hi, mem_image] at ht

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
x✝ : x ∈ ⋃ i, f i '' s i
t : Set β
i : ι
hi : (fun i ↦ f i '' s i) i = t
ht : ∃ x_1 ∈ s i, f i x_1 = x
⊢ x ∈ range (hs.piecewise f)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
s : Set V
x✝ : Maximal (fun x ↦ (induce x G).Connected) s
hconn : (fun x ↦ (induce x G).Connected) s
h : ∀ ⦃y : Set V⦄, (fun x ↦ (induce x G).Connected) y → s ⊆ y → y ⊆ s
⊢ ∃ C, C.supp = s

pp: case refine_2
V : Type u
G : SimpleGraph V
s : Set V
x✝ : ∃ C, C.supp = s
C : G.ConnectedComponent
h : C.supp = s
⊢ Maximal (fun x ↦ (induce x G).Connected) s

Tactic:
· have ⟨v, hv⟩ := hconn.nonempty
    suffices s ≤ (G.connectedComponentMk v).supp from
      ⟨G.connectedComponentMk v, le_antisymm (h (connected_toSimpleGraph _) this) this⟩
    exact fun u hu ↦ ConnectedComponent.sound <|
      hconn.preconnected ⟨u, hu⟩ ⟨v, hv⟩ |>.map <| Embedding.induce s |>.toHom

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
s : Set V
x✝ : ∃ C, C.supp = s
C : G.ConnectedComponent
h : C.supp = s
⊢ Maximal (fun x ↦ (induce x G).Connected) s
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.IsBridge s(u, v)
⊢ G.Reachable u v ↔ G.Adj u v

Tactic:
refine ⟨fun hreach ↦ G.mem_edgeSet.mp ?_, Adj.reachable⟩

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
h : G.IsBridge s(u, v)
hreach : G.Reachable u v
⊢ s(u, v) ∈ G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

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

Tactic:
contrapose

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: V : Type u
G : SimpleGraph V
⊢ ↑G.cliqueNum ≤ G.chromaticNumber

Tactic:
by
  have ⟨s, hs⟩ := G.exists_isNClique_cliqueNum
  exact hs.card_eq ▸ hs.isClique.card_le_chromaticNumber

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
f₁ f₂ f₃ f₄ : Finset α → β
inst✝ : ExistsAddOfLE β
u : Finset α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ u → ∀ ⦃t : Finset α⦄, t ⊆ u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
h𝒜 : 𝒜 ⊆ u.powerset
hℬ : ℬ ⊆ u.powerset
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s

Tactic:
induction u using Finset.induction generalizing f₁ f₂ f₃ f₄ 𝒜 ℬ with

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ completeBipartiteGraph α β ⊑ G →
    ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right

Tactic:
by
    refine fun ⟨f⟩ ↦ ⟨univ.map ⟨f ∘ Sum.inl, f.injective.comp Sum.inl_injective⟩,
      univ.map ⟨f ∘ Sum.inr, f.injective.comp Sum.inr_injective⟩, by simp, by simp,
      fun _ hl _ hr ↦ ?_⟩
    rw [mem_coe, mem_map] at hl hr
    replace ⟨_, _, hl⟩ := hl
    replace ⟨_, _, hr⟩ := hr
    rw [← hl, ← hr]
    exact f.toHom.map_adj (by simp)

Goal state after:
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:
rw [← 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.Metric

Goal state before:
pp: V : Type u_1
u v : V
h : u ≠ v
⊢ ⊥.edist u v = ⊤

Tactic:
by
  rwa [ne_eq, ← reachable_bot.not, ← edist_ne_top_iff_reachable.not, not_not] at h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ cons ⋯ (Walk.boxProdLeft H b w).ofBoxProdLeft = cons' x y z h w

Tactic:
simp [ofBoxProdLeft_boxProdLeft]

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

Goal state before:
pp: case mpr
V : Type u_1
G : SimpleGraph V
⊢ (Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath) → G.Connected ∧ ∀ (u v : V) (x y : G.Path u v), x = y

Tactic:
· rintro ⟨hV, h⟩
    refine ⟨Connected.mk ?_, ?_⟩
    · intro v w
      obtain ⟨p, _⟩ := h v w
      exact p.reachable
    · rintro v w ⟨p, hp⟩ ⟨q, hq⟩
      simp only [ExistsUnique.unique (h v w) hp hq]

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

Goal state before:
pp: n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
G✝ : SimpleGraph (Fin n)
inst✝ : DecidableRel G✝.Adj
h' : H'.Free G✝
⊢ #G✝.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H

Tactic:
contrapose! h'

Goal state after:
n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
G✝ : SimpleGraph (Fin n)
inst✝ : DecidableRel G✝.Adj
h' : extremalNumber (Fintype.card (Fin n)) H < #G✝.edgeFinset
⊢ H' ⊑ G✝
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : Minimal Connected G
x✝² x✝¹ : V
x✝ : G.Adj x✝² x✝¹
hbr : ¬G.IsBridge s(x✝², x✝¹)
⊢ G.deleteEdges {s(x✝², x✝¹)} < G

Tactic:
by simpa [deleteEdges, ← edgeSet_ssubset_edgeSet]

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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
w : V
hadj : (fun w ↦ G.Adj v w) w
⊢ w ∈ p.support

Tactic:
have : ¬(p.concat hadj).IsPath := by grind [length_concat]

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
w : V
hadj : (fun w ↦ G.Adj v w) w
this : ¬(p.concat hadj).IsPath
⊢ w ∈ p.support
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x y : V
h : G.Adj y x
⊢ C.get y x h = C.get x y ⋯

Tactic:
by
  simp [EdgeLabeling.get, Sym2.eq_swap]

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
⊢ Fin (r * t) → Fin r × Fin t

Tactic:
refine fun v ↦ (⟨v % r, ?_⟩, ⟨v / r, ?_⟩)
    · have ⟨hr, _⟩ := CanonicallyOrderedAdd.mul_pos.mp v.pos
      exact Nat.mod_lt v hr
    · exact Nat.div_lt_of_lt_mul v.prop

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

Goal state before:
pp: case h₂
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
c₁ c₂ : Fin n
v₁ : ↑(C.colorClass c₁)
v₂ : ↑(C.colorClass c₂)
hc : c₁ = c₂
hv : (F c₁) v₁ = (F c₂) v₂
v₁' : ↑(C.colorClass c₂) := ⋯
⊢ v₁ ≍ v₁'

Tactic:
rw [Subtype.heq_iff_coe_eq]
        simp [hc]

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

Goal state before:
pp: case neg.refine_2
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
i₁ i₂ : Fin r
h :
  ∀ (a : V),
    a ∈ map { toFun := fun j ↦ f (i₁, j), inj' := ⋯ } univ ↔ a ∈ map { toFun := fun j ↦ f (i₂, j), inj' := ⋯ } univ
this : NeZero t
⊢ i₁ = i₂

Tactic:
obtain ⟨_, heq⟩ : ∃ j, f (i₁, j) = f (i₂, 0) := by simpa using h <| f (i₂, 0)

Goal state after:
case neg.refine_2
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
i₁ i₂ : Fin r
h :
  ∀ (a : V),
    a ∈ map { toFun := fun j ↦ f (i₁, j), inj' := ⋯ } univ ↔ a ∈ map { toFun := fun j ↦ f (i₂, j), inj' := ⋯ } univ
this : NeZero t
w✝ : Fin t
heq : f (i₁, w✝) = f (i₂, 0)
⊢ i₁ = i₂
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ G.ediam = ⊤ → G.radius = ⊤

Tactic:
contrapose

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ ¬G.radius = ⊤ → ¬G.ediam = ⊤