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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝¹ : a ∈ t
h✝ : a ∈ u
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

pp: case neg
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝¹ : a ∈ t
h✝ : a ∉ u
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

pp: case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝¹ : a ∉ t
h✝ : a ∈ u
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

pp: case neg
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝¹ : a ∉ t
h✝ : a ∉ u
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝¹ : a ∈ t
h✝ : a ∈ u
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

case neg
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝¹ : a ∈ t
h✝ : a ∉ u
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝¹ : a ∉ t
h✝ : a ∈ u
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

case neg
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝¹ : a ∉ t
h✝ : a ∉ u
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1
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✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : NoAccidental t
⊢ (graph t).cliqueFinset 3 = map toTriangle t

Tactic:
by
  simp [cliqueFinset_eq_image, map_eq_image]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ δₘ[A, B] ≤ A.dens⁻¹

Tactic:
by
  rw [dens, inv_div, divConst]; gcongr; exact card_le_univ _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s₁ s₂ t₁ t₂ : Finset α
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
⊢ Eₘ[s₁, t₁] ≤ Eₘ[s₂, t₂]

Tactic:
unfold mulEnergy; gcongr

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
t : Finset α
h : 0 < Eₘ[∅, t]
⊢ False

pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s : Finset α
h : 0 < Eₘ[s, ∅]
⊢ False

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
t : Finset α
h : 0 < Eₘ[∅, t]
⊢ False

case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s : Finset α
h : 0 < Eₘ[s, ∅]
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case h₂.refine_1.ha
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
this : 0 < ε
⊢ 0 ≤ ↑(#(star hP G ε hU V))

pp: case hb
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
this : 0 < ε
⊢ 0 ≤ 4 ^ #P.parts

Tactic:
<;>

Goal state after:
case h₂.refine_1.ha
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
this : 0 < ε
⊢ 0 ≤ ↑(#(star hP G ε hU V))

case hb
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
this : 0 < ε
⊢ 0 ≤ 4 ^ #P.parts
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: ε : ℝ
hε : 0 < ε
n : ℕ
hn : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hs₁ : A ⊆ range n
hs₂ : #A = rothNumberNat n
hs₃ : ThreeAPFree ↑A
⊢ ¬ε * ↑n < ↑(#A)

Tactic:
exact fun hδn ↦ roth_3ap_theorem_nat ε hε hn _ hs₁ hδn.le hs₃

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

Goal state before:
pp: case h₁
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ (f₁ s a).totalDegree ≤ p - 1

pp: case h₂
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ (f₂ s a).totalDegree ≤ p - 1

Tactic:
<;>

Goal state after:
case h₁
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ (f₁ s a).totalDegree ≤ p - 1

case h₂
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ (f₂ s a).totalDegree ≤ p - 1
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case h₁
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ ∀ i ∈ univ, (X i ^ (p - 1)).totalDegree ≤ p - 1

pp: case h₂
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ ∀ i ∈ univ, (a ↑i • X i ^ (p - 1)).totalDegree ≤ p - 1

Tactic:
<;>

Goal state after:
case h₁
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ ∀ i ∈ univ, (X i ^ (p - 1)).totalDegree ≤ p - 1

case h₂
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ ∀ i ∈ univ, (a ↑i • X i ^ (p - 1)).totalDegree ≤ p - 1
Module: Mathlib.Combinatorics.Additive.SubsetSum

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
insert_subset : insert 0 A ⊆ (insert a A).subsetSum
vadd_subset : a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum
⊢ #(insert 0 A) + #A.subsetSum = #(insert 0 A) + #(a +ᵥ A.subsetSum)

Tactic:
by simp [vadd_finset_def, card_image_of_injOn]

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

Goal state before:
pp: case false
n : ℕ
hs : n.bitIndices.SortedLT
this : List.Pairwise (fun a b ↦ a < b) n.bitIndices
⊢ (bit false n).bitIndices.SortedLT

pp: case true
n : ℕ
hs : n.bitIndices.SortedLT
this : List.Pairwise (fun a b ↦ a < b) n.bitIndices
⊢ (bit true n).bitIndices.SortedLT

Tactic:
<;>

Goal state after:
case false
n : ℕ
hs : n.bitIndices.SortedLT
this : List.Pairwise (fun a b ↦ a < b) n.bitIndices
⊢ (bit false n).bitIndices.SortedLT

case true
n : ℕ
hs : n.bitIndices.SortedLT
this : List.Pairwise (fun a b ↦ a < b) n.bitIndices
⊢ (bit true n).bitIndices.SortedLT
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case bit.false
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
⊢ i ∈ (bit false n).bitIndices ↔ (bit false n).testBit i = true

pp: case bit.true
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
⊢ i ∈ (bit true n).bitIndices ↔ (bit true n).testBit i = true

Tactic:
<;>

Goal state after:
case bit.false
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
⊢ i ∈ (bit false n).bitIndices ↔ (bit false n).testBit i = true

case bit.true
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
⊢ i ∈ (bit true n).bitIndices ↔ (bit true n).testBit i = true
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case bit.false.zero
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
⊢ 0 ∈ (bit false n).bitIndices ↔ (bit false n).testBit 0 = true

pp: case bit.false.succ
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
n✝ : ℕ
⊢ n✝ + 1 ∈ (bit false n).bitIndices ↔ (bit false n).testBit (n✝ + 1) = true

pp: case bit.true.zero
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
⊢ 0 ∈ (bit true n).bitIndices ↔ (bit true n).testBit 0 = true

pp: case bit.true.succ
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
n✝ : ℕ
⊢ n✝ + 1 ∈ (bit true n).bitIndices ↔ (bit true n).testBit (n✝ + 1) = true

Tactic:
<;>

Goal state after:
case bit.false.zero
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
⊢ 0 ∈ (bit false n).bitIndices ↔ (bit false n).testBit 0 = true

case bit.false.succ
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
n✝ : ℕ
⊢ n✝ + 1 ∈ (bit false n).bitIndices ↔ (bit false n).testBit (n✝ + 1) = true

case bit.true.zero
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
⊢ 0 ∈ (bit true n).bitIndices ↔ (bit true n).testBit 0 = true

case bit.true.succ
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
n✝ : ℕ
⊢ n✝ + 1 ∈ (bit true n).bitIndices ↔ (bit true n).testBit (n✝ + 1) = true
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H1.h₀
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ (m₁✝ 1 + m₂✝ 1) * n✝ 2 - (m₁✝ 2 + m₂✝ 2) * n✝ 1 = m₁✝ 1 * n✝ 2 - m₁✝ 2 * n✝ 1 + (m₂✝ 1 * n✝ 2 - m₂✝ 2 * n✝ 1)

pp: case H1.h₁
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ (m₁✝ 2 + m₂✝ 2) * n✝ 0 - (m₁✝ 0 + m₂✝ 0) * n✝ 2 = m₁✝ 2 * n✝ 0 - m₁✝ 0 * n✝ 2 + (m₂✝ 2 * n✝ 0 - m₂✝ 0 * n✝ 2)

pp: case H1.h₂
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ (m₁✝ 0 + m₂✝ 0) * n✝ 1 - (m₁✝ 1 + m₂✝ 1) * n✝ 0 = m₁✝ 0 * n✝ 1 - m₁✝ 1 * n✝ 0 + (m₂✝ 0 * n✝ 1 - m₂✝ 1 * n✝ 0)

Tactic:
<;>

Goal state after:
case H1.h₀
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ (m₁✝ 1 + m₂✝ 1) * n✝ 2 - (m₁✝ 2 + m₂✝ 2) * n✝ 1 = m₁✝ 1 * n✝ 2 - m₁✝ 2 * n✝ 1 + (m₂✝ 1 * n✝ 2 - m₂✝ 2 * n✝ 1)

case H1.h₁
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ (m₁✝ 2 + m₂✝ 2) * n✝ 0 - (m₁✝ 0 + m₂✝ 0) * n✝ 2 = m₁✝ 2 * n✝ 0 - m₁✝ 0 * n✝ 2 + (m₂✝ 2 * n✝ 0 - m₂✝ 0 * n✝ 2)

case H1.h₂
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ (m₁✝ 0 + m₂✝ 0) * n✝ 1 - (m₁✝ 1 + m₂✝ 1) * n✝ 0 = m₁✝ 0 * n✝ 1 - m₁✝ 1 * n✝ 0 + (m₂✝ 0 * n✝ 1 - m₂✝ 1 * n✝ 0)
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H3.h₀
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ m✝ 1 * (n₁✝ 2 + n₂✝ 2) - m✝ 2 * (n₁✝ 1 + n₂✝ 1) = m✝ 1 * n₁✝ 2 - m✝ 2 * n₁✝ 1 + (m✝ 1 * n₂✝ 2 - m✝ 2 * n₂✝ 1)

pp: case H3.h₁
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ m✝ 2 * (n₁✝ 0 + n₂✝ 0) - m✝ 0 * (n₁✝ 2 + n₂✝ 2) = m✝ 2 * n₁✝ 0 - m✝ 0 * n₁✝ 2 + (m✝ 2 * n₂✝ 0 - m✝ 0 * n₂✝ 2)

pp: case H3.h₂
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ m✝ 0 * (n₁✝ 1 + n₂✝ 1) - m✝ 1 * (n₁✝ 0 + n₂✝ 0) = m✝ 0 * n₁✝ 1 - m✝ 1 * n₁✝ 0 + (m✝ 0 * n₂✝ 1 - m✝ 1 * n₂✝ 0)

Tactic:
<;>

Goal state after:
case H3.h₀
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ m✝ 1 * (n₁✝ 2 + n₂✝ 2) - m✝ 2 * (n₁✝ 1 + n₂✝ 1) = m✝ 1 * n₁✝ 2 - m✝ 2 * n₁✝ 1 + (m✝ 1 * n₂✝ 2 - m✝ 2 * n₂✝ 1)

case H3.h₁
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ m✝ 2 * (n₁✝ 0 + n₂✝ 0) - m✝ 0 * (n₁✝ 2 + n₂✝ 2) = m✝ 2 * n₁✝ 0 - m✝ 0 * n₁✝ 2 + (m✝ 2 * n₂✝ 0 - m✝ 0 * n₂✝ 2)

case H3.h₂
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ m✝ 0 * (n₁✝ 1 + n₂✝ 1) - m✝ 1 * (n₁✝ 0 + n₂✝ 0) = m✝ 0 * n₁✝ 1 - m✝ 1 * n₁✝ 0 + (m✝ 0 * n₂✝ 1 - m✝ 1 * n₂✝ 0)
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inl
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
b : α
x✝ : b ∈ s
⊢ ¬b = b → b ∉ s ∧ b ≤ b ↔ b ≤ b ∧ (b ∈ s → b = b)

pp: case inr
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
x✝ : b ∈ s
hba : b ≠ a
⊢ ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
b : α
x✝ : b ∈ s
⊢ ¬b = b → b ∉ s ∧ b ≤ b ↔ b ≤ b ∧ (b ∈ s → b = b)

case inr
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
x✝ : b ∈ s
hba : b ≠ a
⊢ ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h : (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a}
b : α
hb : b ∈ s
⊢ b ≠ a

pp: case refine_2
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h : ∀ b ∈ s, b < a
⊢ ¬s = {a}

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h : (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a}
b : α
hb : b ∈ s
⊢ b ≠ a

case refine_2
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h : ∀ b ∈ s, b < a
⊢ ¬s = {a}
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h✝ : a ∈ s
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x

pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h✝ : a ∉ s
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h✝ : a ∈ s
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x

case neg
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h✝ : a ∉ s
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 1 * (v 0 * w 1 - v 1 * w 0) - u 2 * (v 2 * w 0 - v 0 * w 2) =
    (u 2 * v 0 - u 0 * v 2) * w 2 - (u 0 * v 1 - u 1 * v 0) * w 1 +
      (v 1 * (u 0 * w 1 - u 1 * w 0) - v 2 * (u 2 * w 0 - u 0 * w 2))

pp: case h₁
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 2 * (v 1 * w 2 - v 2 * w 1) - u 0 * (v 0 * w 1 - v 1 * w 0) =
    (u 0 * v 1 - u 1 * v 0) * w 0 - (u 1 * v 2 - u 2 * v 1) * w 2 +
      (v 2 * (u 1 * w 2 - u 2 * w 1) - v 0 * (u 0 * w 1 - u 1 * w 0))

pp: case h₂
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * (v 2 * w 0 - v 0 * w 2) - u 1 * (v 1 * w 2 - v 2 * w 1) =
    (u 1 * v 2 - u 2 * v 1) * w 1 - (u 2 * v 0 - u 0 * v 2) * w 0 +
      (v 0 * (u 2 * w 0 - u 0 * w 2) - v 1 * (u 1 * w 2 - u 2 * w 1))

Tactic:
<;>

Goal state after:
case h₀
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 1 * (v 0 * w 1 - v 1 * w 0) - u 2 * (v 2 * w 0 - v 0 * w 2) =
    (u 2 * v 0 - u 0 * v 2) * w 2 - (u 0 * v 1 - u 1 * v 0) * w 1 +
      (v 1 * (u 0 * w 1 - u 1 * w 0) - v 2 * (u 2 * w 0 - u 0 * w 2))

case h₁
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 2 * (v 1 * w 2 - v 2 * w 1) - u 0 * (v 0 * w 1 - v 1 * w 0) =
    (u 0 * v 1 - u 1 * v 0) * w 0 - (u 1 * v 2 - u 2 * v 1) * w 2 +
      (v 2 * (u 1 * w 2 - u 2 * w 1) - v 0 * (u 0 * w 1 - u 1 * w 0))

case h₂
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * (v 2 * w 0 - v 0 * w 2) - u 1 * (v 1 * w 2 - v 2 * w 1) =
    (u 1 * v 2 - u 2 * v 1) * w 1 - (u 2 * v 0 - u 0 * v 2) * w 0 +
      (v 0 * (u 2 * w 0 - u 0 * w 2) - v 1 * (u 1 * w 2 - u 2 * w 1))
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 : ℙ K V
⊢ ∀ (a b : { v // v ≠ 0 }), (projectivizationSetoid K V) a b → K ∙ ↑a = K ∙ ↑b

Tactic:
by
    rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨x, rfl : x • b = a⟩
    exact Submodule.span_singleton_group_smul_eq _ x _

Goal state after:
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
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Tactic:
refine ⟨m, hmt, hms, fun a hma ↦ ⟨fun has ↦ not_imp_comm.1 (hm _ has) hma.asymm, fun hat ↦ ?_⟩⟩

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
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
a : α
hma : m < a
hat : a ∈ t
⊢ a ∈ s
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : (crossProduct v) w = 0
⊢ Quotient.mk'' ((fun v w ↦ if h : (crossProduct ↑v) ↑w = 0 then v else ⟨(crossProduct ↑v) ↑w, h⟩) ⟨v, hv⟩ ⟨w, hw⟩) =
    mk F v hv

pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : ¬(crossProduct v) w = 0
⊢ Quotient.mk'' ((fun v w ↦ if h : (crossProduct ↑v) ↑w = 0 then v else ⟨(crossProduct ↑v) ↑w, h⟩) ⟨v, hv⟩ ⟨w, hw⟩) =
    mk F ((crossProduct v) w) h

Tactic:
<;>

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : (crossProduct v) w = 0
⊢ Quotient.mk'' ((fun v w ↦ if h : (crossProduct ↑v) ↑w = 0 then v else ⟨(crossProduct ↑v) ↑w, h⟩) ⟨v, hv⟩ ⟨w, hw⟩) =
    mk F v hv

case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : ¬(crossProduct v) w = 0
⊢ Quotient.mk'' ((fun v w ↦ if h : (crossProduct ↑v) ↑w = 0 then v else ⟨(crossProduct ↑v) ↑w, h⟩) ⟨v, hv⟩ ⟨w, hw⟩) =
    mk F ((crossProduct v) w) h
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : (crossProduct v) w = 0
⊢ Quotient.mk'' (if h : True then ⟨v, hv⟩ else ⟨0, ⋯⟩) = mk F v hv

pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : ¬(crossProduct v) w = 0
⊢ Quotient.mk'' (if h : False then ⟨v, hv⟩ else ⟨(crossProduct v) w, ⋯⟩) = mk F ((crossProduct v) w) h

Tactic:
<;>

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : (crossProduct v) w = 0
⊢ Quotient.mk'' (if h : True then ⟨v, hv⟩ else ⟨0, ⋯⟩) = mk F v hv

case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : ¬(crossProduct v) w = 0
⊢ Quotient.mk'' (if h : False then ⟨v, hv⟩ else ⟨(crossProduct v) w, ⋯⟩) = mk F ((crossProduct v) w) h
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: 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
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
p₁ p₂ : P
hp₁ : ∀ x ∈ s, ¬p₁ ∉ x
hp₂ : ∀ x ∈ s, ¬p₂ ∉ x
⊢ p₁ = p₂

Tactic:
Classical.not_not

Goal state after:
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
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
p₁ p₂ : P
hp₁ : ∀ x ∈ s, p₁ ∈ x
hp₂ : ∀ x ∈ s, p₂ ∈ x
⊢ p₁ = p₂
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
x : Perm α
⊢ (∀ (a_1 : α), ¬a_1 ∉ {a} ↔ a_1 ∈ fixedPoints ⇑x) ↔ ∀ (x_1 : α), x_1 ∈ {a} ↔ x_1 ∈ fixedPoints ⇑x

Tactic:
Classical.not_not

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

Goal state before:
pp: case refine_2
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
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
hx : x ∈ ↑H
⊢ a * x ∈ ↑A

Tactic:
norm_cast
      rwa [← mul_mem_A_comm ha, ← smul_eq_mul, ← mem_inv_smul_finset_iff, inv_mem hx]

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

Goal state before:
pp: case ind.succ.succ.a
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ n + 1 < n + 1 + 1

pp: case ind.succ.succ.a
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ n < n + 1 + 1

Tactic:
<;>

Goal state after:
case ind.succ.succ.a
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ n + 1 < n + 1 + 1

case ind.succ.succ.a
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ n < n + 1 + 1
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case «0»
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
j : Fin 2
⊢ (A * Bᵀ) ((fun i ↦ i) ⟨0, ⋯⟩) j = 0 ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
j : Fin 2
⊢ (A * Bᵀ) ((fun i ↦ i) ⟨1, ⋯⟩) j = 0 ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
j : Fin 2
⊢ (A * Bᵀ) ((fun i ↦ i) ⟨0, ⋯⟩) j = 0 ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
j : Fin 2
⊢ (A * Bᵀ) ((fun i ↦ i) ⟨1, ⋯⟩) j = 0 ((fun i ↦ i) ⟨1, ⋯⟩) j