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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : n ∈ {i | 1 ≤ i ∧ i ≤ p.length}
m : ℕ
hm : m ∈ {i | 1 ≤ i ∧ i ≤ p.length}
hnm : p.getVert n = p.getVert m
⊢ n = m

Tactic:
← SimpleGraph.Walk.length_tail_add_one
    (p.not_nil_of_tail_not_nil (not_nil_of_isCycle_cons hpc)),

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : n ∈ {i | 1 ≤ i ∧ i ≤ p.tail.length + 1}
m : ℕ
hm : m ∈ {i | 1 ≤ i ∧ i ≤ p.tail.length + 1}
hnm : p.getVert n = p.getVert m
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
⊢ ∀ (a : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)), False

Tactic:
intro f

Goal state after:
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)
⊢ False
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
B : Finset G
⊢ σₘ[∅, B] = 0

Tactic:
by simp [mulConst]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
⊢ σₘ[A, ∅] = 0

Tactic:
by simp [mulConst]

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑σₘ[A, B] = ↑(#(A * B)) / ↑(#A)

Tactic:
by simp [mulConst]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
⊢ δₘ[A] ≤ σₘ[A] ^ 2

Tactic:
obtain rfl | hA' := A.eq_empty_or_nonempty
  · simp
  refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A * #A)
  calc
    _ = #(A / A) * (#A : ℚ≥0) := by rw [← mul_assoc, divConst_mul_card]
    _ ≤ #(A * A) * #(A * A) := by norm_cast; exact ruzsa_triangle_inequality_div_mul_mul ..
    _ = _ := by rw [← mulConst_mul_card]; ring

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

Goal state before:
pp: case refine_2.refine_2
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ (∑ x_1, if ↑x x_1 ≠ 0 then 1 else 0) = 0

Tactic:
simpa only [f₁, map_sum, ZMod.pow_card_sub_one, map_pow, eval_X] using x.2.1

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

Goal state before:
pp: n : ℕ
⊢ (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n

Tactic:
by
  induction n using binaryRec with
  | zero => simp
  | bit b n hs =>
    have hrw : (fun i ↦ 2 ^ i) ∘ (fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i := by
      ext i; simp [pow_add, mul_comm]
    cases b
    · simpa [hrw, List.sum_map_mul_left]
    simp [hrw, List.sum_map_mul_left, hs, add_comm (a := 1)]

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

Goal state before:
pp: a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL✝ : (a :: map (fun x ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) (map (fun x ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), a' ∈ map (fun x ↦ x + a + 1) L₀ → a + 1 ≤ a'
x : ℕ
⊢ 2 ^ x * 2 ^ a * 2 = 2 ^ a * (2 * 2 ^ x)

Tactic:
ac_rfl

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : toColex s ≤ toColex t
htu : toColex t ≤ toColex u
has : a ∈ s
hat : a ∉ t
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
have ⟨c, hct, hcs, hbc⟩ := hst hb.1 hb.2.1

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : toColex s ≤ toColex t
htu : toColex t ≤ toColex u
has : a ∈ s
hat : a ∉ t
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b
c : α
hct : c ∈ ofColex (toColex t)
hcs : c ∉ ofColex (toColex s)
hbc : b ≤ c
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ ofColex (toColex t), a ∉ ofColex (toColex s) ∧ ∀ b ∈ ofColex (toColex s), b ∉ ofColex (toColex t) → b < a
u : Finset α := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Tactic:
have hu : u.Nonempty := h.imp fun _ ↦ mem_u.2

Goal state after:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ ofColex (toColex t), a ∉ ofColex (toColex s) ∧ ∀ b ∈ ofColex (toColex s), b ∉ ofColex (toColex t) → b < a
u : Finset α := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
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
D D' : ℙ K V
h : D ≠ D'
a : K
hD : a • D.rep = D'.rep
this : a ≠ 0
⊢ ∃ a, a • D.rep = D'.rep

Tactic:
refine ⟨(Ne.isUnit this).unit, by simp [← hD]⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Option α
f : Perm α
⊢ f ∈ fiber a ↔ ∃ F ∈ derangements (Option α), F none = a ∧ removeNone F = f

Tactic:
simp [RemoveNone.fiber, derangements]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : Perm α), x ∉ fiber none

Tactic:
intro f

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
⊢ f ∉ fiber none
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements α) = numDerangements (card α)

Tactic:
← card_derangements_invariant (card_fin _)

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements (Fin (card α))) = numDerangements (card α)
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ ↑(numDerangements (n + 1)) =
    ∑ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x)) +
      (-1) ^ (n + 1) * ↑((n + 1 + 1).ascFactorial (n + 1 - (n + 1)))

Tactic:
numDerangements_succ,

Goal state after:
case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ (↑n + 1) * ↑(numDerangements n) - (-1) ^ n =
    ∑ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x)) +
      (-1) ^ (n + 1) * ↑((n + 1 + 1).ascFactorial (n + 1 - (n + 1)))
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
simp_rw [Set.PairwiseDisjoint, Set.Pairwise, disjoint_left]

Goal state after:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∀ ⦃x : ℕ × ℕ⦄,
    x ∈ ↑(antidiagonal n) →
      ∀ ⦃y : ℕ × ℕ⦄,
        y ∈ ↑(antidiagonal n) →
          x ≠ y →
            ∀ ⦃a : BinaryTree Unit⦄,
              a ∈ pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2) →
                a ∉ pairwiseNode (treesOfNumNodesEq y.1) (treesOfNumNodesEq y.2)
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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
⊢ z •> A⁻¹ ⊆ a •> (A⁻¹ * A * (A⁻¹ * A))

Tactic:
mul_assoc _ A,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
⊢ z •> A⁻¹ ⊆ a •> (A⁻¹ * (A * (A⁻¹ * A)))
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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
⊢ a⁻¹ * z ∈ A⁻¹ * A * A

Tactic:
simp [← hz, mul_mem_mul, ha, hb, hc]

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

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i k : ℕ
hi : count U (List.take i (List.take (i + k) ↑p)) = count D (List.take i (List.take (i + k) ↑p))
⊢ count D (List.take i (List.take (i + k) ↑p) ++ List.drop i (List.take (i + k) ↑p)) ≤
    count U (List.take i (List.take (i + k) ↑p) ++ List.drop i (List.take (i + k) ↑p))

Tactic:
take_append_drop

Goal state after:
p q : DyckWord
h : p ≠ 0
i k : ℕ
hi : count U (List.take i (List.take (i + k) ↑p)) = count D (List.take i (List.take (i + k) ↑p))
⊢ count D (List.take (i + k) ↑p) ≤ count U (List.take (i + k) ↑p)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case neg
m n : ℕ
hm : ¬m = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
· by_cases hn : n = 0
    · simp [hn]
    · rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]]
      simp [count_replicate]

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

Goal state before:
pp: case inr.intro.calc_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑l

Tactic:
have ineq : #A * #A ≤ ((2 - K) * l + (K - 1) * #S) * #A := by
      calc
            (#A : ℝ) * #A
        _ = #A * #A⁻¹ := by simp
        _ = #(A ×ˢ A⁻¹) := by simp
        _ = ∑ z ∈ S, ↑(r z) := by
          norm_cast
          exact card_eq_sum_card_fiberwise fun xy hxy ↦
            mul_mem_mul (mem_product.mp hxy).1 (mem_product.mp hxy).2
        _ = ∑ z ∈ S with (K - 1) * #A < r z, ↑(r z) + ∑ z ∈ S with r z ≤ (K - 1) * #A, ↑(r z) := by
          norm_cast; simp_rw [← not_lt, sum_filter_add_sum_filter_not]
        _ ≤ ∑ z ∈ S with (K - 1) * #A < r z, ↑(#A)
          + ∑ z ∈ S with r z ≤ (K - 1) * #A, (K - 1) * #A := by
          gcongr with z hz z hz
          · exact convolution_le_card_left
          · simp_all
        _ = l * #A + (#S - l) * (K - 1) * #A := by
          simp [hk, ← not_lt, mul_assoc,
            ← S.card_filter_add_card_filter_not fun z ↦ (K - 1) * #A < r z]
        _ = ((2 - K) * l + (K - 1) * #S) * #A := by ring

Goal state after:
case inr.intro.calc_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
ineq : ↑(#A) * ↑(#A) ≤ ((2 - K) * ↑l + (K - 1) * ↑(#S)) * ↑(#A)
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑l
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ 0 ≠ p ↔ 0 < p

Tactic:
ne_iff_lt_iff_le

Goal state after:
p : DyckWord
⊢ 0 ≤ 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
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
k : ℕ
| x ^ (k + 1 + 1) * ∏ n ∈ Finset.range (k + 1), (1 - x ^ (n + 1))

Tactic:
rw [pow_add, pow_add, mul_assoc (x ^ k), mul_comm (x ^ k), mul_assoc (x ^ 1 * x ^ 1)]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
k : ℕ
| x ^ 1 * x ^ 1 * (x ^ k * ∏ n ∈ Finset.range (k + 1), (1 - x ^ (n + 1)))
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
hK : K ≤ 1
hS : S.Nonempty
hA : IsFragment K S A
hB : IsFragment K S B
hAB : (A ∩ B).Nonempty
⊢ IsFragment K S (A ∩ B)

Tactic:
by
  unfold IsFragment at *
  have := expansion_submodularity (S := S) (A := A) (B := B) (K := K)
  have := connectivity_le_expansion hK hS hAB
  have := connectivity_le_expansion hK hS <| hAB.mono inter_subset_union
  linarith

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
x' y' : α
⊢ G.IsLink e x' y' ↔ x = x' ∧ y = y' ∨ x = y' ∧ y = x'

Tactic:
by
  refine ⟨h.eq_and_eq_or_eq_and_eq, ?_⟩
  rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
  · assumption
  exact h.symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e✝ f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
e : β
he : e ∈ edgeSet
⊢ Std.Symm (IsLink e)

Tactic:
by
    simp_rw [symm_def, ← hIsLink]
    exact (G.isLink_symm <| hedgeSet ▸ he).symm

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
v : α
e : β
f : α → α'
h : G.Inc e v
⊢ (map f G).Inc e (f v)

Tactic:
obtain ⟨w, hw⟩ := h

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
v : α
e : β
f : α → α'
w : α
hw : G.IsLink e v w
⊢ (map f G).Inc e (f v)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
⊢ (M ＼ D).IsBasis' I X ↔ M.IsBasis' I (X \ D)

Tactic:
rw [isBasis'_iff_isBasis_inter_ground, delete_isBasis_iff, delete_ground, sdiff_eq,
    inter_comm M.E, ← inter_assoc, ← sdiff_eq, ← isBasis'_iff_isBasis_inter_ground,
    and_iff_left_iff_imp, inter_comm, ← inter_sdiff_assoc]

Goal state after:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis' I (X \ D) → Disjoint ((M.E ∩ X) \ D) D
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : ↥sᶜ
⊢ ↑(↑f ↑x) - #s < Fintype.card ↥sᶜ

Tactic:
have := (mem_prefixed.1 f.2 x).not.1 (Finset.mem_compl.1 x.2)

Goal state after:
X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : ↥sᶜ
this : ¬↑(↑f ↑x) < #s
⊢ ↑(↑f ↑x) - #s < Fintype.card ↥sᶜ
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : ↥sᶜ
⊢ ↑(↑f ↑x) - #s < Fintype.card ↥sᶜ

Tactic:
have := (mem_prefixed.1 f.2 x).not.1 (Finset.mem_compl.1 x.2)
        simp at this ⊢
        omega

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
s t : Finset X
inst✝ : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
⊢ ∀ ⦃a : Numbering X⦄, a.IsPrefix s → ¬a.IsPrefix t

Tactic:
intro f

Goal state after:
X : Type u_1
inst✝¹ : Fintype X
s t : Finset X
inst✝ : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
⊢ f.IsPrefix s → ¬f.IsPrefix t
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

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

Tactic:
by
  simp_rw [indep_iff, hI.contract_isBase_iff, union_subset_iff]
  exact ⟨fun ⟨B, ⟨hBI, hdj⟩, hJB⟩ ↦ ⟨disjoint_of_subset_left hJB hdj, _, hBI,
    hJB.trans subset_union_left, subset_union_right⟩,
    fun ⟨hdj, B, hB, hJB, hIB⟩ ↦ ⟨B \ I,⟨by simpa [union_eq_self_of_subset_right hIB],
      disjoint_sdiff_left⟩, subset_sdiff.2 ⟨hJB, hdj⟩ ⟩⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ M.Indep (I ∪ J) ↔ M.Indep (J \ I ∪ I)

Tactic:
sdiff_union_self,

Goal state after:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ M.Indep (I ∪ J) ↔ M.Indep (J ∪ I)
Module: Mathlib.Combinatorics.HalesJewett

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

pp: 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

pp: 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

Tactic:
· rw [hs, Finset.mem_filter]
    exact ⟨Finset.mem_univ _, l.proper.choose_spec⟩

Goal state after:
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 α
hI : M.Indep I
hB : (M ／ I).IsBasis J X
⊢ M.IsBasis (J ∪ I) (X ∪ I)

Tactic:
by
  simp_rw [IsBasis, hI.contract_indep_iff, contract_ground, subset_sdiff,
    maximal_subset_iff, and_imp] at hB
  refine hB.1.1.1.2.isBasis_of_maximal_subset (union_subset_union_left _ hB.1.1.2)
    fun K hK hKJ hKX ↦ ?_
  rw [union_subset_iff] at hKJ
  rw [hB.1.2 (t := K \ I) disjoint_sdiff_left (by simpa [sdiff_union_of_subset hKJ.2])
    (sdiff_subset_iff.2 (by rwa [union_comm])) (subset_sdiff.2 ⟨hKJ.1, hB.1.1.1.1⟩),
    sdiff_union_of_subset hKJ.2]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
⊢ Disjoint J (X \ I ∪ I) ∧ M.Indep (J ∪ I) ↔ M.Indep (J ∪ I) ∧ Disjoint X J

Tactic:
sdiff_union_self,

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
⊢ Disjoint J (X ∪ I) ∧ M.Indep (J ∪ I) ↔ M.Indep (J ∪ I) ∧ Disjoint X J
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ X \ C ∪ J ⊆ M.closure (I \ C ∪ C)

Tactic:
sdiff_union_self,

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ X \ C ∪ J ⊆ M.closure (I ∪ C)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ (M ／ X).loops = M.E \ X ∧ (M ／ X).E = M.E \ X

Tactic:
simp [hX.closure_eq]

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

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
⊢ ∀ ⦃a b c : WideSubquiver.toType V (geodesicSubtree r)⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f

Tactic:
by
      rintro a b c ⟨e, p, h⟩ ⟨f, q, j⟩
      cases h.symm.trans j
      constructor <;> rfl

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
B : Set (MvPolynomial σ R)
hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) fun b ↦ ↑b) g + r ∧
      (∀ (b : ↑B), m.toSyn (m.degree (↑b * g b)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c

Tactic:
by
  obtain ⟨g, r, H⟩ := m.div (b := fun (p : B) ↦ p) (fun b ↦ hB b b.prop) f
  exact ⟨g, r, H.1, H.2.1, fun c hc b hb ↦ H.2.2 c hc ⟨b, hb⟩⟩

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

Goal state before:
pp: case neg
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'.cons e = p'.comp (e.toPath.comp nil)

Tactic:
simp [comp_toPath_eq_cons]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mp
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ {0}ᶜ ⊆ A → A = Set.univ

pp: case mpr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ A = Set.univ → {0}ᶜ ⊆ A

Tactic:
· refine fun h => Set.eq_univ_of_forall fun x => ?_
    rcases eq_or_ne x 0 with rfl | hx
    · exact hA
    · exact h hx

Goal state after:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ A = Set.univ → {0}ᶜ ⊆ A