mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
x y : A
⊢ (x, y) ∈ mulAntidiagonal 1 ↔ (x, y) ∈ {(1, 1)}

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ StrictMono (toZ i0)

Tactic:
intro j

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j : ι
⊢ ∀ ⦃b : ι⦄, j < b → toZ i0 j < toZ i0 b
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: case mp
A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
a b : A
inst✝¹ : DecidablePred fun x ↦ x = a
inst✝ : Decidable (a ≤ a + b)
⊢ a ≤ a + b ∧ b = a + b - a

Tactic:
exact ⟨le_add_right le_rfl, (add_tsub_cancel_left _ _).symm⟩

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:
simp

Goal state after:
Module: Mathlib.Order.Disjointed

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case zero
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ j ∈ range 0, f (0 - 1 - j) = ∏ j ∈ range 0, f j

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case succ
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ j ∈ Ico (n✝ + 1 - (n✝ + 1)) (n✝ + 1 - 0), f j = ∏ x ∈ Ico 0 (n✝ + 1), f x

Tactic:
simp

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

Goal state before:
pp: n i✝ : ℕ
a✝ : ℕ × ℕ
⊢ (map ((fun i ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n))[i✝]? = some a✝ ↔
    (map (Prod.map Nat.succ id ∘ (fun i ↦ (i, n - i)) ∘ Nat.succ) (range n))[i✝]? = some a✝

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∏ i ≤ a, f i.succ / f i.castSucc = f a.succ / f 0

Tactic:
rw [← prod_ite_mem_eq, prod_fin_eq_prod_range]
  convert! prod_range_div (fun i ↦ if hi : i < n + 1 then f ⟨i, hi⟩ else 1) (a + 1) using 1 with k
    hk
  · exact prod_congr_of_eq_on_inter (by grind) (by grind) (by simp_all; grind)
  · grind

Goal state after:
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:
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:
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:
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:
simp

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

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ {a ∈ antidiagonal n | a.2 ≤ k} =
    map ({ toFun := fun x ↦ x + (n - k), inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal k)

Tactic:
ext ⟨i, j⟩
  suffices i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i by simpa
  refine ⟨fun hi ↦ ⟨k - j, tsub_add_cancel_of_le hi.2, ?_⟩, ?_⟩
  · rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2,
      add_tsub_cancel_right]
  · rintro ⟨l, hl, rfl⟩
    refine ⟨?_, hl ▸ Nat.le_add_left j l⟩
    rw [add_assoc, add_comm, add_assoc, add_comm j l, hl]
    exact Nat.sub_add_cancel h

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:
simp

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

Goal state before:
pp: α : Type u
inst✝² : Semiring α
inst✝¹ : Nontrivial α
inst✝ : NoZeroDivisors α
x✝ : α
⊢ x✝ ∈ ⊥.primeCompl ↔ x✝ ∈ nonZeroDivisors α

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : { a // IsIdempotentElem a }
⊢ ↑aᶜᶜ = ↑a

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
⊢ ↑0ᶜ = ↑1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
⊢ ↑1ᶜ = ↑0

Tactic:
simp

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

Goal state before:
pp: case zero
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
⊢ 1 = x ^ 0 * y ^ (0 - 0) * ↑(Nat.choose 0 0)

Tactic:
rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]

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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
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:
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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
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:
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:
simp

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
inst✝ : DecidableEq ι
i : ι
r : R i
hr : r ∈ I i
⊢ Pi.single i r ∈ pi I

Tactic:
intro j

Goal state after:
ι : Type u_1
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
inst✝ : DecidableEq ι
i : ι
r : R i
hr : r ∈ I i
j : ι
⊢ Pi.single i r j ∈ I 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:
simp

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

Goal state before:
pp: case inr.base
n k : ℕ
⊢ ∑ m ∈ Icc k k, m.choose k = (k + 1).choose (k + 1)

Tactic:
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:
simp

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

Goal state before:
pp: case empty
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
⊢ Multiset.sum 0 ^ (Multiset.card 0 * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) 0).toFinset

Tactic:
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:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
S : Ideal R
inst✝ : S.IsTwoSided
x✝ : R
⊢ ((factor ⋯).comp (mk S)) x✝ = ((RingHom.id (R ⧸ S)).comp (mk S)) x✝

Tactic:
simp

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

Goal state before:
pp: case zero
n : ℕ
⊢ ∑ k ∈ range (0 + 1), (-1) ^ k * ↑((n + 1).choose k) = (-1) ^ 0 * ↑(n.choose 0)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x✝ : R
⊢ (((factor H2).comp (factor H1)).comp (mk S)) x✝ = ((factor ⋯).comp (mk S)) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x : R ⧸ S
⊢ ((factor H2).comp (factor H1)) x = (factor ⋯) x

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ ∑ m ∈ range (0 + 1), (-1) ^ m * ↑(Nat.choose 0 m) = if 0 = 0 then 1 else 0

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ x ∈ range n, f (x + 1) (n - x) ^ n.choose (x + 1)) * f (n + 1) (n - n) ^ n.choose (n + 1) * f 0 (n + 1) =
    (∏ k ∈ range n, f (k + 1) (n + 1 - (k + 1)) ^ n.choose (k + 1)) * f 0 (n + 1 - 0) ^ n.choose 0

Tactic:
simp

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

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
h : ⊥ = ⊤
⊢ 1 ∉ ⊥

Tactic:
simp

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

Goal state before:
pp: case zero
d : ℕ
⊢ ∑ ij ∈ antidiagonal 0, (d + ij.2).choose d = (d + 0 + 1).choose (d + 1)

Tactic:
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:
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 j : ι
x✝ : ⊥ ≤ j
h : (partialSups f) (Order.succ j) = f ⊥ ⊔ (partialSups (f ∘ Order.succ)) j
⊢ (partialSups (f ∘ Order.succ)) (Order.succ j) = (partialSups (f ∘ Order.succ)) j ⊔ (f ∘ Order.succ) (Order.succ j)

Tactic:
simp

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

Goal state before:
pp: case zero
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
⊢ 0 ∈ span (range fun i ↦ Pi.single i 1)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
⊢ span (range fun i ↦ Pi.single i 1) = ⊤

Tactic:
rw [_root_.eq_top_iff]
  rintro x -
  induction x using Pi.single_induction with
  | zero => simp
  | add f g hf hg => exact Ideal.add_mem _ hf hg
  | single i r =>
      rw [show Pi.single i r = Pi.single i r * Pi.single i 1 by simp [← Pi.single_mul_left]]
      exact Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨i, rfl⟩)

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

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ![⊥, ⊤] ((fun I ↦ if I = ⊥ then 0 else 1) ⊥) = ⊥

Tactic:
simp

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

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ![⊥, ⊤] ((fun I ↦ if I = ⊥ then 0 else 1) ⊤) = ⊤

Tactic:
simp

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

Goal state before:
pp: case «0»
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ (fun I ↦ if I = ⊥ then 0 else 1) (![⊥, ⊤] ((fun i ↦ i) ⟨0, ⋯⟩)) = (fun i ↦ i) ⟨0, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: case «1»
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ (fun I ↦ if I = ⊥ then 0 else 1) (![⊥, ⊤] ((fun i ↦ i) ⟨1, ⋯⟩)) = (fun i ↦ i) ⟨1, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
x y : α →₀ M
x✝ : α
⊢ (x + y) x✝ = (⇑x + ⇑y) x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
x : R
y : α →₀ M
x✝ : α
⊢ (x • y) x✝ = ((RingHom.id R) x • ⇑y) x✝

Tactic:
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:
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
⊢ ((((inr R P M ∘ₗ f) ^ 0) ∘ₗ inl R P M) (x 0)).1 = x 0

Tactic:
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:
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:
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:
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:
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:
simp

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

Goal state before:
pp: case he
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
⊢ ⋂ i ∈ ∅, s i ∈ f ↔ ∀ i ∈ ∅, s i ∈ f

Tactic:
simp

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

Goal state before:
pp: case h₁
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
⊢ ∀ (x : β), ⋂ i ∈ {x}, s i ∈ f ↔ ∀ i ∈ {x}, s i ∈ f

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
x✝ : α →₀ M
⊢ (x✝ ∈ submodule fun x ↦ ⊤) ↔ x✝ ∈ ⊤

Tactic:
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_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:
simp

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ pure a ≤ 𝓟 s ↔ a ∈ s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
m : α → β
⊢ comap m (g ⊓ 𝓟 (range m)) = comap m g

Tactic:
simp

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

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

Tactic:
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:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
s✝ : Set α
⊢ (inl '' s✝ᶜ)ᶜ ∈ map inr g ↔ s✝ ∈ ⊥

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
s✝ : Set β
⊢ (inr '' s✝ᶜ)ᶜ ∈ map inl f ↔ s✝ ∈ ⊥

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : Tendsto (g ∘ f) a c
hg : comap g c ≤ b
⊢ Tendsto f a b

Tactic:
rw [tendsto_iff_comap] at hfg ⊢

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : a ≤ comap (g ∘ f) c
hg : comap g c ≤ b
⊢ a ≤ comap f b
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl f ≤ map inl ⊤

Tactic:
simp

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

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inr g ≤ map inr ⊤

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl ⊤ ⊓ map inr ⊤ ≤ ⊥

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ a ∈ s, f a ∈ t

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun x1 x2 ↦ x1 ⊇ x2) S
ne : S.Nonempty
t : Set α
⊢ DirectedOn ((fun i ↦ 𝓟 (s i)) ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) S

Tactic:
directedOn_iff_directed,

Goal state after:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (s ⁻¹'o fun x1 x2 ↦ x1 ⊇ x2) Subtype.val
ne : S.Nonempty
t : Set α
⊢ Directed ((fun i ↦ 𝓟 (s i)) ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) Subtype.val
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : Filter β
hα : IsEmpty α
⊢ ¬⊥.NeBot ↔ ¬(Nonempty α ∧ f.NeBot)

Tactic:
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:
simp

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

Goal state before:
pp: case inr
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

Tactic:
have : ∀ j, Nonempty (α j) := Classical.nonempty_pi.1 H

Goal state after:
case inr
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
this : ∀ (j : ι), Nonempty (α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot
Module: Mathlib.Order.Filter.Basic

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

Tactic:
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:
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:
simp

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

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

Tactic:
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:
simp

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

Goal state before:
pp: α : Type u_1
p : Set α → Prop
he : p ∅
hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s
hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)
s : Set α
⊢ sᶜ ∈ comk p he hmono hunion ↔ p s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : f.NeBot
s : Set α
hs : m '' s ∈ f
⊢ (comap m f ⊓ 𝓟 s).NeBot

Tactic:
neBot_inf_comap_iff_map',

Goal state after:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : f.NeBot
s : Set α
hs : m '' s ∈ f
⊢ (f ⊓ map m (𝓟 s)).NeBot
Module: Mathlib.Order.Filter.Map

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

Tactic:
simp

Goal state after: