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

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
n : ℕ
hA : A.Nonempty
⊢ ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)

Tactic:
induction n with

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hC : C ∈ A.powerset.erase ∅
hCmin : ∀ x' ∈ A.powerset.erase ∅, ↑(#(C * B)) / ↑(#C) ≤ ↑(#(x' * B)) / ↑(#x')
⊢ ↑(#(B ^ m / B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ (m + n) * ↑(#A)

Tactic:
mem_erase,

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hC : C ≠ ∅ ∧ C ∈ A.powerset
hCmin : ∀ x' ∈ A.powerset.erase ∅, ↑(#(C * B)) / ↑(#C) ≤ ↑(#(x' * B)) / ↑(#x')
⊢ ↑(#(B ^ m / B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ (m + n) * ↑(#A)
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ #(A ∩ x •> B⁻¹) = A.convolution B x

Tactic:
by
  simp [card_inter_smul]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V → W
G G' : SimpleGraph V
h : G ≤ G'
u v : V
ha : G.Adj u v
huv : f u ≠ f v
⊢ (SimpleGraph.map f G').Adj (f u) (f v)

Tactic:
exact ⟨huv, _, _, h ha, rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case neg
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
w : α
hw : w ∈ s
hwx : f w < f x
y : α
hy : y ∈ s
⊢ (f w).succ ≤ (f y).succ

Tactic:
rw [(Nat.succ_le_of_lt hwx).antisymm (hs hx hw)]

Goal state after:
case neg
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
w : α
hw : w ∈ s
hwx : f w < f x
y : α
hy : y ∈ s
⊢ f x ≤ (f y).succ
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Subsingleton V
⊢ G.minDegree = 0

Tactic:
cases isEmpty_or_nonempty V

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Subsingleton V
h✝ : IsEmpty V
⊢ G.minDegree = 0

case inr
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Subsingleton V
h✝ : Nonempty V
⊢ G.minDegree = 0
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
⊢ G.minDegree ≤ H.minDegree

Tactic:
cases isEmpty_or_nonempty V

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
h✝ : IsEmpty V
⊢ G.minDegree ≤ H.minDegree

case inr
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
h✝ : Nonempty V
⊢ G.minDegree ≤ H.minDegree
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Subsingleton V
⊢ G.maxDegree = 0

Tactic:
cases isEmpty_or_nonempty V

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Subsingleton V
h✝ : IsEmpty V
⊢ G.maxDegree = 0

case inr
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Subsingleton V
h✝ : Nonempty V
⊢ G.maxDegree = 0
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
⊢ G.maxDegree ≤ k

Tactic:
cases isEmpty_or_nonempty V

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
h✝ : IsEmpty V
⊢ G.maxDegree ≤ k

case inr
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
h✝ : Nonempty V
⊢ G.maxDegree ≤ k
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ ⊤.maxDegree = Fintype.card V - 1

Tactic:
cases isEmpty_or_nonempty V

Goal state after:
case inl
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : IsEmpty V
⊢ ⊤.maxDegree = Fintype.card V - 1

case inr
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : Nonempty V
⊢ ⊤.maxDegree = Fintype.card V - 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ ⊤.minDegree = Fintype.card V - 1

Tactic:
cases isEmpty_or_nonempty V

Goal state after:
case inl
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : IsEmpty V
⊢ ⊤.minDegree = Fintype.card V - 1

case inr
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : Nonempty V
⊢ ⊤.minDegree = Fintype.card V - 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ G.minDegree ≤ (induce s G).minDegree

Tactic:
cases isEmpty_or_nonempty V

Goal state after:
case inl
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : IsEmpty V
⊢ G.minDegree ≤ (induce s G).minDegree

case inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
⊢ G.minDegree ≤ (induce s G).minDegree
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
a : α
⊢ a ∈ (image (fun a ↦ {b ∈ x | s a b}) x).sup id ↔ a ∈ x

Tactic:
simp_rw [sup_image, id_comp, mem_sup, mem_filter]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
a : α
⊢ (∃ i ∈ x, a ∈ x ∧ s i a) ↔ a ∈ x
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
hi : i ∈ Q
⊢ i ∈ R

Tactic:
rwa [hz2.2 _ (hQ hi), ← hz1.2 _ (hQ hi)]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe.coe
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
X : C
a b : ℤ
h : WithBotTop.coe a ≤ WithBotTop.coe b
⊢ IsIso ((t.eTruncLT.obj (WithBotTop.coe a)).map ((t.eTruncLTι (WithBotTop.coe b)).app X))

Tactic:
exact t.isIso_truncLT_map_truncLTι_app a b (by simpa using h) X

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
⊢ (image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset).sup id = s

Tactic:
by
      refine (Finset.sup_le fun t ht ↦ ?_).antisymm fun a ha ↦ ?_
      · rw [mem_image] at ht
        obtain ⟨A, _, rfl⟩ := ht
        exact s.filter_subset _
      · rw [mem_sup]
        refine
          ⟨{i ∈ s | ∀ t ∈ F, t ∈ {u ∈ F | a ∈ u} ↔ i ∈ t},
            mem_image_of_mem _ (mem_powerset.2 <| filter_subset _ _),
            mem_filter.2 ⟨ha, fun t ht ↦ ?_⟩⟩
        rw [mem_filter]
        exact and_iff_right ht

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

Goal state before:
pp: ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
a : α × β
⊢ a ∈ interedges r s (t.biUnion f) ↔ a ∈ t.biUnion fun b ↦ interedges r s (f b)

Tactic:
simp only [mem_interedges_iff, mem_biUnion]

Goal state after:
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
a : α × β
⊢ a.1 ∈ s ∧ (∃ a_1 ∈ t, a.2 ∈ f a_1) ∧ r a.1 a.2 ↔ ∃ a_1 ∈ t, a.1 ∈ s ∧ a.2 ∈ f a_1 ∧ r a.1 a.2
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G.edgeSet
s : Finset (Sym2 V)
inst✝ : Fintype ↑(G.deleteEdges ↑s).edgeSet
⊢ (G.deleteEdges ↑s).edgeFinset = G.edgeFinset \ s

Tactic:
by
  ext e
  simp [edgeSet_deleteEdges]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
f : G.Copy H
⊢ G.maxDegree ≤ H.maxDegree

Tactic:
cases isEmpty_or_nonempty V

Goal state after:
case inl
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
f : G.Copy H
h✝ : IsEmpty V
⊢ G.maxDegree ≤ H.maxDegree

case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
f : G.Copy H
h✝ : Nonempty V
⊢ G.maxDegree ≤ H.maxDegree
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
f : G.Copy H
hf : Surjective ⇑f
h✝ : Nonempty W
v : V
⊢ G.minDegree ≤ H.degree (f v)

Tactic:
grw [← f.degree_le, ← minDegree_le_degree]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ↑(G.neighborSet v) ≃ ↑(H.neighborSet v)
hfin : (G.neighborSet v).Finite
⊢ H.neighborSet v = G.neighborSet v

Tactic:
lift H.neighborSet v to Finset V using h.set_finite_iff.mp hfin with s hs

Goal state after:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
hfin : (G.neighborSet v).Finite
s : Finset V
hs : ↑s = H.neighborSet v
h : ↑(G.neighborSet v) ≃ ↑↑s
⊢ ↑s = G.neighborSet v
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: case cons.cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective ⇑f
u v u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ ⦃p' : G.Walk v✝¹ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : Walk.map f (cons h✝¹ p✝¹) = Walk.map f (cons h✝ p✝)
⊢ cons h✝¹ p✝¹ = cons h✝ p✝

Tactic:
simp only [map_cons, cons.injEq] at h
      grind

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u✝ : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
h : u ∈ (cons r p).support
hx : ¬v = u
⊢ u ∈ p.support

Tactic:
by
        cases h
        · exact (hx rfl).elim
        · assumption

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.dropUntil u h).darts <:+ p.darts

Tactic:
by
  grw [dropUntil_eq_drop, darts_copy, darts_drop, List.drop_suffix]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.takeUntil u h).support.tail ++ (c.dropUntil u h).support.tail ~r c.support.tail

Tactic:
← tail_support_append,

Goal state after:
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ ((c.takeUntil u h).append (c.dropUntil u h)).support.tail ~r c.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : 0 < n
h : (p.drop 1).IsPath
⊢ (p.drop n).IsPath

Tactic:
← Nat.add_sub_of_le hn,

Goal state after:
V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : 0 < n
h : (p.drop 1).IsPath
⊢ (p.drop (Nat.succ 0 + (n - Nat.succ 0))).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case succ.cons
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u v✝ : V
h✝¹ : G.Adj u v✝
p✝ : G.Walk v✝ v
h✝ : (cons h✝¹ p✝).length ≤ n + 1
h : p✝.length + 1 ≤ n + 1
⊢ (cons h✝¹ p✝).take (n + 1) = (cons h✝¹ p✝).copy ⋯ ⋯

Tactic:
Nat.add_le_add_iff_right

Goal state after:
case succ.cons
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u v✝ : V
h✝¹ : G.Adj u v✝
p✝ : G.Walk v✝ v
h✝ : (cons h✝¹ p✝).length ≤ n + 1
h : p✝.length ≤ n
⊢ (cons h✝¹ p✝).take (n + 1) = (cons h✝¹ p✝).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ G.IsNClique n s → H.IsNClique n s

Tactic:
simp_rw [isNClique_iff]

Goal state after:
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ G.IsClique ↑s ∧ #s = n → H.IsClique ↑s ∧ #s = n
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
⊢ p.length = ⋯.toWalk.length

Tactic:
by simp [hp.length_eq_one_of_mem_edges h]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ ε < 2⁻¹

Tactic:
refine lt_of_mul_lt_mul_right (α := 𝕜) (a := Fintype.card α ^ 2) ?_ (by positivity)
  calc
        ε * Fintype.card α ^ 2
    _ ≤ #G.edgeFinset := by simpa using hε.le_card_edgeFinset (by simp)
    _ ≤ (Fintype.card α).choose 2 := by gcongr; exact card_edgeFinset_le_card_choose_two
    _ < 2⁻¹ * Fintype.card α ^ 2 := by
      simpa [← div_eq_inv_mul] using Nat.choose_lt_pow_div (by positivity) le_rfl

Goal state after:
Module: Mathlib.Combinatorics.Compactness

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

Tactic:
have instDiscr (a : α) : DiscreteTopology (β a) := discreteTopology_bot _

Goal state after:
α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun a ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology (β a)
⊢ ∃ χ, ∀ (s : Finset α), ∃ t, s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H2
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![(c✝ • m✝) 1 * n✝ 2 - (c✝ • m✝) 2 * n✝ 1, (c✝ • m✝) 2 * n✝ 0 - (c✝ • m✝) 0 * n✝ 2,
      (c✝ • m✝) 0 * n✝ 1 - (c✝ • m✝) 1 * n✝ 0] =
    c✝ • ![m✝ 1 * n✝ 2 - m✝ 2 * n✝ 1, m✝ 2 * n✝ 0 - m✝ 0 * n✝ 2, m✝ 0 * n✝ 1 - m✝ 1 * n✝ 0]

Tactic:
smul_vec3,

Goal state after:
case H2
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![(c✝ • m✝) 1 * n✝ 2 - (c✝ • m✝) 2 * n✝ 1, (c✝ • m✝) 2 * n✝ 0 - (c✝ • m✝) 0 * n✝ 2,
      (c✝ • m✝) 0 * n✝ 1 - (c✝ • m✝) 1 * n✝ 0] =
    ![c✝ • (m✝ 1 * n✝ 2 - m✝ 2 * n✝ 1), c✝ • (m✝ 2 * n✝ 0 - m✝ 0 * n✝ 2), c✝ • (m✝ 0 * n✝ 1 - m✝ 1 * n✝ 0)]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H4
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![m✝ 1 * (c✝ • n✝) 2 - m✝ 2 * (c✝ • n✝) 1, m✝ 2 * (c✝ • n✝) 0 - m✝ 0 * (c✝ • n✝) 2,
      m✝ 0 * (c✝ • n✝) 1 - m✝ 1 * (c✝ • n✝) 0] =
    c✝ • ![m✝ 1 * n✝ 2 - m✝ 2 * n✝ 1, m✝ 2 * n✝ 0 - m✝ 0 * n✝ 2, m✝ 0 * n✝ 1 - m✝ 1 * n✝ 0]

Tactic:
smul_vec3,

Goal state after:
case H4
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![m✝ 1 * (c✝ • n✝) 2 - m✝ 2 * (c✝ • n✝) 1, m✝ 2 * (c✝ • n✝) 0 - m✝ 0 * (c✝ • n✝) 2,
      m✝ 0 * (c✝ • n✝) 1 - m✝ 1 * (c✝ • n✝) 0] =
    ![c✝ • (m✝ 1 * n✝ 2 - m✝ 2 * n✝ 1), c✝ • (m✝ 2 * n✝ 0 - m✝ 0 * n✝ 2), c✝ • (m✝ 0 * n✝ 1 - m✝ 1 * n✝ 0)]
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b ∉ t.erase m
⊢ b < a

Tactic:
mem_erase,

Goal state after:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : ¬(b ≠ m ∧ b ∈ t)
⊢ b < a
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 :
  ![w 0, w 1, w 2] 0 • ![v 0, v 1, v 2] = ![v 0, v 1, v 2] 0 • ![w 0, w 1, w 2] →
    -![w 0, w 1, w 2] 0 = 0 ∧ ![v 0, v 1, v 2] 0 = 0
h21 :
  ![w 0, w 1, w 2] 1 • ![v 0, v 1, v 2] = ![v 0, v 1, v 2] 1 • ![w 0, w 1, w 2] →
    -![w 0, w 1, w 2] 1 = 0 ∧ ![v 0, v 1, v 2] 1 = 0
h22 :
  ![w 0, w 1, w 2] 2 • ![v 0, v 1, v 2] = ![v 0, v 1, v 2] 2 • ![w 0, w 1, w 2] →
    -![w 0, w 1, w 2] 2 = 0 ∧ ![v 0, v 1, v 2] 2 = 0
⊢ False

Tactic:
smul_vec3,

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 :
  ![![w 0, w 1, w 2] 0 • v 0, ![w 0, w 1, w 2] 0 • v 1, ![w 0, w 1, w 2] 0 • v 2] =
      ![v 0, v 1, v 2] 0 • ![w 0, w 1, w 2] →
    -![w 0, w 1, w 2] 0 = 0 ∧ ![v 0, v 1, v 2] 0 = 0
h21 :
  ![![w 0, w 1, w 2] 1 • v 0, ![w 0, w 1, w 2] 1 • v 1, ![w 0, w 1, w 2] 1 • v 2] =
      ![v 0, v 1, v 2] 1 • ![w 0, w 1, w 2] →
    -![w 0, w 1, w 2] 1 = 0 ∧ ![v 0, v 1, v 2] 1 = 0
h22 :
  ![![w 0, w 1, w 2] 2 • v 0, ![w 0, w 1, w 2] 2 • v 1, ![w 0, w 1, w 2] 2 • v 2] =
      ![v 0, v 1, v 2] 2 • ![w 0, w 1, w 2] →
    -![w 0, w 1, w 2] 2 = 0 ∧ ![v 0, v 1, v 2] 2 = 0
⊢ False
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 :
  ![![w 0, w 1, w 2] 0 • v 0, ![w 0, w 1, w 2] 0 • v 1, ![w 0, w 1, w 2] 0 • v 2] =
      ![v 0, v 1, v 2] 0 • ![w 0, w 1, w 2] →
    -![w 0, w 1, w 2] 0 = 0 ∧ ![v 0, v 1, v 2] 0 = 0
h21 :
  ![![w 0, w 1, w 2] 1 • v 0, ![w 0, w 1, w 2] 1 • v 1, ![w 0, w 1, w 2] 1 • v 2] =
      ![v 0, v 1, v 2] 1 • ![w 0, w 1, w 2] →
    -![w 0, w 1, w 2] 1 = 0 ∧ ![v 0, v 1, v 2] 1 = 0
h22 :
  ![![w 0, w 1, w 2] 2 • v 0, ![w 0, w 1, w 2] 2 • v 1, ![w 0, w 1, w 2] 2 • v 2] =
      ![v 0, v 1, v 2] 2 • ![w 0, w 1, w 2] →
    -![w 0, w 1, w 2] 2 = 0 ∧ ![v 0, v 1, v 2] 2 = 0
⊢ False

Tactic:
smul_vec3,

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 :
  ![![w 0, w 1, w 2] 0 • v 0, ![w 0, w 1, w 2] 0 • v 1, ![w 0, w 1, w 2] 0 • v 2] =
      ![![v 0, v 1, v 2] 0 • w 0, ![v 0, v 1, v 2] 0 • w 1, ![v 0, v 1, v 2] 0 • w 2] →
    -![w 0, w 1, w 2] 0 = 0 ∧ ![v 0, v 1, v 2] 0 = 0
h21 :
  ![![w 0, w 1, w 2] 1 • v 0, ![w 0, w 1, w 2] 1 • v 1, ![w 0, w 1, w 2] 1 • v 2] =
      ![![v 0, v 1, v 2] 1 • w 0, ![v 0, v 1, v 2] 1 • w 1, ![v 0, v 1, v 2] 1 • w 2] →
    -![w 0, w 1, w 2] 1 = 0 ∧ ![v 0, v 1, v 2] 1 = 0
h22 :
  ![![w 0, w 1, w 2] 2 • v 0, ![w 0, w 1, w 2] 2 • v 1, ![w 0, w 1, w 2] 2 • v 2] =
      ![![v 0, v 1, v 2] 2 • w 0, ![v 0, v 1, v 2] 2 • w 1, ![v 0, v 1, v 2] 2 • w 2] →
    -![w 0, w 1, w 2] 2 = 0 ∧ ![v 0, v 1, v 2] 2 = 0
⊢ False
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b ∉ t.erase m
⊢ b < w

Tactic:
mem_erase,

Goal state after:
case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : ¬(b ≠ m ∧ b ∈ t)
⊢ b < w
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

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

Tactic:
← crossProduct_ne_zero_iff_linearIndependent,

Goal state after:
F : Type u_1
inst✝ : Field F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
⊢ (crossProduct w) v ≠ 0 ↔ ¬(crossProduct v) w = 0
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁
hst : toColex s = toColex t
⊢ False

Tactic:
simp only [toColex_inj] at hst
    exact ht.2 <| hst ▸ hs.1

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

Goal state before:
pp: n : ℕ
⊢ ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n

Tactic:
induction n with

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

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

Tactic:
induction n with

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2
step3 : ∑ i ∈ {i | i.1 ∈ i.2}ᶜ.toFinset, lineCount L i.1 = ∑ i ∈ {i | i.1 ∈ i.2}ᶜ.toFinset, pointCount P i.2
⊢ lineCount L p = pointCount P l

Tactic:
exact
      ((Finset.sum_eq_sum_iff_of_le fun i hi =>
              HasLines.pointCount_le_lineCount (by exact Set.mem_toFinset.mp hi)).mp
          step3.symm (p, l) (Set.mem_toFinset.mpr hpl)).symm

Goal state after: