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

Goal state before:
pp: case 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
⊢ #(Finset.map { toFun := Subtype.val, inj' := ⋯ } {a_1 | ↑x a_1 ≠ 0}) = p

Tactic:
rw [card_map]

Goal state after:
case 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
⊢ #{a_1 | ↑x a_1 ≠ 0} = p
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices
⊢ (2 ^ (k + 1) * n).bitIndices = map (fun x ↦ x + (k + 1)) n.bitIndices

Tactic:
rw [add_comm, pow_add, pow_one, mul_assoc, bitIndices_two_mul, ih, List.map_map, comp_add_right]

Goal state after:
case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices
⊢ map (fun x ↦ x + (k + 1)) n.bitIndices = map (fun x ↦ x + (1 + k)) n.bitIndices
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
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) ↔ ∃ a, a • w = v

Tactic:
constructor

Goal state after:
case mp
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v

case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ ¬LinearIndependent F ![v, w] ↔ (crossProduct v) w = 0

Tactic:
constructor

Goal state after:
case neg.mp
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ ¬LinearIndependent F ![v, w] → (crossProduct v) w = 0

case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ (crossProduct v) w = 0 → ¬LinearIndependent F ![v, w]
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
⊢ D' = D

Tactic:
← mk_rep D,

Goal state after:
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
⊢ D' = mk K D.rep ⋯
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
⊢ 1 ≤ #({l}.biUnion t)

Tactic:
Finset.singleton_biUnion,

Goal state after:
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
⊢ 1 ≤ #(t l)
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) ↔ f ∈ {f | fixedPoints ⇑f ⊆ {a}}

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) → f ∈ {f | fixedPoints ⇑f ⊆ {a}}

case mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ {f | fixedPoints ⇑f ⊆ {a}} → f ∈ fiber (some a)
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ Perm.decomposeOption.symm (some a, f) ∈ derangements (Option α) ∧
    Perm.decomposeOption (Perm.decomposeOption.symm (some a, f)) = (some a, f)

Tactic:
constructor

Goal state after:
case h.left
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ Perm.decomposeOption.symm (some a, f) ∈ derangements (Option α)

case h.right
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ Perm.decomposeOption (Perm.decomposeOption.symm (some a, f)) = (some a, f)
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
⊢ ⊤.toSimpleGraphInclusive = ⊤

Tactic:
ext

Goal state after:
V : Type u_1
x✝¹ x✝ : V
⊢ ⊤.toSimpleGraphInclusive.Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
⊢ ⊤.toSimpleGraphStrict = ⊤

Tactic:
ext

Goal state after:
V : Type u_1
x✝¹ x✝ : V
⊢ ⊤.toSimpleGraphStrict.Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
⊢ ⊥.toSimpleGraphInclusive = ⊥

Tactic:
ext

Goal state after:
V : Type u_1
x✝¹ x✝ : V
⊢ ⊥.toSimpleGraphInclusive.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
⊢ ⊥.toSimpleGraphStrict = ⊥

Tactic:
ext

Goal state after:
V : Type u_1
x✝¹ x✝ : V
⊢ ⊥.toSimpleGraphStrict.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.Digraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
ι✝ : Type u_2
κ✝ : ι✝ → Type u_2
f : (a : ι✝) → κ✝ a → Digraph V
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
ext

Goal state after:
ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
ι✝ : Type u_2
κ✝ : ι✝ → Type u_2
f : (a : ι✝) → κ✝ a → Digraph V
x✝¹ x✝ : V
⊢ (⨅ a, ⨆ b, f a b).Adj x✝¹ x✝ ↔ (⨆ g, ⨅ a, f a (g a)).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
this : ∀ (p : P), lineCount L p = n
⊢ lineCount L p = lineCount L q

Tactic:
by exact (this p).trans (this q).symm

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
⊢ ((antidiagonal n).attach.biUnion fun ijh ↦ pairwiseNode (treesOfNumNodesEq (↑ijh).1) (treesOfNumNodesEq (↑ijh).2)) =
    (antidiagonal n).biUnion fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
ext

Goal state after:
n : ℕ
a✝ : BinaryTree Unit
⊢ (a✝ ∈
      (antidiagonal n).attach.biUnion fun ijh ↦
        pairwiseNode (treesOfNumNodesEq (↑ijh).1) (treesOfNumNodesEq (↑ijh).2)) ↔
    a✝ ∈ (antidiagonal n).biUnion fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:

Tactic:
a •> (A⁻¹ * A) <• a⁻¹ ⊆ a •> (A⁻¹ * A) * A⁻¹ := op_smul_finset_subset_mul (by simpa)
      _ ⊆ A * (A⁻¹ * A) * A⁻¹ := by grw [smul_finset_subset_mul (by simpa)]
      _ = A⁻¹ * A := by
        simp_rw [← coe_inj, coe_mul]
        rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]

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
M : Type u_7
inst✝² : Zero 𝕜
inst✝¹ : LE α
inst✝ : SMulZeroClass M 𝕜
c : M
⊢ c • 0 = 0

Tactic:
ext

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
M : Type u_7
inst✝² : Zero 𝕜
inst✝¹ : LE α
inst✝ : SMulZeroClass M 𝕜
c : M
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (c • 0) a✝¹ b✝ = 0 a✝¹ b✝
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✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
⊢ f * (g + h) = f * g + f * h

Tactic:
ext

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (f * (g + h)) a✝¹ b✝ = (f * g + f * h) a✝¹ b✝
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✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
⊢ (f + g) * h = f * h + g * h

Tactic:
ext

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ ((f + g) * h) a✝¹ b✝ = (f * h + g * h) a✝¹ b✝
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✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
⊢ 0 * f = 0

Tactic:
ext

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (0 * f) a✝¹ b✝ = 0 a✝¹ b✝
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✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
⊢ f * 0 = 0

Tactic:
ext

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (f * 0) a✝¹ b✝ = 0 a✝¹ b✝
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✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
⊢ 1 * f = f

Tactic:
ext

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (1 * f) a✝¹ b✝ = f a✝¹ b✝
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✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
⊢ f * 1 = f

Tactic:
ext

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (f * 1) a✝¹ b✝ = f a✝¹ b✝
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✝⁵ : Preorder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
⊢ f • 0 = 0

Tactic:
ext

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Preorder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (f • 0) a✝¹ b✝ = 0 a✝¹ b✝
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✝⁵ : Preorder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g h : IncidenceAlgebra 𝕝 α
⊢ f • (g + h) = f • g + f • h

Tactic:
ext

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Preorder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g h : IncidenceAlgebra 𝕝 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (f • (g + h)) a✝¹ b✝ = (f • g + f • h) a✝¹ b✝
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✝⁵ : Preorder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f g : IncidenceAlgebra 𝕜 α
h : IncidenceAlgebra 𝕝 α
⊢ (f + g) • h = f • h + g • h

Tactic:
ext

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Preorder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f g : IncidenceAlgebra 𝕜 α
h : IncidenceAlgebra 𝕝 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ ((f + g) • h) a✝¹ b✝ = (f • h + g • h) a✝¹ b✝
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✝⁵ : Preorder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕝 α
⊢ 0 • f = 0

Tactic:
ext

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Preorder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕝 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (0 • f) a✝¹ b✝ = 0 a✝¹ b✝
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 𝕜 𝕝
⊢ (algebraMap 𝕜 𝕝) 1 • 1 = 1

Tactic:
ext

Goal state after:
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 𝕜 𝕝
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ ((algebraMap 𝕜 𝕝) 1 • 1) a✝¹ b✝ = 1 a✝¹ b✝
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
constructor

Goal state after:
case neg.left
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ count U (List.take (p.firstReturn + 1) (↑p ++ ↑q)) = count D (List.take (p.firstReturn + 1) (↑p ++ ↑q))

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
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ count U (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D])) =
      count D (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D])) ∧
    ∀ j < (↑p).length + 1,
      decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false

Tactic:
constructor

Goal state after:
case left
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ count U (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D])) =
    count D (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D]))

case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ ∀ j < (↑p).length + 1,
    decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
rw [ne_comm, iff_comm, ne_iff_lt_iff_le]
  exact DyckWord.zero_le p

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

Goal state before:
pp: case e'_5
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
⊢ X ^ ((i + 1) * 0) + ∑ k ∈ range (m - 1), X ^ ((i + 1) * (1 + k)) =
    1 + ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))

Tactic:
congrm $(by simp) + ?_

Goal state after:
case e'_5
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
⊢ ∑ k ∈ range (m - 1), X ^ ((i + 1) * (1 + k)) = ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hK : K ≤ 1
hS : S.Nonempty
⊢ 0 ≤ expansion K S A

Tactic:
nlinarith [mul_card_le_expansion (K := K) hS (A := A)]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hK : K < 1
hS : S.Nonempty
hA : A.Nonempty
this : 0 < ↑(#A)
⊢ 0 < expansion K S A

Tactic:
nlinarith [mul_card_le_expansion (K := K) hS (A := A)]

Goal state after:
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
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 : ℕ), powMulProdOneSubPow n✝ n x
n : ℕ
⊢ (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = (n + 1) * (3 * n + 4) / 2 + (2 * n + 3)

Tactic:
← Nat.add_mul_div_left _ _ (by simp)

Goal state after:
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 : ℕ), powMulProdOneSubPow n✝ n x
n : ℕ
⊢ (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = ((n + 1) * (3 * n + 4) + 2 * (2 * n + 3)) / 2
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
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 : ℕ), powMulProdOneSubPow n✝ n x
h : ∀ (n : ℕ), (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = (n + 1) * (3 * n + 4) / 2 + (2 * n + 3)
n : ℕ
⊢ (n + 1 + 1) * (3 * (n + 1) + 4) / 2 = (n + 1) * (3 * n + 4) / 2 + (3 * n + 5)

Tactic:
← Nat.add_mul_div_left _ _ (by simp)

Goal state after:
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 : ℕ), powMulProdOneSubPow n✝ n x
h : ∀ (n : ℕ), (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = (n + 1) * (3 * n + 4) / 2 + (2 * n + 3)
n : ℕ
⊢ (n + 1 + 1) * (3 * (n + 1) + 4) / 2 = ((n + 1) * (3 * n + 4) + 2 * (3 * n + 5)) / 2
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)
⊢ ↑(#(A * S)) - K * ↑(#A) ≤ (2 - ε) * ↑(#S) - (1 - ε / 2) * ↑(#S)

Tactic:
by gcongr; 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' : α
⊢ x = x' ∧ y = y' ∨ x = y' ∧ y = x' → G.IsLink e x' y'

Tactic:
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)

Goal state after:
case inl
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
⊢ G.IsLink e x y

case inr
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
⊢ G.IsLink e y x
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' : α
⊢ x = x' ∧ y = y' ∨ x = y' ∧ y = x' ↔ s(x, y) = s(x', y')

Tactic:
Sym2.eq_iff

Goal state after:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
x' y' : α
⊢ x = x' ∧ y = y' ∨ x = y' ∧ y = x' ↔ x = x' ∧ y = y' ∨ x = y' ∧ y = x'
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ noEdge ∅ β ≤ G

Tactic:
constructor

Goal state after:
case vertexSet_mono
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ autoParam (V(noEdge ∅ β) ⊆ V(G)) IsSubgraph.vertexSet_mono._autoParam

case isLink_mono
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, (noEdge ∅ β).IsLink e x y → G.IsLink e x y) IsSubgraph.isLink_mono._autoParam
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

Goal state after:
case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
⊢ G₁.Inc e = G₂.Inc f → G₁.IsLink e = G₂.IsLink f

case mpr
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
⊢ G₁.IsLink e = G₂.IsLink f → G₁.Inc e = G₂.Inc f