mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ HasSum (fun n ↦ C ((coeff n) (pentagonalSeries R)) * X ^ n) (pentagonalSeries R)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ HasSum (fun n ↦ C ((coeff n) (pentagonalSeries R)) * X ^ n) (pentagonalSeries R)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommRing α
s : Finset α
x : α × α × α
inst✝ : Fact (IsUnit 2)
a : α
ha : a ∈ s
y b : α
hb : b ∈ s
h : y + 2 * b = y + 2 * a
⊢ y + a = y + b

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommRing α
s : Finset α
x : α × α × α
inst✝ : Fact (IsUnit 2)
a : α
ha : a ∈ s
y b : α
hb : b ∈ s
h : y + 2 * b = y + 2 * a
⊢ a = b
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommRing α
s : Finset α
x : α × α × α
inst✝ : Fact (IsUnit 2)
a : α
ha : a ∈ s
y b : α
hb : b ∈ s
h : y + b = y + a
⊢ y + 2 * a = y + 2 * b

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommRing α
s : Finset α
x : α × α × α
inst✝ : Fact (IsUnit 2)
a : α
ha : a ∈ s
y b : α
hb : b ∈ s
h : y + b = y + a
⊢ a = b
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)
⊢ ↑S ⊆ ↑H * ↑Z

Tactic:
simpa using

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)
⊢ ↑S ⊆ ↑H * ↑S
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
this✝ : TopologicalSpace R := ⊥
this : DiscreteTopology R
h :
  ∀ (d : ℕ),
    Tendsto (fun i ↦ (coeff d) (∏ b ∈ i, (1 - X ^ (b + 1)))) (SummationFilter.unconditional ℕ).filter
      (𝓝 ((coeff d) (pentagonalSeries R)))
⊢ ∀ᶠ (s : Finset ℕ) in atTop, (coeff n) (∏ n ∈ s, (1 - X ^ (n + 1))) = (coeff n) (pentagonalSeries R)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
this✝ : TopologicalSpace R := ⊥
this : DiscreteTopology R
h :
  ∀ (d : ℕ),
    Tendsto (fun i ↦ (coeff d) (∏ b ∈ i, (1 - X ^ (b + 1)))) (SummationFilter.unconditional ℕ).filter
      (𝓝 ((coeff d) (pentagonalSeries R)))
⊢ ∃ a, ∀ (b : Finset ℕ), a ⊆ b → (coeff n) (∏ n ∈ b, (1 - X ^ (n + 1))) = (coeff n) (pentagonalSeries R)
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∀ᶠ (s : Finset ℕ) in atTop, (coeff n) (∏ n ∈ s, (1 - X ^ (n + 1))) = (coeff n) (pentagonalSeries R)

Tactic:
let : TopologicalSpace R := ⊥
  have : DiscreteTopology R := ⟨rfl⟩
  have h := (multipliable_one_sub_X_pow R).hasProd
  rw [tprod_one_sub_X_pow' R, HasProd, tendsto_iff_coeff_tendsto] at h
  simpa using h n

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
n : ℕ
⊢ ∀ᶠ (x' : Finset ℕ) in (SummationFilter.unconditional ℕ).filter,
    (coeff n) (∏ b ∈ x', (1 - X ^ (b + 1))) = (coeff n) (pentagonalSeries R)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
n : ℕ
⊢ ∃ a, ∀ (b : Finset ℕ), a ⊆ b → (coeff n) (∏ b ∈ b, (1 - X ^ (b + 1))) = (coeff n) (pentagonalSeries R)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case e_a
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)
⊢ (↑H).toFinset * Z = (↑H).toFinset * S

Tactic:
simpa using

Goal state after:
case e_a
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)
⊢ (↑H).toFinset * Z = (↑H).toFinset * S
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 n ↦ x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))
hlhs : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hrhs : Summable fun k ↦ (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
htail :
  Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
    atTop (𝓝 0)
h :
  ∀ (n : ℕ),
    ∏' (n : ℕ), (1 - x ^ (n + 1)) -
        (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x =
      ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))
h1 : ∀ (k : ℕ), pentagonal (↑k + 1) = (k + 1) * (3 * k + 2) / 2
h2 : ∀ (k : ℕ), pentagonal (-↑k) = k * (3 * k + 1) / 2
⊢ Tendsto
    (fun x_1 ↦
      ∏' (n : ℕ), (1 - x ^ (n + 1)) -
          (-1) ^ (x_1 + 1) * x ^ ((x_1 + 1) * (3 * x_1 + 4) / 2) * ∑' (n : ℕ), powMulProdOneSubPow x_1 n x -
        ∏' (n : ℕ), (1 - x ^ (n + 1)))
    atTop (𝓝 0)

Tactic:
simpa using

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 n ↦ x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))
hlhs : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hrhs : Summable fun k ↦ (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
htail :
  Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
    atTop (𝓝 0)
h :
  ∀ (n : ℕ),
    ∏' (n : ℕ), (1 - x ^ (n + 1)) -
        (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x =
      ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))
h1 : ∀ (k : ℕ), pentagonal (↑k + 1) = (k + 1) * (3 * k + 2) / 2
h2 : ∀ (k : ℕ), pentagonal (-↑k) = k * (3 * k + 1) / 2
⊢ Tendsto
    (fun x_1 ↦
      -((-1) ^ (x_1 + 1) * x ^ ((x_1 + 1) * (3 * x_1 + 4) / 2) *
          ∑' (n : ℕ), x ^ ((x_1 + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (x_1 + i + 1))))
    atTop (𝓝 0)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: ⊢ (fun n ↦ 2) =o[atTop] fun n ↦ ↑n / 3

Tactic:
simpa using

Goal state after:
⊢ Tendsto (fun x ↦ 3⁻¹ * ↑x) atTop atTop
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
hn : 6 ≤ n
this : 0 ≤ ↑n / 3 - 2
⊢ ‖(↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))‖ ≤ ↑(ruzsaSzemerediNumberNat n)

Tactic:
simpa using

Goal state after:
n : ℕ
hn : 6 ≤ n
this : 0 ≤ ↑n / 3 - 2
⊢ (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-(4 * √(Real.log ↑((n - 3) / 6)))) ≤ ↑(ruzsaSzemerediNumberNat n)
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
h : V(G) ⊆ X ∧ E(G) = ∅
e : β
x y : α
he : G.IsLink e x y
⊢ (noEdge X β).IsLink e x y

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
h : V(G) ⊆ X ∧ E(G) = ∅
e : β
x y : α
he : G.IsLink e x y
⊢ False
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
E₀ : Set β
h : G.restrict E₀ = G
⊢ E(G) ⊆ E₀

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
E₀ : Set β
h : G.restrict E₀ = G
⊢ E(G) ⊆ E₀
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
he : V(G) = ∅
e : β
x y : α
h : G.IsLink e x y
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
he : V(G) = ∅
e : β
x y : α
h : G.IsLink e x y
⊢ False
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ V(H.restrict F) ⊆ V(G.restrict F)

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ V(H) ⊆ V(G)
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
h : V(G) = ∅
e : β
x y : α
he : G.IsLink e x y
⊢ ⊥.IsLink e x y

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
h : V(G) = ∅
e : β
x y : α
he : G.IsLink e x y
⊢ False
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ x y, G.IsLink e x y
⊢ ∀ ⦃e : β⦄, e ∈ E → Std.Symm (G.IsLink e)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ x y, G.IsLink e x y
⊢ ∀ ⦃e : β⦄, e ∈ E(G) → Std.Symm (G.IsLink e)
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ x y, G.IsLink e x y
⊢ ∀ ⦃e : β⦄, e ∈ E → Std.Symm (G.IsLink e)

Tactic:
simpa [show E = E(G) by simp [Set.ext_iff, hE, G.edge_mem_iff_exists_isLink]]
      using G.isLink_symm

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inl.inl
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
val✝ : α
hm : m.idxFun i = Sum.inl val✝
⊢ Sum.inl a = Sum.inl val✝

Tactic:
simpa using

Goal state after:
case inl.inl
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
val✝ : α
hm : m.idxFun i = Sum.inl val✝
⊢ a = val✝
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inl.inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
val✝ : η
hm : m.idxFun i = Sum.inr val✝
⊢ Sum.inl a = Sum.inr val✝

Tactic:
simpa using

Goal state after:
case inl.inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
val✝ : η
hm : m.idxFun i = Sum.inr val✝
⊢ False
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inr.inl
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
a : α
hm : m.idxFun i = Sum.inl a
b : α
hba : b ≠ a
⊢ Sum.inr e = Sum.inl a

Tactic:
simpa using

Goal state after:
case inr.inl
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
a : α
hm : m.idxFun i = Sum.inl a
b : α
hba : b ≠ a
⊢ False
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inr.inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
hef : e ≠ f
⊢ False

Tactic:
simpa using

Goal state after:
case inr.inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
hef : e ≠ f
⊢ False
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_1.none
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : l.idxFun i = some a
hi : m.idxFun i = none
⊢ none = some a

Tactic:
simpa using

Goal state after:
case refine_1.none
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : l.idxFun i = some a
hi : m.idxFun i = none
⊢ False
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_1.some
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : l.idxFun i = some a
val✝ : α
hi : m.idxFun i = some val✝
⊢ some val✝ = some a

Tactic:
simpa using

Goal state after:
case refine_1.some
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : l.idxFun i = some a
val✝ : α
hi : m.idxFun i = some val✝
⊢ val✝ = a
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_2.none
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : m.idxFun i = some a
hi : l.idxFun i = none
⊢ none = some a

Tactic:
simpa using

Goal state after:
case refine_2.none
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : m.idxFun i = some a
hi : l.idxFun i = none
⊢ False
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_2.some
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : m.idxFun i = some a
val✝ : α
hi : l.idxFun i = some val✝
⊢ some val✝ = some a

Tactic:
simpa using

Goal state after:
case refine_2.some
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : m.idxFun i = some a
val✝ : α
hi : l.idxFun i = some val✝
⊢ val✝ = a
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: 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))

Tactic:
simpa using

Goal state after:
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' ∈ FP (Stream'.drop (n + n') a)
Module: Mathlib.Combinatorics.Hindman

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

Tactic:
have := Set.inter_subset_right (ih (succ p) ?_)

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

case h.cons'.refine_1
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)
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)
⊢ Fintype.card ↥s ≤ Fintype.card X

Tactic:
simpa using

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)
⊢ #s ≤ Fintype.card X
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:
simpa using

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)
⊢ ↑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ᶜ)
⊢ ↑n < Fintype.card X - #s

Tactic:
simpa using

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ᶜ)
⊢ ↑n < Fintype.card X - #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
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hn : ↑n < #s
⊢ ↑n < Fintype.card ↥s

Tactic:
simpa using

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
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ᶜ
x : X
hx : x ∈ s
⊢ ↑(g ⟨x, hx⟩) < #s

Tactic:
simpa using

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ᶜ
x : X
hx : x ∈ s
⊢ ↑(g ⟨x, hx⟩) < #s
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case mp
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ᶜ
x : X
hx : x ∈ s
⊢ ↑({ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
          invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
          left_inv := ⋯, right_inv := ⋯ }
        x) <
    #s

Tactic:
simpa using

Goal state after:
case mp
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ᶜ
x : X
hx : x ∈ s
⊢ ↑(g ⟨x, ⋯⟩) < #s
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ (M✶ ＼ C)✶ = M ↔ Disjoint C M.E

Tactic:
← dual_inj,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
⊢ (M✶ ＼ C)✶✶ = M✶ ↔ Disjoint C M.E
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
inst✝ : DecidableEq X
s : Finset X
⊢ #(prefixed s) = (#s)! * (Fintype.card X - #s)!

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝¹ : Fintype X
inst✝ : DecidableEq X
s : Finset X
⊢ #(prefixed s) = (#s)! * (Fintype.card X - #s)!
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ M ／ (X \ I ∪ I) = M ／ I ＼ (X \ I)

Tactic:
← dual_inj,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ (M ／ (X \ I ∪ I))✶ = (M ／ I ＼ (X \ I))✶
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ Disjoint {e} I

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ e ∉ I
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk i ⁻¹' I ⊆ Bs i
i : ι
⊢ (M i).IsBase (Sigma.mk i ⁻¹' univ.sigma Bs)

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk i ⁻¹' I ⊆ Bs i
i : ι
⊢ (M i).IsBase (Bs i)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
⊢ ∀ ⦃K : Set α⦄, Disjoint K J → M.Indep (K ∪ J) → K ⊆ X → I ⊆ K ∪ J → K ⊆ I

Tactic:
exact fun K hJK hKJi hKX hIJK ↦ by
    simp [hIX.eq_of_subset_indep hKJi hIJK (union_subset hKX (hJI.trans hIX.subset))]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
⊢ (M ／ J).IsBasis' (I \ J) X

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
⊢ (M ／ J).IsBasis (I \ J) (X ∩ (M.E \ J))