mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℝ := ⋯
hK : K < 1
ex : Finset G → ℝ := ⋯
κ : ℝ := ⋯
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)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
this : (1 - K) * ↑(#((↑H).toFinset * S)) ≤ (1 - ε / 2) * ↑(#(↑H).toFinset)
⊢ (1 - ε / 2) * ↑(#(↑H).toFinset) = (1 - K) * ((2 / ε - 1) * ↑(#(↑H).toFinset))

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := ⋯
hK : K < 1
ex : Finset G → ℝ := ⋯
κ : ℝ := ⋯
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)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
this : (1 - K) * ↑(#((↑H).toFinset * S)) ≤ (1 - ε / 2) * ↑(#(↑H).toFinset)
⊢ (1 - ε / 2) * ↑(#(↑H).toFinset) = (1 - K) * ((2 / ε - 1) * ↑(#(↑H).toFinset))
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
hn : 6 ≤ ↑n
⊢ 0 ≤ ↑n / 3 - 2

Tactic:
;

Goal state after:
n : ℕ
hn : 6 ≤ ↑n
⊢ 0 ≤ ↑n / 3 - 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)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
this : (1 - K) * ↑(#((↑H).toFinset * S)) ≤ (1 - ε / 2) * ↑(#(↑H).toFinset)
⊢ (1 - ε / 2) * ↑(Fintype.card ↥H) = ε / 2 * ((2 / ε - 1) * ↑(Fintype.card ↥H))

Tactic:
;

Goal state after:
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)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
this : (1 - K) * ↑(#((↑H).toFinset * S)) ≤ (1 - ε / 2) * ↑(#(↑H).toFinset)
⊢ (1 - ε / 2) * ↑(Fintype.card ↥H) = ε / 2 * ((2 / ε - 1) * ↑(Fintype.card ↥H))
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
he : e ∈ E(H)
⊢ H.IsNonloopAt e x ↔ G.IsNonloopAt e x

Tactic:
by
  simp_rw [Graph.IsNonloopAt, hHG.isLink_iff he]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ H ≤i G ↔ ∀ (e : β) (x y : α), G.IsLink e x y → x ∈ V(H) → y ∈ V(H) → e ∈ E(H)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ H ≤i G ↔ ∀ (e : β) (x y : α), G.IsLink e x y → x ∈ V(H) → y ∈ V(H) → e ∈ E(H)
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : H.IsLink e x y
hHG : H ≤c G
hin : x ∈ V(H)
⊢ y ∈ V(H)

Tactic:
;

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : H.IsLink e x y
hHG : H ≤c G
hin : x ∈ V(H)
⊢ y ∈ V(H)
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : H.IsLink e y x
hHG : H ≤c G
hin : y ∈ V(H)
⊢ x ∈ V(H)

Tactic:
;

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : H.IsLink e y x
hHG : H ≤c G
hin : y ∈ V(H)
⊢ x ∈ V(H)
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
⊢ [x ∈ V(H), y ∈ V(H), e ∈ E(H)].TFAE

Tactic:
tfae_have 1 → 2 := (hHG.mem_iff_of_isLink he).mp
  tfae_have 2 → 3 := (hHG.isLink_congr · |>.mpr he.symm |>.edge_mem)
  tfae_have 3 → 1 := (he.anti_of_mem hHG.le · |>.left_mem)
  tfae_finish

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
⊢ H ≤c G ↔ ∀ (x y : α), G.Adj x y → x ∈ V(H) → y ∈ V(H)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
⊢ H ≤c G ↔ ∀ (x y : α), G.Adj x y → x ∈ V(H) → y ∈ V(H)
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
⊢ ¬H ≤c G ↔ ∃ x y, G.Adj x y ∧ x ∈ V(H) ∧ y ∉ V(H)

Tactic:
by
  contrapose!; symm
  exact ⟨fun hncl ↦ ⟨hHG, fun e x ⟨y, hexy⟩ hxH =>
    hHG.isLink_of_mem_mem hexy hxH (hncl x y ⟨e, hexy⟩ hxH) |>.edge_mem⟩,
    fun hcl _ _ hexy ↦ (hcl.mem_iff_of_adj hexy).mp⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ y✝ : α
e✝ : β
G H✝ H G₁ G₂ : Graph α β
h₁ : H ≤ G₁
h₂ : H ≤ G₂
e : β
x y : α
h : H.IsLink e x y
⊢ { vertexSet := V(G₁) ∩ V(G₂), IsLink := fun e x y ↦ G₁.IsLink e x y ∧ G₂.IsLink e x y,
        edgeSet := {e | e ∈ E(G₁) ∩ E(G₂) ∧ ∀ (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y}, isLink_symm := ⋯,
        eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }.IsLink
    e x y

Tactic:
simp [h₁.isLink_mono h, h₂.isLink_mono h]

Goal state after:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case ht
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 : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x ↦ x * m) '' N ∈ S

pp: case hts
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 : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x ↦ x * m) '' N ⊆ N

Tactic:
· refine ⟨(continuous_const_mul m).isClosedMap _ N_closed, ⟨_, ⟨m, hm, rfl⟩⟩, ?_⟩
        rintro _ ⟨m'', hm'', rfl⟩ _ ⟨m', hm', rfl⟩
        exact ⟨m'' * m * m', N_mul _ (N_mul _ hm'' _ hm) _ hm', mul_assoc _ _ _⟩

Goal state after:
case hts
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 : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x ↦ x * m) '' N ⊆ N
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case refine_1.inl
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}
hcs : ∅ ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) ∅
⊢ Set.univ.Nonempty

Tactic:
apply Set.univ_nonempty

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι → α) → κ
hl : IsMono C l
⊢ IsMono (fun x ↦ C (⇑eα.symm ∘ ⇑eα ∘ x)) l

Tactic:
;

Goal state after:
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι → α) → κ
hl : IsMono C l
⊢ IsMono (fun x ↦ C (⇑eα.symm ∘ ⇑eα ∘ x)) l
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ m * m' ∈ FP a

Tactic:
exact FP.tail _ _ (hn _ hm')

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
⊢ ↑l.toSubspaceUnit a i = ↑l (a ()) i

Tactic:
;

Goal state after:
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
⊢ ↑l.toSubspaceUnit a i = ↑l (a ()) i
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
ι : Type u_6
inst✝ : Nonempty ι
x : α
x✝ : ι
⊢ ↑(diagonal α ι) x x✝ = x

Tactic:
;

Goal state after:
α : Type u_5
ι : Type u_6
inst✝ : Nonempty ι
x : α
x✝ : ι
⊢ ↑(diagonal α ι) x x✝ = x
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R = M ＼ (M.E \ (M ↾ R).E)

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R = M ＼ (M.E \ (M ↾ R).E)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R = M ＼ (M.E \ (M ↾ R).E)

Tactic:
delete_compl,

Goal state after:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R = M ↾ (M ↾ R).E
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
⊢ M ＼ D ≤r M

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
D : Set α
⊢ M ＼ D ≤r M
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n' (Stream'.drop n a)), m * m' ∈ FP (Stream'.drop n a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n' + n) a)
⊢ m * m' ∈ FP (Stream'.drop n a)

Tactic:
apply hn

Goal state after:
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n' (Stream'.drop n a)), m * m' ∈ FP (Stream'.drop n a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n' + n) a)
⊢ m' ∈ FP (Stream'.drop n' (Stream'.drop n a))
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
⊢ ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l

Tactic:
intro r

Goal state after:
case pos
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
h : M.IsBasis I X
hX : Disjoint X D
⊢ M.IsBasis I X ∧ Disjoint X D

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I D X : Set α
h : M.IsBasis I X
hX : Disjoint X D
⊢ M.IsBasis I X ∧ Disjoint X D
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : Fin (Fintype.card ↥s)
⊢ ↑(↑f ((Equiv.symm ↑f) ⟨↑n, ⋯⟩)) < #s

Tactic:
;

Goal state after:
X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : Fin (Fintype.card ↥s)
⊢ ↑(↑f ((Equiv.symm ↑f) ⟨↑n, ⋯⟩)) < #s
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : Fin (Fintype.card ↥sᶜ)
⊢ ¬↑(↑f ((Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩)) < #s

Tactic:
;

Goal state after:
X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : Fin (Fintype.card ↥sᶜ)
⊢ ¬↑(↑f ((Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩)) < #s
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : ℕ
hn : n < Fintype.card ↥sᶜ
⊢ (fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩) ((fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩) ⟨n, hn⟩) = ⟨n, hn⟩

Tactic:
;

Goal state after:
X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : ℕ
hn : n < Fintype.card ↥sᶜ
⊢ (fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩) ((fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩) ⟨n, hn⟩) = ⟨n, hn⟩
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hn : ¬↑n < #s
⊢ ↑n - #s < Fintype.card X - #s

Tactic:
;

Goal state after:
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hn : ¬↑n < #s
⊢ ↑n - #s < Fintype.card X - #s
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_3
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ C (#s • x + ∑ i ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0) = (fun v ↦ C (∑ i, ↑(v i))) (↑l ⟨x, xs⟩)

Tactic:
;

Goal state after:
case refine_3
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ C (#s • x + ∑ i ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0) = (fun v ↦ C (∑ i, ↑(v i))) (↑l ⟨x, xs⟩)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis J C
hdj : Disjoint C X
h_ind : M.Indep (I ∪ J)
⊢ (M ／ C).IsBasis I X

Tactic:
have h' := h.contract_isBasis hJC

Goal state after:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis J C
hdj : Disjoint C X
h_ind : M.Indep (I ∪ J)
h' : M.Indep (I \ C ∪ J) → (M ／ C).IsBasis (I \ C) (X \ C)
⊢ (M ／ C).IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ (M ／ C).IsNonloop e ↔ e ∈ M.E \ M.closure C

Tactic:
by
  rw [isNonloop_iff_mem_compl_loops, contract_ground, contract_loops_eq]
  refine ⟨fun ⟨he,heC⟩ ↦ ⟨he.1, fun h ↦ heC ⟨h, he.2⟩⟩,
    fun h ↦ ⟨⟨h.1, fun heC ↦ h.2 ?_⟩, fun h' ↦ h.2 h'.1⟩⟩
  rw [← closure_inter_ground]
  exact (M.subset_closure (C ∩ M.E)) ⟨heC, h.1⟩

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h_empty
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval : ∀ (x : PEmpty.{u_2 + 1} → R), (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) → (eval x) P = 0
m : PEmpty.{u_2 + 1} →₀ ℕ
d : PEmpty.{u_2 + 1}
⊢ m d = 0 d

Tactic:
;

Goal state after:
case h_empty
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval : ∀ (x : PEmpty.{u_2 + 1} → R), (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) → (eval x) P = 0
m : PEmpty.{u_2 + 1} →₀ ℕ
d : PEmpty.{u_2 + 1}
⊢ m d = 0 d
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i ↦ (M i).E)
x✝ : α
⊢ x✝ ∈ (Matroid.disjointSigma M h).E ↔ x✝ ∈ ⋃ i, (M i).E

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i ↦ (M i).E)
x✝ : α
⊢ x✝ ∈ (Matroid.disjointSigma M h).E ↔ x✝ ∈ ⋃ i, (M i).E
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
hc' : c ∉ r'.support
this : c ∈ r'.support ∪ ((monomial (m.degree f)) (m.leadingCoeff f)).support
⊢ c = m.degree f

Tactic:
rw [Finset.mem_union, Classical.or_iff_not_imp_left] at this

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
hc' : c ∉ r'.support
this : c ∉ r'.support → c ∈ ((monomial (m.degree f)) (m.leadingCoeff f)).support
⊢ c = m.degree f
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: case hle
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ ∀ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] ≤ f i

Tactic:
intro r

Goal state after:
case hle
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
r : Fin (Nat.succ 0).succ → D
⊢ r ∈ ω.tt ![![a, b], ![b, a]] → f ![a, b] ≤ f r
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : IsSStronglyConnected V
i j : V
⊢ Nonempty (Path i j)

Tactic:
;

Goal state after:
V : Type u_2
inst✝ : Quiver V
h : IsSStronglyConnected V
i j : V
⊢ Nonempty (Path i j)
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : IsSStronglyConnected V
i j : V
p : Path i j
h✝ : 0 < p.length
⊢ Nonempty (Path i j)

Tactic:
;

Goal state after:
V : Type u_2
inst✝ : Quiver V
h : IsSStronglyConnected V
i j : V
p : Path i j
h✝ : 0 < p.length
⊢ Nonempty (Path i j)
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h_sc : IsStronglyConnected V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
⊢ IsSStronglyConnected V

Tactic:
by
  intro i j
  obtain ⟨p₁⟩ := h_sc i i₀
  obtain ⟨p₂⟩ := h_sc j₀ j
  let p : Path i j := p₁.comp (e₀.toPath.comp p₂)
  have hp_pos : 0 < p.length := by
    simpa [p, Path.length_comp, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] using
      Nat.succ_pos (p₁.length + p₂.length)
  exact ⟨p, hp_pos⟩

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
⊢ ∀ i_1 ∈ S, IsRegular (m.leadingCoeff (X i - C i_1))

Tactic:
intro r

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
r : R
⊢ r ∈ S → IsRegular (m.leadingCoeff (X i - C r))
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
a b : V
p : Path a b
⊢ p.vertices.length = p.length + 1

Tactic:
by
  induction p with
  | nil => simp
  | cons p' e ih =>
    simp [vertices_cons, length_cons, ih]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Quiver V
R : Type u_2
inst✝ : Monoid R
w : V → V → R
a b c : V
p : Path a b
e : b ⟶ c
⊢ weight (fun {i j} x ↦ w i j) (p.cons e) = weight (fun {i j} x ↦ w i j) p * w b c

Tactic:
;

Goal state after:
V : Type u_1
inst✝¹ : Quiver V
R : Type u_2
inst✝ : Monoid R
w : V → V → R
a b c : V
p : Path a b
e : b ⟶ c
⊢ weight (fun {i j} x ↦ w i j) (p.cons e) = weight (fun {i j} x ↦ w i j) p * w b c
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
i : σ
⊢ 0 < #(S i)

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
i : σ
⊢ 0 < #(S i)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case nil.nil
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ : U
a✝ : (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩
⊢ ⟨u, Path.nil⟩ = ⟨u, Path.nil⟩

Tactic:
;

Goal state after:
case nil.nil
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ : U
a✝ : (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩
⊢ ⟨u, Path.nil⟩ = ⟨u, Path.nil⟩
Module: Mathlib.Combinatorics.Quiver.Schreier

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
x : SchreierGraph V ι
s : S
hs : ι s • (ι s)⁻¹ • x = x
⊢ ⟨(ι ((labelling V ι).map ⟨s, hs⟩))⁻¹ • x, ⟨s, ⋯⟩⟩ = ⟨(ι s)⁻¹ • x, ⟨s, hs⟩⟩

Tactic:
;

Goal state after:
V : Type u_1
M : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
x : SchreierGraph V ι
s : S
hs : ι s • (ι s)⁻¹ • x = x
⊢ ⟨(ι ((labelling V ι).map ⟨s, hs⟩))⁻¹ • x, ⟨s, ⋯⟩⟩ = ⟨(ι s)⁻¹ • x, ⟨s, hs⟩⟩