mathlib-initiative/mathlib-tactics huggingface dataset:
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
e : σ ≃ τ
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 τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
this : (rename ⇑e.symm) P = 0
that : RingHom.ker (rename ⇑e.symm) = ⊥
⊢ P = 0

Tactic:
rwa [← RingHom.mem_ker, that] at this

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 ∩ X ⊆ M.closure (C ∪ X) \ C ∧ M.closure (C ∪ X) \ C ∩ X ⊆ (M ／ C).closure X

Tactic:
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 α
C D C' : Set α
h : Disjoint C' D
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C') ＼ D

Tactic:
contract_delete_contract',

Goal state after:
α : Type u_1
M : Matroid α
C D C' : Set α
h : Disjoint C' D
⊢ M ／ (C ∪ C' \ D) ＼ D = M ／ (C ∪ C') ＼ D
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C D C' D' : Set α
⊢ M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C' \ D) ＼ (D ∪ D')

Tactic:
contract_delete_contract',

Goal state after:
α : Type u_1
M : Matroid α
C D C' D' : Set α
⊢ M ／ (C ∪ C' \ D) ＼ D ＼ D' = M ／ (C ∪ C' \ D) ＼ (D ∪ D')
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: case inl
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]
ha0 : a = r 0
hb1 : b = r 1
⊢ r 0 ≠ r 1

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 [ha0, hb1] at hab
      exact hab

Goal state after:
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
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
⊢ m = single i (e ())

Tactic:
· rw [← hm]
    ext j
    by_cases hj : j = i
    · rw [hj, mapDomain_apply (Function.injective_of_subsingleton _), single_eq_same]
    · rw [mapDomain_of_notMem_range, single_eq_of_ne hj]
      simp [Set.range_const, Set.mem_singleton_iff, hj]

Goal state after:
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
⊢ φ.symmetrify.costar u = ⇑(symmetrifyCostar (φ.obj u)).symm ∘ Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)

Tactic:
rw [Equiv.eq_symm_comp (e := Quiver.symmetrifyCostar (φ.obj u))]
  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] <;>
    simp

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α := 𝒜.sup id
hu : ∀ s ∈ 𝒜, s ⊆ u
⊢ p 𝒜

Tactic:
clear_value u

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α
hu : ∀ s ∈ 𝒜, s ⊆ u
⊢ p 𝒜
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: h : Set.ofPred Odd = {n | n % 2 = 1}
⊢ schnirelmannDensity {n | n % 2 = 1} = 2⁻¹

Tactic:
rw [schnirelmannDensity_setOfPred_mod_eq_one (by norm_num1), Nat.cast_two]

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

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u : Finset α
⊢ s ○ t ○ u = s ○ u ○ t

Tactic:
disjSups_assoc,

Goal state after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u : Finset α
⊢ s ○ (t ○ u) = s ○ (u ○ t)
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ x,
      (↑(#((𝒜 ∪ ℬ).truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) +
        ↑(#((𝒜 ⊼ ℬ).truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x))) =
    ∑ x,
      (↑(#(𝒜.truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) +
        ↑(#(ℬ.truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)))

Tactic:
Finset.sum_congr rfl fun s _ ↦ _

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ univ.sum ?m.48 =
    ∑ x,
      (↑(#(𝒜.truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) +
        ↑(#(ℬ.truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)))

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ Finset α → ℚ

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ,
    ↑(#((𝒜 ∪ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
        ↑(#((𝒜 ⊼ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
      ?m.48 s
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ x,
      (↑(#((𝒜 ∪ ℬ).truncatedInf x)) / (↑(#x) * ↑((card α).choose #x)) +
        ↑(#((𝒜 ⊻ ℬ).truncatedInf x)) / (↑(#x) * ↑((card α).choose #x))) =
    ∑ x,
      (↑(#(𝒜.truncatedInf x)) / (↑(#x) * ↑((card α).choose #x)) +
        ↑(#(ℬ.truncatedInf x)) / (↑(#x) * ↑((card α).choose #x)))

Tactic:
Finset.sum_congr rfl fun s _ ↦ _

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ univ.sum ?m.48 =
    ∑ x,
      (↑(#(𝒜.truncatedInf x)) / (↑(#x) * ↑((card α).choose #x)) +
        ↑(#(ℬ.truncatedInf x)) / (↑(#x) * ↑((card α).choose #x)))

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ Finset α → ℚ

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ,
    ↑(#((𝒜 ∪ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
        ↑(#((𝒜 ⊻ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) =
      ?m.48 s
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜 # k ∨ s ∈ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜

Tactic:
mem_slice,

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜 ∧ #s = k ∨ s ∈ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h : IsLowerSet ↑𝒜
s : Finset α
hs : s ∈ 𝒜.shatterer
⊢ s ∈ 𝒜

Tactic:
obtain ⟨t, ht, hst⟩ := (mem_shatterer.1 hs).exists_superset

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h : IsLowerSet ↑𝒜
s : Finset α
hs : s ∈ 𝒜.shatterer
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v ↔ Relation.ReflTransGen G.Adj u v

Tactic:
by
  constructor
  · rintro ⟨h⟩
    induction h with
    | nil => rfl
    | cons h' _ ih => exact (Relation.ReflTransGen.single h').trans ih
  · intro h
    induction h with
    | refl => rfl
    | tail _ ha hr => exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ C.toSimpleGraph.Preconnected

Tactic:
intro ⟨u, hu⟩ ⟨v, hv⟩

Goal state after:
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⟩
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: W₁ : Type u_2
W₂ : Type u_3
⊢ (completeBipartiteGraph W₁ W₂).edgeSet = Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
by
  refine Set.ext <| Sym2.ind fun u v ↦ ⟨fun h ↦ ?_, fun ⟨⟨a, b⟩, z⟩ ↦ ?_⟩
  · cases u <;> cases v <;> simp_all
  · grind [completeBipartiteGraph_adj, mem_edgeSet]

Goal state after:
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
h : i ≠ 0
h' : i < p.length
⊢ (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2

Tactic:
rw [hp.neighborSet_toSubgraph_internal h h']

Goal state after:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
⊢ {p.getVert (i - 1), p.getVert (i + 1)}.ncard = 2
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: case inl
α : 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₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
⊢ w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    w'.ofBoxProdLeft.length + 1 +
      (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight else ⋯ ▸ w'.ofBoxProdRight).length

Tactic:
rw [add_comm, add_comm w'.ofBoxProdLeft.length 1, add_assoc]

Goal state after:
case inl
α : 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₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
⊢ 1 + (w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length) =
    1 +
      (w'.ofBoxProdLeft.length +
        (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight else ⋯ ▸ w'.ofBoxProdRight).length)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ (∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H) → H.Preconnected

Tactic:
intro hw

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
⊢ H.Preconnected
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∉ q.support
⊢ w ∈ (q.concat ⋯).support

Tactic:
exact q.support_subset_support_concat _ q.end_mem_support

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
p₀ : G.Walk u w
p₁ : G.Walk w v
hp₀ : p₀.IsPath
hp₁ : p₁.IsPath
happend : p = p₀.append p₁
⊢ v ∉ p₀.support

Tactic:
exact fun hxp => (happend ▸ hp).ne_of_mem_support_of_append hadj.symm.ne' hxp
    (p₁.end_mem_support) rfl

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

Goal state before:
pp: case memEdges
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
⊢ ((f a).firstDart ⋯).edge ∈ G.edgeFinset

pp: case inj
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
⊢ ∀ (a₁ : V) (ha₁ : a₁ ∈ {default}ᶜ) (a₂ : V) (ha₂ : a₂ ∈ {default}ᶜ),
    ((f a₁).firstDart ⋯).edge = ((f a₂).firstDart ⋯).edge → a₁ = a₂

pp: case surj
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
⊢ ∀ b ∈ G.edgeFinset, ∃ a, ∃ (ha : a ∈ {default}ᶜ), ((f a).firstDart ⋯).edge = b

Tactic:
case memEdges => simp

Goal state after:
case inj
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
⊢ ∀ (a₁ : V) (ha₁ : a₁ ∈ {default}ᶜ) (a₂ : V) (ha₂ : a₂ ∈ {default}ᶜ),
    ((f a₁).firstDart ⋯).edge = ((f a₂).firstDart ⋯).edge → a₁ = a₂

case surj
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
⊢ ∀ b ∈ G.edgeFinset, ∃ a, ∃ (ha : a ∈ {default}ᶜ), ((f a).firstDart ⋯).edge = b
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: 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, u ≠ v ∧ G.degree u = 1 ∧ G.degree v = 1

Tactic:
have ⟨u', v', hne⟩ := exists_pair_ne V

Goal state after:
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'
⊢ ∃ u v, u ≠ v ∧ G.degree u = 1 ∧ G.degree v = 1
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ EdgeLabeling.labelGraph G.toTopEdgeLabeling 0 = Gᶜ

Tactic:
ext x y; simp [imp_false]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
inst✝ : DecidableEq V
C : TopEdgeLabeling V (Fin 2)
⊢ ∀ (x y : V) (h : ⊤.Adj x y),
    EdgeLabeling.get (EdgeLabeling.labelGraph C 1).toTopEdgeLabeling x y h = EdgeLabeling.get C x y h

Tactic:
grind [toTopEdgeLabeling_get, TopEdgeLabeling.labelGraph_adj, Adj.ne]

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
⊢ t ∈ fp.part s ↔ fp.part s = fp.part t

Tactic:
rw [fp.mem_part_iff_part_eq_part (mem_univ t) (mem_univ s), eq_comm]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #K.verts = r * t

Tactic:
simp_rw [verts, card_disjiUnion, id_eq, sum_congr rfl fun _ ↦ K.card_mem_parts, sum_const,
    smul_eq_mul, mul_eq_mul_right_iff]
  exact K.card_parts

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
huv : ∀ (i : α), u = i
⊢ v = u

Tactic:
exact (huv v).symm

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

Goal state before:
pp: case inr
n r : ℕ
hr : r > 0
⊢ #(turanGraph n r).edgeFinset = (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
have ring₁ (n) : (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) =
        n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2 := by
      nth_rw 1 [← Nat.mod_add_div n r, Nat.sq_sub_sq, add_tsub_cancel_left,
        show (n % r + r * (n / r) + n % r) * (r * (n / r)) * (r - 1) =
          (2 * ((n % r) * (n / r) * (r - 1)) + r * (r - 1) * (n / r) ^ 2) * r by grind]
      rw [Nat.mul_div_mul_right _ _ hr, Nat.mul_add_div zero_lt_two]
    rcases lt_or_ge n r with h | h
    · rw [Nat.mod_eq_of_lt h, tsub_self, zero_mul, Nat.zero_div, zero_add]
      have := card_edgeFinset_top_eq_card_choose_two (V := Fin n)
      rw [Fintype.card_fin] at this; convert! this
      rw [turanGraph_eq_top]; exact .inr h.le
    · let n' := n - r
      have n'r : n = n' + r := by lia
      rw [n'r, card_edgeFinset_turanGraph_add, card_edgeFinset_turanGraph, ring₁, ring₁,
        add_rotate, ← add_assoc, Nat.add_mod_right, Nat.add_div_right _ hr]
      congr 1
      have rd : 2 ∣ r * (r - 1) := (Nat.even_mul_pred_self _).two_dvd
      rw [← Nat.div_mul_right_comm rd, ← Nat.div_mul_right_comm rd, ← Nat.choose_two_right]
      have ring₂ : n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
          n' % r * (n' / r + 1) * (r - 1) + r.choose 2 +
          r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2 := by grind
      rw [ring₂, ← add_assoc]; congr 1
      rw [← add_rotate, ← add_rotate _ _ (r.choose 2)]; congr 1
      rw [Nat.choose_two_right, Nat.div_mul_cancel rd, mul_add_one, add_mul, ← add_assoc,
        ← add_rotate, add_comm _ (_ * _)]; congr 1
      rw [← mul_rotate, ← add_mul, add_comm, mul_comm _ r, Nat.div_add_mod n' r]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
K L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
⊢ Finite (G.ComponentCompl ↑∅)

Tactic:
dsimp [ComponentCompl]

Goal state after:
case inl
V : Type u
G : SimpleGraph V
K L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
⊢ Finite (induce (↑∅)ᶜ G).ConnectedComponent
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
⊢ IsGLB {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x} H.turanDensity

Tactic:
have h_bdd : BddBelow { (extremalNumber n H / n.choose 2 : ℝ) | n ∈ Set.Ici 2 } := by
    refine ⟨0, fun x ⟨_, _, hx⟩ ↦ ?_⟩
    rw [← hx]
    positivity
  refine Real.isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici ?_
    (antitoneOn_extremalNumber_div_choose_two H) h_bdd
  have h_tto := Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici
    (antitoneOn_extremalNumber_div_choose_two H) h_bdd
  rwa [← h_tto.limUnder_eq] at h_tto

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

Goal state before:
pp: case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
G : SimpleGraph (Fin m ⊕ Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
x✝¹ x✝ : Fin m ⊕ Fin n
hadj : G.Adj x✝¹ x✝
h_le : (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph V W)).Adj x✝¹ x✝
⊢ (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph V W)).Adj x✝¹ x✝

Tactic:
exact h_le

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

Goal state before:
pp: case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : t ≤ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
⊢ ∃ x ∈ powersetCard t p, ∀ x_1 ∈ x, G.Adj v x_1

Tactic:
obtain ⟨s, hs⟩ := powersetCard_nonempty.mpr hs

Goal state after:
case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs✝ : t ≤ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
s : Finset (Fin n)
hs : s ∈ powersetCard t ({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
⊢ ∃ x ∈ powersetCard t p, ∀ x_1 ∈ x, G.Adj v x_1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_free : (completeBipartiteGraph α β).Free G
x✝¹ x✝ : V ⊕ W
hadj : G.Adj x✝¹ x✝
h_le : (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph (Fin m) (Fin n))).Adj x✝¹ x✝
⊢ (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph (Fin m) (Fin n))).Adj x✝¹ x✝

Tactic:
exact h_le

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case mpr
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
⊢ Even (t ∪ u).ncard

Tactic:
obtain hfin | hnfin := (t ∪ u).finite_or_infinite

Goal state after:
case mpr.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : (t ∪ u).Finite
⊢ Even (t ∪ u).ncard

case mpr.inr
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hnfin : (t ∪ u).Infinite
⊢ Even (t ∪ u).ncard