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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
v w : α
s : Finset α
n : ℕ
hc : (G ⊔ edge v w).IsNClique n s
hx : v ∈ s
⊢ #(s.erase v) = n - 1

Tactic:
by rw [card_erase_of_mem hx, hc.2]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
⊢ (cons hadj p).IsPath

Tactic:
refine cons_isPath_iff .. |>.mpr ⟨hp, fun hup ↦ h u (p.takeUntil u hup |>.cons hadj) ?_ ?_⟩

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ (cons hadj (p.takeUntil u hup)).IsSubwalk (cons hadj p)

case refine_2
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ (cons hadj (p.takeUntil u hup)).IsCycle
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Fintype α
f : completeGraph α ⊑ G
⊢ completeGraph (Fin (Fintype.card α)) ⊑ G

Tactic:
exact (Iso.completeGraph <| equivFin α).isContained'.trans f

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
hle : H ⊑ G
h : ¬H.CliqueFree n
⊢ ¬G.CliqueFree n

Tactic:
rw [not_cliqueFree_iff_top_isContained] at h ⊢

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
hle : H ⊑ G
h : completeGraph (Fin n) ⊑ H
⊢ completeGraph (Fin n) ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : x = y
⊢ completeGraph (Fin n) ⊑ G

Tactic:
rwa [← hx, e, hy, replaceVertex_self, not_cliqueFree_iff_top_isContained] at h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map (⇑f) G).IsClique ↑s
hn : #s ≠ 1
hs' : map f (s.preimage ⇑f ⋯) = s
⊢ #(s.preimage ⇑f ⋯) = #s

Tactic:
by rw [← card_map f, hs']

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : ε ≤ 0
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
apply (mul_nonpos_of_nonpos_of_nonneg (triangleRemovalBound_nonpos hε) _).trans

Goal state after:
case inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : ε ≤ 0
⊢ 0 ≤ ↑(#(G.cliqueFinset 3))

α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : ε ≤ 0
⊢ 0 ≤ ↑(Fintype.card α) ^ 3
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
x✝ : Finset (α ⊕ β ⊕ γ)
⊢ x✝ ∈ (graph t).cliqueSet 3 ↔ x✝ ∈ ⇑toTriangle '' ↑t

Tactic:
exact is3Clique_iff

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
x y : ℕ
hx : x ∈ L
x✝ : y ∈ L
⊢ x - (a + 1) < y - (a + 1) ↔ x < y

Tactic:
tsub_lt_tsub_iff_right (haL _ hx)

Goal state after:
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
x y : ℕ
hx : x ∈ L
x✝ : y ∈ L
⊢ x < y ↔ x < y
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : Finset α → (a : α) → β a
⊢ ∃ χ, ∀ (s : Finset α), ∃ t, s ⊆ t ∧ ∀ x ∈ s, χ x = g t x

Tactic:
classical
  let instTop (a : α) : TopologicalSpace (β a) := ⊥
  have instDiscr (a : α) : DiscreteTopology (β a) := discreteTopology_bot _
  let e (s : Finset α) : Set ((a : α) → β a) := {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
  have (s : Finset α) : s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ x, f x = g t x} = e s := by simp [e]
  have he' (s : Finset α) : IsClosed (e s) := by
    rw [← this]
    exact (isClosed_discrete _).preimage (by fun_prop)
  have he'' (B : Finset (Finset α)) : (⋂ i ∈ B, e i).Nonempty := by
    refine ⟨g (B.biUnion id), ?_⟩
    simp only [Set.mem_iInter, Set.mem_ofPred_eq, e]
    intro i hi
    exact ⟨_, subset_biUnion_of_mem id hi, by simp⟩
  simpa using! CompactSpace.iInter_nonempty he' he''

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
⊢ toColex (cons a s ha) ≤ toColex (cons b s hb) ↔ a ≤ b

Tactic:
rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
⊢ ∀ (a b : { v // v ≠ 0 }), (projectivizationSetoid K V) a b → (projectivizationSetoid L W) ⟨f ↑a, ⋯⟩ ⟨f ↑b, ⋯⟩

Tactic:
rintro ⟨u, hu⟩ ⟨v, hv⟩ ⟨a, ha⟩
      use Units.map σ.toMonoidHom a
      dsimp at ha ⊢
      simp [f.map_smulₛₗ, ← ha, Units.smul_def]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ toColex (s.erase a) ≤ toColex (t.erase m)

Tactic:
rw [eq_of_subset_of_card_le this]

Goal state after:
case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ #(s.erase a) ≤ #(t.erase m)
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁

Tactic:
← sdiff_eq_empty_iff_subset

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
⊢ 𝒜₁ \ 𝒜₂ = ∅ ∨ 𝒜₂ \ 𝒜₁ = ∅
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case inr.h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ (crossProduct ((crossProduct v) w)) (-(crossProduct v) w) = 0

Tactic:
map_neg,

Goal state after:
case inr.h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ -(crossProduct ((crossProduct v) w)) ((crossProduct v) w) = 0
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case inr.h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ -(crossProduct ((crossProduct v) w)) ((crossProduct v) w) = 0

Tactic:
_root_.cross_self,

Goal state after:
case inr.h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ -0 = 0
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)
⊢ v.cross w = w.cross v

Tactic:
by
  rcases eq_or_ne v w with rfl | h
  · rfl
  · induction v with | h v hv =>
    induction w with | h w hw =>
    rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
      ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]

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

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑((k + (n - k)).factorial / k.factorial) / ↑n.factorial = (-1) ^ k / ↑k.factorial

Tactic:
add_tsub_cancel_of_le h_le

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑(n.factorial / k.factorial) / ↑n.factorial = (-1) ^ k / ↑k.factorial
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ #(A * A) < 2 * #A

Tactic:
rw [← Nat.cast_lt (α := ℚ), Nat.cast_mul, Nat.cast_two]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ↑(#(A * A)) < 2 * ↑(#A)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a b c d x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ∀ {x : G}, x ∈ ↑A⁻¹ * ↑A → x⁻¹ ∈ ↑A⁻¹ * ↑A

Tactic:
intro x
    simp only [Set.mem_mul, Set.mem_inv, coe_inv, forall_exists_index, mem_coe,
      and_imp]
    rintro a ha b hb rfl
    exact ⟨b⁻¹, by simpa using hb, a⁻¹, ha, by simp⟩

Goal state after:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
this : 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#A) ^ 2
⊢ #(A⁻¹ * A) < 2 * #A

Tactic:
rw [← Nat.cast_lt (α := ℚ), Nat.cast_mul, Nat.cast_two]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
this : 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#A) ^ 2
⊢ ↑(#(A⁻¹ * A)) < 2 * ↑(#A)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ {l₁ l₂ : ℙ K (Fin 3 → K)} → l₁ ≠ l₂ → ℙ K (Fin 3 → K)

Tactic:
by
      intro v w _
      exact cross v w

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ {p₁ p₂ : ℙ K (Fin 3 → K)} → p₁ ≠ p₂ → ℙ K (Fin 3 → K)

Tactic:
by
      intro v w _
      exact cross v w

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case e_a
m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
Finset.prod_multiset_map_count

Goal state after:
case e_a
m : Multiset ℕ
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case refine_3
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ a •> ↑H = ↑H <• a

Tactic:
· simpa [H, invMulSubgroup_eq_inv_mul, ← coe_inv, ← coe_mul, ← coe_smul_finset]
      using smul_inv_mul_eq_inv_mul_opSMul h ha

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
⊢ mu 𝕜 = mu' 𝕜

Tactic:
exact left_inv_eq_right_inv (mu_mul_zeta _ _) (zeta_mul_mu' _ _)

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case neg
p : DyckWord
h : ¬p = 0
⊢ (ofTree p.insidePart.toTree).nest + ofTree p.outsidePart.toTree = p

Tactic:
ofTree_toTree p.insidePart,

Goal state after:
case neg
p : DyckWord
h : ¬p = 0
⊢ p.insidePart.nest + ofTree p.outsidePart.toTree = p
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ HasSum (fun b ↦ powMulProdOneSubPow k b x + x ^ (3 * k + 5) * powMulProdOneSubPow (k + 1) b x) (0 - aux k 0 x)

Tactic:
rw [((hsum _).add ((hsum _).mul_left _)).hasSum_iff_tendsto_nat]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto
    (fun n ↦ ∑ i ∈ Finset.range n, (powMulProdOneSubPow k i x + x ^ (3 * k + 5) * powMulProdOneSubPow (k + 1) i x))
    atTop (𝓝 (0 - aux k 0 x))
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: case succ
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
⊢ (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2

Tactic:
stirlingFirst_self,

Goal state after:
case succ
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
⊢ (n + 1) * 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a : G
ha✝ : a ∈ n⁻¹ •> N
ha : a⁻¹ * a ∈ a⁻¹ •> n⁻¹ •> N
⊢ a⁻¹ ∈ n⁻¹ •> N

Tactic:
inv_mul_cancel

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a : G
ha✝ : a ∈ n⁻¹ •> N
ha : 1 ∈ a⁻¹ •> n⁻¹ •> N
⊢ a⁻¹ ∈ n⁻¹ •> N
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ HasSum (fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) (pentagonalSeries R)

Tactic:
by
  suffices HasSum ((fun n ↦ C ((pentagonalSeries R).coeff n) * X ^ n) ∘ pentagonal)
      (pentagonalSeries R) by
    convert this
    simp
  rw [pentagonal_injective.hasSum_iff fun n hn ↦ by simp [coeff_pentagonalSeries_eq_zero R hn]]
  simpa [monomial_eq_C_mul_X_pow] using (pentagonalSeries R).hasSum_of_monomials_self

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

Goal state before:
pp: n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ ruzsaSzemerediNumberNat (Fintype.card (α ⊕ α ⊕ α)) = ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
Fintype.card_sum,

Goal state after:
n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ ruzsaSzemerediNumberNat (Fintype.card α + (Fintype.card α + Fintype.card α)) = ruzsaSzemerediNumberNat (6 * n + 3)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
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)
this : (1 - K) * ↑(#((↑H).toFinset * S)) ≤ (1 - ε / 2) * ↑(#(↑H).toFinset)
⊢ (1 - K) * ↑(#((↑H).toFinset * S)) ≤ (1 - K) * ((2 / ε - 1) * ↑(#(↑H).toFinset))

Tactic:
apply le_of_le_of_eq this

Goal state after:
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)
this : (1 - K) * ↑(#((↑H).toFinset * S)) ≤ (1 - ε / 2) * ↑(#(↑H).toFinset)
⊢ (1 - ε / 2) * ↑(#(↑H).toFinset) = (1 - K) * ((2 / ε - 1) * ↑(#(↑H).toFinset))
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
⊢ G₁.Inc e = G₂.Inc f ↔ G₁.IsLink e = G₂.IsLink f

Tactic:
constructor <;> rintro h
  · ext x y
    rw [isLink_iff_inc, isLink_iff_inc, h]
  · simp [funext_iff, Inc, h]

Goal state after:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x ↦ x * m) '' N = N

Tactic:
apply hN.eq_of_subset

Goal state after:
case ht
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := ⋯
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x ↦ x * m) '' N ∈ S

case hts
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := ⋯
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x ↦ x * m) '' N ⊆ N
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x ↦ x * m) '' N = N
⊢ N ∩ {m' | m' * m = m} = N

Tactic:
apply hN.eq_of_subset

Goal state after:
case ht
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := ⋯
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x ↦ x * m) '' N = N
⊢ N ∩ {m' | m' * m = m} ∈ S

case hts
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := ⋯
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x ↦ x * m) '' N = N
⊢ N ∩ {m' | m' * m = m} ⊆ N
Module: Mathlib.Combinatorics.Matroid.Minor.Order

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤m M
⊢ ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D

Tactic:
by
  obtain ⟨C, D, rfl⟩ := h
  exact ⟨C ∩ M.E, (D ∩ M.E) \ C, inter_subset_right, sdiff_subset.trans inter_subset_right,
    disjoint_sdiff_right.mono_left inter_subset_left,
    by simp [delete_eq_delete_iff, inter_assoc, inter_sdiff_assoc]⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C D : Set α
hE : M.E ⊆ (M ／ C).E \ D
⊢ M = M ／ C ＼ D

Tactic:
contract_ground,

Goal state after:
α : Type u_1
M : Matroid α
C D : Set α
hE : M.E ⊆ (M.E \ C) \ D
⊢ M = M ／ C ＼ D
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ ¬(Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ (M ／ I).E ↔ Disjoint J I ∧ ¬M.Indep (J ∪ I) ∧ J ∪ I ⊆ M.E

Tactic:
contract_ground,

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB : Maximal (fun A ↦ (Disjoint A I ∧ M.Indep (A ∪ I)) ∧ A ⊆ X) J ∧ X ⊆ (M ／ I).E
⊢ M.IsBasis (J ∪ I) (X ∪ I)

Tactic:
contract_ground,

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB : Maximal (fun A ↦ (Disjoint A I ∧ M.Indep (A ∪ I)) ∧ A ⊆ X) J ∧ X ⊆ M.E \ I
⊢ M.IsBasis (J ∪ I) (X ∪ I)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
⊢ ∃ a > 0, ∃ b c, ∀ s ∈ S, C (a • s + b) = c

Tactic:
refine ⟨#s, Finset.card_pos.mpr ⟨l.proper.choose, ?_⟩, ∑ i ∈ sᶜ, ((l.idxFun i).map ?_).getD 0,
    c, ?_⟩

Goal state after:
case refine_1
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
⊢ ⋯.choose ∈ s

case refine_2
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
i : ι
⊢ ↥S → M

case refine_3
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
⊢ ∀ s_1 ∈ S, C (#s • s_1 + ∑ i ∈ sᶜ, (Option.map ?refine_2 (l.idxFun i)).getD 0) = c
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis I X
hJI : J ⊆ I
h : (M ／ J).IsBasis (I \ J) (X ∩ (M ／ J).E)
⊢ (M ／ J).IsBasis (I \ J) (X \ J)

Tactic:
contract_ground,

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis I X
hJI : J ⊆ I
h : (M ／ J).IsBasis (I \ J) (X ∩ (M.E \ J))
⊢ (M ／ J).IsBasis (I \ J) (X \ J)