mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a + b * a + (a * b + b) = a + (0 + b)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a + b * a + (a * b + b) = a + b
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
⊢ IsCompactElement ⊤

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : Semiring α
⊢ IsCompactElement (span {1})
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
this : ∑ m ∈ range (n + 1), 1 ^ m * 1 ^ (n - m) * ↑(n.choose m) = (1 + 1) ^ n
⊢ ∑ m ∈ range (n + 1), n.choose m = 2 ^ n

Tactic:
simpa using

Goal state after:
n : ℕ
this : ∑ m ∈ range (n + 1), 1 ^ m * 1 ^ (n - m) * ↑(n.choose m) = (1 + 1) ^ n
⊢ ∑ m ∈ range (n + 1), n.choose m = 2 ^ n
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
t : (2 * n + 1).choose n ≤ ∑ i ∈ range (n + 1), (2 * n + 1).choose i
⊢ (2 * n + 1).choose n ≤ 4 ^ n

Tactic:
simpa using

Goal state after:
n : ℕ
t : (2 * n + 1).choose n ≤ ∑ i ∈ range (n + 1), (2 * n + 1).choose i
⊢ (2 * n + 1).choose n ≤ 4 ^ n
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I J : (i : ι) → Ideal (R i)
le : pi I ≤ pi J
i : ι
r : R i
hr : r ∈ I i
⊢ r ∈ J i

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I J : (i : ι) → Ideal (R i)
le : pi I ≤ pi J
i : ι
r : R i
hr : r ∈ I i
⊢ r ∈ J i
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
a✝ : c ∈ Finset.range (k + 1)
⊢ a ^ c * b ^ (k - c) ∈ I

Tactic:
by_cases h : m ≤ c

Goal state after:
case pos
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
a✝ : c ∈ Finset.range (k + 1)
h : m ≤ c
⊢ a ^ c * b ^ (k - c) ∈ I

case neg
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
a✝ : c ∈ Finset.range (k + 1)
h : ¬m ≤ c
⊢ a ^ c * b ^ (k - c) ∈ I
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case zero
n : ℕ
⊢ ∑ i ∈ range (n + 1), multichoose 0 i = (n + 0).choose 0

Tactic:
simp [Finset.sum_range_succ']

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m ∈ x.powerset, (-1) ^ #m = if x = ∅ then 1 else 0

Tactic:
sum_powerset_apply_card

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m ∈ range (#x + 1), (#x).choose m • (-1) ^ m = if x = ∅ then 1 else 0
Module: Mathlib.Data.Nat.Choose.Sum

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

Tactic:
simpa using

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose (i + 1)) * f 0 (n + 1) =
    ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i
⊢ (∏ x ∈ range (n + 1), f (x + 1) (n - x) ^ n.choose x) * ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i =
    (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ x ∈ range (n + 1), f (x + 1) (n - x) ^ n.choose x
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n i : ℕ
hi : i ∈ range (n + 1)
⊢ i ≤ n

Tactic:
simpa using

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n i : ℕ
hi : i ∈ range (n + 1)
⊢ i ≤ n
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ i ∈ range (n + 2), ↑((n + 1).choose i) * f i (n + 1 - i) =
    ∑ i ∈ range (n + 1), ↑(n.choose i) * f i (n + 1 - i) + ∑ i ∈ range (n + 1), ↑(n.choose i) * f (i + 1) (n - i)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ i ∈ range (n + 2), ↑((n + 1).choose i) * f i (n + 1 - i) =
    ∑ i ∈ range (n + 1), ↑(n.choose i) * f i (n + 1 - i) + ∑ i ∈ range (n + 1), ↑(n.choose i) * f (i + 1) (n - i)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ ij ∈ antidiagonal (n + 1), ↑((n + 1).choose ij.1) * f ij.1 ij.2 =
    ∑ ij ∈ antidiagonal n, ↑(n.choose ij.1) * f ij.1 (ij.2 + 1) +
      ∑ ij ∈ antidiagonal n, ↑(n.choose ij.2) * f (ij.1 + 1) ij.2

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ ij ∈ antidiagonal (n + 1), ↑((n + 1).choose ij.1) * f ij.1 ij.2 =
    ∑ ij ∈ antidiagonal n, ↑(n.choose ij.1) * f ij.1 (ij.2 + 1) +
      ∑ ij ∈ antidiagonal n, ↑(n.choose ij.2) * f (ij.1 + 1) ij.2
Module: Mathlib.Algebra.Order.SuccPred.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁶ : SemilatticeSup α
inst✝⁵ : LinearOrder ι
inst✝⁴ : Add ι
inst✝³ : One ι
inst✝² : OrderBot ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
⊢ (partialSups f) (i + 1) = f ⊥ ⊔ (partialSups (f ∘ fun k ↦ k + 1)) i

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁶ : SemilatticeSup α
inst✝⁵ : LinearOrder ι
inst✝⁴ : Add ι
inst✝³ : One ι
inst✝² : OrderBot ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
⊢ (partialSups f) i ⊔ f (Order.succ i) = f ⊥ ⊔ (partialSups (f ∘ fun k ↦ Order.succ k)) i
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case a
α : Type u_1
B : FilterBasis α
U : Set α
⊢ U ∈ B.filter → U ∈ generate B.sets

Tactic:
U_in

Goal state after:
case a
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.filter
⊢ U ∈ generate B.sets
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
p : α → Submodule R M
i : α
x : M
hx : x ∈ comap (lsingle i) (submodule p)
⊢ x ∈ p i

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
i : α
x : M
hx : x ∈ comap (lsingle i) (submodule p)
⊢ x ∈ p i
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
i✝ j✝ : ι
hi : p i✝
hj : p j✝
⊢ ∃ k, p k ∧ s k ⊆ s i✝ ∩ s j✝

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
i✝ j✝ : ι
hi : p i✝
hj : p j✝
⊢ ∃ k, p k ∧ s k ⊆ s i✝ ∩ s j✝
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₂)
i : ι
s : Set α
hs : s ∈ f i
⊢ p s

Tactic:
simpa using

Goal state after:
α : 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₂)
i : ι
s : Set α
hs : s ∈ f i
⊢ p s
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
⊢ l = ⊤ ↔ ∀ (i : ι), p i → s i = univ

Tactic:
by
  simp [← top_le_iff, h.ge_iff]

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

Goal state before:
pp: case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'

Tactic:
simpa using

Goal state after:
case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ ∀ (i' : ι), p i' → ∃ i, p' i ∧ s' i ⊆ s i'

Tactic:
simpa using

Goal state after:
case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ ∀ (i' : ι), p i' → ∃ i, p' i ∧ s' i ⊆ s i'
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✝
x✝ y✝ : Set α
ha : x✝ ∈ {s | ∀ (t : Set α), q t → q (s ∩ t)}
hb : y✝ ∈ {s | ∀ (t : Set α), q t → q (s ∩ t)}
t : Set α
ht : q t
⊢ q (x✝ ∩ y✝ ∩ t)

Tactic:
simpa using

Goal state after:
α : 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✝
x✝ y✝ : Set α
ha : x✝ ∈ {s | ∀ (t : Set α), q t → q (s ∩ t)}
hb : y✝ ∈ {s | ∀ (t : Set α), q t → q (s ∩ t)}
t : Set α
ht : q t
⊢ q (x✝ ∩ (y✝ ∩ t))
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)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
C : ∀ (i : ι), ∀ s ∈ f i, q s
⊢ univ ∈ {t | q t}

Tactic:
simpa using

Goal state after:
α : 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)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
C : ∀ (i : ι), ∀ s ∈ f i, q s
⊢ p univ
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
hm : Injective m
⊢ map m f ≤ map m g ↔ f ≤ g

Tactic:
rw [map_le_iff_le_comap, comap_map hm]

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 : a ≤ comap (g ∘ f) c
hg : comap g c ≤ b
⊢ comap (g ∘ f) c ≤ comap f b

Tactic:
simpa using

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
⊢ comap (g ∘ f) c ≤ comap f b
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
inst✝ : Nonempty ι
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
⊢ ¬(iInf f).NeBot → ¬∀ (i : ι), (f i).NeBot

Tactic:
simpa using

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
inst✝ : Nonempty ι
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
⊢ (∃ i, ∅ ∈ f i) → ∃ i, ∅ ∈ f i
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
t u : Set α
⊢ u ∈ l ⊔ 𝓟 t ↔ ∃ i, p i ∧ s i ∪ t ⊆ u

Tactic:
simp only [(hl.sup' (hasBasis_principal t)).mem_iff, PProd.exists, and_true,
      Unique.exists_iff]

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 α
hl : l.HasBasis p s
s' : Set α
⊢ (𝓟 s' ⊓ l).HasBasis p fun i ↦ s' ∩ s i

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
s' : Set α
⊢ (l ⊓ 𝓟 s').HasBasis p fun i ↦ s' ∩ s i
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
h : ∀ U ∈ f, (U ∩ sᶜ).Nonempty
hs : s ∈ f
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
f : Filter α
s : Set α
h : ∀ U ∈ f, (U ∩ sᶜ).Nonempty
hs : s ∈ f
⊢ False
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ ￢𝓟 s = 𝓟 sᶜ

Tactic:
simpa using

Goal state after:
α : Type u
s : Set α
⊢ ￢𝓟 s = 𝓟 sᶜ
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
s : ι → Set α
h : l.HasBasis (fun x ↦ True) s
⊢ l = ⨅ i, 𝓟 (s i)

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Sort u_4
l : Filter α
s : ι → Set α
h : l.HasBasis (fun x ↦ True) s
⊢ l = ⨅ i, 𝓟 (s i)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p q : α → Prop
h : ∀ᶠ (x : α) in f, p x ↔ q x
hq : ∀ᶠ (x : α) in f, q x
⊢ ∀ᶠ (x : α) in f, q x ↔ p x

Tactic:
simpa using

Goal state after:
α : Type u
f : Filter α
p q : α → Prop
h : ∀ᶠ (x : α) in f, p x ↔ q x
hq : ∀ᶠ (x : α) in f, q x
⊢ ∀ᶠ (x : α) in f, p x ↔ q x
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p q : α → Prop
f : Filter α
hp : ∀ᶠ (x : α) in f, p x
hq : ∃ᶠ (x : α) in f, q x
⊢ ∃ᶠ (x : α) in f, p x ∧ q x

Tactic:
simpa using

Goal state after:
α : Type u
p q : α → Prop
f : Filter α
hp : ∀ᶠ (x : α) in f, p x
hq : ∃ᶠ (x : α) in f, q x
⊢ ∃ᶠ (x : α) in f, p x ∧ q x
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p : α → Prop
f : Filter α
H : ∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, p x ∧ q x
hp : ∀ᶠ (x : α) in f, ¬(fun x ↦ p x) x
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u
p : α → Prop
f : Filter α
H : ∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, p x ∧ q x
hp : ∀ᶠ (x : α) in f, ¬(fun x ↦ p x) x
⊢ False
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι' : Sort u_5
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
sa : Set α
h : lb.HasBasis pb sb
⊢ (𝓟 sa ×ˢ lb).HasBasis pb fun x ↦ sa ×ˢ sb x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι' : Sort u_5
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
sa : Set α
h : lb.HasBasis pb sb
⊢ (𝓟 (Prod.fst ⁻¹' sa) ⊓ Filter.comap Prod.snd lb).HasBasis pb fun x ↦ Prod.fst ⁻¹' sa ∩ Prod.snd ⁻¹' sb x
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι' : Sort u_5
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
sa : Set α
h : lb.HasBasis pb sb
⊢ (𝓟 sa ×ˢ lb).HasBasis pb fun x ↦ sa ×ˢ sb x

Tactic:
simpa only [prod_eq_inf, comap_principal, prod_eq] using (h.comap Prod.snd).principal_inf _

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A
U : Set β
⊢ U ∈ F → f x ∈ U

Tactic:
U_in

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A
U : Set β
U_in : U ∈ F
⊢ f x ∈ U
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
h : la.HasBasis pa sa
sb : Set β
⊢ (la ×ˢ 𝓟 sb).HasBasis pa fun x ↦ sa x ×ˢ sb

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
h : la.HasBasis pa sa
sb : Set β
⊢ (Filter.comap Prod.fst la ⊓ 𝓟 (Prod.snd ⁻¹' sb)).HasBasis pa fun x ↦ Prod.fst ⁻¹' sa x ∩ Prod.snd ⁻¹' sb
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A
U : Set β
U_in : U ∈ F
⊢ f x ∈ U

Tactic:
simpa using

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A
U : Set β
U_in : U ∈ F
⊢ f x ∈ U
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι' : Sort u_5
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
h : lb.HasBasis pb sb
⊢ (⊤ ×ˢ lb).HasBasis pb fun x ↦ univ ×ˢ sb x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι' : Sort u_5
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
h : lb.HasBasis pb sb
⊢ (⊤ ×ˢ lb).HasBasis pb fun x ↦ univ ×ˢ sb x
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
h : la.HasBasis pa sa
⊢ (la ×ˢ ⊤).HasBasis pa fun x ↦ sa x ×ˢ univ

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
h : la.HasBasis pa sa
⊢ (la ×ˢ ⊤).HasBasis pa fun x ↦ sa x ×ˢ univ
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ B ∈ F, f x ∈ B
V : Set α
U : Set β
⊢ U ∈ F → f ⁻¹' U ⊆ V → x ∈ V

Tactic:
U_in

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ B ∈ F, f x ∈ B
V : Set α
U : Set β
U_in : U ∈ F
⊢ f ⁻¹' U ⊆ V → x ∈ V
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddGroup β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
⊢ f - g =ᶠ[l] 0

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝ : AddGroup β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
⊢ f - g =ᶠ[l] 0
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddGroup β
f g : α → β
l : Filter α
h : f - g =ᶠ[l] 0
⊢ f =ᶠ[l] g

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝ : AddGroup β
f g : α → β
l : Filter α
h : f - g =ᶠ[l] 0
⊢ f =ᶠ[l] g
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
hl : la.HasBasis pa sa
i j : ι
hi : pa i
hj : pa j
⊢ ∃ k, pa k ∧ sa k ⊆ sa i ∧ sa k ⊆ sa j

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
hl : la.HasBasis pa sa
i j : ι
hi : pa i
hj : pa j
⊢ ∃ k, pa k ∧ sa k ⊆ sa i ∧ sa k ⊆ sa j
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
H : Filter β
hHG : H ≤ G
⊢ map m ((fun x ↦ F ⊓ comap m x) H) = H

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
H : Filter β
hHG : H ≤ G
⊢ H ≤ map m F
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
m : α → β
⊢ InjOn (map m) (Iic (𝓟 s)) ↔ InjOn m s

Tactic:
by
  refine ⟨fun hm x hx y hy hxy ↦ ?_, fun hm F hF G hG ↦ ?_⟩
  · rwa [← pure_injective.eq_iff, ← map_pure, ← map_pure, hm.eq_iff, pure_injective.eq_iff]
      at hxy <;> rwa [mem_Iic, pure_le_principal]
  · simp [map_eq_map_iff_of_injOn (le_principal_iff.mp hF) (le_principal_iff.mp hG) hm]

Goal state after:
Module: Mathlib.Algebra.Group.Action.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_4
β : Type u_5
inst✝¹ : SMul M β
e : α ≃ β
inst✝ : FaithfulSMul M β
this : SMul M α := Equiv.smul M e
m₁ m₂ : M
⊢ (∀ (a : α), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
simpa using

Goal state after:
M : Type u_1
α : Type u_4
β : Type u_5
inst✝¹ : SMul M β
e : α ≃ β
inst✝ : FaithfulSMul M β
this : SMul M α := Equiv.smul M e
m₁ m₂ : M
⊢ (∀ (a : α), m₁ • e a = m₂ • e a) → m₁ = m₂
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
⊢ map f atTop = atTop

Tactic:
refine le_antisymm (hf.tendsto_atTop_atTop fun c ↦ ?_) ?_

Goal state after:
case refine_1
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
c : β
⊢ ∃ a, c ≤ f a

case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
⊢ atTop ≤ map f atTop
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
⊢ ∀ (i' : α), True → f '' Ici i' ∈ atTop

Tactic:
intro a _

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
a✝ : True
⊢ f '' Ici a ∈ atTop
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : r • (m₁ - m₂) = 0
⊢ m₁ = m₂

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
G : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : r • (m₁ - m₂) = 0
⊢ m₁ = m₂
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : AddMonoid M
inst✝ : IsAddTorsionFree M
n : ℕ
x : M
hx : n ≠ 0 ∧ x ≠ 0
⊢ n • x ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : AddMonoid M
inst✝ : IsAddTorsionFree M
n : ℕ
x : M
hx : n ≠ 0 ∧ x ≠ 0
⊢ ¬x = 0 ∧ ¬n = 0
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : IsAddTorsionFree G
n : ℤ
x : G
hx : n ≠ 0 ∧ x ≠ 0
⊢ n • x ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : IsAddTorsionFree G
n : ℤ
x : G
hx : n ≠ 0 ∧ x ≠ 0
⊢ ¬x = 0 ∧ ¬n = 0
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst✝³ : Zero R
inst✝² : Zero β
inst✝¹ : SMul R β
inst✝ : NoZeroSMulDivisors R β
this✝¹ : Zero α := e.zero
this✝ : SMul R α := Equiv.smul R e
r : R
m : α
⊢ r • m = 0 → r = 0 ∨ m = 0

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst✝³ : Zero R
inst✝² : Zero β
inst✝¹ : SMul R β
inst✝ : NoZeroSMulDivisors R β
this✝¹ : Zero α := e.zero
this✝ : SMul R α := Equiv.smul R e
r : R
m : α
⊢ r • e m = 0 → r = 0 ∨ e m = 0