mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ sSup s ∈ s

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ sSup s ∈ s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
⊢ False

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := CompleteLattice.WellFoundedGT.isSupFiniteCompact α s

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ False
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
⊢ 0 ∈ span R (s • t)

Tactic:
;

Goal state after:
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
⊢ 0 ∈ span R (s • t)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
c₁ c₂ : S
x✝¹ : c₁ ∈ span R s
x✝ : c₂ ∈ span R s
ih₁ : c₁ • x ∈ span R (s • t)
ih₂ : c₂ • x ∈ span R (s • t)
⊢ c₁ • x + c₂ • x ∈ span R (s • t)

Tactic:
;

Goal state after:
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
c₁ c₂ : S
x✝¹ : c₁ ∈ span R s
x✝ : c₂ ∈ span R s
ih₁ : c₁ • x ∈ span R (s • t)
ih₂ : c₂ • x ∈ span R (s • t)
⊢ c₁ • x + c₂ • x ∈ span R (s • t)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
b : R
c : S
x✝ : c ∈ span R s
hc : c • x ∈ span R (s • t)
⊢ b • c • x ∈ span R (s • t)

Tactic:
;

Goal state after:
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
b : R
c : S
x✝ : c ∈ span R s
hc : c • x ∈ span R (s • t)
⊢ b • c • x ∈ span R (s • t)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_1
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ 0 ∈ span R (s • t)

Tactic:
;

Goal state after:
case refine_1
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ 0 ∈ span R (s • t)
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ (∀ a ∈ s, f a ≠ 0) ↔ ∀ a ∈ s, f a ≠ 0

Tactic:
;

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ (∀ a ∈ s, f a ≠ 0) ↔ ∀ a ∈ s, f a ≠ 0
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ y✝ : S
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
⊢ x✝ • y ∈ span R (s • t) → y✝ • y ∈ span R (s • t) → (x✝ + y✝) • y ∈ span R (s • t)

Tactic:
;

Goal state after:
case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ y✝ : S
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
⊢ x✝ • y ∈ span R (s • t) → y✝ • y ∈ span R (s • t) → (x✝ + y✝) • y ∈ span R (s • t)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ y✝ : S
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
⊢ x✝ • y ∈ span R (s • t) → y✝ • y ∈ span R (s • t) → x✝ • y + y✝ • y ∈ span R (s • t)

Tactic:
;

Goal state after:
case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ y✝ : S
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
⊢ x✝ • y ∈ span R (s • t) → y✝ • y ∈ span R (s • t) → x✝ • y + y✝ • y ∈ span R (s • t)
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : One F
inst✝¹ : One β
inst✝ : IsOneApply F α β
x✝ : α
⊢ 1 x✝ = 1 x✝

Tactic:
;

Goal state after:
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : One F
inst✝¹ : One β
inst✝ : IsOneApply F α β
x✝ : α
⊢ 1 x✝ = 1 x✝
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Mul F
inst✝¹ : Mul β
inst✝ : IsMulApply F α β
f g : F
x✝ : α
⊢ (f * g) x✝ = (⇑f * ⇑g) x✝

Tactic:
;

Goal state after:
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Mul F
inst✝¹ : Mul β
inst✝ : IsMulApply F α β
f g : F
x✝ : α
⊢ (f * g) x✝ = (⇑f * ⇑g) x✝
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Div F
inst✝¹ : Div β
inst✝ : IsDivApply F α β
f g : F
x✝ : α
⊢ (f / g) x✝ = (⇑f / ⇑g) x✝

Tactic:
;

Goal state after:
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Div F
inst✝¹ : Div β
inst✝ : IsDivApply F α β
f g : F
x✝ : α
⊢ (f / g) x✝ = (⇑f / ⇑g) x✝
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Inv F
inst✝¹ : Inv β
inst✝ : IsInvApply F α β
f : F
x✝ : α
⊢ f⁻¹ x✝ = (⇑f)⁻¹ x✝

Tactic:
;

Goal state after:
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Inv F
inst✝¹ : Inv β
inst✝ : IsInvApply F α β
f : F
x✝ : α
⊢ f⁻¹ x✝ = (⇑f)⁻¹ x✝
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : SMul M F
inst✝¹ : SMul M β
inst✝ : IsSMulApply M F α β
n : M
f : F
x✝ : α
⊢ (n • f) x✝ = (n • ⇑f) x✝

Tactic:
;

Goal state after:
M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : SMul M F
inst✝¹ : SMul M β
inst✝ : IsSMulApply M F α β
n : M
f : F
x✝ : α
⊢ (n • f) x✝ = (n • ⇑f) x✝
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Pow F M
inst✝¹ : Pow β M
inst✝ : IsPowApply M F α β
f : F
n : M
x✝ : α
⊢ (f ^ n) x✝ = (⇑f ^ n) x✝

Tactic:
;

Goal state after:
M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Pow F M
inst✝¹ : Pow β M
inst✝ : IsPowApply M F α β
f : F
n : M
x✝ : α
⊢ (f ^ n) x✝ = (⇑f ^ n) x✝
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : One F'
inst✝ : IsOneApplyEqSelf F' α
x✝ : α
⊢ 1 x✝ = id x✝

Tactic:
;

Goal state after:
F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : One F'
inst✝ : IsOneApplyEqSelf F' α
x✝ : α
⊢ 1 x✝ = id x✝
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ ∀ (a : R), ∀ x ∈ span R s, x • y ∈ span R (s • t) → (a • x) • y ∈ span R (s • t)

Tactic:
intro r

Goal state after:
case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
r : R
⊢ ∀ x ∈ span R s, x • y ∈ span R (s • t) → (r • x) • y ∈ span R (s • t)
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : Mul F'
inst✝ : IsMulApplyEqComp F' α
f g : F'
x✝ : α
⊢ (f * g) x✝ = (⇑f ∘ ⇑g) x✝

Tactic:
;

Goal state after:
F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : Mul F'
inst✝ : IsMulApplyEqComp F' α
f g : F'
x✝ : α
⊢ (f * g) x✝ = (⇑f ∘ ⇑g) x✝
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0✝ : S
y : A
hy✝ : y ∈ t
r : R
s0 : S
hx✝ : s0 ∈ span R s
hy : s0 • y ∈ span R (s • t)
⊢ (r • s0) • y ∈ span R (s • t)

Tactic:
;

Goal state after:
case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0✝ : S
y : A
hy✝ : y ∈ t
r : R
s0 : S
hx✝ : s0 ∈ span R s
hy : s0 • y ∈ span R (s • t)
⊢ (r • s0) • y ∈ span R (s • t)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0✝ : S
y : A
hy✝ : y ∈ t
r : R
s0 : S
hx✝ : s0 ∈ span R s
hy : s0 • y ∈ span R (s • t)
⊢ r • s0 • y ∈ span R (s • t)

Tactic:
;

Goal state after:
case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0✝ : S
y : A
hy✝ : y ∈ t
r : R
s0 : S
hx✝ : s0 ∈ span R s
hy : s0 • y ∈ span R (s • t)
⊢ r • s0 • y ∈ span R (s • t)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x : A
hx : x ∈ restrictScalars R (span S t)
⊢ k • x ∈ restrictScalars R (span S t)

Tactic:
;

Goal state after:
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x : A
hx : x ∈ restrictScalars R (span S t)
⊢ k • x ∈ restrictScalars R (span S t)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
x✝ : M
⊢ x✝ ∈ ⇑(span S ↑p).subtype '' range ⇑(inclusionSpan S p) ↔ x✝ ∈ ↑p

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
x✝ : M
⊢ x✝ ∈ ⇑(span S ↑p).subtype '' range ⇑(inclusionSpan S p) ↔ x✝ ∈ ↑p
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i | f i ≠ ⊥}
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) (s.sup id)

Tactic:
rw [← Finset.sup_erase_bot]

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i | f i ≠ ⊥}
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) ((s.erase ⊥).sup id)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mp.inl
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
a b : R
hb : b • a • 0 = 0
⊢ ∃ z, z • a • 0 = 0

pp: case mp.inr
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ ∃ z, z • a • y = y

Tactic:
;

Goal state after:
case mp.inl
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
a b : R
hb : b • a • 0 = 0
⊢ ∃ z, z • a • 0 = 0

case mp.inr
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ ∃ z, z • a • y = y
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
hf : Injective ⇑f
⊢ x ∈ comap f (span R₂ (⇑f '' s)) ↔ x ∈ span R s

Tactic:
← Submodule.map_span,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
hf : Injective ⇑f
⊢ x ∈ comap f (map f (span R s)) ↔ x ∈ span R s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) (s.sup id)

Tactic:
rw [← Finset.sup_erase_bot]

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) ((s.erase ⊥).sup id)
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
a : κ
⊢ (∏ i ∈ s, (f i).indicator (g i)) a = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) a

Tactic:
;

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
a : κ
⊢ (∏ i ∈ s, (f i).indicator (g i)) a = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) a
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
⊢ sSup (range fun x ↦ f ↑x) ⊓ a = ⊥

Tactic:
inf_comm,

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
⊢ a ⊓ sSup (range fun x ↦ f ↑x) = ⊥
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : ↑u ⊆ range fun x ↦ f ↑x
t : Set ι
ht : t ⊆ s
ht' : t.Finite
htu : u.sup id = ⨆ i ∈ t, f i
⊢ a ⊓ u.sup id = ⊥

Tactic:
inf_comm,

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : ↑u ⊆ range fun x ↦ f ↑x
t : Set ι
ht : t ⊆ s
ht' : t.Finite
htu : u.sup id = ⨆ i ∈ t, f i
⊢ u.sup id ⊓ a = ⊥
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝ : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ ⟨b, hbk⟩ = ⊤

Tactic:
;

Goal state after:
case inl
α : Type u_2
inst✝ : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ ⟨b, hbk⟩ = ⊤
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝ : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ ↑⟨b, hbk⟩ = ↑⊤

Tactic:
;

Goal state after:
case inl
α : Type u_2
inst✝ : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ ↑⟨b, hbk⟩ = ↑⊤
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: F : Type u_8
α : Type u_9
β : Type u_10
ι : Type u_11
inst✝⁴ : FunLike F α β
inst✝³ : CommMonoid β
inst✝² : CommMonoid F
inst✝¹ : IsOneApply F α β
inst✝ : IsMulApply F α β
s : Finset ι
f : ι → F
x✝ : α
⊢ (∏ i ∈ s, f i) x✝ = (∏ i ∈ s, ⇑(f i)) x✝

Tactic:
;

Goal state after:
F : Type u_8
α : Type u_9
β : Type u_10
ι : Type u_11
inst✝⁴ : FunLike F α β
inst✝³ : CommMonoid β
inst✝² : CommMonoid F
inst✝¹ : IsOneApply F α β
inst✝ : IsMulApply F α β
s : Finset ι
f : ι → F
x✝ : α
⊢ (∏ i ∈ s, f i) x✝ = (∏ i ∈ s, ⇑(f i)) x✝
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: M₀ : Type u_4
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a : M₀
l : List M₀
⊢ (a :: l).prod = 0 ↔ 0 ∈ a :: l

Tactic:
prod_cons,

Goal state after:
M₀ : Type u_4
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a : M₀
l : List M₀
⊢ a * l.prod = 0 ↔ 0 ∈ a :: l
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
z✝ : α
⊢ z✝ ∈ S → z✝ ≤ sSup S

Tactic:
;

Goal state after:
case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
z✝ : α
⊢ z✝ ∈ S → z✝ ≤ sSup S
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

pp: case neg
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : ¬1 < s.card
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
;

Goal state after:
case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

case neg
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : ¬1 < s.card
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: M₀ : Type u_3
inst✝ : CommMonoidWithZero M₀
s : Multiset M₀
h : 0 ∈ s
s' : Multiset M₀
hs' : s = 0 ::ₘ s'
⊢ s.prod = 0

Tactic:
;

Goal state after:
M₀ : Type u_3
inst✝ : CommMonoidWithZero M₀
s : Multiset M₀
h : 0 ∈ s
s' : Multiset M₀
hs' : s = 0 ::ₘ s'
⊢ s.prod = 0
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
s : Multiset M₀
l : List M₀
⊢ l.prod = 0 ↔ 0 ∈ ↑l

Tactic:
;

Goal state after:
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
s : Multiset M₀
l : List M₀
⊢ l.prod = 0 ↔ 0 ∈ ↑l
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
s t : Set M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
a : R
x : M
y : M'
hx : (x, y).1 ∈ ↑p
hy : (x, y).2 ∈ ↑q₁
⊢ a • (x, y) ∈ ↑p ×ˢ ↑q₁

Tactic:
;

Goal state after:
R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
s t : Set M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
a : R
x : M
y : M'
hx : (x, y).1 ∈ ↑p
hy : (x, y).2 ∈ ↑q₁
⊢ a • (x, y) ∈ ↑p ×ˢ ↑q₁
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : M × M'
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : M × M'
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x : M
y : M'
⊢ (x, y) ∈ ⊥.prod ⊥ ↔ (x, y) ∈ ⊥

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x : M
y : M'
⊢ (x, y) ∈ ⊥.prod ⊥ ↔ (x, y) ∈ ⊥