mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ w.orthogonal (v.cross w)

Tactic:
by
  rw [orthogonal_comm]
  exact cross_orthogonal_right h

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
a₁✝ a₂✝ : Finset ℕ
⊢ (fun s ↦ ∑ i ∈ s, n ^ i) a₁✝ = (fun s ↦ ∑ i ∈ s, n ^ i) a₂✝ → a₁✝ = a₂✝

Tactic:
h

Goal state after:
n : ℕ
hn : 2 ≤ n
a₁✝ a₂✝ : Finset ℕ
h : (fun s ↦ ∑ i ∈ s, n ^ i) a₁✝ = (fun s ↦ ∑ i ∈ s, n ^ i) 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
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
x a : G
ha : a ∈ A
⊢ a •> (x <• a) ∈ A <• a ↔ a * x ∈ A

Tactic:
smul_comm,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
x a : G
ha : a ∈ A
⊢ a •> x <• a ∈ A <• a ↔ a * x ∈ A
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ ↑(derangements (Option α)) ≃ (a : α) × ↑{f | fixedPoints ⇑f ⊆ {a}}

Tactic:
by
  have fiber_none_is_false : Equiv.RemoveNone.fiber (@none α) → False := by
    rw [Equiv.RemoveNone.fiber_none]
    exact IsEmpty.false
  calc
    derangements (Option α) ≃ Equiv.Perm.decomposeOption '' derangements (Option α) :=
      Equiv.image _ _
    _ ≃ Σ a : Option α, ↥(Equiv.RemoveNone.fiber a) := setProdEquivSigma _
    _ ≃ Σ a : α, ↥(Equiv.RemoveNone.fiber (some a)) :=
      sigmaOptionEquivOfSome _ fiber_none_is_false
    _ ≃ Σ a : α, { f : Perm α | fixedPoints f ⊆ {a} } := by
      simp_rw [Equiv.RemoveNone.fiber_some]
      rfl

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
x : G
hA : ↑(#(B * A)) < K * ↑(#A)
hx : x ∈ B⁻¹ * B
⊢ (2 - K) * ↑(#A) < ↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = x}))

Tactic:
simp only [mem_mul, mem_inv, exists_exists_and_eq_and] at hx
  obtain ⟨a, ha, b, hb, rfl⟩ := hx
  rw [card_mul_inv_eq_convolution_inv]
  simpa [card_smul_inter_smul] using lt_card_smul_inter_smul hA ha hb

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

Goal state before:
pp: ι : Sort u_1
V : Type u_2
a b : V
f : ι → Digraph V
⊢ (⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b

Tactic:
by simp [iSup]

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

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
hK₁ : 1 < K
hKφ : K < φ
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
hA₁ : ↑(#(∅⁻¹ * ∅)) ≤ K * ↑(#∅)
hA₂ : ↑(#(∅ * ∅⁻¹)) ≤ K * ↑(#∅)
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑∅ * ↑∅⁻¹

Tactic:
exact ⟨⊥, inferInstance, ∅, by simp; positivity⟩

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

Goal state before:
pp: p : DyckWord
⊢ 2 * p.semilength = (↑p).length

Tactic:
nth_rw 1 [two_mul, semilength, p.count_U_eq_count_D, semilength]

Goal state after:
p : DyckWord
⊢ count D ↑p + count U ↑p = (↑p).length
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case e'_6
p : DyckWord
⊢ count U = countP fun a ↦ decide ¬(a == D) = true

Tactic:
rw [count]

Goal state after:
case e'_6
p : DyckWord
⊢ (countP fun x ↦ x == U) = countP fun a ↦ decide ¬(a == D) = true
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c : 𝕜
f : IncidenceAlgebra 𝕝 α
⊢ c • f = { toFun := fun c ↦ (algebraMap 𝕜 𝕝) c • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } c * f

Tactic:
ext a b hab; simp [if_pos hab, constSMul_apply, Algebra.smul_def]

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

Goal state before:
pp: case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ ∀ j < p.firstReturn, decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false

Tactic:
· intro j hj
      rw [take_append, show j + 1 - p.toList.length = 0 by lia,
        take_zero, append_nil]
      simpa using (count_D_lt_count_U_of_lt_firstReturn hj).ne'

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ y ≥ x, (mu 𝕜) x y * g y = ∑ y ≥ x, (mu 𝕜) x y * ∑ z ≥ y, f z

Tactic:
h

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

Goal state before:
pp: p q : DyckWord
h : p ≤ q
⊢ ↑p <:+: ↑q

Tactic:
induction h with

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

Goal state before:
pp: p q : DyckWord
h : p ≤ q
⊢ ↑p <:+: ↑q

Tactic:
by
  induction h with
  | refl => exact infix_refl _
  | tail _pm mq ih =>
    rename_i m r
    rcases eq_or_ne r 0 with rfl | hr
    · rw [insidePart_zero, outsidePart_zero, or_self] at mq
      rwa [mq] at ih
    · have : [U] ++ r.insidePart ++ [D] ++ r.outsidePart = r :=
        DyckWord.ext_iff.mp (nest_insidePart_add_outsidePart hr)
      grind

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≤ x, f y
x : α
⊢ f x = ∑ y ≤ x, (mu 𝕜) y x * g y

Tactic:
by
  convert! moebius_inversion_top (α := αᵒᵈ) f g h x using 3
  rw [← mu_toDual]; rfl

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

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Ring 𝕜
inst✝¹ : Preorder α
inst✝ : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬(x.1 ≤ y.1 ∧ x.2 ≤ y.2)
⊢ f x.1 y.1 * g x.2 y.2 = 0

Tactic:
not_and_or

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Ring 𝕜
inst✝¹ : Preorder α
inst✝ : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x.1 ≤ y.1 ∨ ¬x.2 ≤ y.2
⊢ f x.1 y.1 * g x.2 y.2 = 0
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

Goal state before:
pp: x y : ℤ
⊢ pentagonal x = pentagonal y → x = y

Tactic:
h

Goal state after:
x y : ℤ
h : pentagonal x = pentagonal y
⊢ x = y
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
i : ℕ
h✝ : p (i + 1)
⊢ ∑' (j : ℕ), X ^ ((i + 1) * j) = 1 + ∑' (j : ℕ), 1 • X ^ ((i + 1) * (j + 1))

Tactic:
rw [tsum_eq_zero_add' ?_]
      · simp
      simp_rw [pow_mul, pow_add]
      apply Summable.mul_right
      exact summable_pow_of_constantCoeff_eq_zero (by simp)

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i b : ℕ
hn : b ∈ range (m - 1)
⊢ X ^ ((i + 1) * (1 + b)) = (if b + 1 < m then 1 else 0) • X ^ ((i + 1) * (b + 1))

Tactic:
rw [add_comm 1 b]

Goal state after:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i b : ℕ
hn : b ∈ range (m - 1)
⊢ X ^ ((i + 1) * (b + 1)) = (if b + 1 < m then 1 else 0) • X ^ ((i + 1) * (b + 1))
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
a b : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
⊢ (fun i ↦ (↑i + 1) * m - 1) a = (fun i ↦ (↑i + 1) * m - 1) b → a = b

Tactic:
h

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
a b : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
h : (fun i ↦ (↑i + 1) * m - 1) a = (fun i ↦ (↑i + 1) * m - 1) b
⊢ a = b
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: case succ
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
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)
n : ℕ
ih :
  ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x
h : ∀ (n : ℕ), (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = (n + 1) * (3 * n + 4) / 2 + (2 * n + 3)
⊢ ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) *
        (1 - x ^ (2 * n + 3) - x ^ (3 * n + 5) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x) =
    ∑ x_1 ∈ Finset.range (n + 1), (-1) ^ x_1 * (x ^ (x_1 * (3 * x_1 + 1) / 2) - x ^ ((x_1 + 1) * (3 * x_1 + 2) / 2)) +
        (-1) ^ (n + 1) * (x ^ ((n + 1) * (3 * (n + 1) + 1) / 2) - x ^ ((n + 1 + 1) * (3 * (n + 1) + 2) / 2)) +
      (-1) ^ (n + 1 + 1) * x ^ ((n + 1 + 1) * (3 * (n + 1) + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x

Tactic:
h

Goal state after:
case succ
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
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)
n : ℕ
ih :
  ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x
h : ∀ (n : ℕ), (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = (n + 1) * (3 * n + 4) / 2 + (2 * n + 3)
⊢ ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) *
        (1 - x ^ (2 * n + 3) - x ^ (3 * n + 5) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
        (-1) ^ (n + 1) * (x ^ ((n + 1) * (3 * (n + 1) + 1) / 2) - x ^ ((n + 1) * (3 * n + 4) / 2 + (2 * n + 3))) +
      (-1) ^ (n + 1 + 1) * x ^ ((n + 1 + 1) * (3 * (n + 1) + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: case succ
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
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)
n : ℕ
ih :
  ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x
h✝ : ∀ (n : ℕ), (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = (n + 1) * (3 * n + 4) / 2 + (2 * n + 3)
h : ∀ (n : ℕ), (n + 1 + 1) * (3 * (n + 1) + 4) / 2 = (n + 1) * (3 * n + 4) / 2 + (3 * n + 5)
⊢ ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) *
        (1 - x ^ (2 * n + 3) - x ^ (3 * n + 5) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
        (-1) ^ (n + 1) * (x ^ ((n + 1) * (3 * (n + 1) + 1) / 2) - x ^ ((n + 1) * (3 * n + 4) / 2 + (2 * n + 3))) +
      (-1) ^ (n + 1 + 1) * x ^ ((n + 1 + 1) * (3 * (n + 1) + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x

Tactic:
h

Goal state after:
case succ
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
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)
n : ℕ
ih :
  ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x
h✝ : ∀ (n : ℕ), (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = (n + 1) * (3 * n + 4) / 2 + (2 * n + 3)
h : ∀ (n : ℕ), (n + 1 + 1) * (3 * (n + 1) + 4) / 2 = (n + 1) * (3 * n + 4) / 2 + (3 * n + 5)
⊢ ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) *
        (1 - x ^ (2 * n + 3) - x ^ (3 * n + 5) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
        (-1) ^ (n + 1) * (x ^ ((n + 1) * (3 * (n + 1) + 1) / 2) - x ^ ((n + 1) * (3 * n + 4) / 2 + (2 * n + 3))) +
      (-1) ^ (n + 1 + 1) * x ^ ((n + 1) * (3 * n + 4) / 2 + (3 * n + 5)) *
        ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : CommRing α
s✝ : Finset α
x✝ : α × α × α
s : Finset α
x a b : α
h : x = x ∧ x + a = x + b ∧ x + 2 * a = x + 2 * b
⊢ (x, a) = (x, b)

Tactic:
obtain rfl := add_right_injective _ h.2.1

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : CommRing α
s✝ : Finset α
x✝ : α × α × α
s : Finset α
x a : α
h : x = x ∧ x + a = x + a ∧ x + 2 * a = x + 2 * a
⊢ (x, a) = (x, a)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : CommRing α
s✝ : Finset α
x : α × α × α
s : Finset α
⊢ Function.Injective fun xa ↦ (xa.1, xa.1 + xa.2, xa.1 + 2 * xa.2)

Tactic:
rintro ⟨x, a⟩ ⟨y, b⟩ h
      simp only [Prod.ext_iff] at h
      obtain rfl := h.1
      obtain rfl := add_right_injective _ h.2.1
      rfl

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

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

Tactic:
div_le_iff₀ (zero_lt_three' ℝ),

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
h : H.IsNonloopAt e x
⊢ G.IsNonloopAt e x

Tactic:
obtain ⟨y, hxy, he⟩ := h
  exact ⟨y, hxy, he.mono hHG⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hV : V(H) = V(G)
h : H ≤i G
e : β
he : e ∈ E(G)
⊢ e ∈ E(H)

Tactic:
obtain ⟨_, _, hxy⟩ := G.exists_isLink_of_mem_edgeSet he
    exact h.isLink_of_mem_mem hxy (hV ▸ hxy.left_mem) (hV ▸ hxy.right_mem) |>.edge_mem

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
x y : α
⊢ (G₁.Inc e x ∧ G₁.Inc e y ∧ ∀ (z : α), G₁.Inc e z → z = x ∨ z = y) ↔
    G₂.Inc f x ∧ G₂.Inc f y ∧ ∀ (z : α), G₂.Inc f z → z = x ∨ z = y

Tactic:
h

Goal state after:
case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
x y : α
⊢ (G₂.Inc f x ∧ G₂.Inc f y ∧ ∀ (z : α), G₂.Inc f z → z = x ∨ z = y) ↔
    G₂.Inc f x ∧ G₂.Inc f y ∧ ∀ (z : α), G₂.Inc f z → z = x ∨ z = y
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
y : α
⊢ ¬G.IsNonloopAt e y

Tactic:
rintro ⟨z, hyz, hy⟩
  rw [← h.eq_of_inc hy.inc_left, ← h.eq_of_inc hy.inc_right] at hyz
  exact hyz rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x : α), G₁.Inc e x ↔ G₂.Inc e x
x✝² : β
x✝¹ x✝ : α
⊢ (G₁.Inc x✝² x✝¹ ∧ G₁.Inc x✝² x✝ ∧ ∀ (z : α), G₁.Inc x✝² z → z = x✝¹ ∨ z = x✝) ↔
    G₂.Inc x✝² x✝¹ ∧ G₂.Inc x✝² x✝ ∧ ∀ (z : α), G₂.Inc x✝² z → z = x✝¹ ∨ z = x✝

Tactic:
h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hG : G.Loopless
hle : H ≤ G
⊢ H.Loopless

Tactic:
rw [loopless_iff_forall_ne_of_adj] at hG ⊢

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hG : ∀ (u v : α), G.Adj u v → u ≠ v
hle : H ≤ G
⊢ ∀ (u v : α), H.Adj u v → u ≠ v
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}
⊢ ∃ m, m * m = m

Tactic:
rsuffices ⟨N, hN⟩ : ∃ N', Minimal (· ∈ S) N'

Goal state after:
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
⊢ ∃ m, m * m = m

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', Minimal (fun x ↦ x ∈ S) N'
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : D₁ ∩ M.E = D₂ ∩ M.E
⊢ M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)

Tactic:
h

Goal state after:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : D₁ ∩ M.E = D₂ ∩ M.E
⊢ M ＼ (D₂ ∩ M.E) = M ＼ (D₂ ∩ M.E)
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m : M
⊢ m ∈ FP a → ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p

Tactic:
h

Goal state after:
case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m : M
h : m ∈ FP a
⊢ ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m : M
h : m ∈ FP a
⊢ ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p

Tactic:
induction h with

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : Fintype X
s t : Finset X
inst✝ : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
ht : f.IsPrefix t
hst' : #s ≤ #t
⊢ False

pp: case inr
X : Type u_1
inst✝¹ : Fintype X
s t : Finset X
inst✝ : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
ht : f.IsPrefix t
hts' : #t ≤ #s
⊢ False

Tactic:
· exact hst <| hs.subset_of_card_le_card ht hst'

Goal state after:
case inr
X : Type u_1
inst✝¹ : Fintype X
s t : Finset X
inst✝ : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
ht : f.IsPrefix t
hts' : #t ≤ #s
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
⊢ m.toSyn (m.degree (m.subLTerm f)) < m.toSyn (m.degree f)

Tactic:
by
  rw [lt_iff_le_and_ne]
  refine ⟨degree_sub_LTerm_le f, ?_⟩
  classical
  intro hf'
  simp only [EmbeddingLike.apply_eq_iff_eq] at hf'
  have : m.subLTerm f ≠ 0 := by
    intro h
    simp only [h, degree_zero] at hf'
    exact hf hf'.symm
  rw [← coeff_degree_ne_zero_iff (m := m), hf'] at this
  apply this
  simp [subLTerm, coeff_monomial, leadingCoeff]

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case of_equiv
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
⊢ P = 0

Tactic:
| @of_equiv σ τ e h =>

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
⊢ ∃ h,
    (∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree) ∧
      f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h

Tactic:
let : LinearOrder σ := WellOrderingRel.isWellOrder.linearOrder

Goal state after:
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
⊢ ∃ h,
    (∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree) ∧
      f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
Module: Mathlib.Data.Set.Sups

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
c : α
⊢ c ∈ s ⊻ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = c

Tactic:
simp [(· ⊻ ·)]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case h
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
a✝ : 0 < x
hxm : x ≤ m
⊢ x % m = 1 → x = 1

Tactic:
h

Goal state after:
case h
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
a✝ : 0 < x
hxm : x ≤ m
h : x % m = 1
⊢ x = 1
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : SemilatticeSup α
s t : Finset α
c : α
⊢ c ∈ s ⊻ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = c

Tactic:
simp [(· ⊻ ·)]

Goal state after: