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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
B : Set β
f : α → β
n : ℕ
s t : Multiset α
⊢ (∀ ⦃x : α⦄, x ∈ s → x ∈ ∅) →
    (∀ ⦃x : α⦄, x ∈ t → x ∈ ∅) → s.card = n → t.card = n → s.prod = t.prod → (map f s).prod = (map f t).prod

Tactic:
aesop (add simp eq_zero_of_forall_notMem)

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑N * (↑N ^ (2 / ↑n) * (rexp (↑n - 2) * ↑n))⁻¹

Tactic:
gcongr _ * ?_

Goal state after:
case hbc
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ rexp (-4 * √(log ↑N)) ≤ (↑N ^ (2 / ↑n) * (rexp (↑n - 2) * ↑n))⁻¹
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
⊢ (∃ b, ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1) ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
refine ⟨?_, fun h => ⟨_, h⟩⟩

Goal state after:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ (∃ b, ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1) → ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
⊢ G.edgeFinset.Nonempty ↔ G ≠ ⊥

Tactic:
Finset.nonempty_iff_ne_empty,

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
⊢ G.edgeFinset ≠ ∅ ↔ G ≠ ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ Fintype.card ↑(G.commonNeighbors v w) < G.degree v

Tactic:
rw [← Set.toFinset_card]
  refine Finset.card_lt_card <| Finset.ssubset_iff.mpr ⟨w, ?_, ?_⟩
  · rw [Set.mem_toFinset]
    apply notMem_commonNeighbors_right
  · simpa [Finset.insert_subset_iff, G.commonNeighbors_subset_neighborSet_left v w]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ a = ⊥

Tactic:
← P.sup_parts

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ P.parts.sup id = ⊥
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
x : α
hx : x ∈ ↑((image (fun x ↦ x ⊓ b) P.parts).erase ⊥)
y : α
hy : y ∈ ↑((image (fun x ↦ x ⊓ b) P.parts).erase ⊥)
hxy : x ≠ y
⊢ (Disjoint on id) x y

Tactic:
simp only [coe_erase, coe_image, Set.mem_sdiff, Set.mem_image, Set.mem_singleton_iff] at hx hy
    obtain ⟨⟨px, hpx, rfl⟩, _⟩ := hx
    obtain ⟨⟨py, hpy, rfl⟩, _⟩ := hy
    simpa [Function.onFun, id_eq]
      using (P.disjoint hpx hpy fun h => hxy (h ▸ rfl)).mono inf_le_left inf_le_left

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst✝ : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
x : α
hx : x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}
y : α
hy : y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}
hxy : x ⊓ b = y ⊓ b
⊢ x = y

Tactic:
by_contra hne
    simp only [Finset.mem_filter] at hx hy
    have : Disjoint (x ⊓ b) (y ⊓ b) := (P.disjoint hx.1 hy.1 hne).mono inf_le_left inf_le_left
    grind

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ ∃ t ∈ P.parts, a ∈ t

Tactic:
← P.sup_parts

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ P.parts.sup id
⊢ ∃ t ∈ P.parts, a ∈ t
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts

Tactic:
by
  obtain ⟨r, hrs, hr⟩ := P.part_surjOn.exists_bijOn_subset
  lift r to Finset α using s.finite_toSet.subset hrs
  exact ⟨r, mod_cast hrs, hr⟩

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts = 0
⊢ #s % #P.parts ≤ #P.parts

pp: case inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts > 0
⊢ #s % #P.parts ≤ #P.parts

Tactic:
· rw [h]
    rw [Finset.card_eq_zero, parts_eq_empty_iff, bot_eq_empty, ← Finset.card_eq_zero] at h
    rw [h]

Goal state after:
case inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts > 0
⊢ #s % #P.parts ≤ #P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
t : Finset α
ht : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = t
⊢ id t ⊆ s

Tactic:
obtain ⟨A, _, rfl⟩ := ht

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F A : Finset (Finset α)
left✝ : A ∈ F.powerset
⊢ id ({i ∈ s | ∀ t ∈ F, t ∈ A ↔ i ∈ t}) ⊆ s
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : Disjoint s s'
t : Finset β
⊢ Disjoint (interedges r s t) (interedges r s' t)

Tactic:
by
  rw [Finset.disjoint_left] at hs ⊢
  intro _ hx hy
  rw [mem_interedges_iff] at hx hy
  exact hs hx.1 hy.1

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ #((P.nonUniforms G ε).biUnion fun x ↦ x.1 ×ˢ x.2) ≤ ∑ x ∈ P.nonUniforms G ε, #x.1 * #x.2

Tactic:
← card_product

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ #((P.nonUniforms G ε).biUnion fun x ↦ x.1 ×ˢ x.2) ≤ ∑ x ∈ P.nonUniforms G ε, #(x.1 ×ˢ x.2)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ↑(#((P.nonUniforms G ε).biUnion fun x ↦
          match x with
          | (U, V) => U ×ˢ V)) <
    4 * ε * ↑(#A) ^ 2

Tactic:
by
  calc
    _ ≤ ∑ i ∈ P.nonUniforms G ε, (#i.1 * #i.2 : 𝕜) := by
        norm_cast; simp_rw [← card_product]; exact card_biUnion_le
    _ < _ := hP.sum_nonUniforms_lt' hA hε hG
    _ ≤ ε * (#A + #A) ^ 2 := by gcongr; exact P.card_parts_le_card
    _ = _ := by ring

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s₁ s₂ : Finset α
hs : (s₁, s₂) ∈ P.parts.offDiag
a✝¹ : ⟨(s₁, s₂), hs⟩ ∈ ↑P.parts.offDiag.attach
t₁ t₂ : Finset α
ht : (t₁, t₂) ∈ P.parts.offDiag
a✝ : ⟨(t₁, t₂), ht⟩ ∈ ↑P.parts.offDiag.attach
hst : ⟨(s₁, s₂), hs⟩ ≠ ⟨(t₁, t₂), ht⟩
u v : Finset α
huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
⊢ False

Tactic:
mem_offDiag

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s₁ s₂ : Finset α
hs✝ : (s₁, s₂) ∈ P.parts.offDiag
hs : (s₁, s₂).1 ∈ P.parts ∧ (s₁, s₂).2 ∈ P.parts ∧ (s₁, s₂).1 ≠ (s₁, s₂).2
a✝¹ : ⟨(s₁, s₂), hs✝⟩ ∈ ↑P.parts.offDiag.attach
t₁ t₂ : Finset α
ht✝ : (t₁, t₂) ∈ P.parts.offDiag
ht : (t₁, t₂).1 ∈ P.parts ∧ (t₁, t₂).2 ∈ P.parts ∧ (t₁, t₂).1 ≠ (t₁, t₂).2
a✝ : ⟨(t₁, t₂), ht✝⟩ ∈ ↑P.parts.offDiag.attach
hst : ⟨(s₁, s₂), hs✝⟩ ≠ ⟨(t₁, t₂), ht✝⟩
u v : Finset α
huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ ∀ B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts, #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m

Tactic:
intro B hB

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
hB : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts
⊢ #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 4 ^ #P.parts * ε ^ 5 ≤ 4 ^ #P.parts * ε ^ 4

Tactic:
gcongr _ * ?_

Goal state after:
case hbc
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ ε ^ 5 ≤ ε ^ 4
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (G.subgraphOfAdj h).support = {u, v}

Tactic:
by
  ext
  rw [Subgraph.mem_support]
  simp only [subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
  refine ⟨?_, fun h ↦ h.elim (fun hl ↦ ⟨v, .inl ⟨hl.symm, rfl⟩⟩) fun hr ↦ ⟨u, .inr ⟨rfl, hr.symm⟩⟩⟩
  rintro ⟨_, hw⟩
  exact hw.elim (fun h1 ↦ .inl h1.1.symm) fun hr ↦ .inr hr.2.symm

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 2 ^ (#P.parts - 1) * ↑m * (↑(#U) * ε) ≤ 2 ^ (#P.parts - 1) * ↑m * (2 * ↑(#(G.nonuniformWitness ε U V)))

Tactic:
gcongr _ * ?_

Goal state after:
case hbc
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ ↑(#U) * ε ≤ 2 * ↑(#(G.nonuniformWitness ε U V))
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
u v : V
⊢ (G'.deleteVerts s).Adj u v ↔ u ∈ G'.verts ∧ u ∉ s ∧ v ∈ G'.verts ∧ v ∉ s ∧ G'.Adj u v

Tactic:
simp [and_assoc]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ nil.support
⊢ List.count u (nil.takeUntil u h).support = 1

pp: case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
h : u ∈ (cons h✝ p✝).support
⊢ List.count u ((cons h✝ p✝).takeUntil u h).support = 1

Tactic:
· rw [mem_support_nil_iff] at h
    subst u
    simp

Goal state after:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
h : u ∈ (cons h✝ p✝).support
⊢ List.count u ((cons h✝ p✝).takeUntil u h).support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ (p.append p').support.tail = p.support.tail ++ p'.support.tail

Tactic:
by
  rw [support_append, List.tail_append_of_ne_nil (support_ne_nil _)]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
h : u ∈ (cons h✝ p✝).support
⊢ List.count u ((cons h✝ p✝).takeUntil u h).support = 1

Tactic:
cases h
    · simp
    · simp! only
      split_ifs with h' <;> rw [eq_comm] at h' <;> subst_vars <;> simp! [*, List.count_cons]

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : n = 0
hm0 : ¬m = 0
hnm : v = p.getVert (m - 1)
⊢ n = m

Tactic:
have hvp : v ∉ p.support := by aesop

Goal state after:
case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : n = 0
hm0 : ¬m = 0
hnm : v = p.getVert (m - 1)
hvp : v ∉ p.support
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
refine ⟨a, b, c, ?_⟩

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case h
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
xy : α × α
a✝ : xy ∈ univ
⊢ (regularityReduced P G (ε / 8) (ε / 4)).Adj xy.1 xy.2 → G.Adj xy.1 xy.2

Tactic:
exact fun hxy ↦ regularityReduced_le hxy

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
⊢ #univ * #A = #B

Tactic:
← card_product

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
⊢ #(univ ×ˢ A) = #B
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #s * #t ≤ Eₘ[s, t]

Tactic:
← card_product

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #(s ×ˢ t) ≤ Eₘ[s, t]
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #({x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}) =
    ∑ x ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) * #({xy ∈ s ×ˢ t | xy.1 * xy.2 = x})

Tactic:
← card_product

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #({x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}) =
    ∑ x ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x})
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: case neg
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := ⋯
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ⋯
x : σ → K
hx✝ : x ∉ S
i : ι
hi : i ∈ s
hx : (eval x) (f i) ≠ 0
⊢ 1 - (eval x) (f i) ^ (q - 1) = 0

Tactic:
rw [pow_card_sub_one_eq_one (eval x (f i)) hx, sub_self]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ toColex s ≤ toColex {a} ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)

Tactic:
simp only [toColex_le_toColex, mem_singleton, exists_eq_left]
  refine forall₂_congr fun b _ ↦ ?_; obtain rfl | hba := eq_or_ne b a <;> aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K ↥((Equiv.refl (Submodule K V)) H) = 1
v : ↥H
hv₀ : v ≠ 0
hv : ∀ (w : ↥H), ∃ c, c • v = w
⊢ ↑(K ∙ ↑v) = ↑H

Tactic:
Submodule.span_singleton_eq_range

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K ↥((Equiv.refl (Submodule K V)) H) = 1
v : ↥H
hv₀ : v ≠ 0
hv : ∀ (w : ↥H), ∃ c, c • v = w
⊢ (Set.range fun x ↦ x • ↑v) = ↑H
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case pos
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : D = D'
⊢ LinearIndepOn K id {D.rep, D'.rep}

pp: case neg
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : ¬D = D'
⊢ LinearIndepOn K id {D.rep, D'.rep}

Tactic:
· simpa [h] using D'.rep_nonzero

Goal state after:
case neg
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : ¬D = D'
⊢ LinearIndepOn K id {D.rep, D'.rep}
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
⊢ (if h : (crossProduct (a • ↑x✝⁴)) (b • ↑x✝¹) = 0 then x✝⁵ else ⟨(crossProduct (a • ↑x✝⁴)) (b • ↑x✝¹), ⋯⟩) ≈
    if h : (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁴ else ⟨(crossProduct ↑x✝⁴) ↑x✝¹, h⟩

Tactic:
LinearMap.map_smul_of_tower,

Goal state after:
F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
⊢ (if h : b • (a • crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁵ else ⟨b • (a • crossProduct ↑x✝⁴) ↑x✝¹, ⋯⟩) ≈
    if h : (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁴ else ⟨(crossProduct ↑x✝⁴) ↑x✝¹, h⟩
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal v

Tactic:
exact cross_orthogonal_left h

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
l : L
hs₀ : ¬#{l} = 0
hs₁ : #{l} = 1
p : P
hl : p ∉ l
⊢ #(t l) ≠ 0

Tactic:
exact Finset.card_ne_zero_of_mem (Set.mem_toFinset.mpr hl)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // a ∈ fixedPoints ⇑↑f } ⊕ { f // a ∉ fixedPoints ⇑↑f } ≃
    { f // fixedPoints ⇑f ⊆ {a} ∧ a ∈ fixedPoints ⇑f } ⊕ { f // fixedPoints ⇑f ⊆ {a} ∧ a ∉ fixedPoints ⇑f }

Tactic:
refine Equiv.sumCongr ?_ ?_
      · exact subtypeSubtypeEquivSubtypeInter
          (fun x : Perm α => fixedPoints x ⊆ {a})
          (a ∈ fixedPoints ·)
      · exact subtypeSubtypeEquivSubtypeInter
          (fun x : Perm α => fixedPoints x ⊆ {a})
          (a ∉ fixedPoints ·)

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
⊢ ∑ l, lineCount L (f l) = ∑ p ∈ map { toFun := f, inj' := hf₁ } univ, lineCount L p

Tactic:
rw [sum_map]; dsimp

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
⊢ some (f x) ≠ (Equiv.swap none (some a)) (some x)

Tactic:
have ne_1 : some x ≠ none := Option.some_ne_none _

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
⊢ some (f x) ≠ (Equiv.swap none (some a)) (some x)