mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
n : ℕ
M : Fin n.succ → Type u_1
inst✝² : Semiring R
inst✝¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝ : (i : Fin n.succ) → Module R (M i)
x y : M 0 × ((i : Fin n) → M i.succ)
⊢ ∀ (i : Fin n), (consEquiv M).toFun (x + y) i.succ = ((consEquiv M).toFun x + (consEquiv M).toFun y) i.succ

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
n : ℕ
M : Fin n.succ → Type u_1
inst✝² : Semiring R
inst✝¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝ : (i : Fin n.succ) → Module R (M i)
c : R
x : M 0 × ((i : Fin n) → M i.succ)
⊢ ∀ (i : Fin n), (consEquiv M).toFun (c • x) i.succ = ((RingHom.id R) c • (consEquiv M).toFun x) i.succ

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
n : ℕ
f : M →ₗ[R] M₂ →ₗ[R] M₃
g : M →ₗ[R] M₂ →ₗ[R] Fin n → M₃
x y : M
z : M₂
⊢ ((f (x + y)).vecCons (g (x + y))) z = ((f x).vecCons (g x) + (f y).vecCons (g y)) z

Tactic:
by
      simp only [f.map_add, g.map_add, LinearMap.add_apply, LinearMap.vecCons_apply,
        Matrix.cons_add_cons (f x z)]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (LinearMap.snd R M M₂) (m, 0) ∈ ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (LinearMap.fst R M M₂) (0, n) ∈ ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Fintype.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), Finite ↑(f ⁻¹' {y})
val✝ : Fintype β
⊢ ∀ (x : α), x ∈ univ.biUnion fun y ↦ (f ⁻¹' {y}).toFinset

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : AddCommGroup M₄
module_M : Module R M
module_M₂ : Module R M₂
module_M₃ : Module R M₃
module_M₄ : Module R M₄
e₁ : M ≃ₗ[R] M₂
e₂ : M₃ ≃ₗ[R] M₄
f : M →ₗ[R] M₄
p : M × M₃
⊢ (fun p ↦ (e₁.symm p.1, e₂.symm (p.2 - f (e₁.symm p.1))))
      (((↑e₁ ∘ₗ LinearMap.fst R M M₃).prod (↑e₂ ∘ₗ LinearMap.snd R M M₃ + f ∘ₗ LinearMap.fst R M M₃)).toFun p) =
    p

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : AddCommGroup M₄
module_M : Module R M
module_M₂ : Module R M₂
module_M₃ : Module R M₃
module_M₄ : Module R M₄
e₁ : M ≃ₗ[R] M₂
e₂ : M₃ ≃ₗ[R] M₄
f : M →ₗ[R] M₄
p : M₂ × M₄
⊢ ((↑e₁ ∘ₗ LinearMap.fst R M M₃).prod (↑e₂ ∘ₗ LinearMap.snd R M M₃ + f ∘ₗ LinearMap.fst R M M₃)).toFun
      ((fun p ↦ (e₁.symm p.1, e₂.symm (p.2 - f (e₁.symm p.1)))) p) =
    p

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d : M
⊢ InjOn (fun x ↦ x + d) (Ici a)

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d : M
⊢ InjOn (fun x ↦ x + d) (Ioi a)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case zero
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hi : Iio i = ∅
⊢ (partialSups (disjointed f)) i = (partialSups f) i

Tactic:
simp only [partialSups_apply, Iic_eq_cons_Iio, hi, disjointed_apply, sup'_eq_sup, sup_cons,
      sup_empty, sdiff_bot]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: M : Type u_2
inst✝¹ : Monoid M
inst✝ : HasMulAntidiagonal M
a : M
⊢ (1, a) ∈ mulAntidiagonal a

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
hι : Nonempty ι
⊢ ∀ {a b : ι}, (Equiv.ofInjective (toZ hι.some) ⋯) a ≤ (Equiv.ofInjective (toZ hι.some) ⋯) b ↔ a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

Tactic:
rw [disjointed_apply]
    have : Iio (succ i) = Iic i := by
      ext
      simp only [mem_Iio, lt_succ_iff_eq_or_lt_of_not_isMax h, mem_Iic, le_iff_lt_or_eq, Or.comm]
    rw [this, ← sup'_eq_sup nonempty_Iic, ← partialSups_apply, hf.partialSups_eq,
      sdiff_sup_cancel <| hf <| le_succ i]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : Monoid A
inst✝ : HasMulAntidiagonal A
⊢ LeftInverse (fun x ↦ ⟨x.1 * x.2, ⟨x, ⋯⟩⟩) fun x ↦ ↑x.snd

Tactic:
rintro ⟨n, ⟨k, l⟩, h⟩
    rw [mem_mulAntidiagonal] at h
    exact Sigma.subtype_ext h rfl

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m n : ι
hm : n ≤ m
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
⊢ (Ioc n m).sup (disjointed f) = f m \ f n

Tactic:
induction hm using Succ.rec with
  | rfl => simp
  | succ m hm ih =>
    by_cases h'm : IsMax m
    · simpa [Order.succ_eq_iff_isMax.mpr h'm] using ih
    · rw [← Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax hm h'm]
      simp only [sup_insert, hf.disjointed_succ h'm, ih]
      exact sdiff_sup_sdiff_cancel (hf (Order.le_succ m)) (hf hm)

Goal state after:
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)

Tactic:
rw [antidiagonal_succ, antidiagonal_succ', map_cons, map_map, Prod.map_apply]

Goal state after:
n : ℕ
⊢ (0, n + 1 + 1) ::ₘ ((n + 1).succ, id 0) ::ₘ map (Prod.map Nat.succ id ∘ Prod.map id Nat.succ) (antidiagonal n) =
    (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
⊢ ∀ {a b : ι},
    { toFun := toZ hι.some, invFun := fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some,
            left_inv := ⋯, right_inv := ⋯ }
          a ≤
        { toFun := toZ hι.some, invFun := fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some,
            left_inv := ⋯, right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
xy : ℕ × ℕ
⊢ xy ∈ { val := Multiset.Nat.antidiagonal n, nodup := ⋯ } ↔ xy.1 + xy.2 = n

Tactic:
mem_def,

Goal state after:
n : ℕ
xy : ℕ × ℕ
⊢ xy ∈ { val := Multiset.Nat.antidiagonal n, nodup := ⋯ }.val ↔ xy.1 + xy.2 = n
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (0, n + 1) ∉ map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (antidiagonal n)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (n + 1, 0) ∉ map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (n + 2, 0) ∉
    map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
      (antidiagonal n)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (0, n + 2) ∉
    cons (n + 2, 0)
      (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
        (antidiagonal n))
      ⋯

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
h : 1 ∈ I
⊢ 1 * 1 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * y ^ (n - i.succ).succ * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)

Tactic:
pow_succ' y,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * (y * y ^ (n - i.succ)) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)

Tactic:
rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
        rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
⊢ 2 ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ (x + y) ^ (n + 1) = ∑ x_1 ∈ range n.succ, (x * t n x_1 + y * t n x_1.succ) + y ^ (n + 1)

Tactic:
sum_add_distrib,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ (x + y) ^ (n + 1) = ∑ x_1 ∈ range n.succ, x * t n x_1 + ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
s : Set α
⊢ Submodule.span α s = span s

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
⊢ span ∅ = ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
⊢ span univ = ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ span ↑I = I

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
x : α
⊢ x ∈ span {x}

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
x : α
⊢ span {x} ≤ I ↔ x ∈ I

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
s : Set α
⊢ span s = ⊥ ↔ ∀ x ∈ s, x = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
x : α
⊢ span {x} = ⊥ ↔ x = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
⊢ span {0} = ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
⊢ span 0 = ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
s : Set α
⊢ span (insert 0 s) = span s

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
s : Set α
⊢ span (s \ {0}) = span s

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ.e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)

Tactic:
h_last,

Goal state after:
case succ.e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * 0 + y ^ (n + 1)
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ IsCoatom I ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
SetLike.isCoatom_iff,

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ (I ≠ ⊤ ∧ ∀ (H : Ideal α) (g : α), I ≤ H → g ∉ I → g ∈ H → H = ⊤) ↔
    1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ ∑ x ∈ range (2 * n + 1), (2 * n).choose (2 * n / 2) = (2 * n + 1) * (2 * n).choose n

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n✝ k n : ℕ
hmn✝ : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ n + 1 ∉ Ico k (n + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ x_1 ∈ s, x_1 - x ∈ I
a : R
a_in : a ∈ s
h : a - x ∈ I
⊢ ↑⟨-(a - x), ⋯⟩ + a = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred.PartialSups

Goal state before:
pp: ι : Type u_2
inst✝⁴ : LinearOrder ι
α : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrder ι
inst✝¹ : SuccOrder ι
inst✝ : OrderBot ι
f : ι → α
i : ι
⊢ (partialSups f) (Order.succ ⊥) = f ⊥ ⊔ (partialSups (f ∘ Order.succ)) ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ 0 ∉ x.support → ((((inr R P M ∘ₗ f) ^ 0) ∘ₗ inl R P M) (x 0)).1 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
s t : Set α
α✝ : Type ?u.14
x : α✝
x✝ : Set α✝
⊢ x✝ ∈ {s | x ∈ s} ↔ x✝ ∈ 𝓟 {x}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
s t : Set α
⊢ ∀ (s : Set α), s ∈ {s | ∀ (x : α), x ∈ s} ↔ s ∈ sSup (range pure)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
s t : Set α
⊢ ∀ (s : Set α), s ∈ univ ↔ s ∈ sSup ∅

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
⊢ univ = univ ∩ univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
⊢ ∀ (s : Set α), s ∈ {s | s ∈ f ∧ s ∈ g} ↔ s ∈ sSup {f, g}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
⊢ l.HasBasis (fun i ↦ p i ∧ q i) s

Tactic:
by
  refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i, hpi, hti⟩ => h.mem_iff.2 ⟨i, hpi.1, hti⟩⟩⟩
  rcases h.mem_iff.1 ht with ⟨i, hpi, hti⟩
  rcases hq i hpi with ⟨j, hpj, hqj, hji⟩
  exact ⟨j, ⟨hpj, hqj⟩, hji.trans hti⟩

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
s t : Set α
hqs : q s
hqt : q t
⊢ univ ∈ {s | ∀ (t : Set α), q t → q (s ∩ t)}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
⊢ p s

Tactic:
have p_of_f : ∀ i, ∀ s ∈ f i, p s := fun i s hs ↦ by simpa using ins hs uni
  let q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ t', t ⊆ t' → p t'
  have q_mono : Monotone q := fun a b hab ha ↦
    ⟨mem_of_superset ha.1 hab, fun t hbt ↦ ha.2 _ (hab.trans hbt)⟩
  have A : ∀ i, ∀ s ∈ f i, ∀ t, q t → q (s ∩ t) := fun i s hs t ht ↦ by
    use inter_mem (mem_iInf_of_mem _ hs) ht.1
    intro u hu
    have : u = (u ∪ s) ∩ (u ∪ t) := by
      rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu
    rw [this]
    exact ins (mem_of_superset hs subset_union_right) (ht.2 _ subset_union_right)
  have B : ∀ s t, q s → q t → q (s ∩ t) := fun s t hqs hqt ↦ by
    let 𝓕 : Filter α :=
    { sets := {s | ∀ t, q t → q (s ∩ t)}
      univ_sets := by simp
      sets_of_superset ha hab t ht := q_mono (inter_subset_inter_left _ hab) (ha t ht)
      inter_sets ha hb t ht := by simpa [inter_assoc] using ha _ (hb _ ht) }
    exact (le_iInf_iff.mpr A : 𝓕 ≤ iInf f) hqs.1 _ hqt
  have C : ∀ i, ∀ s ∈ f i, q s := fun i s hs ↦
    ⟨mem_iInf_of_mem _ hs, fun t hst ↦ p_of_f _ _ (mem_of_superset hs hst)⟩
  let 𝓖 : Filter α :=
  { sets := {t | q t}
    univ_sets := by simpa [q] using uni
    sets_of_superset ha hab :=
      ⟨mem_of_superset ha.1 hab, fun t hbt ↦ ha.2 _ (hab.trans hbt)⟩
    inter_sets := B _ _ }
  have : 𝓖 ≤ iInf f := le_iInf_iff.mpr C
  exact (this hs).2 s subset_rfl

Goal state after:
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ x ∈ ⋃ i ∈ s, Ici i

Tactic:
rw [mem_iUnion₂]

Goal state after:
case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ ∃ i, ∃ (_ : i ∈ s), x ∈ Ici i
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
p : ι → Prop
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i
x✝ : Set α
⊢ x✝ ∈ l ↔ ∃ i, x✝ ∈ f ↑i

Tactic:
simp only [Subtype.exists, h, exists_prop]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
U : Set α
⊢ U ∈ ⊤ ↔ ∃ i, True ∧ univ ⊆ U

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
t U : Set α
⊢ U ∈ 𝓟 t ↔ ∃ i, True ∧ t ⊆ U

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
h : ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p x
a✝ : α
pa : a✝ ∈ univ → p a✝
⊢ a✝ ∈ univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
⊢ ¬∃ᶠ (x : α) in f, False

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
q : α → Prop
⊢ (∃ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∃ᶠ (x : α) in f, q x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
inst✝ : f.NeBot
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x ∨ q) ↔ (∃ᶠ (x : α) in f, p x) ∨ q

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p : α → Prop
⊢ ¬∃ᶠ (x : α) in ⊥, p x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s : Set α
l : Filter α
⊢ (∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ ∅) ↔ ∀ᶠ (x : α) in l, x ∉ s

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
s : Set α
⊢ 𝓟 s = map Subtype.val ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn m s
F : Filter α
hF : F ∈ Iic (𝓟 s)
G : Filter α
hG : G ∈ Iic (𝓟 s)
⊢ map m F = map m G → F = G

Tactic:
· simp [map_eq_map_iff_of_injOn (le_principal_iff.mp hF) (le_principal_iff.mp hG) hm]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
p : α → Prop
inst✝ : Nonempty α
⊢ (∀ (i : α), True → ∃ x ∈ Ici i, p x) ↔ ∀ (a : α), ∃ b, a ≤ b ∧ p b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
p : α → Prop
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
⊢ (∀ (i : α), True → ∃ x ∈ Ioi i, p x) ↔ ∀ (a : α), ∃ b > a, p b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
⊢ atTop = comap Subtype.val atTop

Tactic:
rcases isEmpty_or_nonempty (Ioi a) with h | ⟨⟨b, hb⟩⟩

Goal state after:
case inl
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
h : IsEmpty ↑(Ioi a)
⊢ atTop = comap Subtype.val atTop

case inr
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a b : α
hb : b ∈ Ioi a
⊢ atTop = comap Subtype.val atTop