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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite M
⊢ Module.Finite R M

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosedOn D (f i)
⊢ ∀ x ∈ range f, DirSupClosedOn D x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
hb : b₁ < b₂
ha : a < 0
⊢ a • b₂ < a • b₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosedOn D (f i)
⊢ DirSupClosedOn D (⋂ i, f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosed (f i)
⊢ ∀ x ∈ range f, DirSupClosed x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₁ • _b < a₂ • _b

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosed (f i)
⊢ DirSupClosed (⋂ i, f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInaccOn D (f i)
⊢ ∀ x ∈ range f, DirSupInaccOn D x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLE α β
h : a • b₁ ≤ a • b₂
ha : a < 0
⊢ b₂ ≤ b₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInaccOn D (f i)
⊢ DirSupInaccOn D (⋃ i, f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInacc (f i)
⊢ ∀ x ∈ range f, DirSupInacc x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLT α β
h : a • b₁ < a • b₂
ha : a ≤ 0
⊢ b₂ < b₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInacc (f i)
⊢ DirSupInacc (⋃ i, f i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_7
P : Type u_6
inst✝² : Semiring S
inst✝¹ : AddCommMonoid P
inst✝ : Module S P
σ : R →+* S
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
s : Set M
hsfin : s.Finite
hs : span R s = ⊤
p : P
x✝ : p ∈ ⊤
⊢ p ∈ ⇑f '' ↑(span R s)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_7
P : Type u_6
inst✝² : Semiring S
inst✝¹ : AddCommMonoid P
inst✝ : Module S P
σ : R →+* S
hM : Module.Finite R M
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
⊢ Module.Finite S P

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ DirSupClosedOn D (s ∩ t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁸ : Ring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsOrderedRing α
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : a < 0
⊢ a • b₁ ≤ a • b₂ ↔ b₂ ≤ b₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupClosed s
ht : DirSupClosed t
⊢ DirSupClosed (s ∩ t)

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupInaccOn D (s ∪ t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁸ : Ring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsOrderedRing α
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ a • b₁ < a • b₂ ↔ b₂ < b₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupInacc s
ht : DirSupInacc t
⊢ DirSupInacc (s ∪ t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁸ : Ring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsOrderedRing α
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ 0 < a • b ↔ b < 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_7
P : Type u_6
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Bijective ⇑f
x✝ : Module.Finite S P
⊢ (map f ⊤).FG

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁸ : Ring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsOrderedRing α
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ a • b < 0 ↔ 0 < b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
⊢ d ∩ s ∪ d ∩ t = d

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_6
M : ι → Type u_7
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), Module.Finite R (M i)
⊢ ⊤.FG

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ Ideal.span ↑{1} = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
by

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

Goal state before:
pp: R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
hM : Module.Finite R M
⊢ Module.Finite A M

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
by

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

Goal state before:
pp: R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : Finset A
hs : span R ↑s = ⊤
t : Finset M
ht : span A ↑t = ⊤
⊢ span R (image2 (fun x1 x2 ↦ x1 • x2) ↑s ↑t) = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : Preorder α
inst✝⁷ : Preorder β
inst✝⁶ : Preorder γ
inst✝⁵ : SMul α β
inst✝⁴ : SMul α γ
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : SMulPosReflectLE α β
inst✝ : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
⊢ _a₁ ≤ _a₂

Tactic:
by

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

Goal state before:
pp: A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst✝⁶ : CommSemiring A₁
inst✝⁵ : CommSemiring B₁
inst✝⁴ : CommSemiring A₂
inst✝³ : Semiring B₂
inst✝² : Algebra A₁ B₁
inst✝¹ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
inst✝ : Module.Finite A₁ B₁
this✝ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
x : A₁
⊢ (algebraMap A₁ B₁) x = (algebraMap A₂ B₁) ((algebraMap A₁ A₂) x)

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu✝ : d ⊆ s ∪ t
hdu : d ⊆ t ∪ s
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst✝ : d ∩ s ∪ d ∩ t = d
hdst : d ∩ t ∪ d ∩ s = d
this :
  ∀ {α : Type u_1} {s t : Set α} {D : Set (Set α)} [inst : Preorder α],
    IsLowerSet D →
      DirSupClosedOn D s →
        DirSupClosedOn D t →
          ∀ ⦃d : Set α⦄,
            d ∈ D →
              d ⊆ s ∪ t →
                d.Nonempty →
                  DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d →
                    ∀ ⦃a : α⦄,
                      IsLUB d a →
                        d ∩ s ∪ d ∩ t = d →
                          DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s) → a ∈ s ∪ t
h : ¬(DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s))
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ t ∪ d ∩ s)

Tactic:
by

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

Goal state before:
pp: A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst✝⁶ : CommSemiring A₁
inst✝⁵ : CommSemiring B₁
inst✝⁴ : CommSemiring A₂
inst✝³ : Semiring B₂
inst✝² : Algebra A₁ B₁
inst✝¹ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
inst✝ : Module.Finite A₁ B₁
this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this✝ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
this : IsScalarTower A₁ A₂ B₁
r : A₂
⊢ e₂.toFun ((algebraMap A₂ B₁) r) = (algebraMap A₂ B₂) r

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulStrictMono α γ
⊢ ∀ ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : β × γ⦄, b₁ < b₂ → a • b₁ < a • b₂

Tactic:
by

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

Goal state before:
pp: A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst✝⁶ : CommSemiring A₁
inst✝⁵ : CommSemiring B₁
inst✝⁴ : CommSemiring A₂
inst✝³ : Semiring B₂
inst✝² : Algebra A₁ B₁
inst✝¹ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
inst✝ : Module.Finite A₁ B₁
⊢ Module.Finite A₂ B₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ DirSupClosedOn D (s ∪ t)

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupInaccOn D (s ∩ t)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
S₁ S₂ : Submodule R V
h₁ : Module.Finite R ↥S₁
h₂ : Module.Finite R ↥S₂
⊢ Module.Finite R ↥(S₁ ⊔ S₂)

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupClosed s
ht : DirSupClosed t
⊢ DirSupClosed (s ∪ t)

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupInacc s
ht : DirSupInacc t
⊢ DirSupInacc (s ∩ t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosStrictMono α γ
⊢ ∀ ⦃b : β × γ⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, a₁ < a₂ → a₁ • b < a₂ • b

Tactic:
by

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

Goal state before:
pp: R : Type u_2
V : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
⊢ Module.Finite R ↥(s.sup S)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
A : Type u_3
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
S : Submodule A M
inst✝ : Module.Finite R A
hS : S.FG
⊢ (Submodule.restrictScalars R S).FG

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosReflectLT α β
inst✝ : SMulPosReflectLT α γ
⊢ ∀ ⦃b : β × γ⦄, 0 ≤ b → ∀ ⦃a₁ a₂ : α⦄, a₁ • b < a₂ • b → a₁ < a₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
⊢ DirSupInaccOn D s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : (i : ι) → Preorder (β i)
inst✝² : (i : ι) → SMul α (β i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : ∀ (i : ι), SMulPosReflectLE α (β i)
_b : (i : ι) → β i
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
⊢ _a₁ ≤ _a₂

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
A : Type u_3
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule R M
hS : S.FG
⊢ (span A ↑S).FG

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.Finite
hf : f.Finite
⊢ (g.comp f).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
⊢ ∀ ⦃d : Set α⦄,
    d ∈ Set.univ →
      d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).Finite
⊢ g.Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : PartialOrder α
inst✝² : (i : ι) → PartialOrder (β i)
inst✝¹ : (i : ι) → SMulWithZero α (β i)
inst✝ : ∀ (i : ι), PosSMulStrictMono α (β i)
⊢ ∀ ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : (i : ι) → β i⦄, b₁ < b₂ → a • b₁ < a • b₂

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
⊢ ⊤.FG

Tactic:
Submodule.fg_def,

Goal state after:
R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
⊢ ∃ S, S.Finite ∧ Submodule.span R≥0 S = ⊤
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
H : ∀ b ∈ t, ¬Ici b ∩ t ⊆ s
⊢ IsCofinalFor t (t \ s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : PartialOrder α
inst✝² : (i : ι) → PartialOrder (β i)
inst✝¹ : (i : ι) → SMulWithZero α (β i)
inst✝ : ∀ (i : ι), SMulPosStrictMono α (β i)
⊢ ∀ ⦃b : (i : ι) → β i⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, a₁ < a₂ → a₁ • b < a₂ • b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
⊢ {1, -1}.Finite

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
⊢ ∃ b ∈ t, Ici b ∩ t ⊆ s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : R
hx : 0 ≤ x
⊢ 1 ∈ {1, -1}

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ DirSupInacc s ↔
    ∀ ⦃d : Set α⦄,
      d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : PartialOrder α
inst✝² : (i : ι) → PartialOrder (β i)
inst✝¹ : (i : ι) → SMulWithZero α (β i)
inst✝ : ∀ (i : ι), SMulPosReflectLT α (β i)
⊢ ∀ ⦃b : (i : ι) → β i⦄, 0 ≤ b → ∀ ⦃a₁ a₂ : α⦄, a₁ • b < a₂ • b → a₁ < a₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
ha : a ∈ s
⊢ b ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
hs : DirSupInacc s
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
⊢ a ∈ s ↔ b ∈ s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : R
hx : x ≤ 0
⊢ -1 ∈ {1, -1}

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ DirSupClosed {a}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 ≤ a
b₁ b₂ : β
hb : b₁ ≤ b₂
⊢ a • b₁ ≤ a • b₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : LinearOrder α
⊢ DirSupClosedOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s

Tactic:
by

Goal state after: