mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk.mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝¹ b✝ : R
inst✝ : I.IsTwoSided
a✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ pi fun x ↦ I
b : ι → R
y✝ : (ι → R) ⧸ pi fun x ↦ I
c : ι → R
⊢ Quot.mk (⇑(Submodule.quotientRel I)) a •
      (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) b + Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c) =
    Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) b +
      Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c

Tactic:
;

Goal state after:
case mk.mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝¹ b✝ : R
inst✝ : I.IsTwoSided
a✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ pi fun x ↦ I
b : ι → R
y✝ : (ι → R) ⧸ pi fun x ↦ I
c : ι → R
⊢ Quot.mk (⇑(Submodule.quotientRel I)) a •
      (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) b + Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c) =
    Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) b +
      Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk.mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝ b✝ : R
inst✝ : I.IsTwoSided
r✝ : R ⧸ I
a : R
s✝ : R ⧸ I
b : R
x✝ : (ι → R) ⧸ pi fun x ↦ I
c : ι → R
⊢ (Quot.mk (⇑(Submodule.quotientRel I)) a + Quot.mk (⇑(Submodule.quotientRel I)) b) •
      Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c =
    Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c +
      Quot.mk (⇑(Submodule.quotientRel I)) b • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c

Tactic:
;

Goal state after:
case mk.mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝ b✝ : R
inst✝ : I.IsTwoSided
r✝ : R ⧸ I
a : R
s✝ : R ⧸ I
b : R
x✝ : (ι → R) ⧸ pi fun x ↦ I
c : ι → R
⊢ (Quot.mk (⇑(Submodule.quotientRel I)) a + Quot.mk (⇑(Submodule.quotientRel I)) b) •
      Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c =
    Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c +
      Quot.mk (⇑(Submodule.quotientRel I)) b • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝ b : R
inst✝ : I.IsTwoSided
x✝ : (ι → R) ⧸ pi fun x ↦ I
a : ι → R
⊢ 0 • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a = 0

Tactic:
;

Goal state after:
case mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝ b : R
inst✝ : I.IsTwoSided
x✝ : (ι → R) ⧸ pi fun x ↦ I
a : ι → R
⊢ 0 • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
x✝ : (ι → R) ⧸ pi fun x ↦ I
a✝¹ : ι → R
y✝ : (ι → R) ⧸ pi fun x ↦ I
a✝ : ι → R
⊢ Quotient.liftOn'
      (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝¹ + Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝)
      (fun f i ↦ (Quotient.mk I) (f i)) ⋯ =
    Quotient.liftOn' (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝¹) (fun f i ↦ (Quotient.mk I) (f i)) ⋯ +
      Quotient.liftOn' (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝) (fun f i ↦ (Quotient.mk I) (f i)) ⋯

Tactic:
;

Goal state after:
case mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
x✝ : (ι → R) ⧸ pi fun x ↦ I
a✝¹ : ι → R
y✝ : (ι → R) ⧸ pi fun x ↦ I
a✝ : ι → R
⊢ Quotient.liftOn'
      (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝¹ + Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝)
      (fun f i ↦ (Quotient.mk I) (f i)) ⋯ =
    Quotient.liftOn' (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝¹) (fun f i ↦ (Quotient.mk I) (f i)) ⋯ +
      Quotient.liftOn' (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝) (fun f i ↦ (Quotient.mk I) (f i)) ⋯
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
m✝ : R ⧸ I
a✝¹ : R
x✝ : (ι → R) ⧸ pi fun x ↦ I
a✝ : ι → R
⊢ Quotient.liftOn' (Quot.mk (⇑(Submodule.quotientRel I)) a✝¹ • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝)
      (fun f i ↦ (Quotient.mk I) (f i)) ⋯ =
    (RingHom.id (R ⧸ I)) (Quot.mk (⇑(Submodule.quotientRel I)) a✝¹) •
      Quotient.liftOn' (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝) (fun f i ↦ (Quotient.mk I) (f i)) ⋯

Tactic:
;

Goal state after:
case mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
m✝ : R ⧸ I
a✝¹ : R
x✝ : (ι → R) ⧸ pi fun x ↦ I
a✝ : ι → R
⊢ Quotient.liftOn' (Quot.mk (⇑(Submodule.quotientRel I)) a✝¹ • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝)
      (fun f i ↦ (Quotient.mk I) (f i)) ⋯ =
    (RingHom.id (R ⧸ I)) (Quot.mk (⇑(Submodule.quotientRel I)) a✝¹) •
      Quotient.liftOn' (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝) (fun f i ↦ (Quotient.mk I) (f i)) ⋯
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Finite ↥?m.9 ∧ Finite (R ⧸ ?m.9)

pp: R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Ideal R

Tactic:
;

Goal state after:
R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Finite ↥?m.9 ∧ Finite (R ⧸ ?m.9)

R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Ideal R
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
α : Type u_5
inst✝ : Unique α
m : M
⊢ ((finsuppUnique R M α).symm m) default = (single default m) default

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
α : Type u_5
inst✝ : Unique α
m : M
⊢ ((finsuppUnique R M α).symm m) default = (single default m) default
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq α
x : α
x✝¹ : M
x✝ : α
⊢ (lcoeFun ∘ₗ lsingle x) x✝¹ x✝ = (LinearMap.single R (fun x ↦ M) x) x✝¹ x✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq α
x : α
x✝¹ : M
x✝ : α
⊢ (lcoeFun ∘ₗ lsingle x) x✝¹ x✝ = (LinearMap.single R (fun x ↦ M) x) x✝¹ x✝
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inr
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
inj : Injective ⇑f
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
n : ℕ
hn : n = s.max' ne
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
;

Goal state after:
case inr
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
inj : Injective ⇑f
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
n : ℕ
hn : n = s.max' ne
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
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
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ((comapDomain.addMonoidHom ⋯) x).support ∪ ((comapDomain.addMonoidHom ⋯) y).support = ∅
⊢ (comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y

Tactic:
;

Goal state after:
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
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ((comapDomain.addMonoidHom ⋯) x).support ∪ ((comapDomain.addMonoidHom ⋯) y).support = ∅
⊢ (comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
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
p' : ι → Prop
s' : ι → Set α
hp : ∀ (i : ι), p i ↔ p' i
hs : ∀ (i : ι), p i → s i = s' i
t : Set α
⊢ (∃ i, p i ∧ s i ⊆ t) ↔ ∃ i, p i ∧ s' i ⊆ t

Tactic:
;

Goal state after:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
p' : ι → Prop
s' : ι → Set α
hp : ∀ (i : ι), p i ↔ p' i
hs : ∀ (i : ι), p i → s i = s' i
t : Set α
⊢ (∃ i, p i ∧ s i ⊆ t) ↔ ∃ i, p i ∧ s' i ⊆ t
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
q : α → Prop
⊢ (¬∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → ¬q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

Tactic:
;

Goal state after:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (¬∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → ¬q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) ↔ ∃ u ∈ f, P u ∧ Q u

Tactic:
by
  constructor
  · rintro ⟨⟨u, huf, hPu⟩, v, hvf, hQv⟩
    exact
      ⟨u ∩ v, inter_mem huf hvf, hP inter_subset_left hPu, hQ inter_subset_right hQv⟩
  · rintro ⟨u, huf, hPu, hQu⟩
    exact ⟨⟨u, huf, hPu⟩, u, huf, hQu⟩

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
q : α → Prop
⊢ (∀ (i : ι), p i → ∃ x ∈ s i, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

Tactic:
;

Goal state after:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (∀ (i : ι), p i → ∃ x ∈ s i, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
a✝ : I
⊢ ((mapRange.linearMap f) { support := x.support, toFun := y, mem_support_toFun := ⋯ }) a✝ = x a✝

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
a✝ : I
⊢ ((mapRange.linearMap f) { support := x.support, toFun := y, mem_support_toFun := ⋯ }) a✝ = x a✝
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'
⊢ l ≤ l'

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'
⊢ l' ≤ l

Tactic:
· rw [hl.le_basis_iff hl']
    simpa using h'

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'
⊢ l' ≤ l
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s t : Set α
⊢ ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓟 t, s ∩ t = t₁ ∩ t₂

Tactic:
;

Goal state after:
α : Type u
s t : Set α
⊢ ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓟 t, s ∩ t = t₁ ∩ t₂
Module: Mathlib.Order.Filter.Map

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

Tactic:
inf_comm,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl g ⊓ map inr f = ⊥
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
f g : Filter α
⊢ (∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃s' : Set α⦄, s' ∈ g → (s ∩ s').Nonempty) ↔
    ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∀ {U : Set α}, U ∈ g → ∃ x, p x ∧ x ∈ U

Tactic:
;

Goal state after:
α : Type u_1
f g : Filter α
⊢ (∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃s' : Set α⦄, s' ∈ g → (s ∩ s').Nonempty) ↔
    ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∀ {U : Set α}, U ∈ g → ∃ x, p x ∧ x ∈ U
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
f g : Filter α
⊢ (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x

Tactic:
inf_comm

Goal state after:
α : Type u_1
f g : Filter α
⊢ (g ⊓ f).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x
Module: Mathlib.Order.Filter.Map

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

Tactic:
;

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : Filter α
h✝ : IsEmpty β
⊢ ¬⊥.NeBot ↔ ¬(f.NeBot ∧ Nonempty β)
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:
;

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : Filter β
hα : IsEmpty α
⊢ ¬⊥.NeBot ↔ ¬(Nonempty α ∧ f.NeBot)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ {x | p x}ᶜ ∉ l

Tactic:
;

Goal state after:
α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ {x | p x}ᶜ ∉ l
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
x : α
⊢ (∀ (t : Set α) (x_1 : ι), p x_1 → s x_1 ⊆ t → x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i

Tactic:
exact ⟨fun h i hi => h (s i) i hi Subset.rfl, fun h t i hi ht => ht (h i hi)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter α
m : α → β
t : Set α
htg : t ∈ g
h : InjOn m t
f : Filter ↑t
⊢ map m (map Subtype.val f ⊓ g) = map m (map Subtype.val f) ⊓ map m g

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
g : Filter α
m : α → β
t : Set α
htg : t ∈ g
h : InjOn m t
f : Filter ↑t
⊢ map m (map Subtype.val f ⊓ g) = map m (map Subtype.val f) ⊓ map m g
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) = map f F ⊓ G

Tactic:
apply le_antisymm
  · calc
      map f (F ⊓ comap f G) ≤ map f F ⊓ (map f <| comap f G) := map_inf_le
      _ ≤ map f F ⊓ G := inf_le_inf_left (map f F) map_comap_le
  · rintro U ⟨V, V_in, W, ⟨Z, Z_in, hZ⟩, h⟩
    apply mem_inf_of_inter (image_mem_map V_in) Z_in
    calc
      f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z) := by rw [image_inter_preimage]
      _ ⊆ f '' (V ∩ W) := by gcongr
      _ = f '' f ⁻¹' U := by rw [h]
      _ ⊆ U := image_preimage_subset f U

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Semigroup β
mul : Mul α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

Tactic:
;

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Semigroup β
mul : Mul α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Semigroup β
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
;

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Semigroup β
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommSemigroup β
mul : Mul α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

Tactic:
;

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommSemigroup β
mul : Mul α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommSemigroup β
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
;

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommSemigroup β
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsLeftCancelMul β
this : Mul α := e.mul
⊢ IsLeftCancelMul α

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsLeftCancelMul β
this : Mul α := e.mul
⊢ IsLeftCancelMul α
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsRightCancelMul β
this : Mul α := e.mul
⊢ IsRightCancelMul α

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsRightCancelMul β
this : Mul α := e.mul
⊢ IsRightCancelMul α
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsCancelMul β
this : Mul α := e.mul
⊢ IsCancelMul α

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsCancelMul β
this : Mul α := e.mul
⊢ IsCancelMul α
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
F : Filter β
u : α → β
inst✝ : Nonempty α
⊢ (∀ {p : β → Prop}, (∀ᶠ (x : β) in F, p x) → ∀ (a : α), ∃ b, a ≤ b ∧ p (u b)) ↔
    ∀ U ∈ F, ∀ (N : α), ∃ n, N ≤ n ∧ u n ∈ U

Tactic:
;

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
F : Filter β
u : α → β
inst✝ : Nonempty α
⊢ (∀ {p : β → Prop}, (∀ᶠ (x : β) in F, p x) → ∀ (a : α), ∃ b, a ≤ b ∧ p (u b)) ↔
    ∀ U ∈ F, ∀ (N : α), ∃ n, N ≤ n ∧ u n ∈ U
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
this : IsDirectedOrder ↑s
c : α
hc : a ≤ c
⊢ ∃ x, ↑x = c ∧ ∀ (a : { x // x ∈ s }), ↑a ≤ c ↔ a ≤ x

Tactic:
exact ⟨⟨c, h hc⟩, rfl, fun _ ↦ .rfl⟩

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

Goal state before:
pp: k : ℕ
hk : 0 < k
a b : ℕ
x✝ : 1 ≤ b
⊢ a / k ≤ b ↔ a ≤ k * b + (k - 1)

Tactic:
by rw [Nat.div_le_iff_le_mul_add_pred hk]

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

Goal state before:
pp: k : ℕ
hk : 0 < k
b : ℕ
x✝ : 1 ≤ b
⊢ k - 1 < k

Tactic:
;

Goal state after:
k : ℕ
hk : 0 < k
b : ℕ
x✝ : 1 ≤ b
⊢ k - 1 < k
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:
;

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
⊢ n • x ≠ 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:
;

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
⊢ n • x ≠ 0
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
e : α ≃ β
inst✝² : AddCommMonoid β
inst✝¹ : Module R β
inst✝ : Module.IsTorsionFree R β
this✝¹ : AddCommMonoid α := e.addCommMonoid
this✝ : Module R α := Equiv.module R e
⊢ Module.IsTorsionFree R α

Tactic:
;

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
e : α ≃ β
inst✝² : AddCommMonoid β
inst✝¹ : Module R β
inst✝ : Module.IsTorsionFree R β
this✝¹ : AddCommMonoid α := e.addCommMonoid
this✝ : Module R α := Equiv.module R e
⊢ Module.IsTorsionFree R α
Module: Mathlib.Algebra.Module.Congruence.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : SMul R M
inst✝ : SMul S N
φ : R → S
f : M →ₑ[φ] N
r : R
x✝¹ x✝ : M
h : f x✝¹ = f x✝
⊢ f (r • x✝¹) = f (r • x✝)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : SMul R M
inst✝ : SMul S N
φ : R → S
f : M →ₑ[φ] N
r : R
x✝¹ x✝ : M
h : f x✝¹ = f x✝
⊢ f (r • x✝¹) = f (r • x✝)
Module: Mathlib.Algebra.Module.Congruence.Defs

Goal state before:
pp: case mk
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module S M
inst✝ : Module S N
f : M →ₗ[S] N
hf : Function.Surjective ⇑f
s : S
x✝ : ModuleCon.Quotient M (ker f.toDistribMulActionHom)
a✝ : M
⊢ (AddCon.quotientKerEquivOfSurjective f.toAddMonoidHom hf).toFun
      (s • Quot.mk (⇑(ker f.toDistribMulActionHom).toSetoid) a✝) =
    (RingHom.id S) s •
      (AddCon.quotientKerEquivOfSurjective f.toAddMonoidHom hf).toFun
        (Quot.mk (⇑(ker f.toDistribMulActionHom).toSetoid) a✝)

Tactic:
;

Goal state after:
case mk
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module S M
inst✝ : Module S N
f : M →ₗ[S] N
hf : Function.Surjective ⇑f
s : S
x✝ : ModuleCon.Quotient M (ker f.toDistribMulActionHom)
a✝ : M
⊢ (AddCon.quotientKerEquivOfSurjective f.toAddMonoidHom hf).toFun
      (s • Quot.mk (⇑(ker f.toDistribMulActionHom).toSetoid) a✝) =
    (RingHom.id S) s •
      (AddCon.quotientKerEquivOfSurjective f.toAddMonoidHom hf).toFun
        (Quot.mk (⇑(ker f.toDistribMulActionHom).toSetoid) a✝)
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ ↑P ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ ↑P ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ ↑Q ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ ↑Q ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩